Λ-терм

Материал из свободной русской энциклопедии «Традиция». Вы можете дополнить или исправить его.
Перейти к навигации Перейти к поиску

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

  1. v∈Id⇒v∈Exprv \in Id \Rightarrow v \in Expr
  2. v∈Id,E∈Expr⇒λv.E∈Exprv \in Id, E \in Expr \Rightarrow \lambda v.E \in Expr
  3. E,E′∈Expr⇒(EE′)∈ExprE, E' \in Expr \Rightarrow (EE') \in Expr
  4. E∈Expr⇒(E)∈ExprE \in Expr \Rightarrow (E) \in Expr

Здесь IdId — множество идентификаторов, ExprExpr — множество λ-термов. Других λ-термов нет.

См. также[править | править код]

Источник — https://traditio.wiki/w/index.php?title=Λ-терм&oldid=102197