Go backward to Recursive Definitions Go up to Top Go forward to Substitution Principles

Fixed Point Semantics

• Functional G: Environment -> Environment

  G⁰ = lambda i._|_
  G¹ = updateenv [[I]] (E[[E₁]](G⁰)) e
      = updateenv [[I]] (E[[E₁]](lambda i._|_)) e
  G² = updateenv [[I]] (E[[E₁]](G¹)) e
      = updateenv [[I]] (E[[E₁]]
          (updateenv [[I]] (E[[E₁]](G¹)) e)) e
  ...
  Gⁱ⁺¹ = updateenv [[I]] (E[[E₁]](Gⁱ)) e

• Environment Gⁱ⁺¹ can handle i recursive references to [[I]] in [[E₁]].
• Limit G can handle unlimited number of recursive references.

Not necessary to refer to theory to define and use recursive environments!