A Rho-Calculus of explicit constraint application

Autor: Horatiu Cirstea, Germain Faure, Claude Kirchner
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í: 2007
Předmět:
Matching (statistics)
General Computer Science
Computer science
0102 computer and information sciences
02 engineering and technology
01 natural sciences
Theoretical Computer Science
explicit substitutions
Computer Science::Logic in Computer Science
3-dimensional matching
0202 electrical engineering
electronic engineering
information engineering
Calculus
rewriting calculus
Pattern matching
Mathematics
[INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC]
explicit substitution
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
ρ-calculus
matching
Substitution (algebra)
020207 software engineering
explicit matching
Symbolic computation
Term (time)
Computer Science Applications
Constraint (information theory)
Tree traversal
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Explicit substitution
pattern matching
010201 computation theory & mathematics
Rewriting
constraints
Software
Computer Science(all)
Zdroj: Higher-Order and Symbolic Computation
Higher-Order and Symbolic Computation, 2007, Special Issue on Rewriting Logic and its Applications, 20, pp.37-72. ⟨10.1007/s10990-007-9004-2⟩
Workshop on Rewriting Logic and Applications
Workshop on Rewriting Logic and Applications, Mar 2004, Barcelona (Spain), Spain
WRLA
Higher-Order and Symbolic Computation, Springer Verlag, 2007, Special Issue on Rewriting Logic and its Applications, 20, pp.37-72. ⟨10.1007/s10990-007-9004-2⟩
ISSN: 1388-3690
1573-0557
DOI: 10.1007/s10990-007-9004-2⟩
Popis: International audience; Theoretical presentations of the rho-calculus often treat the matching constraint computations as an atomic operation although matching constraints are explicitly expressed. Actual implementations have to take a much more realistic view: computations needed in order to find the solutions of a matching equation can have an important impact on the (efficiency of the) calculus for some matching theories and the substitution application usually involves a term traversal. Following the works on explicit substitutions in the -calculus, we present two versions of the rho-calculus, one with explicit matching and one with explicit substitutions, together with a version that combines the two and considers efficiency issues and more precisely the composition of substitutions. The approach is general, allowing the extension to various matching theories. We establish the confluence of the calculus and the termination of the explicit constraint handling and application sub-calculus.
Databáze: OpenAIRE
Externí odkaz: