Go backward to Example Go up to Top

Recursive Bindings

D ::= ...| rec abs I=M | ...
abs in {proc, fun, class, ...}

D[[rec abs I=M]] = lambda e. lambda s. (e', (return s))
    where e' = (updateenv [[I]] inM(M[[M]]e') e)

Means for terminating recursive invocations.

E ::= E₁+E₂ | ...| if E₁ then E₂ else E₃
T ::= nat | ...| if E then T₁ else T₂

Which constructions are chosen, depends on language pragmatics.