推 yzugsr:推推 10/02 08:54
推 horngsh:Programming Language by Sebesta看完再看完GCC實作, 再來 10/02 18:40
→ horngsh:吵, 或許會較有意義. 10/02 18:41
→ xcycl:那本太粗淺了... 10/03 07:42
推 kirk76:看這一串系列文感覺好像又多了解了一些 感謝 11/26 16:42
→ abzxcx:好深奧 03/13 18:26
有件事情必須分清楚，程式語言上的函數，並不等同於數學上函數。
再來是實作跟語言也必須搞清楚，程式語言通常只規範，
但不說明該如何實作，雖然兩者通常都有關係。
因此，若是只看待 Agda 這個例子，if 是直接被定義為
語言內的函數，因此 if 的確是個函數。如果仔細看這個語言，
會發現語言定義的內容極為精簡，包括連整數都是透過
inductive data types 在「語言之內」定義出來，
沒有所謂的 primitive data type 。
既然他是程式語言上的函數，那每個函數是不是能夠對應一個
數學上的函數呢？那我們就必須把語言每個組件都對應到數學結構上，
data type 必須要有對應的數學結構，這樣才能說明函數的是什麼。
因為在 Agda 上有 termination checker，可以保證每個語言上的函數，
給定輸入就有輸出。雖然這語言具備 dependent type，但若只考慮
simple type 的部分，每個 data type D 可以單純地對應一個集合 D'。
對於 f : D -> E 上 Agda 的函數，
配合 termination checker，f(x) 必然回傳 E 上的資料。
因此 D -> E 的 Agda 函數則對應 D' -> E' 上的集合函數。
若考慮有 side-effect 的語言，為了說明把問題簡化一下，
我們考慮一個語言僅有 global variable, 沒有 exception, 變數名稱僅由英文字母組成,
不考慮如何分析語法的問題，程式僅由 statement 與 expression
（無限整數以及其操作）也沒有任何自行宣告或定義的函數等。
（所以這是一個沒有函數的語言）
在這語言內唯一會改變變數的值的 statement ，只有 assignment, =
然後也僅有 Boolean type。這可能稱不上一個有用的程式語言，但為了說明這已經夠了。
語法就像這樣
statement = {statement} | statement ; statement | skip
if (expression) then statement else statement | variable = expression
既然我們考慮的變數名稱僅以英文字母 EN = {a, ... z, A, ..., Z} 組成，
我們寫 EN+ 代表所有長度不為零的有限字串集合，有限字串在數學中可以用有限序列
也就是 N| -> EN 的函數來表達，其中 N| 代表 {0, ..., N-1} 的集合。
而每個變數名稱與一個值連繫在一起，可能是 true, false 或是 undefined，
（我並沒有說每個值預設為 undefined，這在這邊不重要）
那麼，實際上程式的狀態是代表一個函數 s : EN+ ---> {true, false, undefined}，
我們用 Bool' 代表 {true, false, undefined}，狀態 states 則是
{s : EN+ ---> Bool'} 這個從 EN+ 到 Bool' 的函數空間。
而我們知道 statement 會改變程式的狀態，*而且*若執行的狀態一樣的話，
同個 statement 會傳回一樣的狀態。也就是實際上，statement p 會對應到
一個函數 [p] : states -> states 。（用 [p] 代表 p 對應的數學結構，
而目前也可以將 [-] 當作是一個從程式到某個*預先知道*的數學結構上）
而在語言中我們並沒有 undefined ，所以從 expression 可以對應到
Bool' 上一個元素，但反過來並沒有，只有一個一對一的對應，將這個
對應的函數同樣用 [-] 代表。
那麼語言中唯一實際上會改變狀態的 assignment，對應到怎樣的函數呢？
var = expression
把目前狀態 s 對應到的狀態 s' ，除了 var 會對應 expression 之外，其他都一樣，
也就是
s(t) if t != var
s'(t) =
[expression] if t = var
也就是說 [var = expression](s) = s'。注意，[var = expression]
是一個狀態到狀態的函數。那麼 statement ; statement 則對應到函數合成，
[p ; q](s) = [q]( [p](s) ) = ([q] o [p])(s)。還有 [skip] 則是 identity
function，也就是 [skip](s) = s。
而最後 if 對應的語意，則很自然的對應如下
[p](s) if [expression] = true
[if (expression) then p else q] s =
[q)(s) otherwise
因此 if 的確能在數學上看作函數。相關資料，誠如我前一篇所講的，
這領域稱為 formal semantics，而這方法只是其中一種。
實務上可以用在檢驗程式的正確性，在非常關鍵的程式，例如交通控制的部分，
就有必要套用這類技術，不然上線後的錯誤可能會導致非常嚴重的問題。
在這個語言下，undefined 似乎沒什麼重要的，但如果考慮一般的語言，
會有跑不完的情況下，我們可以對應到 partial function ，
也就是並不是所有定義域上的元素都有對應，而這類含數可以透過
將這些沒有定義的元素，送到同一個元素上，得到 (total) function。
題外話，在這個觀點下，imperative 語言的狀態其實是被藏起來了，
操作的時候不能明確指出會被用到的變數有哪些，沒辦法只看函數的
signature 得知這件事情；而反過來, functional 的語言則是將
狀態包裝在特定的結構下傳遞，並不是像很多人認為的，FP 沒有狀態可以用。
※ 引述《ggg12345 (ggg)》之銘言：
: ※ 引述《godfat (godfat 真常)》之銘言：
: : 在現今 imperative 語言充斥的環境下，if 大多是 statement,
: : 而在有些有點 functional programming 意味的語言下，會是 expression.
: : 另外在很少數的地方，if 確實是個 function.
: : 在 if 是 function 的世界裡，例如 Agda 中，他的定義是
: : if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A
: : if true then t else f = t
: : if false then t else f = f
: : 可以在這邊看到程式，這是 Agda standard library
: : http://www.cs.nott.ac.uk/~nad/repos/lib/src/Data/Bool.agda
: : 這一個 function 用到了 mixfix:
: : http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Mixfix
: : 也就是說，當我們寫 if b then t else f 時，用一般語言的語法可以看成：
: : if(b, t, f)
: : 也當然了，整個程式本身是沒有任何 side-effect 的，否則這也無法成立。
: =============
: 假如是想寫一個 interpreter 或 compiler, 來句譯這個 if_statement:
: if(Boolean_Expression) then do {S_t} else do {S_f};
: 可以定義 IF_Func(Boolean_Expression, S_t, S_f)
: 根據 Boolean_expression 計算結果, 使 function 傳回的結果就是 S_t 或 S_f
: 再定義一個 Branch_do "function"(??? 有疑慮的 function):
: Branch_do(S)
: 就是跳躍到 statement label S 去執行.
: if_statement 就變換成:
: Branch_do(IF_Func(Boolean_Expression, S_t, S_f))
: 也就是 if_statement 可以用 function statement 做出來(合成).
: 兩者的差異就是對人在認知上的可讀性與方便性(人使用的語言).
: 在使用特定 compiler 的程式語言上, 當然最好不要把 if(b) 跟 foo(x) 解
: 說成是同一類的 function statement, 表面的形式雖像, 但 compiler 不是
: 全用同一個過程方法去處理.
: 通常, function_statement 是要得到計算結果, 不會有 Branch_do 這個可
: "隨意改變" 執行次序的功能在內.
: 當然, 這限制是可以被打破的, 但 Branch_do 就是 goto 是有麻煩顧忌的.
: Branch_do(S) 是相當於 Execute(Instruction_pointer, S), 就嚴謹的
: function 定義言, 她是 procedure 或 subroutine, 她改變了帶入的參數
: 值, 數學上的 function 是不會改變帶入的自變數. 就 Execute 言, 這不
: 是 數學上的 function.
: 就執行次序言, Branch_do(S) 還是個一去不回來的 procedure. 要適用
: call-return procedure 慣例還有其困難性. 但 procedure 是否一定要
: 執行 return instruction ? 顯然, 不執行 return 是特異的使用法.
: 推 yauhh:有個問題,call-return是非常必要的特徵嗎? 10/01 16:47
: 程式語言裡的 function 或 procedure 都是表明有 call-return 關係,
: 調用了 function , 執行後會回到下一句 statement 執行. 除了要結束
: 程式的執行, 才將 cpu 執行的 控制權還給 OS 或 shell, 才會一去不回.
: call-return 暗示了下一個執行次序, 是很固定的, 不會隨計算而變.(
: 除了 divid by zero trap 這類例外).
: 數學的 function 都是表示函數值是依據 表示式 計算後的結果, 不涉及
: 之後是再如何進行下一個步驟.
: 這裡的 Branch_do(S) 就不會是一般 高階程式語言 可以敘述出來的
: function routine.
: 換言之, if statement 是很有威力的指令, 使用他與 計算式 可以變化
: 出很多功能, 幾乎所有 computing function 都能實現. 但 function
: computing routine 若沒有 Branch_do(S) 功能的協助就很難兜出程式
: 語言上可改變執行次序的 if-statement.
: ※ 編輯: ggg12345 來自: 140.115.4.12 (10/01 19:54)
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 147.188.193.87
※ 編輯: xcycl 來自: 147.188.193.87 (10/02 06:02)