第6章遞歸類型(參考版)
2024-10-02 15:49本頁(yè)面
【正文】 第 6章 遞歸類型 ? 遞歸定義的類型的例子 – 自然數(shù)表的類型 類型等式 t ? unit + (nat ? t)的一個(gè)解 – 二叉樹(shù)的類型 類型等式 t ? unit + (t ? t)的一個(gè)解 使用“ ? ” 表示解是要使兩邊同構(gòu)，而不是相等 歸納類型對(duì)應(yīng)到 上述 類型同構(gòu)等式的初始解 例：自然數(shù)類型 余歸納類型對(duì)應(yīng)到它們的終結(jié)解 例：自然數(shù)流類型 引 言 本章的主要內(nèi)容 ? 直觀地介紹余歸納的定義、余歸納的證明原理和余代數(shù) ? 形式地介紹遞歸類型 ? 形式地介紹歸納類型和余歸納類型 ? 解釋 – 代數(shù)方法是從“構(gòu)造的”角度研究抽象數(shù)據(jù)類型 – 余代數(shù)方法是從“觀察的”的角度描述 像 對(duì)象、自動(dòng)機(jī)、進(jìn)程、軟件構(gòu)件等基于狀態(tài)的系統(tǒng)。 歸納和余歸納 余歸納現(xiàn)象 ? 例 數(shù)據(jù) 集 A上的有限表集可歸納地定義 如下 (1) 基礎(chǔ) 情況： nil是有限 表 (2) 迭代 規(guī)則 ： 若 a?A且 ?是有限表，則 cons(a, ?)是有限 表 (3) 最小 化條件 ：此外 ，有限表集中不含其它 元素 最小 化 規(guī)則指 所定義的集合是 滿足 (1)和 (2)兩條約束 的最小集合 ， 無(wú) 任何垃圾在其中 歸納和余歸納 ? 例 數(shù)據(jù)集 A上的無(wú)限表集（流）可余歸納地定義如下 (1) 迭代規(guī)則： 若 a?A且 ?是無(wú)限表，則 cons(a, ?)是無(wú)限表 (2) 最大化條件：數(shù)據(jù)集 A上的無(wú)限表集是滿足迭代規(guī)則的最大集合 最大化條件表示所有未被 (1)排除的元素都被包含在所定義的集合中，即該集合中任何無(wú)限表都可以通過(guò)應(yīng)用規(guī)則 (1)若干次（可能是無(wú)限次）而得到 歸納和余歸納 ? 比較 – 兩種表 都有觀察算子 head和運(yùn)算算子 tail head(cons(a, ?)) = a tail(cons(a, ?)) = ? – 計(jì)算 有限表 表長(zhǎng)的函數(shù) length length(nil) = 0 length(cons(a, ?)) = 1 + length(?) – 若 有函數(shù) f : A ? A，定義 其應(yīng)用到無(wú)限表所有元素的 拓展函數(shù) ext(f ) head(ext(f )(?)) = f (head(?)) tail(ext(f )(?)) = ext(f )(tail(?)) 歸納和余歸納 ? 例 無(wú)限表 上的 odd運(yùn)算 （忽略所有 偶數(shù)位置的元素 ） head(odd(?)) = head(?) tail(odd(?)) = odd(tail(tail(?))) – 用等式演算可得 head(tail(odd(?))) = head(odd(tail(tail(?)))) = head(tail(tail(?))) – 不難證明，對(duì)所有的自然數(shù) n head(tail(n) (odd(?))) = head(tail(2n) (?)) 歸納和余歸納 ? 余歸納定義的數(shù)據(jù)和函數(shù)的性質(zhì)證明 可以用歸納法來(lái)證明 ，例如證明 head(tail(n) (odd(?))) = head(tail(2n) (?)) 互模擬 —— 余歸納證明專用方法 – 從數(shù)學(xué)上刻畫(huà)系統(tǒng)（如對(duì)象、進(jìn)程等）行為等價(jià)這個(gè)直觀概念 – 指兩個(gè)系統(tǒng)從觀測(cè)者角度看，可以互相模擬對(duì)方的行為 歸納和余歸納 ? 例：無(wú)限表 定義 odd head(odd(?)) = head(?) tail(odd(?)) = odd(tail(tail(?))) 定義 even even = odd ? tail 定義 merge head(merge(?, ?)) = head(?) tail(merge(?, ?)) = merge(?, (tail(?)) 歸納和余歸納 基于互模擬證明 merge(odd(?), even(?)) = ? – 互模擬是滿足下面條件的關(guān)系 R： 若 ??, ?? ?R， 則 head(?) = head(?) 并且 ?tail(?), tail(?)? ?R – 基于互模擬的余歸納證明原理是： 對(duì)互模擬關(guān)系 R，若 ??, ?? ?R，則 ? = ? – 定義關(guān)系 R =
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1