檢視 Program=Proof筆記的原始碼

{{Nav|程式語言、邏輯學}}
: 題名：Program=Proof
: 中譯（暫）：證明=程式
:作者：Samuel Mimram 
:{{isbn|9798615591839}}
---

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

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

檢查程式：

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

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

自動化證明：
* 特定問題會比較快
* 但不代表能一定求解出證明

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

依值型別：
* Agda 與 Coq 幫助漸次展開證明
* 證明時間 > 測試時間
* 重要的軟體使用之驗證

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

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

</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、垃圾回收等等。

; 迴圈
<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


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