可计算函数的编程语言PCF

PCF的语法

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

PCF的化归策略