Computer Science – Programming Languages
Scientific paper
2000-11-06
Computer Science
Programming Languages
Scientific paper
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.
Huber Michael
Schmidt-Schauß Manfred
No associations
LandOfFree
A Lambda-Calculus with letrec, case, constructors and non-determinism does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A Lambda-Calculus with letrec, case, constructors and non-determinism, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Lambda-Calculus with letrec, case, constructors and non-determinism will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-707868