Distributive Rho-Calculus
| Autor: | Horatiu Cirstea, Clément Houtmann, Benjamin Wack |
|---|---|
| Přispěvatelé: | Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2006 |
| Předmět: |
General Computer Science
Process calculus lambda calculus 0102 computer and information sciences 02 engineering and technology 01 natural sciences Theoretical Computer Science Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering rewriting calculus Calculus of communicating systems Mathematics Discrete mathematics Natural deduction fixpoints [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 16. Peace & justice term rewriting systems Algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Confluence TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Church encoding Computer Science::Programming Languages 020201 artificial intelligence & image processing Situation calculus Typed lambda calculus Computer Science(all) Normalisation by evaluation |
| Zdroj: | WRLA 2006 WRLA 2006, Apr 2006, Vienna, Austria. pp.29, ⟨10.1016/j.entcs.2007.06.010⟩ WRLA |
| DOI: | 10.1016/j.entcs.2007.06.010⟩ |
| Popis: | International audience; The rewriting calculus has been introduced as a general formalism that uniformly integrates rewriting and lambda-calculus. In this calculus all the basic ingredients of rewriting such as rewrite rules, rule applications and results are first-class objects. The rewriting calculus has been originally designed and used for expressing the semantics of rule based as well as object oriented paradigms. We have previously shown that convergent term rewriting systems and classic strategies can be encoded naturally in the calculus. In this paper, we go a step further and we propose an extended version of the calculus that allows one to encode unrestricted term rewriting systems. This version of the calculus features a new evaluation rule describing the behavior of the result structures and a call-by-value evaluation strategy. We prove the confluence of the obtained calculus and the correctness and completeness of the proposed encoding. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|