登录
注册
书目下载
联系我们
移动端
扫码关注-登录移动端
帮助中心
高等教育出版社产品信息检索系统
图书产品
数字化产品
期刊产品
会议信息
电子书
线上书展
顶部
首页
图书产品
程序设计语言理论(第二版)
收藏
程序设计语言理论(第二版)
作者:
陈意云 张昱
定价:
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 类型推断算法
习题
参考文献
相关图书
面向对象程序设计基础(第二版)
李师贤 李文军 周晓聪 李宏新 林瑛
35.00 元
收藏
C++程序设计(第三版 影印版)
Nell Dale Chip Weems
50.00 元
收藏
程序设计语言概念(第七版 影印版)
[美] Robert W. Sebesta
49.00 元
收藏
C++程序设计实验教程
李师贤等
25.70 元
收藏
C++程序设计实验教程(换封面)
李师贤等
30.00 元
收藏
Java程序设计(第2版)
刘宝林
28.00 元
收藏
Java面向对象程序设计
苏健
36.70 元
收藏
C语言程序设计(第2版)
苏小红 王宇颖 孙志岗 等编著
43.00 元
收藏
C语言程序设计(第2版)
苏小红 王宇颖 孙志岗 等编著
43.00 元
收藏
程序设计案例教程(C语言版)
赵秀岩 于晓强
49.80 元
收藏
C/C++程序设计案例教程实验与实训指导
梅险等
25.20 元
收藏
C程序设计实践教程
张鸣华
36.90 元
收藏
C语言程序设计(第3版)
苏小红 王宇颖 孙志岗 等
45.00 元
收藏
新标准C++程序设计
郭炜
29.60 元
收藏
C语言程序设计(第4版)
苏小红 赵玲玲 孙志岗 王宇颖 等
49.00 元
收藏
选择收货地址
收货人
地址
联系方式
使用新地址
使用新地址
所在地区
请选择
详细地址
收货人
联系电话
设为默认
设为默认收货地址