第8章依賴類型PPT課件

1、第第8章章 依賴類型依賴類型 本章內(nèi)容本章內(nèi)容 帶依賴類型的演算，包括依賴積與依賴和帶依賴類型的演算，包括依賴積與依賴和 概要介紹概要介紹Dependent ML（DML），以此來展示），以此來展示怎樣把依賴類型用到實(shí)際語言中，這是當(dāng)前程序怎樣把依賴類型用到實(shí)際語言中，這是當(dāng)前程序設(shè)計(jì)語言研究的一個(gè)課題設(shè)計(jì)語言研究的一個(gè)課題 帶廣義積與廣義和的直謂式演算，以及它們同帶廣義積與廣義和的直謂式演算，以及它們同SML及其相近語言的模塊系統(tǒng)的聯(lián)系及其相近語言的模塊系統(tǒng)的聯(lián)系8.1 引引 言言 項(xiàng)和類型之間的關(guān)系項(xiàng)和類型之間的關(guān)系(1) 項(xiàng)項(xiàng) 類型類型 項(xiàng)項(xiàng)多態(tài)性多態(tài)性：( t :U1. x : t.x

2、) int = x : int.x(2) 類型類型 類型類型 類型類型類型類型表達(dá)式的表達(dá)式的分類分類：從：從 1: 1和和 2: 2得到得到 1 2: 1 2(3) 項(xiàng)項(xiàng) 項(xiàng)項(xiàng) 項(xiàng)項(xiàng)簡單類型化簡單類型化 演算中函數(shù)演算中函數(shù)應(yīng)用應(yīng)用：( x : int.x)5 = 5(4) 類型類型 項(xiàng)項(xiàng) 類型類型依賴依賴類型類型：依賴于項(xiàng)的類型依賴于項(xiàng)的類型8.1 引引 言言 依賴類型的應(yīng)用依賴類型的應(yīng)用 zero_vector : n: nat.vector n 對(duì)給定的自然數(shù)對(duì)給定的自然數(shù)n，該函數(shù)該函數(shù)返回長度為返回長度為n的零向量的零向量（vector是一個(gè)類型構(gòu)造符是一個(gè)類型構(gòu)造符） cons:

3、 n: nat.data vector n vector (n+1) 構(gòu)造較長向量的函數(shù)構(gòu)造較長向量的函數(shù)cons的類型的類型 sprintf : f: Format.Data(f) String 函數(shù)函數(shù)sprintf的類型的一個(gè)簡化版本的類型的一個(gè)簡化版本 依賴類型的使用可以對(duì)項(xiàng)給出更精確的定型，因依賴類型的使用可以對(duì)項(xiàng)給出更精確的定型，因而用類型系統(tǒng)可以更多地排除有不良行為的項(xiàng)而用類型系統(tǒng)可以更多地排除有不良行為的項(xiàng)8.2 帶依賴類型的演算帶依賴類型的演算8.2.1 依賴積類型依賴積類型介紹一種最簡單的依賴類型系統(tǒng)介紹一種最簡單的依賴類型系統(tǒng) LF，它是奠定邏，它是奠定邏輯框架輯框架Ed

4、inburgh LF的類型系統(tǒng)的一種簡化版本的類型系統(tǒng)的一種簡化版本索引類型索引類型A上的依賴積類型上的依賴積類型x:A.B是一族集合是一族集合B(x) | x A的笛卡兒積的笛卡兒積積的元素都是函數(shù)積的元素都是函數(shù)f，對(duì)每個(gè)，對(duì)每個(gè)a A有有f(a) a xB若若x在表達(dá)式在表達(dá)式B中沒有自由出現(xiàn)中沒有自由出現(xiàn)則則對(duì)每個(gè)對(duì)每個(gè)a A都有都有f(a) B依賴積類型依賴積類型 x:A.B退化為函數(shù)類型退化為函數(shù)類型AB依賴積類型依賴積類型 x:A.B是函數(shù)類型是函數(shù)類型AB的一種拓廣的一種拓廣8.2 帶依賴類型的演算帶依賴類型的演算 集合族集合族 B(x) | x A的每個(gè)集合的每個(gè)集合B(x)

5、對(duì)應(yīng)一個(gè)以類型對(duì)應(yīng)一個(gè)以類型A的的元素元素x為索引的類型為索引的類型 這一族類型構(gòu)成一個(gè)以類型這一族類型構(gòu)成一個(gè)以類型A的元素為索引的類的元素為索引的類型族型族8.2 帶依賴類型的演算帶依賴類型的演算 良形上下文的公理和推理規(guī)則良形上下文的公理和推理規(guī)則 有有項(xiàng)、類型和種類三種語法項(xiàng)、類型和種類三種語法范疇范疇 未經(jīng)檢查的預(yù)備未經(jīng)檢查的預(yù)備種類種類、預(yù)備類型和預(yù)備項(xiàng)、預(yù)備類型和預(yù)備項(xiàng)的的文法文法語法語法范疇范疇項(xiàng)目項(xiàng)目具體具體形式形式種類種類 := Type | x: .k類型類型 := b | t | x: . | M項(xiàng)項(xiàng)M := c | x | x: .M | MM 特點(diǎn)：特點(diǎn)：依賴依賴積

6、類型和類型積類型和類型應(yīng)用應(yīng)用作作為類型。為類型。在在 M中，中， 只允許是依賴積只允許是依賴積類型類型，它，它決定決定了了一一個(gè)類型個(gè)類型族族。種類種類用來區(qū)分常規(guī)用來區(qū)分常規(guī)類型和類型和類型類型族族8.2 帶依賴類型的演算帶依賴類型的演算 上下文上下文 := | , x : | , t : k 項(xiàng)項(xiàng)變量的類型變量的類型約束約束、類型類型變量的種類變量的種類約束約束 把把 看成有序看成有序的的，設(shè)計(jì)設(shè)計(jì)證明系統(tǒng)來證明上下文良證明系統(tǒng)來證明上下文良形形與否與否并不困難并不困難 下面下面把把 看成無序的看成無序的集合集合，以簡化定類規(guī)則和定，以簡化定類規(guī)則和定型規(guī)則的設(shè)計(jì)型規(guī)則的設(shè)計(jì)8.2 帶依

7、賴類型的演算帶依賴類型的演算 良形種類的兩條形成規(guī)則良形種類的兩條形成規(guī)則 Type (base kind) (type family kind) : Type , x : k x: .k8.2 帶依賴類型的演算帶依賴類型的演算 定類規(guī)則定類規(guī)則 b : (對(duì)基調(diào)中的每個(gè)類型常量對(duì)基調(diào)中的每個(gè)類型常量b : ) (cstk) (vark) (Type Intro ) ( k Elim) (kind eq) 1 : Type , x : 1 2 : Type ( x : 1. 2) : Type t : t : 1 : ( x: 2. ) M : 2 1M : M/x : 1 1= 2 : 2

8、8.2 帶依賴類型的演算帶依賴類型的演算 定型規(guī)則定型規(guī)則 c : (對(duì)基調(diào)中的每個(gè)項(xiàng)常量對(duì)基調(diào)中的每個(gè)項(xiàng)常量c : ) (cst) (var) ( Intro) ( Elim) (type eq) x : : Type x : 1 : Type , x : 1 M : 2 x: 1.M : ( x : 1. 2) M1 : ( x: 1. 2) M2 : 1 M1M2 : M2/x 2 M : 1 1= 2 M : 2 8.2 帶依賴類型的演算帶依賴類型的演算 良形良形的的種類斷言、定類斷言和定型斷言是相種類斷言、定類斷言和定型斷言是相互定義的互定義的，導(dǎo)致的結(jié)果是導(dǎo)致的結(jié)果是 在證明該系統(tǒng)

9、中的性質(zhì)時(shí)，需要使用同時(shí)結(jié)構(gòu)歸在證明該系統(tǒng)中的性質(zhì)時(shí)，需要使用同時(shí)結(jié)構(gòu)歸納或者使用全面度量的推導(dǎo)高度，來對(duì)不同形式納或者使用全面度量的推導(dǎo)高度，來對(duì)不同形式的斷言進(jìn)行同時(shí)證明的斷言進(jìn)行同時(shí)證明8.2 帶依賴類型的演算帶依賴類型的演算 依賴類型用于表示其它類型理論和形式系統(tǒng)依賴類型用于表示其它類型理論和形式系統(tǒng) 例例 描述描述語言：語言：基于依賴類型系統(tǒng)基于依賴類型系統(tǒng)的語言的語言 對(duì)象語言對(duì)象語言：簡單類型化簡單類型化 演算演算 對(duì)象語言的類型和各種類型的項(xiàng)都用描述語言的對(duì)象語言的類型和各種類型的項(xiàng)都用描述語言的項(xiàng)表示項(xiàng)表示 它們分屬描述語言的不同類型，以便體現(xiàn)對(duì)象語它們分屬描述語言的不同類型

10、，以便體現(xiàn)對(duì)象語言的類型系統(tǒng)言的類型系統(tǒng) 若不出現(xiàn)依賴性，則若不出現(xiàn)依賴性，則在描述語言中，在描述語言中， x: .k和和 x: 1. 2分別簡化成分別簡化成 k和和 1 2的形式的形式8.2 帶依賴類型的演算帶依賴類型的演算 具體描述具體描述Ty:Type/ Ty用于表示對(duì)象語言的類型用于表示對(duì)象語言的類型Tm:Ty Type / Tm用于用于表示對(duì)象語言的項(xiàng)表示對(duì)象語言的項(xiàng)base:Tyarrow:Ty Ty Tyapp: A:Ty. B:Ty.Tm(arrow A B) Tm A Tm Blam: A:Ty. B:Ty.(Tm ATm B) Tm(arrow A B)A:Ty/ A是是對(duì)

11、象語言的一個(gè)類型對(duì)象語言的一個(gè)類型TmA:Type / TmA是是種類種類Type的另一的另一個(gè)個(gè)類型類型x:TmA/ x是是對(duì)象對(duì)象語言中類型語言中類型A的項(xiàng)的項(xiàng)8.2 帶依賴類型的演算帶依賴類型的演算 具體描述具體描述Ty:Type/ Ty用于表示對(duì)象語言的類型用于表示對(duì)象語言的類型Tm:Ty Type / Tm用于表示對(duì)象語言的項(xiàng)用于表示對(duì)象語言的項(xiàng)base:Tyarrow:Ty Ty Tyapp: A:Ty. B:Ty.Tm(arrow A B) Tm A Tm Blam: A:Ty. B:Ty.(Tm ATm B) Tm(arrow A B)arrowAB :Ty/ arrowAB是

12、是對(duì)象語言的函數(shù)類型對(duì)象語言的函數(shù)類型lam A A ( x:Tm A.x) : Tm(arrow A A)/ 對(duì)象語言對(duì)象語言的恒等函數(shù)的恒等函數(shù) x:A.x8.2 帶依賴類型的演算帶依賴類型的演算 邏輯邏輯框架框架提供提供機(jī)制來描繪構(gòu)成一個(gè)邏輯的語法和證明系機(jī)制來描繪構(gòu)成一個(gè)邏輯的語法和證明系統(tǒng)的統(tǒng)的系統(tǒng)系統(tǒng) 具體具體的描述機(jī)制依賴于所用的邏輯的描述機(jī)制依賴于所用的邏輯框架框架 邏輯框架邏輯框架Edinburgh LF推崇的方式體現(xiàn)在它的推崇的方式體現(xiàn)在它的口號(hào)口號(hào)“判斷作為類型判斷作為類型”(judgments-as-types)中中，其含義是類型用來捕獲一個(gè)邏輯的其含義是類型用來捕獲一

13、個(gè)邏輯的判斷判斷，下一下一章章將介紹這方面的一些將介紹這方面的一些知識(shí)知識(shí)8.2 帶依賴類型的演算帶依賴類型的演算8.2.2 依賴和依賴和類型類型 依賴和同樣可以看成直截了當(dāng)?shù)募险撘蕾嚭屯瑯涌梢钥闯芍苯亓水?dāng)?shù)募险摌?gòu)造構(gòu)造 x:A.B叫做索引集合叫做索引集合A上的依賴和上的依賴和類型類型 它它是一族集合是一族集合B(x) | x A的可區(qū)分的的可區(qū)分的并并 該和的成員是序?qū)υ摵偷某蓡T是序?qū)?a, b ，其中，其中a A，b a xB 若若x在表達(dá)式在表達(dá)式B中沒有自由出現(xiàn)，那么對(duì)每個(gè)中沒有自由出現(xiàn)，那么對(duì)每個(gè)a A都有都有b B，這時(shí)，這時(shí)依賴依賴和和類型類型 x:A.B退化為二元積退化為二

14、元積類型類型A B8.2 帶依賴類型的演算帶依賴類型的演算 拓展拓展8.2.1節(jié)節(jié) LF的項(xiàng)和的項(xiàng)和類型類型語法范疇語法范疇項(xiàng)目項(xiàng)目具體具體形式形式種類種類 := 類型類型 := | x: . 項(xiàng)項(xiàng)M := | x: = M, M: | first(M) | second(M) 序?qū)π驅(qū)?x: 1 = M1, M2: 2 中顯式地加入了類型中顯式地加入了類型 x: 1. 2，用來修飾，用來修飾M1和和M2 若若 2: 1 Type、M1: 1并且并且M2: 2M1，則則序?qū)π驅(qū)?M1, M2 的的類型類型是是 x: 1. 2（或（或 1 2M1）8.2 帶依賴類型的演算帶依賴類型的演算 增加一

15、條定類規(guī)則增加一條定類規(guī)則 (Type Intro )這條規(guī)則只引入這條規(guī)則只引入Type種類的依賴和類型種類的依賴和類型 1 : Type , x : 1 2 : Type ( x : 1. 2) : Type 8.2 帶依賴類型的演算帶依賴類型的演算 增加定型規(guī)則增加定型規(guī)則 ( Intro) ( Elim)1 ( Elim)2 ( x: 1. 2):Type M1: 1 M2:M1/x 2 x: 1 = M1, M2: 2 :( x: 1. 2) M:( x: 1. 2) first(M): 1 M:( x: 1. 2) second(M):first(M)/x 28.2 帶依賴類型的演

16、算帶依賴類型的演算 增加增加項(xiàng)上相等關(guān)系規(guī)則項(xiàng)上相等關(guān)系規(guī)則 ( first) ( second) ( sp) ( x: 1. 2) : Type M1: 1 M2:M1/x 2 first( x: 1 = M1, M2: 2 ) = M1: 1 ( x: 1. 2):Type M1: 1 M2:M1/x 2 second( x: 1 = M1, M2: 2 ) = M2:M1/x 2 ( x : 1. 2):Type ( x : 1 = first(M), second(M) : 2 ) = M:( x: 1. 2) 8.3 帶依賴類型的程序設(shè)計(jì)帶依賴類型的程序設(shè)計(jì) 把把依賴類型加到程序設(shè)計(jì)

17、語言中依賴類型加到程序設(shè)計(jì)語言中 在有依賴類型的情況下，類型檢查依賴于類型等在有依賴類型的情況下，類型檢查依賴于類型等價(jià)的判定價(jià)的判定 類型等價(jià)的判定又依賴于項(xiàng)等價(jià)的判定類型等價(jià)的判定又依賴于項(xiàng)等價(jià)的判定 這就要求打基礎(chǔ)的項(xiàng)語言是強(qiáng)范式化的這就要求打基礎(chǔ)的項(xiàng)語言是強(qiáng)范式化的 直接把依賴類型加到實(shí)際程序設(shè)計(jì)語言上，不可直接把依賴類型加到實(shí)際程序設(shè)計(jì)語言上，不可避免地導(dǎo)致不可判定的類型檢查避免地導(dǎo)致不可判定的類型檢查 為了降低類型檢查算法的復(fù)雜性，必須犧牲依賴為了降低類型檢查算法的復(fù)雜性，必須犧牲依賴類型的某些一般性類型的某些一般性8.3 帶依賴類型的程序設(shè)計(jì)帶依賴類型的程序設(shè)計(jì) DML(Depe

18、ndent ML) 類型對(duì)項(xiàng)的依賴不可以出現(xiàn)在任意類型的項(xiàng)上類型對(duì)項(xiàng)的依賴不可以出現(xiàn)在任意類型的項(xiàng)上 只能出現(xiàn)在某些作為索引類型只能出現(xiàn)在某些作為索引類型（稱為類別）（稱為類別）的項(xiàng)的項(xiàng)上上 類型檢查產(chǎn)生屬于索引類別的項(xiàng)上的一個(gè)約束系類型檢查產(chǎn)生屬于索引類別的項(xiàng)上的一個(gè)約束系統(tǒng)統(tǒng) 導(dǎo)致類型檢查轉(zhuǎn)換為索引類別上的約束求解問題導(dǎo)致類型檢查轉(zhuǎn)換為索引類別上的約束求解問題 目前目前DML將將索引類別限制到整型，并且是它的線索引類別限制到整型，并且是它的線性子集性子集8.3 帶依賴類型的程序設(shè)計(jì)帶依賴類型的程序設(shè)計(jì)8.3.1 簡化簡化DML的的實(shí)例實(shí)例 幾個(gè)和向量有關(guān)的例子幾個(gè)和向量有關(guān)的例子 有基本有

19、基本類型類型data 有有基本基本類型族類型族vector : intType，其中，其中vectorn指稱長度為指稱長度為n的的data數(shù)組數(shù)組 nil : vector0 cons : n:int.data vectorn vectorn+1 定型規(guī)則定型規(guī)則的的模板模板Match-Vector t1: vectori , i = 0 t2: , n:int, x:data, l:vectorn, i = n+1 t3: match t1 with nil t2 | consn(x, l) t3 : 8.3 帶依賴類型的程序設(shè)計(jì)帶依賴類型的程序設(shè)計(jì) 例例 把兩個(gè)向量拼接成一個(gè)向量的把兩個(gè)向

20、量拼接成一個(gè)向量的函數(shù)函數(shù)append append的類型的類型 m:int. n:int.vectormvectornvectorm+n append的函數(shù)的函數(shù)體體 append-body = m:int. n:int. l:vectorm. t:vectorn. match l with nil t | consr(x, y) consr+n(x, appendrn(y, t) 需要證明需要證明append的函數(shù)體和的函數(shù)體和append有同樣的有同樣的類型類型8.3 帶依賴類型的程序設(shè)計(jì)帶依賴類型的程序設(shè)計(jì) 令令 = m:int, n:int, l:vectorm, t:vectorn

21、，在在逆向應(yīng)用規(guī)則逆向應(yīng)用規(guī)則(Match-Vector)后，則需要證明后，則需要證明 , m=0 t:vectorm+n 和和 , r:int, x:data, y:vectorr, m=r+1 consr+n(x, appendrn(y, t):vectorm+n 對(duì)于第對(duì)于第1個(gè)證明要求，由于個(gè)證明要求，由于 , m=0 n = m+n，因此用下面的類型等價(jià)因此用下面的類型等價(jià)規(guī)則規(guī)則 對(duì)于第對(duì)于第2個(gè)證明要求，個(gè)證明要求，由聲明由聲明appendrn(y, t)的的類型是類型是vectorr+n， 再由再由vectorr+n+1等價(jià)于等價(jià)于vectorm+n i = j vectori

22、 = vectorj8.4 廣義積與廣義和廣義積與廣義和8.4.1 廣義積與廣義和廣義積與廣義和概念概念 x:A.B和和 x:A.B分別稱為分別稱為索引集合索引集合A上族上族B的的積與積與和和 若若x代表項(xiàng)，代表項(xiàng)，A代表類型，則他們分別稱為代表類型，則他們分別稱為依賴積依賴積與依賴與依賴和和（8.2節(jié)）節(jié)） 若若x代表類型，代表類型，A代表類型的聚集，則代表類型的聚集，則 t:T. （或或 t:T. ）表現(xiàn)為）表現(xiàn)為多態(tài)類型多態(tài)類型（7.2節(jié)）節(jié)） x:A.B尚未討論過尚未討論過8.4 廣義積與廣義和廣義積與廣義和8.4.2 帶廣義積與廣義和的直謂式演算帶廣義積與廣義和的直謂式演算 拓展第拓

23、展第7章的章的 到一種函數(shù)演算到一種函數(shù)演算 除了假設(shè)除了假設(shè)U1 U2外，還外，還假設(shè)假設(shè)U1 U2 廣義和同廣義和同ML的結(jié)構(gòu)非常密切，廣義積對(duì)捕獲依的結(jié)構(gòu)非常密切，廣義積對(duì)捕獲依賴類型化的函子是必須的賴類型化的函子是必須的 廣義積與廣義和廣義積與廣義和會(huì)會(huì)使得使得 , , 的形式化大大復(fù)雜的形式化大大復(fù)雜起來起來8.4 廣義積與廣義和廣義積與廣義和1、語法語法 , , 未經(jīng)檢查的預(yù)備項(xiàng)由下面文法給出：未經(jīng)檢查的預(yù)備項(xiàng)由下面文法給出：M := U1 | U2 | b | M M | x : M.M | x : M.M| x | c | x:M.M | M M| x: M = M, M: M

24、 | first (M) | second (M) 第一行給出類型表達(dá)式的第一行給出類型表達(dá)式的形式形式 第二第二行是行是 , 的項(xiàng)的的項(xiàng)的形式形式 第三第三行的行的表達(dá)式同表達(dá)式同廣義和廣義和有關(guān)有關(guān) 這這三類三類表達(dá)式相互依賴表達(dá)式相互依賴8.4 廣義積與廣義和廣義積與廣義和2、定型規(guī)則、定型規(guī)則（ 是是U1或者是類型） , , 的定型規(guī)則是的定型規(guī)則是7.2.1節(jié)節(jié) , 規(guī)則的一個(gè)拓展規(guī)則的一個(gè)拓展 ( U2) ( Intro) ( Elim) :U2 , x: :U2 ( x: . ):U2 :U2 , x : :U2 , x: M: ( x: .M) : ( x: . ) M:( x

25、: . ) N: MN : N/x 8.4 廣義積與廣義和廣義積與廣義和 ( U2) ( Intro) ( Elim)1 ( Elim)2 :U2 , x: :U2 ( x: . ):U2 :U2 , x : :U2 , x: M/xN:M/x x: =M, N: : ( x: . ) M:( x: . ) first(M): M:( x: . ) second(M) : first(M)/x 8.4 廣義積與廣義和廣義積與廣義和 這些定型規(guī)則結(jié)合等式公理可用于定型推導(dǎo)這些定型規(guī)則結(jié)合等式公理可用于定型推導(dǎo) 例：不需要等式推理的定型推導(dǎo)例：不需要等式推理的定型推導(dǎo)x : ( t:U1.t),

26、y: first x first x, z: first x yz: first x 8.4 廣義積與廣義和廣義積與廣義和 例例 let聲明聲明let x: = M in N second( x: = M, N )例舉例舉說明說明這種形式的表達(dá)式的定型：這種形式的表達(dá)式的定型：let x:( t:U1.t)= t:U1=int, 3: t in ( z:int. z) (second x) second( x:( t:U1.t)= t:U1=int, 3:t ,( z:int.z)(second x) )(1)首先需要證明首先需要證明 t:U1 = int, 3: t 有類型有類型 t:U1.

27、t(2)再證明再證明 x:( t:U1.t)= t:U1=int,3:t , ( z:int. z)(second x) 有類型有類型 x: ( t: U1.t).int8.4 廣義積與廣義和廣義積與廣義和 例例 let聲明聲明let x: = M in N second( x: = M, N )(2) 再證明再證明 x:( t:U1.t)= t:U1=int, 3:t , ( z:int. z)(second x) 有類型有類型 x: ( t: U1.t).int(3) 根據(jù)根據(jù)( Intro)規(guī)則規(guī)則, 證明下式便足夠了證明下式便足夠了M/x( z:int. z)(second x) :

28、M/xint(4) 由由( Elim2)，second M及其類型是及其類型是second( t:U1= int, 3:t ) : first( t:U1= int, 3:t )/tt(5)使用下面的等式公理使用下面的等式公理( first)可證上面的類型是可證上面的類型是int8.4 廣義積與廣義和廣義積與廣義和2、等式和歸約、等式和歸約 的等式證明系統(tǒng)包含描述在的等式證明系統(tǒng)包含描述在7.2.3節(jié)節(jié) 的公理和推理規(guī)則的公理和推理規(guī)則，并增加下面的規(guī)則并增加下面的規(guī)則 first( x: = M, N: ) = M: ( first) second( x: = M, N: ) = M/xN:

29、 M/x ( second ) x: = first(M), second(M): =M: x: . ( sp) 公理公理( first)和和( second)可產(chǎn)生項(xiàng)之間的等式，可產(chǎn)生項(xiàng)之間的等式，也可產(chǎn)生類型之間的等式也可產(chǎn)生類型之間的等式8.4 廣義積與廣義和廣義積與廣義和 有關(guān)類型表達(dá)式的其它公理和推理規(guī)則有關(guān)類型表達(dá)式的其它公理和推理規(guī)則 自反公理及對(duì)稱性和傳遞性規(guī)則自反公理及對(duì)稱性和傳遞性規(guī)則 用于類型表達(dá)式相等的同余規(guī)則用于類型表達(dá)式相等的同余規(guī)則 ( Cong) ( Cong) ( Cong) 1= 1 :U1 2= 2 :U1 1 2 = 1 2 :U1 1= 1 :U2 ,

30、 x : 1 2= 2 :U2 x: 1. 2 = x: 1 . 2 : U2 1= 1 :U2 , x : 1 2= 2 :U2 x: 1. 2 = x: 1 . 2 : U2 8.4 廣義積與廣義和廣義積與廣義和 有關(guān)項(xiàng)的公理和推理規(guī)則有關(guān)項(xiàng)的公理和推理規(guī)則 自反公理及對(duì)稱性和傳遞性規(guī)則自反公理及對(duì)稱性和傳遞性規(guī)則 列出有關(guān)列出有關(guān) 和和 類型的項(xiàng)的同余規(guī)則類型的項(xiàng)的同余規(guī)則 , x : M=M : = :Ui x: . M= x: . M : x: . M=M : x: . N=N : MN = M N :N/x M=M : M/xN = M /xN :M/x = :Ui M/x =M/

31、x :Ui x: =M, N: = x: =M , N : : x: . 8.4 廣義積與廣義和廣義積與廣義和 有關(guān)項(xiàng)的公理和推理規(guī)則有關(guān)項(xiàng)的公理和推理規(guī)則 自反公理及對(duì)稱性和傳遞性規(guī)則自反公理及對(duì)稱性和傳遞性規(guī)則 列出有關(guān)列出有關(guān) 和和 類型的項(xiàng)的同余規(guī)則類型的項(xiàng)的同余規(guī)則 M=M : x: . first(M)=first(M ): M=M : x: . second(M)=second(M ):first(M)/x M=N: , x:A context , x:A M=N: 8.4 廣義積與廣義和廣義積與廣義和 把這些等式公理從左到右定向，得到一個(gè)形把這些等式公理從左到右定向，得到一個(gè)形式類似于其它式類似于其它 演算系統(tǒng)的歸約系統(tǒng)演算系統(tǒng)的歸約系統(tǒng) 它是它是強(qiáng)范式化強(qiáng)范式化 的等式理論是可判定的的等式理論是可判定的8.4 廣義積與廣義和廣義積與廣義和8.4.3 ML模塊語言模塊語言 8.3節(jié)的節(jié)的DML嘗試了廣義和與廣義積在依賴類型嘗試了廣義和與廣義積在依賴類型方面的應(yīng)用方面的應(yīng)用 本節(jié)的本節(jié)的SML將廣義和與廣義積應(yīng)用到多態(tài)類型