顶部
  1. 首页
  2. 图书产品
  3. 程序设计语言理论
收藏

程序设计语言理论

样章
作者：
陈意云
定价：
32.00元
ISBN：
978-7-04-015516-7
版面字数：
450.000千字
开本：
16开
全书页数：
340页
装帧形式：
平装
重点项目：
暂无
出版时间：
2004-09-29
读者对象：
高等教育
一级分类：
计算机/教育技术类
二级分类：
计算机类专业核心课程
三级分类：
程序设计基础
  本书给出分析程序设计语言语法性质、操作性质和语义性质的一个框架，该框架基于λ演算系统。全书围绕着λ演算的一个序列来组织，该序列中λ演算的类型系统依次变得越来越复杂，这些λ演算用来分析和讨论相应的程序设计语言概念，如多态性、抽象数据类型、子类型等。以类型系统为中心对程序设计语言进行的这种研究，在软件工程、语言设计、高性能编译器、计算机和网络安全等方面有着重要应用。
  本书可作为高等院校计算机科学及相关专业的研究生教材，也可供计算机软件工程高级技术人员参考。
  • 第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.2.5　递归函数和不动点算子
      • 2.2.6　语法总结和例子
    • 2.3　程序和语义
      • 2.3.1　程序和结果
      • 2.3.2　公理语义
      • 2.3.3　指称语义
      • 2.3.4　操作语义
      • 2.3.5　由各种形式的语义定义的等价关系
    • 2.4　归约和符号解释器
      • 2.4.1　归约的合流性
      • 2.4.2　归约策略
      • 2.4.3　最左归约和惰性归约
      • 2.4.4　并行归约
      • 2.4.5　急切归约
    • 2.5　程序设计实例、表达能力和局限
      • 2.5.1　记录和n　元组
      • 2.5.2　查找自然数
      • 2.5.3　迭代和尾递归
      • 2.5.4　完全递归函数
      • 2.5.5　部分递归函数
      • 2.5.6　并行运算的不可定义性
    • 2.6　衍生和扩充
      • 2.6.1　单元类型与和类型
      • 2.6.2　递归类型
    • 习题
  • 第3章　泛代数和代数数据类型
    • 3.1　引言
    • 3.2　代数、基调和项
      • 3.2.1　代数
      • 3.2.2　代数项的语法
      • 3.2.3　代数以及项在代数中的解释
      • 3.2.4　代换引理
    • 3.3　等式、可靠性和完备性
      • 3.3.1　等式
      • 3.3.2　项代数
      • 3.3.3　语义蕴涵和一个等式证明系统
      • 3.3.4　完备性的形式
      • 3.3.5　同余、商和演绎完备性
      • 3.3.6　非空类别和最小模型性质
    • 3.4　同态和初始性
      • 3.4.1　同态和同构
      • 3.4.2　初始代数
    • 3.5　代数数据类型
      • 3.5.1　代数数据类型
      • 3.5.2　初始代数语义和数据类型归纳
      • 3.5.3　解释没有意义的项
      • 3.5.4　错误值的其他解决方法
    • 3.6　重写系统
      • 3.6.1　基本定义
      • 3.6.2　合流性和可证明的相等性
      • 3.6.3　终止性
      • 3.6.4　临界对
      • 3.6.5　左线性无重叠重写系统
      • 3.6.6　局部合流、终止和合流之间的联系
      • 3.6.7　代数数据类型的应用
    • 习题
  • 第4章　简单类型化λ演算
    • 4.1　引言
    • 4.2　类型
      • 4.2.1　类型的语法
      • 4.2.2　类型的解释
    • 4.3　项
      • 4.3.1　上下文有关语法
      • 4.3.2　λ→项的语法
      • 4.3.3　有积、和及相关类型的项
      • 4.3.4　定型算法
    • 4.4　证明系统
      • 4.4.1　等式和理论
      • 4.4.2　归约规则
      • 4.4.3　有其他规则的归约
    • 4.5　Henkin　模型、可靠性和完备性
      • 4.5.1　一般模型和项的含义
      • 4.5.2　应用结构、外延性和框架
      • 4.5.3　环境条件
      • 4.5.4　类型可靠性和等式可靠性
      • 4.5.5　没有空类型的Henkin模型的完备性
      • 4.5.6　有空类型的完备性
      • 4.5.7　其他类型的Henkin模型
    • 习题
  • 第5章　类型化λ演算的模型
    • 5.1　引言
    • 5.2　论域理论模型和不动点
      • 5.2.1　递归定义和不动点算子
      • 5.2.2　完全偏序集合、提升和笛卡儿积
      • 5.2.3　连续函数
      • 5.2.4　不动点和完全连续体系
      • 5.2.5　PCF的CPO模型
    • 5.3　不动点归纳
    • 5.4　计算适当性和完全抽象
      • 5.4.1　近似定理和计算的适当性
      • 5.4.2　带并行运算的PCF　的完全抽象
    • 习题
  • 第6章　命令式程序
    • 6.1　引言
    • 6.2　Kernel　语言
      • 6.2.1　左值和右值
      • 6.2.2　Kernel　语言的语法
    • 6.3　操作语义
      • 6.3.1　表达式中的基本符号的解释
      • 6.3.2　存储单元和状态
      • 6.3.3　表达式的计算
      • 6.3.4　命令的执行
    • 6.4　指称语义
      • 6.4.1　带状态的类型化λ演算
      • 6.4.2　语义函数
      • 6.4.3　操作语义和指称语义的等价
    • 6.5　Kernel　程序的前后断言
      • 6.5.1　一阶逻辑和部分正确性证明
      • 6.5.2　证明规则
      • 6.5.3　可靠性
      • 6.5.4　相对完备性
    • 6.6　其他语言构造的语义
      • 6.6.1　概述
      • 6.6.2　有局部变量的程序块
      • 6.6.3　过程
      • 6.6.4　程序块和过程声明的组合
    • 习题
  • 第7章　多态性
    • 7.1　引言
      • 7.1.1　概述
      • 7.1.2　类型作为函数变元
      • 7.1.3　一般积与一般和
    • 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　ML　模块语言
      • 7.5.2　带积与和的谓词式演算
      • 7.5.3　带积与和的表示模块
      • 7.5.4　谓词性和两个全域之间的联系
    • 7.6　类型作为规范
      • 7.6.1　公式作为类型的对应
      • 7.6.2　类型作为规范
    • 习题
  • 第8章　子定型及有关概念
    • 8.1　引言
    • 8.2　有子定型的简单类型化λ演算
    • 8.3　记录
      • 8.3.1　记录子定型的一般性质
      • 8.3.2　带记录和子定型的类型化演算
    • 8.4　子定型的语义模型
      • 8.4.1　概述
      • 8.4.2　子定型的转换解释
      • 8.4.3　类型的子集解释
    • 8.5　递归类型和对象的记录模型
    • 8.6　带子类型限制的多态性
    • 习题
  • 第9章　类型推断
    • 9.1　引言
    • 9.2　带类型变量的λ→　类型推断
      • 9.2.1　语言tλ→　
      • 9.2.2　代换、实例与合一
      • 9.2.3　主定型算法
      • 9.2.4　隐式定型
      • 9.2.5　定型和合一的等价
    • 9.3　带多态声明的类型推断
      • 9.3.1　ML类型推断和多态变量
      • 9.3.2　两组隐式定型规则
      • 9.3.3　类型推断算法
    • 习题
  • 参考文献

相关图书

C++程序设计实验教程

李师贤等

￥25.70 收藏

C++程序设计实验教程(换封面)

李师贤等

￥30.00 收藏

C++程序设计（第三版 影印版）

Nell Dale Chip Weems

￥50.00 收藏

C/C++程序设计案例教程实验与实训指导

梅险等

￥25.20 收藏

C程序设计

张长海、陈娟

￥30.00 收藏

C程序设计实践教程

张鸣华

￥36.90 收藏

C语言程序设计

苏小红 王宇颖 孙志岗 等

￥43.00 收藏

C语言程序设计(第2版)

苏小红 王宇颖 孙志岗 等编著

￥43.00 收藏

C语言程序设计(第2版)

苏小红 王宇颖 孙志岗 等编著

￥43.00 收藏

C语言程序设计(第3版)

苏小红 王宇颖 孙志岗 等

￥45.00 收藏

C语言程序设计(第4版)

苏小红 赵玲玲 孙志岗 王宇颖 等

￥49.00 收藏

C语言程序设计(第4版)

苏小红 赵玲玲 孙志岗 王宇颖 等

￥49.00 收藏

C语言程序设计(第4版)（换封面）

苏小红 赵玲玲 孙志岗 王宇颖 等

￥49.00 收藏

C语言程序设计学习指导

苏小红 等

￥32.00 收藏

C语言程序设计学习指导(第3版)

苏小红 王甜甜 车万翔

￥37.50 收藏