「Program=Proof筆記」修訂間的差異

出自Tan Kian-ting的維基
跳至導覽 跳至搜尋
 
行 29： 行 29：


== Ch1 有型別的函數式程設 ==
== Ch1 有型別的函數式程設 ==
===1.1介紹===
<pre>(* 我是註解 *)


print_endline "string" (* 函數使用，一般寫法：print_endline("string")*)
* [[Program=Proof筆記-第1章]]


</pre>
ocamlopt 可以編譯
<pre>
# 2 + 2 ;;
-: int = 4
(* 對結果做型別推導 *)
let s = string_to_int 3.2
(* -> 這會型別錯誤 *)
</pre>
====Type annotation（型別顯式標記）====
比較：
<pre>
let f x = x + 1
let f (x : int ) : int = x + 1
</pre>
====型別====
List.map 的型別：<code>('a -> 'b) -> 'a list -> 'b list</code>
<code>let mapped_list = List.map (fun x -> 2 * x) a_list</code>
====可變變數(reference)====
<pre>
let () =
  let r = ref 0 in (* 可變 reference *)
  for i = 0 to 9 do
    r := !r + 1 (* 刷新 r 值，使其 + 1）
  done
</pre>
另外還有 record、array、GADT、垃圾回收等等。
===1.2基本操作===
<pre>
let () = print_string "foo" (*回傳 unit*)
</pre>
==== 迴圈====
<pre>
let () =
  let r = ref 0 in
    for i = 0 to 9 do
    r := !r +1
  done
</pre>
====部分應用（不需括號）====
int -> (int -> int) 即 int -> int -> int
add 的以下寫法：
<pre>
add x y = x + y
add y = fn x -> x + y
add = fn x y -> x + y
</pre>
====互遞迴====
<pre>
let rec f x = ...
and g x = .....
</pre>
====布林 boolean 操作====
操作子
<pre>
&& || not
條件與區塊
<pre>
if ... then ... else...
while ... do ... done
</pre>
比對操作子
<pre>
== 同一記憶體位置
= 值相等
<> 不等於
</pre>
====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 : ()
<pre>
let f = print_string "foo" (* let f = printString("foo"); *)
let f () = print_string "foo" (* let f = function () { printString("foo") ;}*)
</pre>
===1.3遞迴型別===
tree型別定義如下：
<pre>
type tree =
| Node of int * tree * tree
| Leaf of int
</pre>
以下是合規的tree
<pre>
let t = Node(3, Node(4, Leaf 1, Leaf 3))
</pre>
====模式比對====
<pre>
let sum foo x =
match x with
| Node (n , t1, t2) -> n + sum t1 + sum t2
| Leaf n -> n
</pre>
guard
<pre>|Leaf n when n > 0 -> ...</pre>
語法糖
<pre>let f = function ... 即 let f x = match x with ...</pre>
====Bool====
<pre>type bool = True | False</pre>
====List====
<pre>type 'a list =
| Nil
| Cons of 'a * 'a list</pre>
====coproducts====
<pre>type ('a, 'b) either =
| Left of 'a
| Right of 'b</pre>
====unit====
<pre>type unit = | T</pre>
只有這個值 <code>()</code>
====Empty====
<pre>type Empty = |</pre>
====Natural Number====
<pre>type Nat =
|Zero
|Suc of nat</pre>
====例外處理：Option type and exception====
處理例外的方式
Option type
<pre>type 'a option =
| Some of 'a
| None
</pre>
exception
<pre>let hd l =
  match l with
| x::l -> x
| [] -> raise Not_found</pre>
搭配
<pre>try
...
with
| Not_found -> ...</pre>


[[分類:資訊]]
[[分類:資訊]]
[[分類:邏輯學]]
[[分類:邏輯學]]

於 2024年3月3日 (日) 21:36 的最新修訂

題名：Program=Proof
中譯（暫）：證明=程式
作者：Samuel Mimram
ISBN 9798615591839

---

Ch0 序言

開頭作者舉例一個式子在數字很大的時候會出錯的案例，來說明證明的重要性。

之後提到證明即程式（利用程式的性型別）的概念。

檢查程式：

空中巴士公司使用形式方法來驗證程式是否出錯誤。

CompCert 用 coq 來造出證明程式符合語義的C編譯器。

自動化證明：

  • 特定問題會比較快
  • 但不代表能一定求解出證明

證明數學是一種藝術。和驗證是否錯誤比，較難。就如積分比微分難一樣。

依值型別：

  • Agda 與 Coq 幫助漸次展開證明
  • 證明時間 > 測試時間
  • 重要的軟體使用之驗證

Ch1 有型別的函數式程設

取自「https://kianting.info/wiki/index.php?title=Program%3DProof筆記&oldid=2556」