Go backward to Example Go up to Top Go forward to Self-Application

Self-Application

• Untyped applicative language.
• LAMBDA expression can accept itself as argument.
• LET X = LAMBDA (X) (X X) IN (X X)

  E[[LET X = LAMBDA (X) (X X) IN (X X)]]e₀
  = E[[(X X)]]e₁ where
      e₁ = (updateenv [[X]]
          (E[[LAMBDA (X) (X X)]]e₀) e₀)
  = E[[LAMBDA (X) (X X)]]e₀ (E[[X]]e₁)
  = (lambda d.E[[(X X)]](updateenv [[X]]
      d e₀))(E[[X]]e₁)
  = E[[(X X)]](updateenv [[X]]
      (E[[LAMBDA (X) (X X)]]e₀) e₀)
  = E[[(X X)]]e₁
  = ...

Circular derivation produced!