可计算函数的编程语言PCF

PCF的语法

• 我们使用什么是语言？的上下文无关语法
• 可计算函数的编程语言（Programming Computable Functions，PCF）
  • t = x
  • | fun x -> t
  • | t t
  • | n
  • | t + t | t – t | t * t | t / t
  • | ifz t then t else t
  • | fix x t
  • | let x = t in t
• PCF包含如下部分，它是无类型的Lambda演算之上的扩展
  • （变量）x
  • （抽象）fun x -> t
  • （作用）t t
  • （自然数）n
  • （算术运算）t + t，t – t，t * t，t / t
  • （条件）ifz t then t else t
  • （不动点）fix x t
  • （定义）let x = t in t

PCF的规约策略