2000/11/06 by Manfred Schmidt-Schauß, Schmidt-Schauß, Manfred, Michael Huber +1
Computer Science · #Advanced Software Engineering Methodologies #Artificial Intelligence (cs.AI) #D.3.2 #F.4.1 #FOS: Computer and information sciences #I.2.2 #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #Symbolic Computation (cs.SC) #cs.AI #cs.PL #cs.SC
paper · pdf · doi:10.48550/arxiv.cs/0011008
arxiv created 2000/11/06 · openalex publication_date 2000/11/06 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 αβ(η)-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.