有件事情必须分清楚，程式语言上的函数，并不等同於数学上函数。 再来是实作跟语言也必须搞清楚，程式语言通常只规范， 但不说明该如何实作，虽然两者通常都有关系。 因此，若是只看待 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)