rhb_blog

rao的博客

0%

函数式编程-ML编程基础

发表于 更新于 分类于 ，

ML概览

  • ML强调的是表达式估计
  • ML更倾向于代数
  • ML表达式特征：类型可有可无、值可有可无、效果可有可无
  • 类型检查十分严格

ML标准类型

  • 基础类型(basic types) unit, int, real, bool, string
  • 表(lists) int list, (int -> int) list
  • 元组(tuples) int * int, int * int * real
  • 函数(functions) int -> int, real -> int * int

所有对象都要有类型，不一定显式说明，但必须能静态推导(在编译时该类型能被编译器根据上下文推算出来)。例如：int y=x+3就默认了x和y均是int型，因为会强制类型转换。

  • 单元(unit) 只包含一个元素，用空的括号表示，类似于C语言中的void类型。 ( ) : unit
  • 整型(int) 负号用“~”表示。
  • 浮点型(real)
  • 布尔型(bool) true, false
  • 字符串型(string) 双引号间的字符序列

表

  • 包含相同类型的元素序列
  • 表中元素用“,”分隔，整个表用[ ]括起来
  • 空表：[ ]或nil
  • 表的类型表达式取决于表的元素类型，写作：
    <元素类型> list

如： int list, (int -> int) list

  • 表可以嵌套

如: [1,2,3] : int list [“张三”, “李四”]: string list

  • 相同类型元素的有限序列

  • 元素可以重复出现，其顺序是有意义的

  • 表中元素可以为任意类型，但需具有相同类型

  • 表为多态类型

  • 表的基本函数：

    :: (追加元素), @ (连接表), null (空表测试), hd(返回表头元素), tl(返回非空表的表尾), length(返回表长)

    • [1, 3, 2, 1, 21+21] : int list

    • [true, false, true] : bool list

    • [[1],[2, 3]] : (int list) list

    • [ ] : int list, [ ] : bool list, ……

    • 1::[2, 3] = [1, 2, 3]

    • [1, 2]@[3, 4] = [1, 2, 3, 4]

    • nil = [ ]

元组

  • 包含任意类型数据元素的定长序列
  • 类型表达式：每个元素的类型用*间隔并排列在一起。如： int * int, int * int * real
  • 圆括号中用逗号分隔的数据元素，允许嵌套。如: (“张三”, “男”, 19, 1.75)

​ [((“赵”,”子昂”)，21, 1.81), ((“张”, “文艺”), 20, 1.69)]对应的是((string * string)* int * real)list

记录

  • 类似C中的结构类型，可以包含不同类型的元素
  • 每个元素有个名字
  • 记录的值和类型的写法都用{ }括起来。如： {First_name=“赵”, Last_name=“子昂”}

元组、表和记录的异同点

  • 符号：（） 、 [ ] 、{ }
  • 元素类型：可以不同 、 必须相同 、可以不同
  • 长度：定长 、 变长 、变长

函数

  • 以一定的规则将定义域上的值映射到值域上去
  • 类型由它的定义域类型和值域类型共同描述
  • ->表示定义域到值域的映射

fn: <定义域类型> -> <值域类型>。如: fun add(x, y) = x + y;

ML标准函数

  • 标准布尔函数：not, andalso, orelse。如：not true; true andalso false; true orelse false;

  • 标准算数运算函数：~, +, -, *, div, /。如：6 * 7; 3.0 * 2.0;

    • 运算符重载(operator ): 把同一运算符作用在不同类型上。
    • 重载运算符的两边必须为同一类型。
    • 整数到实数的转换：real
    • 实数到整数的转换：floor(下取整), ceil(上取整), round(四舍五入)，trunc(忽略小数)

  • 标准字符串函数：

    • 把两个字符串合并成一个：^
    • 返回字符串的长度：size

值

  • 每个类型都有一个值的集合
    For each type t there is a set of values

  • 一个类型的表达式求值结果为该类型的一个值(或出错)
    An expression of type t evaluates to a value of type t (or fails to terminate)

函数求值

函数：以一定的规则将定义域上的值映射到值域上

原型： fn:<定义域类型> -> <值域类型>

声明

赋予某个对象一个名字，包括值、类型、签名、结构和函子

  • 函数的声明： fun <函数名> (<形式参数>) : <结果类型> = <函数体>

例：fun divmod(x:int, y:int) : int*int = (x div y, x mod y)

  • 值的声明：val pi = 3.1415；val (q:int, r:int) = divmod(42, 5)；

    采用静态绑定方式——重新声明不会损坏系统、库或程序

  • 类型绑定：type float = real

    type count = int and average = real

  • 值绑定：val m : int = 3+2

    val pi : real = 3.14 and e : real = 2.17

  • 组合声明：val m : int = 3+2

    val n : int = m*m

声明的使用

声明函数：
check : int * int -> bool

局部声明：

let D in E end

1
2
3
4
5
6
fun check(x:int, y:int):bool =
let
	val (q:int, r:int)= divmod(x, y)
in
	(x = q*y + r)
end

全局声明

1
2
3
4
5
6
val pi : real = 3.14;
fun square(r:real) : real = r * r;
fun area(r:real) : real = pi * square(r);

val pi : real = 3.14159;
fun area(r:real) : real = pi * square(r);

声明、类型和值

  • 任意一个类型的表达式都可以进行求值操作
  • 任意一个类型表达式求值的结果为该类型的一个值
  • ML提供重新声明功能
  • 声明将产生名字(变量)和值的绑定(结合)
  • 绑定具有静态作用域

ML =

  • “=”用于类型的等式判断，称为等式类型(“equality types”)
  • 等式类型包括整数、布尔值结合元组、表等构造子生成的类型

模式

  • 只包含变量、构造子(数值、字符、元组、表等)和通配符的表达式

    • 模式中不是构造子的名字，是变量
    • 模式中的变量必须彼此不同
    • 构造子必须和变量区分开来

  • 通配符: _

  • 变量 : x //同一模式中，一个变量不能出现两次

  • 常数 : 42, true, ~3 // 实数和函数没有常数模式

  • 元组 : (p1, …, pk) //p1, …, pk均为模式

  • 表 : nil, p1::p2, [p1, …, pk]

规则说明

  • 部分操作的内建规则：
    • 结合性强于 ->
    • 无结合规则
    • -> 为右结合

替代

  • 给定集合绑定值【 x1:v1,…,xk:vk 】

  • 及表达式e，计为[ x1:v1, …, xk:vk ] e

  • 表达式替换为

  • v1 for x1,…,vk for xk

  • 如

    [ x:2 ] (x + x) is (2 + 2)；[ x:2 ] (fn y => x + y) is (fn y => 2 + y)

    [ x:2 ] (if x>0 then 1 else f(x-1)) is (if 2>0 then 1 else f(2-1))

代码说明

  • 函数定义前，用注释信息描述函数功能，形如(* comments*) ：
    • 函数名字和类型 (类型定义)
    • REQUIRES：参数说明 (明确参数范围)
    • ENSURES：函数在有效参数范围内的执行结果 (函数功能)

范例1：函数eval的说明

fun eval ([ ]:int list) : int = 0
| eval (d::L) = d + 10 * (eval L);

(* eval : int list -> int )
( * REQUIRES: )
( * every integer in L is a decimal digit * ) ( ENSURES: * )
( eval(L) evaluates to a non-negative integer *)

程序正确性证明

  • 基于等式或者推导的方式进行数学证明
  • 程序结构作为指导

为什么要进行程序正确性证明？

传统程序编写地是否正确性依靠分支测试，根据条件分支输入不同的数据检验是否正确？延伸出来很多自动化测试工具，黑盒测试、白盒测试和覆盖度测试。

函数式编程程序正确性证明是代码完成后用严格的数学推导证明对所有可能输入都产生正确结果。

归纳法

简单归纳法

  • 适用于涉及自然数的递归函数
    • 参数为非负整数
    • f(x)的递归调用形如f(y),且size(y)=size(x)-1

完全归纳法

证明对所有非负整数n，P(n)都成立

将P(k)简化为k个子问题： P(0), P(1), … , P(k-1)，且它们均成立时，可以利用{P(0), P(1), … , P(k-1)}推导出P(k)也成立

如：P(0)成立

​ P(1)可由P(0)推导出来

​ P(2)可由P(0)， P(1)推导出来

​ P(3)可由P(0)， P(1)， P(2)推导出来

​ ……

​ P(k)可由P(0), P(1), … , P(k-1)推导出来

  • 适用于涉及自然数的递归函数
    • 参数为非负整数
    • f(x)的递归调用形如f(y),且size(y)<size(x)

结构归纳法

基本情形： P([ ])

归纳步骤：对具有类型t的所有元素y和t list类型的数ys，都有P(ys)成立时， P(y::ys)成立

∀ i < k, P(i)成立的条件下有P(k)

  • 适用于涉及表和树的递归函数

良基归纳法

关系≺是良基的：

不存在无穷降序链：…≺Xn≺…≺X2≺X1,

对所有y’≺y，有P(y)，则P(y’)成立

  • 可以处理广泛的可终止计算问题

近似运行时间（近似时间复杂度）

  • 反映基于大批量数据的程序运行性能

    • 假设基本操作为常量执行时间(Assume basic ops take constant time)

    • 用Ο记号表示算法的时间性能(Give big-O classification)

  • 求解步骤：

    • 1.找出算法中的基本语句：算法中执行次数最多的那条语句就是基本语句，通常是最内层循环的循环体
    • 2.计算基本语句的执行次数的数量级：忽略所有低次幂和最高次幂的系数，保证基本语句执行次数的函数中的最高次幂正确
    • 3.用Ο记号表示算法的时间性能：将基本语句执行次数的数量级放入Ο记号中。

递归分析

递归函数的定义给出了程序的递推关系，执行情况用work表示