Refine
Year of publication
Document Type
- Working Paper (89)
- Conference Proceeding (4)
- Article (3)
Language
- English (96)
Has Fulltext
- yes (96)
Is part of the Bibliography
- no (96)
Keywords
- Lambda-Kalkül (17)
- Formale Semantik (9)
- Operationale Semantik (8)
- lambda calculus (8)
- Programmiersprache (7)
- concurrency (6)
- functional programming (6)
- Nebenläufigkeit (5)
- pi-calculus (5)
- semantics (5)
- Logik (4)
- Verifikation (4)
- adequate translations (4)
- contextual equivalence (4)
- letrec (4)
- automated deduction (3)
- call-by-need (3)
- context lemma (3)
- functional programming languages (3)
- observational semantics (3)
- Funktionale Programmiersprache (2)
- Funktionale Programmierung (2)
- Kontextuelle Gleichheit (2)
- Logics (2)
- Programmtransformation (2)
- Pufferspeicher (2)
- Semantics (2)
- Verification (2)
- call-by-name (2)
- context unification (2)
- infinitary lambda calculus (2)
- lambda-calculus (2)
- lazy evaluation (2)
- logics in artificial intelligence (2)
- non-determinism (2)
- nondeterminism (2)
- programming languages (2)
- rewriting (2)
- second order unification (2)
- unification (2)
- Abstrakte Reduktion (1)
- Alice ML (1)
- Baumgrammatiken (1)
- Call-by-Need (1)
- Clean (1)
- Contextual Equivalence (1)
- Correctness (1)
- Futures (1)
- Haskell (1)
- Kontextuelle Gleicheit (1)
- Lambda Calculus (1)
- Letrec-Kalkül (1)
- ML <Programmiersprache> (1)
- Nichtdeterminismus (1)
- Operational Semantics (1)
- Polynomielles Wortproblem (1)
- Program Transformations (1)
- Programmkalküle (1)
- Programmkorrektheit (1)
- Sharing (1)
- Striktheitsanalyse (1)
- Termination (1)
- Wortproblem (1)
- abstract reduction (1)
- adequate translation (1)
- bisimulation (1)
- call-by-need evaluation (1)
- call-by-need lambda calculus (1)
- formal semantics (1)
- grammar-based compression (1)
- nominal unification (1)
- parallel processes (1)
- polynomial word problem (1)
- precongruence (1)
- program correctness (1)
- programming calculi (1)
- randomized algorithms (1)
- sharing (1)
- similarity (1)
- simulation (1)
- space improvements (1)
- space optimization (1)
- straight line programs (1)
- strictness analysis (1)
- translation (1)
- tree grammars (1)
- verzögerte Auswertung (1)
Institute
- Informatik (96)
We present a higher-order call-by-need lambda calculus enriched with constructors, case-expressions, recursive letrec-expressions, a seq-operator for sequential evaluation and a non-deterministic operator amb that is locally bottom-avoiding. We use a small-step operational semantics in form of a single-step rewriting system that defines a (nondeterministic) normal order reduction. This strategy can be made fair by adding resources for bookkeeping. As equational theory we use contextual equivalence, i.e. terms are equal if plugged into any program context their termination behaviour is the same, where we use a combination of may- as well as must-convergence, which is appropriate for non-deterministic computations. We show that we can drop the fairness condition for equational reasoning, since the valid equations w.r.t. normal order reduction are the same as for fair normal order reduction. We evolve different proof tools for proving correctness of program transformations, in particular, a context lemma for may- as well as mustconvergence is proved, which restricts the number of contexts that need to be examined for proving contextual equivalence. In combination with so-called complete sets of commuting and forking diagrams we show that all the deterministic reduction rules and also some additional transformations preserve contextual equivalence.We also prove a standardisation theorem for fair normal order reduction. The structure of the ordering <=c a is also analysed: Ω is not a least element, and <=c already implies contextual equivalence w.r.t. may-convergence.