Combinator

A combinator is a lambda term with no free variables.

Table of contents
- Omega combinator Combinator
- Fixed-point combinator Combinator
  - Fixed-point theorem for the untyped lambda calculus Fixed-point combinator
  - Recursively enumerable fixed-point combinators Fixed-point combinator

Omega combinator ( $Ω$ )

The omega combinator is the divergent untyped lambda calculus term

Ω = (λ x . xx) (λ x . xx),

whose only beta reduction reproduces

Ω

.

Fixed-point combinator

An untyped lambda term

Y

is a fixed-point combinator when

Y f \equiv_{β} f (Y f)

for every term

f

.

Fixed-point theorem for the untyped lambda calculus

Every lambda term

F

has a fixed point: the term

X = (λ x . F (xx)) (λ x . F (xx))

satisfies

X \equiv_{β} F (X)

. Equivalently, a fixed-point combinator such as

Y = λ f . (λ x . f (xx)) (λ x . f (xx))

satisfies

Y F \equiv_{β} F (Y F)

for every

F

.

Recursively enumerable fixed-point combinators

The set of fixed-point combinators is recursively enumerable. Enumerate closed lambda terms and finite proofs of beta equivalence, and output

Y

whenever a proof of

Y f \equiv_{β} f (Y f)

appears for a fresh variable

f

.

 Ancestors (7)

 Incoming links (3)

 View article source

 Discussion (0)

There are no discussions about this article yet.

 Articles by others on the same topic (0)

There are currently no matching articles.

  See all articles in the same topic Create my own version