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

TL;DR

This paper introduces a non-deterministic call-by-need lambda-calculus with features like case, constructors, letrec, and erratic choice, and demonstrates its semantics and correctness of program transformations.

Contribution

It presents a novel non-deterministic lambda-calculus with a semantics based on contextual equivalence and proves the correctness of several program transformations.

Findings

Correctness of deterministic rules established

Validity of garbage collection and indirection removal rules shown

A successful method for semantics and transformation proofs demonstrated

Abstract

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 standard reduction is defined as a variant of left-most outermost reduction. The semantics is defined by contextual equivalence of expressions instead of using $\alpha\beta(\eta)$-equivalence. It is shown that several program transformations are correct, for example all (deterministic) rules of the calculus, and in addition the rules for garbage collection, removing indirections and unique copy. This shows that the combination of a context lemma and a meta-rewriting on reductions using complete sets of commuting (forking, resp.) diagrams is a useful and successful method for providing a semantics of a functional programming language and proving correctness of program transformations.