上次課程小結(jié)-閱讀頁
2024-11-01 13:44本頁面
【正文】 (t) 或者說 S是代換次數(shù)最少的一個實例，即一旦有了可以確定類型是否等價的代換結(jié)果，就馬上停止代換。此處代換算法僅考慮了函數(shù)的情況，而其它類型構(gòu)造符的類型代換與之類似。 if t is a basic_type then return t。 返回類型變量的一個代換實例 elsif t is t1→t 2 then return subs(t1)→subs(t 2)。 ? 與等價算法比較 ? 在算法中加入其它類型構(gòu)造符 代換算法（續(xù)） if t is a basic_type then return t。 類型變量的代換實例 elsif t is t1→t 2 then return subs(t1)→subs(t 2)。 ? real real ? int→int α→α ? pointer(int) pointer(α) ? αβ 而： ? int ≮ real， 因為 int和 real是不同的基本類型表達式 。 ? int→α ≮ α→α ， 因為 α 的代換不完全，映射的左邊被代換，而右邊沒有代換。 所謂判定類型表達式 e和 f是否能合一，就是能否找到一個代換 S，使得 S(e)=S(f)，即檢查 e和 f在代換 S下是否等價。 多態(tài)函數(shù)的類型檢查（續(xù) 1） 1. fresh(t)： 將類型表達式 t中的約束變元用一新的自由變元來代替 ， 若 t是一個類型常量則結(jié)果仍然是 t自身 。 不同的是fresh產(chǎn)生的是類型變量的自由變元 α 、 β 、 δ 等 。 2. union(m, n)： 構(gòu)造 m和 n的等價類 ， 并在等價類中選取一個代表 。 ? 否則任選其一作為代表 ， 例如可以選取節(jié)點編號小的 。 語義函數(shù)： 多態(tài)函數(shù)的類型檢查（續(xù) 2） 算法 類型表達式的合一算法 輸入 以 m和 n為根的兩棵類型表達式的語法樹 輸出 若 m和 n代表的類型表達式能合一則返回 true否則 false 方法 用下述遞歸函數(shù)進行代換： function unify(m, n: nptr) return boolean is begin end unify。 t := find(n)。 elsif s和 t代表相同基本類型 then union(s,t)。 elsif s和 t代表相同類型構(gòu)造符并分別有孩子節(jié)點 (s1, s2)和 (t1, t2) then union(s, t)。 分別合一左右孩子 elsif s或 t代表一個變量 then union(s, t)。 else return false。 多態(tài)函數(shù)的類型檢查（續(xù) 3） 多態(tài)函數(shù)文法 ()中表達式類型檢查的語義規(guī)則： E→E 1(E2) { γ := mkleaf(newtypevar)。→39。 := γ 。 39。 } |id { := fresh()。則應有未知類型γ ，使得 S(α)=S(β→γ) 。若 m與 n合一成功則其結(jié)果 γ 成為 。 E→E 1(E2) { γ := mkleaf(newtypevar)?！?9。 := γ 。 } E5E1 ( E4 )deref E2 ( E3 )deref qE1 → deref =fresh()=pointer(α 0)→α 0 E2 → deref =fresh()=pointer(α 1)→α 1 E3 → q =fresh()=pointer(pointer(int)) E4 → E2(E3) =γ 1=pointer(int) E5 → E1(E4) =γ 0=int deref(deref(q))的類型檢查（續(xù) 1） 確定 ： 建立葉子 γ 1和→γ 1的新節(jié)點 m： n2:→: 6pointer: 5α1:4pointer(α 1)→α 1 : n3:pointer: 9pointer: 8int: 7pointer(pointer(int)) : 合一 n2和 m，即unify(11, 6)： m : →: 11n3: pointer: 9 γ1: 10pointer: 8int: 7unify(11,6)union(11,6)→6unify(9,5) unfiy(10,4)union(9,5)→5 find(4)=8unify(8,4) union(10,8)→8union(8,4)→8得到 =pointer(int)： pointer: 5 pointer: 8int: 7m:→: 6: E4 → E2(E3) =γ 1=pointer(int) deref(deref(q))的類型檢查（續(xù) 2） 再確定 ： 建立葉子 γ 0和 →γ 0的新節(jié)點 m39。 :→ : 12int: 7合一 n1和 m39。:→: 3有環(huán)類型的合一操作 real: 2→: 1real: 4→: 3→: 5real: 6union(1,5)→1unify(1,3)union(1,3)→1unify(2,4) unfiy(1,5)unify(2,6) unify(1,3)find(1)=find(3)real: 2→: 1→: 1real: 2結(jié) 束（ 2020年 5月 10日） ()與 () 聲明時 id類型的確定 P → D。D D → id : T { addtype(entry(), )。 } () | integer { := integer。} | array[num]of T1 { := array(, )。} () T → T1 → T2 { := → 。 } 返回
教學課件相關(guān)推薦
鄂ICP備17016276號-1