Institution中的liberal理論態(tài)射及正則序類方程邏輯的Lawvere定理.pdf

1、江西師范大學(xué)碩士學(xué)位論文Institution中的liberal理論態(tài)射及正則序類方程邏輯的Lawvere定理姓名：劉富春申請(qǐng)學(xué)位級(jí)別：碩士專業(yè)：數(shù)學(xué)指導(dǎo)教師：應(yīng)明生19961101在面向?qū)ο蟮某绦蛟O(shè)計(jì)語(yǔ)言中，為了解釋抽象數(shù)據(jù)類型間子類型關(guān)系(即繼承關(guān)系)，GoguenJA和MeseguerRM發(fā)展了序類代數(shù)161，并用正則性保證多態(tài)操作符的語(yǔ)義解釋的一致性。第七章首先建立了一個(gè)正則序類方程邏輯Institution，然后證明了正則序類

2、方程邏輯Institution的Lawvere定理[itl第二章預(yù)備知識(shí)號(hào)2.1基本概念馬2.2本文引用的結(jié)果第三章Liberal理論態(tài)射的一些簡(jiǎn)單性質(zhì)這一章主要討論了liberal理論態(tài)射的一些簡(jiǎn)單性質(zhì)。特別是得到了persistent函子的一個(gè)刻劃，證明了liberal理論態(tài)射的復(fù)合仍是liberal理論態(tài)射。定理3.1設(shè)凡:兀~幾，凡:幾~幾都是liberal理論態(tài)射，則凡凡:兀~幾也是liberal理論態(tài)射。(證明略)注記1由此

3、知，有限個(gè)liberal理論態(tài)射的復(fù)合仍是liberal理論態(tài)射，這表明可以用逐步求精的方法處理參數(shù)化數(shù)據(jù)類型。注記2若以理論為對(duì)象，以liberal理論態(tài)射為態(tài)射，可以構(gòu)成一個(gè)范疇，稱為liberal理論范疇，記為7A10定理3.2設(shè)Fl:Tt71F2:T2~幾都是理論態(tài)射，且FlF2:T‘幾是liberal理論態(tài)射。如果臼沿凡模型、同態(tài)可擴(kuò)張，則凡也是liberal理論態(tài)射。(證明略)定理3.3設(shè)F:T一T是liberal理態(tài)射，則