λ演算是一個(gè)把函數(shù)當(dāng)做方程式的理論,是一個(gè)把函數(shù)當(dāng)做表達(dá)式操作的系統(tǒng)。它與可計(jì)算性、計(jì)算機(jī)科學(xué)、邏輯及數(shù)學(xué)等都有存在一定的聯(lián)系。λ演算和圖靈機(jī)是等價(jià)的。且它是函數(shù)編程語(yǔ)言的基礎(chǔ)。此外,λ演算和邏輯系統(tǒng)也存在著奇妙的對(duì)應(yīng)關(guān)系,這種對(duì)應(yīng)關(guān)系稱為Curry-Howard同構(gòu)。我們還可以利用λ演算構(gòu)造各種不同的數(shù)學(xué)模型。因此,對(duì)λ演算的研究,對(duì)計(jì)算理論、程序語(yǔ)言設(shè)計(jì)、邏輯及數(shù)學(xué)等都有重要的意義。標(biāo)準(zhǔn)化、Church-Rosser定理、規(guī)格化、分離屬性等是λ演算的重要性質(zhì)。類型λ演算是在λ演算基礎(chǔ)上為每個(gè)術(shù)語(yǔ)賦予一個(gè)類型,最初為A演算提出的類型系統(tǒng)是簡(jiǎn)單類型。但在簡(jiǎn)單類型系統(tǒng)中,有些術(shù)語(yǔ)是不可類型的,如不能為λx.xx分配類型,因此出現(xiàn)了交類型。交類型是簡(jiǎn)單類型的擴(kuò)展,交類型系統(tǒng)可以為在簡(jiǎn)單類型系統(tǒng)中不可類型的術(shù)語(yǔ)賦予類型。交類型首次被提出是為了對(duì)λ術(shù)語(yǔ)的強(qiáng)標(biāo)準(zhǔn)化進(jìn)行邏輯描述,此后被用來(lái)證明λ演算的各種性質(zhì)。目前為止,λ演算已有很多變種,如Λμ,λGtz是λ演算在Curry-Howard同構(gòu)方向上提出的擴(kuò)展演算。Λμ演算是如的擴(kuò)展,而λμ和經(jīng)典自然演繹是Curry-Howard同構(gòu)的。λGtz演... 

【文章來(lái)源】：浙江大學(xué)浙江省 211工程院校 985工程院校 教育部直屬院校

【文章頁(yè)數(shù)】：75 頁(yè)

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
Abstract
符號(hào)表
第1章 緒論
    1.1 研究背景
    1.2 研究?jī)?nèi)容
    1.3 本文結(jié)構(gòu)
第2章 預(yù)備知識(shí)
    2.1 λ演算
        2.1.1 語(yǔ)法
        2.1.2 規(guī)約策略
    2.2 類型系統(tǒng)
        2.2.1 簡(jiǎn)單類型系統(tǒng)
        2.2.2 交類型系統(tǒng)
    2.3 本章小結(jié)
第3章 標(biāo)準(zhǔn)化定理
    3.1 交類型系統(tǒng)
    3.2 標(biāo)準(zhǔn)化定理
    3.3 本章小結(jié)
第4章 Λμ演算強(qiáng)標(biāo)準(zhǔn)化性質(zhì)的描述
    4.1 Λμ演算
    4.2 交類型系統(tǒng)
    4.3 類型系統(tǒng)的性質(zhì)
    4.4 SN(?)可類型性
    4.5 可類型性(?)SN
    4.6 本章小結(jié)
第5章 λ~(Gtz)演算強(qiáng)標(biāo)準(zhǔn)化性質(zhì)描述
    5.1 λ~(Gtz)-演算語(yǔ)法
    5.2 類型賦予系統(tǒng)
        5.2.1 交類型
        5.2.2 類型系統(tǒng)
    5.3 可類型性(?)SN
    5.4 SN(?)可類型性
    5.5 本章小結(jié)
第6章 總結(jié)與展望
    6.1 工作總結(jié)
    6.2 未來(lái)展望
參考文獻(xiàn)
攻讀碩士學(xué)位期間主要的研究成果
定義表
致謝



本文編號(hào)：3178835