函數(shù)式編程語(yǔ)言、編程和程序驗(yàn)證-展示頁(yè)
2024-10-31 21:04本頁(yè)面
【正文】 ) 5 ? 5 /*應(yīng)用下頁(yè)介紹的 ?公理 */ ? 演 算 簡(jiǎn) 介 ?演算 ?演算是關(guān)于 ?表達(dá)式的一個(gè)推理系統(tǒng)，下面用等式公理系統(tǒng)（公理語(yǔ)義）來(lái)描述 ? 約束變?cè)拿?（ ?公理 ） – ?x:?.M ? ?y:?.?y?x?M， M中無(wú)自由出現(xiàn)的 y – ?N?x?M表示 M中自由出現(xiàn)的 x用表達(dá)式 N代換的結(jié)果 – 例如 ?x:?.x ? ?y:?.y ? 函數(shù)應(yīng)用公理 （ ?公理 ） – (?x:?.M)N ? [N/x]M – 例如 (?x:+4) 4 ? [4/x](x+4) ? 4 + 4 ? 演 算 簡(jiǎn) 介 ? 自反公理、對(duì)稱性規(guī)則、傳遞性規(guī)則 ? 同余規(guī)則 – 相等的函數(shù)作用于相等的變?cè)a(chǎn)生相等的結(jié)果 ? 等式證明規(guī)則允許推導(dǎo)任何一組等式前提的邏輯推論 還可以定義 ?演算的操作語(yǔ)義和指稱語(yǔ)義 M1 = M2, N1 = N2 M1 N1 = M2 N2 ? 演 算 簡(jiǎn) 介 ? 簡(jiǎn)單例子 ( ?x. ( ?y. ?z. ( x + y ) + z ) 3 ) 4 5 = ( ?x. ?z. ( x + 3 ) + z ) 4 5 = ( ?z. ( 4 + 3 ) + z ) 5 = ( 4 + 3 ) + 5 = 12 ? 演 算 簡(jiǎn) 介 ? 復(fù)雜例子：高階函數(shù)應(yīng)用到函數(shù)，得到函數(shù) Curry?,? ? ?f :? ?? ??. ?x:?. ?y:?. f ?x, y? add ? ?p:nat ? nat. (Proj1 p) + (Proj2 p) Curry(add) = ?x:nat. ?y:nat. x + y 演算過(guò)程在下頁(yè)，給 Curry加上角標(biāo)是避免引入多態(tài) 該例體現(xiàn)函數(shù)式語(yǔ)言區(qū)別命令式語(yǔ)言的優(yōu)點(diǎn) – 函數(shù)作為編程語(yǔ)言的第一類實(shí)體，即對(duì)它們的使用沒有限制 – 可以動(dòng)態(tài)地構(gòu)造新函數(shù) ? 演 算 簡(jiǎn) 介 ? 復(fù)雜例子：高階函數(shù)應(yīng)用到函數(shù)，得到函數(shù) Curry(add) ? (?f:nat ? nat ? nat. ?x:nat. ?y:nat. f ?x, y?) add = ?x:nat. ?y:nat. add ?x, y? ? ?x:nat. ?y:nat. (?p:nat ? nat. (Proj1 p) + (Proj2 p)) ?x, y? = ?x:nat. ?y:nat. Proj1?x, y? + Proj2 ?x, y? = ?x:nat. ?y:nat. x + y 函數(shù)式語(yǔ)言 SML及編程簡(jiǎn)介 使用 Standard ML語(yǔ)言，簡(jiǎn)稱 SML ? 例 1（整型）： 輾轉(zhuǎn)相除法求最大公約數(shù) fun gcd(m, n) = /*函數(shù)聲明表達(dá)式 */ if m = 0 then n else gcd(n mod m, m)。 val fraction = fn : int ? int int ? int 引入 let后，表達(dá)式的一般形式是 let D1 D2 … D n in E end let 引入的聲明相當(dāng)于命令式語(yǔ)言的局部聲明， let聲 明可以嵌套，聯(lián)立的 let可用來(lái)聲明相互遞歸的函數(shù) 使用 let可使程序簡(jiǎn)潔，免去重復(fù)計(jì)算公共子表達(dá)式 函數(shù)式語(yǔ)言 SML及編程簡(jiǎn)介 ? 例 3（記錄類型） type student = { name : string。 score : real } type student 記錄是具
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1