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