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