有件事情必須分清楚，程式語言上的函數，並不等同於數學上函數。 再來是實作跟語言也必須搞清楚，程式語言通常只規範， 但不說明該如何實作，雖然兩者通常都有關係。 因此，若是只看待 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)