Formalizing the Dependency Pair Criterion for Innermost Termination
| Autor: | Ariane Alves Almeida, Mauricio Ayala-Rincón |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Functional specification
FOS: Computer and information sciences Computer Science - Logic in Computer Science Functional programming Computer Science - Programming Languages Theoretical computer science Dependency (UML) Relation (database) Computer science 020207 software engineering 02 engineering and technology Term (logic) Operational semantics Logic in Computer Science (cs.LO) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 020204 information systems TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION 0202 electrical engineering electronic engineering information engineering Computer Science::Programming Languages Rewriting Reduction (mathematics) Software Programming Languages (cs.PL) |
| DOI: | 10.48550/arxiv.1911.00406 |
| Popis: | Rewriting is a framework for reasoning about functional programming. The dependency pair criterion is a well-known mechanism to analyze termination of term rewriting systems. Functional specifications with an operational semantics based on evaluation are related, in the rewriting framework, to the innermost reduction relation. This paper presents a PVS formalization of the dependency pair criterion for the innermost reduction relation: a term rewriting system is innermost terminating if and only if it is terminating by the dependency pair criterion. The paper also discusses the application of this criterion to check termination of functional specifications. Comment: Paper accepted for presentation at SBMF 2019 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|