Universitätspublikationen
Refine
Year of publication
Document Type
- Working Paper (57)
- Conference Proceeding (3)
- Article (2)
Language
- English (62)
Has Fulltext
- yes (62)
Is part of the Bibliography
- no (62)
Keywords
- Lambda-Kalkül (11)
- Formale Semantik (8)
- concurrency (6)
- functional programming (6)
- Operationale Semantik (5)
- Programmiersprache (5)
- lambda calculus (5)
- pi-calculus (5)
- Logik (4)
- Verifikation (4)
Institute
- Informatik (62)
We consider matching, rewriting, critical pairs and the Knuth-Bendix confluence test on rewrite rules in a nominal setting extended by atom-variables. Computing critical pairs is done using nominal unification, and rewriting using nominal matching. We utilise atom-variables to formulate rewrite rules, which is an improvement over previous approaches, using usual nominal unification, nominal matching and nominal equivalence of expressions coupled with a freshness constraint. We determine the complexity of several problems in a quantified freshness logic. In particular we show that nominal matching is Πp2-complete. We prove that the adapted Knuth-Bendix confluence test is applicable to a nominal rewrite system with atom-variabes and thus, that there is a decidable test whether confluence of the ground instance of the abstract rewrite system holds. We apply the nominal Knuth Bendix confluence criterion to the theory of monads, and compute a convergent nominal rewrite system modulo alpha-equivalence.
We present an implementation of an interpreter LRPi for the call-by-need calculus LRP, based on a variant of Sestoft's abstract machine Mark 1, extended with an eager garbage collector. It is used as a tool for exact space usage analyses as a support for our investigations into space improvements of call-by-need calculi.