Λ-терм

From Традиция
Jump to navigation Jump to search

λ-терм (лямбда-терм) — в λ-исчислении объект исчисления. Определяется индуктивно следующим образом:

  1. v I d v E x p r v \in Id \Rightarrow v \in Expr
  2. v I d , E E x p r λ v . E E x p r v \in Id, E \in Expr \Rightarrow \lambda v.E \in Expr
  3. E , E E x p r ( E E ) E x p r E, E' \in Expr \Rightarrow (EE') \in Expr
  4. E E x p r ( E ) E x p r E \in Expr \Rightarrow (E) \in Expr

Здесь I d Id — множество идентификаторов, E x p r Expr — множество λ-термов. Других λ-термов нет.

См. также[edit | edit source]