Go backward to Recursive Definitions Go up to Top Go forward to Fixed Point Semantics

Recursive Definitions

• Occurences of I in LETREC refer to the I being declared.

  E[[LETREC I = E₁ IN E₂]] = lambda e. E[[E₂]]e'
      where e' = updateenv [[I]] (E[[E₁]]e')e
  E[[LETREC I = E₁ IN E₂]] = lambda e. E[[E₂]]
      (fix(lambda e'. updateenv [[I]] (E[[E₁]]e')e))

• Example (see Figure 7.8)

  LETREC F =
      LAMBDA (X)
          IFNULL X THEN NIL
          ELSE a₀ CONS F(TAIL X)
  IN F(a₁ CONS a₂ CONS NIL)
  => (a₀ CONS a₀ CONS NIL)