顶部
收藏

程序设计语言理论(第二版)


作者:
陈意云 张昱
定价:
36.50 元
版面字数:
420千字
开本:
16开
装帧形式:
平装
版次:
2
最新版次
印刷时间:
2010年
ISBN:
978-7-04-028404-1
物料号:
28404-00
出版时间:
2010-02-08
读者对象:
高等教育
一级分类:
计算机/教育技术类
二级分类:
计算机类专业核心课程
三级分类:
程序设计基础

本书给出分析程序设计语言语法性质、操作性质和语义性质的一个框架,该框架基于λ演算系统。全书主要围绕着一系列的λ演算来组织,该系列中λ演算的类型系统依次变得越来越复杂,这些&lambda

  • 目录
    • 第1章 引言
      • 1.1 基本概念
        • 1.1.1 程序设计语言的建模
          • 1.1.2 λ表示法
            • 1.1.3 符号和约定
            • 1.2 等式、归约和语义
              • 1.2.1 公理语义
                • 1.2.2 操作语义
                  • 1.2.3 指称语义
                  • 1.3 类型和类型系统
                    • 1.3.1 类型和类型系统
                      • 1.3.2 类型化语言的优点
                      • 1.4 归纳法
                        • 1.4.1 表达式上的归纳
                          • 1.4.2 证明上的归纳
                            • 1.4.3 良基归纳
                            • 习题
                            • 第2章 泛代数和代数数据类型
                              • 2.1 引言
                                • 2.2 代数、基调和项
                                  • 2.2.1 代数
                                    • 2.2.2 代数项的语法
                                      • 2.2.3 代数以及项在代数中的解释
                                        • 2.2.4 代换引理
                                        • 2.3 等式、可靠性和完备性
                                          • 2.3.1 等式
                                            • 2.3.2 项代数
                                              • 2.3.3 语义蕴涵和等式证明系统
                                                • 2.3.4 完备性的形式
                                                  • 2.3.5 同余、商和演绎完备性
                                                    • 2.3.6 非空类别和最小模型完备性
                                                    • 2.4 同态和初始性
                                                      • 2.4.1 同态和同构
                                                        • 2.4.2 初始代数
                                                        • 2.5 代数数据类型
                                                          • 2.5.1 代数数据类型
                                                            • 2.5.2 初始代数语义和数据类型归纳
                                                              • 2.5.3 解释没有意义的项
                                                                • 2.5.4 错误值的其他解决方法
                                                                • 2.6 重写系统
                                                                  • 2.6.1 基本定义
                                                                    • 2.6.2 合流性和可证的相等性
                                                                      • 2.6.3 终止性
                                                                        • 2.6.4 临界对
                                                                          • 2.6.5 左线性无重叠重写系统
                                                                            • 2.6.6 局部合流、终止和合流之间的联系
                                                                              • 2.6.7 代数数据类型的应用
                                                                              • 习题
                                                                              • 第3章 简单类型化λ演算
                                                                                • 3.1 引言
                                                                                  • 3.2 类型和项
                                                                                    • 3.2.1 类型的语法
                                                                                      • 3.2.2 上下文有关语法
                                                                                        • 3.2.3 λ→项的语法
                                                                                          • 3.2.4 带积、和及其他类型的项
                                                                                            • 3.2.5 定型算法
                                                                                            • 3.3 证明系统
                                                                                              • 3.3.1 等式和理论
                                                                                                • 3.3.2 归约规则
                                                                                                  • 3.3.3 有其他规则的归约
                                                                                                  • 3.4 通用模型、可靠性和完备性
                                                                                                    • 3.4.1 通用模型和项的含义
                                                                                                      • 3.4.2 应用结构、外延性和框架
                                                                                                        • 3.4.3 环境条件
                                                                                                          • 3.4.4 类型可靠性和等式可靠性
                                                                                                            • 3.4.5 没有空类型的完备性
                                                                                                              • 3.4.6 有空类型的完备性
                                                                                                                • 3.4.7 其他类型的通用模型
                                                                                                                • 3.5 可计算函数编程语言
                                                                                                                  • 3.5.1 概述
                                                                                                                    • 3.5.2 PCF的语法
                                                                                                                      • 3.5.3 声明和语法美化
                                                                                                                        • 3.5.4 程序和结果
                                                                                                                          • 3.5.5 公理语义
                                                                                                                            • 3.5.6 操作语义
                                                                                                                              • 3.5.7 由各种形式的语义定义的等价关系
                                                                                                                                • 3.5.8 记录和n元组
                                                                                                                                • 3.6 各种归约策略
                                                                                                                                  • 3.6.1 归约策略
                                                                                                                                    • 3.6.2 最左归约和惰性归约
                                                                                                                                      • 3.6.3 并行归约
                                                                                                                                        • 3.6.4 急切归约
                                                                                                                                        • 习题
                                                                                                                                        • 第4章 类型化λ演算的模型
                                                                                                                                          • 4.1 引言
                                                                                                                                            • 4.2 递归函数和不动点算子
                                                                                                                                              • 4.2.1 递归函数和不动点算子
                                                                                                                                                • 4.2.2 有不动点算子的急切归约
                                                                                                                                                  • 4.2.3 PCF语言的编程实例
                                                                                                                                                  • 4.3 论域理论模型和不动点
                                                                                                                                                    • 4.3.1 递归定义和不动点算子
                                                                                                                                                      • 4.3.2 完全偏序集合、提升和笛卡儿积
                                                                                                                                                        • 4.3.3 连续函数
                                                                                                                                                          • 4.3.4 不动点和完备连续层级
                                                                                                                                                            • 4.3.5 PCF的CPO模型
                                                                                                                                                            • 4.4 不动点归纳
                                                                                                                                                              • 习题
                                                                                                                                                              • 第5章 命令式程序的语义
                                                                                                                                                                • 5.1 引言
                                                                                                                                                                  • 5.2 Kernel语言
                                                                                                                                                                    • 5.2.1 存储单元
                                                                                                                                                                      • 5.2.2 表达式的解释
                                                                                                                                                                        • 5.2.3 程序状态
                                                                                                                                                                        • 5.3 操作语义
                                                                                                                                                                          • 5.3.1 表达式的求值
                                                                                                                                                                            • 5.3.2 命令的执行
                                                                                                                                                                            • 5.4 指称语义
                                                                                                                                                                              • 5.4.1 带状态的类型化λ演算
                                                                                                                                                                                • 5.4.2 语义函数
                                                                                                                                                                                  • 5.4.3 操作语义和指称语义的等价
                                                                                                                                                                                  • 5.5 Kernel语言的Hoare逻辑
                                                                                                                                                                                    • 5.5.1 一阶断言
                                                                                                                                                                                      • 5.5.2 证明规则
                                                                                                                                                                                        • 5.5.3 可靠性
                                                                                                                                                                                          • 5.5.4 小结
                                                                                                                                                                                          • 习题
                                                                                                                                                                                          • 第6章 递归类型
                                                                                                                                                                                            • 6.1 引言
                                                                                                                                                                                              • 6.2 归纳和余归纳
                                                                                                                                                                                                • 6.2.1 余归纳现象
                                                                                                                                                                                                  • 6.2.2 归纳和余归纳指南
                                                                                                                                                                                                    • 6.2.3 代数和余代数
                                                                                                                                                                                                    • 6.3 递归类型
                                                                                                                                                                                                      • 6.3.1 递归类型总览
                                                                                                                                                                                                        • 6.3.2 递归的数据结构
                                                                                                                                                                                                        • 6.4 归纳类型和余归纳类型
                                                                                                                                                                                                          • 6.4.1 归纳类型和余归纳类型总览
                                                                                                                                                                                                            • 6.4.2 帮助理解的实例
                                                                                                                                                                                                            • 习题
                                                                                                                                                                                                            • 第7章 多态性
                                                                                                                                                                                                              • 7.1 引言
                                                                                                                                                                                                                • 7.1.1 概述
                                                                                                                                                                                                                  • 7.1.2 类型作为函数变元
                                                                                                                                                                                                                  • 7.2 直谓式多态演算
                                                                                                                                                                                                                    • 7.2.1 类型和项的语法
                                                                                                                                                                                                                      • 7.2.2 和其他形式多态性的比较
                                                                                                                                                                                                                        • 7.2.3 等式证明和归约
                                                                                                                                                                                                                          • 7.2.4 ML风格的多态声明
                                                                                                                                                                                                                          • 7.3 非直谓式多态演算
                                                                                                                                                                                                                            • 7.3.1 引言
                                                                                                                                                                                                                              • 7.3.2 非直谓式多态λ演算的表达力
                                                                                                                                                                                                                                • 7.3.3 归约的终止性
                                                                                                                                                                                                                                • 7.4 数据抽象和存在类型
                                                                                                                                                                                                                                  • 7.5 类型表达式的分类
                                                                                                                                                                                                                                    • 7.5.1 类型表达式的种类
                                                                                                                                                                                                                                      • 7.5.2 类型表达式的定类与相等
                                                                                                                                                                                                                                        • 7.5.3 项的定型
                                                                                                                                                                                                                                        • 习题
                                                                                                                                                                                                                                        • 第8章 依赖类型
                                                                                                                                                                                                                                          • 8.1 引言
                                                                                                                                                                                                                                            • 8.2 带依赖类型的演算
                                                                                                                                                                                                                                              • 8.2.1 依赖积类型
                                                                                                                                                                                                                                                • 8.2.2 依赖和类型
                                                                                                                                                                                                                                                • 8.3 带依赖类型的程序设计
                                                                                                                                                                                                                                                  • 8.3.1 简化DML的实例
                                                                                                                                                                                                                                                    • 8.3.2 简化DML的定义
                                                                                                                                                                                                                                                    • 8.4 广义积与广义和
                                                                                                                                                                                                                                                      • 8.4.1 广义积与广义和概念
                                                                                                                                                                                                                                                        • 8.4.2 带广义积与广义和的直谓式演算
                                                                                                                                                                                                                                                          • 8.4.3 ML模块语言
                                                                                                                                                                                                                                                            • 8.4.4 用积与和来表示模块
                                                                                                                                                                                                                                                              • 8.4.5 直谓性以及两个全域之间的联系
                                                                                                                                                                                                                                                              • 习题
                                                                                                                                                                                                                                                              • 第9章 命题和类型
                                                                                                                                                                                                                                                                • 9.1 引言
                                                                                                                                                                                                                                                                  • 9.2 构造逻辑
                                                                                                                                                                                                                                                                    • 9.2.1 构造语义
                                                                                                                                                                                                                                                                      • 9.2.2 构造逻辑
                                                                                                                                                                                                                                                                        • 9.2.3 命题当作类型
                                                                                                                                                                                                                                                                        • 9.3 经典逻辑
                                                                                                                                                                                                                                                                          • 9.3.1 经典逻辑和构造逻辑的区别与联系
                                                                                                                                                                                                                                                                            • 9.3.2 经典逻辑的规则
                                                                                                                                                                                                                                                                              • 9.3.3 推导消去形式
                                                                                                                                                                                                                                                                                • 9.3.4 证明的动态性
                                                                                                                                                                                                                                                                                • 习题
                                                                                                                                                                                                                                                                                • 第10章 子定型
                                                                                                                                                                                                                                                                                  • 10.1 引言
                                                                                                                                                                                                                                                                                    • 10.2 有子定型的简单类型化λ演算
                                                                                                                                                                                                                                                                                      • 10.3 记录
                                                                                                                                                                                                                                                                                        • 10.3.1 记录子定型的一般性质
                                                                                                                                                                                                                                                                                          • 10.3.2 带记录和子定型的类型化演算
                                                                                                                                                                                                                                                                                          • 10.4 子定型的语义模型
                                                                                                                                                                                                                                                                                            • 10.4.1 概述
                                                                                                                                                                                                                                                                                              • 10.4.2 子定型的转换解释
                                                                                                                                                                                                                                                                                                • 10.4.3 类型的子集解释
                                                                                                                                                                                                                                                                                                • 10.5 对象的递归记录模型
                                                                                                                                                                                                                                                                                                  • 10.5.1 递归记录类型
                                                                                                                                                                                                                                                                                                    • 10.5.2 递归类型的子定型
                                                                                                                                                                                                                                                                                                    • 习题
                                                                                                                                                                                                                                                                                                    • 第11章 类型推断
                                                                                                                                                                                                                                                                                                      • 11.1 引言
                                                                                                                                                                                                                                                                                                        • 11.2 带类型变量的λ→类型推断
                                                                                                                                                                                                                                                                                                          • 11.2.1 语言t→λ
                                                                                                                                                                                                                                                                                                            • 11.2.2 代换、实例与合一
                                                                                                                                                                                                                                                                                                              • 11.2.3 主定型算法
                                                                                                                                                                                                                                                                                                                • 11.2.4 隐式定型
                                                                                                                                                                                                                                                                                                                  • 11.2.5 定型和合一的等价
                                                                                                                                                                                                                                                                                                                  • 11.3 带多态声明的类型推断
                                                                                                                                                                                                                                                                                                                    • 11.3.1 ML类型推断和多态变量
                                                                                                                                                                                                                                                                                                                      • 11.3.2 两组隐式定型规则
                                                                                                                                                                                                                                                                                                                        • 11.3.3 类型推断算法
                                                                                                                                                                                                                                                                                                                        • 习题
                                                                                                                                                                                                                                                                                                                        • 参考文献

                                                                                                                                                                                                                                                                                                                        相关图书