公理语义和指称语义的等价-read.ppt

中国科大 第3章 泛代数和代数数据类型 PCF语言的三部分组成 带函数和积类型的纯类型化?演算 自然数类型和布尔类型 不动点算子 第3章到第5章对这三部分进行透彻的研究 本章研究像自然数类型和布尔类型这样的代数数据类型 3.1 引 言 代数数据类型包括 一个或多个值集 一组在这些集合上的函数 基本限制是其函数不能有函数变元 基本“类型”符号被称为“类别” 泛代数（也叫做等式逻辑） 定义和研究代数数据类型的一般数学框架 本章研究泛代数和它在程序设计中定义常用数据类型时的作用 3.1 引 言 本章主要内容： 代数项和它们在多类别代数中的解释 等式规范（也叫代数规范）和等式证明系统 等式证明系统的可靠性和完备性（公理语义和指称语义的等价） 代数之间的同态关系和初始代数 数据类型的代数理论 从代数规范导出的重写规则（操作语义） 大多数逻辑系统中一些公共的议题将被覆盖 3.2 代数、基调和项 3.2.1 代数 代数 一个或多个集合，叫做载体 一组特征元素和一阶函数，也叫做代数函数 f : A1 ? …? Ak ? A 例：N ? ? N, 0, 1, +, ? ? 载体N是自然数集合 特征元素0, 1?N，也叫做零元函数 函数+, ? : N ? N ? N 3.2 代数、基调和项 多个载体的例子 Apcf ? ?N, B, 0, 1, …, +, true, false, Eq ?, …? 下面开始逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要 定义数据类型 证明性质 进行化简 还必须讨论这种语法描述的语义 A5pcf ? ?N5, B, 0, 1, 2, 3, 4, +5, true, false, Eq ?, …? 3.2 代数、基调和项 3.2.2 代数项的语法 基调? ? ?S，F? S是一个集合，其元素叫做类别 函数符号f : s1? … ? sk ? s的集合F ，其中表达式s1? … ? sk ? s叫做类型 零元函数符号叫做常量符号 例?N ? ?S，F? sorts : nat fctns : 0, 1 : nat ?, ? : nat ? nat ? nat 3.2 代数、基调和项 定义基调的目的是用于写代数项 考虑项中有变量的情况，需假定有一个无穷的符号集合V，其元素称为变量 类别指派? ? ?x1 : s1, …, xk : sk? 基调? ? ?S，F?和类别指派?上类别s的代数项集合Termss (?, ?) 如果x : s ? ?，那么x ? Termss (?, ?) 如果f : s1? … ? sk ? s并且Mi? Termssi(?, ?) (i ? 1, …, k)，那么f M1 … Mk ? Termss (?, ?) 当k ? 0时，如果f : s，那么f ? Termss (?, ?) 3.2 代数、基调和项 例 0, 0 ? 1? Termsnat (?N, ?) 0 ? x ? Termsnat (?N, ?)，其中? ? ? x : nat, …? 代数项中无约束变元，?N?x?M就是简单地把M中x的每个出现都用N代替就是了 记号 ?, x : s? ? ? ? ? x : s?? 引理 如果M ? Termss (?, ?, x : s?)并且N ?Termss?(?, ?)，那么?N?x?M ? Termss (?, ?) 证明 按Termss(?, ?)中项的结构进行归纳 3.2 代数、基调和项 例 用基调?stk ? ?S, F?来写自然数和栈表达式 sorts : nat, stack fctns : 0, 1, 2, … : nat ?, ? : nat ? nat ? nat empty : stack push : nat ? stack ? stack pop : stack ? stack top : stack ? nat push 2 (push 1 (push 0 empty) )是该基调的项 3.2 代数、基调和项 3.2.3 代数以及项在代数中的解释 代数是为代数项提供含义的数学结构 ?是一个基调，则?代数A包含 对每个s ? S，正好有一个载体As 一个解释映射I 把函数I (f ) : As1 ? … ? Ask ? As指派给函数符号 f : s1 ? … ? sk ? s ? F 把I (f ) ? As指派给常量符号f : s ?F ?N代数N写成 N ? ?N, 0N, 1N, ?N, ?N? 3.2 代数、基调和项 代数A的环境? ? : V ? ?s As 环境? 满足? 如果对每个x : s ? ?都有?(x)?As M ? Te