Past exam of the mathematics course of the University of Cambridge / 2002 / iii / Paper 76 / 5 / ii

Table of contents
- Solution ii

Solution

Choose

x

fresh for

F

and put

H = λ x . F (A x (C x))

,

Q = H d (H)

. The preceding coding equations give

C d (H) \equiv_{β} d (d (H)), A d (H) (C d (H)) \equiv_{β} d (H d (H)) = d (Q) .

Consequently

Q \to_{β} F (A d (H) (C d (H))) \equiv_{β} F d (Q) .

This self-quoting fixed point is valid even if

F

has free variables, since the effective Gödel numbering codes open lambda terms too. Freshness of

x

prevents variable capture.

 Ancestors (10)

 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