Go backward to Self-Application Go up to Top Go forward to Recursive Definitions

Recursive Definitions

• Mechanism for recursive LAMBDA forms
• Abstract syntax

  E ::= ...| LETREC I = E₁ IN E₂
      | IFNULL E₁ THEN E₂ ELSE E₃

• IFNULL is conditional on lists

  E[[IFNULL E₁ THEN E₂ ELSE E₃]] =
      lambda e. let x = (E[[E₁]]e) in
          cases x of
              isList(t) -> ((null t) ->
                  (E[[E₂]]e) [] (E[[E₃]]e))
              otherwise -> inError()
          end