函數(shù)式編程語(yǔ)言、編程和程序驗(yàn)證-文庫(kù)吧資料
2024-10-27 21:04本頁(yè)面
【正文】 : int 程序由一個(gè)或多個(gè)表達(dá)式構(gòu)成 程序都可以翻譯成類型化的 ?表達(dá)式，在此不介紹 SML還有其他基本類型： real, bool, string等 函數(shù)式語(yǔ)言 SML及編程簡(jiǎn)介 ? 例 2（積類型）：把分?jǐn)?shù) n/d約分到最簡(jiǎn)分式 fun fraction(n, d) = /*(n, d)是 int ? int的元素 */ let val = gcd(n, d) in (n div , d div ) end。函數(shù)式編程語(yǔ)言、編程和程序驗(yàn)證 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 陳意云 內(nèi) 容 提 要 學(xué)習(xí)函數(shù)式語(yǔ)言是因?yàn)檎n程實(shí)踐所用工具中， 需要用函數(shù)式風(fēng)格編程。另外，需要對(duì)比函數(shù)式 程序和命令式程序在程序驗(yàn)證上的區(qū)別 ? 函數(shù)式編程語(yǔ)言概述 ? ?演算簡(jiǎn)介 ? 函數(shù)式語(yǔ)言 SML及編程簡(jiǎn)介 ? 函數(shù)式語(yǔ)言 SML的模塊系統(tǒng) ? 函數(shù)式程序的驗(yàn)證 函數(shù)式編程語(yǔ)言概述 ? 函數(shù)式編程是一種編程范型 – 它把計(jì)算看作是對(duì)數(shù)學(xué)函數(shù)的求值，避免了狀態(tài)和易變數(shù)據(jù)結(jié)構(gòu) – 函數(shù)是構(gòu)造程序的基本成分，語(yǔ)言還提供構(gòu)造更為復(fù)雜的函數(shù)的機(jī)制，語(yǔ)言禁止使用賦值語(yǔ)句 – 函數(shù)式編程的根基是 ?演算 – ?演算是 1930年代在調(diào)查函數(shù)定義、函數(shù)應(yīng)用和遞歸時(shí)研發(fā)的一個(gè)形式系統(tǒng)，是等價(jià)于圖靈機(jī)的一種抽象的計(jì)算模型 – 許多函數(shù)式編程語(yǔ)言都可看成是在 ?演算基礎(chǔ)上精心制作出的結(jié)果 函數(shù)式編程語(yǔ)言概述 ? 函數(shù)式與命令式的比較 – 函數(shù)式編程強(qiáng)調(diào)函數(shù)應(yīng)用，而命令式編程風(fēng)格強(qiáng)調(diào)狀態(tài)的改變 – 命令式程序的 “ 函數(shù) ” 有副作用，如改變?nèi)肿兞? – 命令式程序缺乏引用透明性，副作用是其根源 引用透明性：可自由地將（子）表達(dá)式替換為它的值而不改變程序（表達(dá)式） – 函數(shù)式程序中，函數(shù)的結(jié)果僅依賴于提供給它的參數(shù) – 沒(méi)有副作用使得理解程序和預(yù)測(cè)程序的行為變得容易，這是研究函數(shù)式語(yǔ)言的一個(gè)關(guān)鍵動(dòng)機(jī) 函數(shù)式編程語(yǔ)言概述 ? 函數(shù)式語(yǔ)言的用途 – 歷史上，（純）函數(shù)式語(yǔ)言一直被學(xué)術(shù)界（而不是商用軟件研發(fā)）重視 – 現(xiàn)在， Scheme, OCaml和 Haskell等函數(shù)式語(yǔ)言已經(jīng)出現(xiàn)在工業(yè)和商業(yè)應(yīng)用中 – 通過(guò)領(lǐng)域?qū)Ｓ镁幊陶Z(yǔ)言，函數(shù)式編程有更廣闊的天地，如 Mathematica（符號(hào)數(shù)學(xué)）、 R（統(tǒng)計(jì)）、 J和 K（金融分析） – 函數(shù)式編程的風(fēng)格也可用于不是專為函數(shù)式編程設(shè)計(jì)的語(yǔ)言中，如 Javascript融入了函數(shù)式編程的功能，類似的還有 Perl語(yǔ)言 ? 演 算 簡(jiǎn) 介 ?表示法 ? ?表示法的主要特征 – ?抽象： 用于定義函數(shù) – ?應(yīng)用： 將所定義的函數(shù)作用于變?cè)? ? ?抽象的例子 （ 自然數(shù)類型上的幾個(gè)例子 ） – 恒等函數(shù) ： ?x : // 命令式表示 Id(x : nat) = x – 后繼函數(shù)： ?x : ? 1 // 函數(shù)式無(wú)需給函數(shù)命名 – 常函數(shù)： ?x : – ?x : ? true 不是良形的表達(dá)式 ? ?表示法寫出的表達(dá)式叫做 ?表達(dá)式 或 ?項(xiàng) ? 演 算 簡(jiǎn) 介 ? ?項(xiàng) ?x : ?.M 和謂詞演算公式 ?x : A.? 的比較 – ?是一個(gè)約束算子 – x是一個(gè)占位符 ，約束變?cè)?，?以重新命名 ?約束變?cè)?而不改變表達(dá)式的含義 – 在 ?x:?.x + y中， x的出現(xiàn)是 約束的， y的出現(xiàn)是 自由的 – 不含自由變?cè)谋磉_(dá)式稱為 閉表達(dá)式 ? ?應(yīng)用： 用項(xiàng)的并置來(lái)表示函數(shù)應(yīng)用，例： – (?x : ) 5 – (?x :
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1