第10章子定型-資料下載頁(yè)
2025-09-19 16:45本頁(yè)面
【導(dǎo)讀】子定型是類(lèi)型上的一種關(guān)系，該關(guān)系隱含一。和子定型有關(guān)的語(yǔ)言概念是記錄、對(duì)象及依。本章考慮子定型和體現(xiàn)子定型在程序設(shè)計(jì)中。等式理論和語(yǔ)義模型。類(lèi)型化面向?qū)ο笳Z(yǔ)言。當(dāng)兩個(gè)類(lèi)型相等時(shí)，若表達(dá)式屬其中一個(gè)類(lèi)型，有子定型的簡(jiǎn)單類(lèi)型化?本節(jié)用子定型來(lái)拓展??–Sub是類(lèi)型常量b,b??在每個(gè)系統(tǒng)中，對(duì)每種類(lèi)型形式，至少有一。對(duì)第二個(gè)變?cè)菃握{(diào)的，但是對(duì)第一個(gè)變?cè)恰nt解釋成一個(gè)函數(shù)集合，這些函數(shù)的定。項(xiàng)的所有定型規(guī)則：、、的正好包含同樣的公理。–通常，只有在??Mx在M中不是自由的。適當(dāng)?shù)囟xM（?是可推導(dǎo)的，因此
【正文】 col_point = ?x: int, y: int, c: color, move: int ? int ? col_point? – 總希望 col_point是 point的子類(lèi)型 – 關(guān)鍵看 “ 相容 ” – 可以通過(guò)考慮操作 序列來(lái)理解 它們的相容性 遞歸類(lèi)型和對(duì)象的記錄模型 ? 第二個(gè)例子： 子定型失敗在表面上類(lèi)似的遞歸記錄類(lèi)型上 type simple_set = ?member? : elt ? bool, insert: elt ? simple_set, intersect: simple_set ? simple_set? type sized_set = ?member? : elt ? bool, insert: elt ? sized_set, intersect: sized_set ? sized_set, size: int? 兩個(gè) intersect的變?cè)?lèi)型是不同的 遞歸類(lèi)型和對(duì)象的記錄模型 type simple_set = ?member? : elt ? bool, insert: elt ? simple_set, intersect: simple_set ? simple_set? type sized_set = ?member? : elt ? bool, insert: elt ? sized_set, intersect: sized_set ? sized_set, size: int? – 假定 s, t: simple_set且 r: sized_set – 計(jì)算兩個(gè)簡(jiǎn)單集合的交集的表達(dá)式 t – 表達(dá)式 t可能會(huì)引起錯(cuò)誤 遞歸類(lèi)型和對(duì)象的記錄模型 type simple_set = ?member? : elt ? bool, insert: elt ? simple_set, intersect: simple_set ? simple_set? type sized_set = ?member? : elt ? bool, insert: elt ? sized_set, intersect: sized_set ? sized_set, size: int? type sized_set? = ?member? : elt ? bool, 改用 insert: elt ? sized_set?, sized_set? intersect: simple_set ? sized_set?, 來(lái)解決 size: int? 遞歸類(lèi)型和對(duì)象的記錄模型 ? ?:, record, ?的等式規(guī)則和子定型規(guī)則 (trans :)（ ） (? :)（ ） record :)（ ） – 需要一條推理規(guī)則從相等斷言得到子定型斷言 ，還需要一條規(guī) 則用于遞歸類(lèi)型 ? :?, ? :? ? :? ? :?, ?? :?? ? ??? :? ??? ?1 : ? 1, . . . , ?n : ? n ? l1:?1 , …, ln:?n, ln+1:?1 , …, ln+m:?m? : ? l1 :?1, …, ln:?n? ? 遞歸類(lèi)型和對(duì)象的記錄模型 ? ?:, record, ?的等式規(guī)則和子定型規(guī)則 – 從相等斷言 得到子定型斷言的規(guī)則 (= :) – 用于遞歸類(lèi)型的規(guī)則 t在 ?中不是自由的 ， s在 ?中不是自由的 (? :) ? = ? ? : ? , s : t ?? : ? ? ?s.? : ?t.? ? 遞歸類(lèi)型和對(duì)象的記錄模型 ? 證明 col_point : point – 最后一步的 形式必定是 – 應(yīng)先證 int : int和 col_point : point ? int ? (int ? col_point) : int ? (int ? point) – 后者從 自反性和假設(shè) col_point : point， 兩次應(yīng)用(? :)規(guī)則可得 col_point : point ? ?x: int, y: int, move: int?int?col_point, c: color? : ?x: int, y: int, move: int?int ? point? ? col_point. ?. . .? : ? point. ?. . .? 遞歸類(lèi)型和對(duì)象的記錄模型 ? 加相等測(cè)試方法到點(diǎn)和有色點(diǎn) ,則子定型失敗 type eq_point = ?x: int, y: int, eq: eq_point ? bool? type eq_col_point=?x: int, y: int, eq:eq_col_point?bool, c: color? – 最后 一步的形式總是 – 需要先證 int : int和 eq_col_point : eq_point ? (eq_col_point ? bool) : (eq_point ? bool) – 后者需要證明 eq_col_point : eq_point ? eq_point : eq_col_point eq_col_point :eq_point ? ?x:int, y:int, eq:eq_col_point?bool, c:color? : ?x: int, y: int, eq: eq_point? bool? ? eq_col_point. ?. . .? : ? eq_point. ?. . .? 習(xí) 題 第一次： , 第二次：
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1