A Lambda-Calculus with letrec, case, constructors and non-determinism

Manfred Schmidt-Schauß, Michael Huber

A non-deterministic call-by-need lambda-calculus \calc with case, constructors, letrec and a (non-deterministic) erratic choice, based on rewriting rules is investigated. A standar…