交类型和λ演算的标准化性质

发布时间：2021-05-10 06:08

　　λ演算是一个把函数当做方程式的理论,是一个把函数当做表达式操作的系统。它与可计算性、计算机科学、逻辑及数学等都有存在一定的联系。λ演算和图灵机是等价的。且它是函数编程语言的基础。此外,λ演算和逻辑系统也存在着奇妙的对应关系,这种对应关系称为Curry-Howard同构。我们还可以利用λ演算构造各种不同的数学模型。因此,对λ演算的研究,对计算理论、程序语言设计、逻辑及数学等都有重要的意义。标准化、Church-Rosser定理、规格化、分离属性等是λ演算的重要性质。类型λ演算是在λ演算基础上为每个术语赋予一个类型,最初为A演算提出的类型系统是简单类型。但在简单类型系统中,有些术语是不可类型的,如不能为λx.xx分配类型,因此出现了交类型。交类型是简单类型的扩展,交类型系统可以为在简单类型系统中不可类型的术语赋予类型。交类型首次被提出是为了对λ术语的强标准化进行逻辑描述,此后被用来证明λ演算的各种性质。目前为止,λ演算已有很多变种,如Λμ,λGtz是λ演算在Curry-Howard同构方向上提出的扩展演算。Λμ演算是如的扩展,而λμ和经典自然演绎是Curry-Howard同构的。λGtz演... 

【文章来源】：浙江大学浙江省 211工程院校 985工程院校 教育部直属院校

【文章页数】：75 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
符号表
第1章 绪论
    1.1 研究背景
    1.2 研究内容
    1.3 本文结构
第2章 预备知识
    2.1 λ演算
        2.1.1 语法
        2.1.2 规约策略
    2.2 类型系统
        2.2.1 简单类型系统
        2.2.2 交类型系统
    2.3 本章小结
第3章 标准化定理
    3.1 交类型系统
    3.2 标准化定理
    3.3 本章小结
第4章 Λμ演算强标准化性质的描述
    4.1 Λμ演算
    4.2 交类型系统
    4.3 类型系统的性质
    4.4 SN(?)可类型性
    4.5 可类型性(?)SN
    4.6 本章小结
第5章 λ~(Gtz)演算强标准化性质描述
    5.1 λ~(Gtz)-演算语法
    5.2 类型赋予系统
        5.2.1 交类型
        5.2.2 类型系统
    5.3 可类型性(?)SN
    5.4 SN(?)可类型性
    5.5 本章小结
第6章 总结与展望
    6.1 工作总结
    6.2 未来展望
参考文献
攻读硕士学位期间主要的研究成果
定义表
致谢



本文编号：3178835