Program=Proof筆記-第1章

導航：首頁 > 程式語言、邏輯學> Program=Proof筆記-第1章

Ch1 有型別的函數式程設

1.1介紹

(* 我是註解 *)

print_endline "string" (*  函數使用，一般寫法：print_endline("string")*)

ocamlopt 可以編譯

# 2 + 2 ;;
-: int = 4
(* 對結果做型別推導 *)

let s = string_to_int 3.2
(* -> 這會型別錯誤 *)

Type annotation（型別顯式標記）

比較：

let f x = x + 1
let f (x : int ) : int = x + 1

型別

List.map 的型別：('a -> 'b) -> 'a list -> 'b list

let mapped_list = List.map (fun x -> 2 * x) a_list

可變變數(reference)

let () = 
  let r = ref 0 in (* 可變 reference *)
  for i = 0 to 9 do
     r := !r + 1 (* 刷新 r 值，使其 + 1）
  done

另外還有 record、array、GADT、垃圾回收等等。

1.2基本操作

let () = print_string "foo" (*回傳 unit*)

迴圈

let () = 
  let r = ref 0 in
    for i = 0 to 9 do
    r := !r +1
  done

部分應用（不需括號）

int -> (int -> int) 即 int -> int -> int

add 的以下寫法：

add x y = x + y
add y = fn x -> x + y
add = fn x y -> x + y

互遞迴

let rec f x = ...
and g x = .....

布林 boolean 操作

操作子

&& || not

條件與區塊
<pre>
if ... then ... else...
while ... do ... done

比對操作子

== 同一記憶體位置
= 值相等
<> 不等於

product type

add (x, y) = x + y

(int * int) -> int，其中的 (int * int)是 product type

list

• []：nil
• x::ls：(cons x ls)
• x1@x2：concat x1 and x2
• List.length：字串長度
• List.map：map
• List.iter：execute a funct90n for list
• List.mem：成員是否在列表內

String

"foo"

Unit

unit : ()

let f = print_string "foo" (* let f = printString("foo"); *)
let f () = print_string "foo" (* let f = function () { printString("foo") ;}*)

1.3遞迴型別

tree型別定義如下：

type tree = 
| Node of int * tree * tree
| Leaf of int

以下是合規的tree

let t = Node(3, Node(4, Leaf 1, Leaf 3))

模式比對

let sum foo x = 
match x with
| Node (n , t1, t2) -> n + sum t1 + sum t2
| Leaf n -> n

guard

|Leaf n when n > 0 -> ...

語法糖

let f = function ... 即 let f x = match x with ...

Bool

type bool = True | False

List

type 'a list = 
| Nil
| Cons of 'a * 'a list

coproducts

type ('a, 'b) either = 
| Left of 'a
| Right of 'b

unit

type unit = | T

只有這個值 ()

Empty

type Empty = |

Natural Number

type Nat = 
|Zero
|Suc of nat

例外處理：Option type and exception

處理例外的方式

Option type

type 'a option = 
| Some of 'a
| None

exception

let hd l =
  match l with
 | x::l -> x
 | [] -> raise Not_found

搭配

try
 ...
with
| Not_found -> ...

抽象化描述

因為排版

• U表示程式語言可操作的物件（項目）的集合
• P(U)表示U的冪集(powerset; U的子集合的集合)
• F是recursive definition，F型別是P(U)->P(U)
  • tree 的型別是F的最小不動點，滿足 F(X) = X 。
  • 因為F是monotone單調的，所以X ⊆Y -> F(X) ⊆ F(Y)
  • F的不動點 $fix(F)=\bigcap \{x\in {\mathcal {P}}({\mathcal {U}})|F(X)\subseteq X\}$
• 在隱微的Kleene fixpoint theorem 假設，可以顯現出

$fix(F)=\bigcup _{n\in \mathbf {N} }F^{n}(\emptyset )$

• 假設我們有type 'a leaf = Leaf 'a | Node (a, 'a leaf ,'a leaf)
• $F^{0}(\emptyset )=\emptyset$
• $F^{1}(\emptyset )=\{Leaf(n)|n\in \mathbf {N} \}$（高度<=1）
• $F^{2}(\emptyset )=\{Leaf(n)|n\in \mathbf {N} \}\cup \{Node(n,t_{1},t_{2})|n\in \mathbf {N} \land t_{1},t_{2}\in F^{1}(\emptyset )\}$（高度<=2）

這個定理這樣推演下去，任何tree都是有固定的高度。

另外tree的集合是F的不動點，一般來說有多個不動點。

推論：$\forall X,s.t.F(X)\subseteq X\rightarrow fix(F)\subseteq X$