Operational termination of membership equational programs: The order-sorted way

Salvador Lucas, José Meseguer

Research output: Contribution to journalConference article

Abstract

Our main goal is automating termination proofs for programs in rewriting-based languages with features such as: (i) expressive type structures, (ii) conditional rules, (iii) matching modulo axioms, and (iv) contextsensitive rewriting. Specifically, we present a new operational termination method for membership equational programs with features (i)-(iv) that can be applied to programs in membership equational logic (MEL). The method first transforms a MEL program into a simpler, yet semantically equivalent, conditional order-sorted (OS) program. Subsequent trasformations make the OS-program unconditonal, and, finally, unsorted. In particular, we extend and generalize to this richer setting an order-sorted termination technique for unconditional OS programs proposed by Ölveczky and Lysne. An important advantage of our method is that it minimizes the use of conditional rules and produces simpler transformed programs whose termination is often easier to prove automatically.

Original languageEnglish (US)
Pages (from-to)189-205
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Dec 1 2008
Event7th International Workshop on Rewriting Logic and its Applications, WRLA 2008 (European Joint Conference on Theory and Practice of Software, ETAPS 2008) - Budapest, Hungary
Duration: Mar 29 2008Mar 30 2008

Fingerprint

Termination
Equational Logic
Rewriting
Logic Programs
Axioms
Modulo
Transform
Minimise
Generalise

Keywords

  • Membership equational logic
  • Operational termination
  • Order-sorted equational logic
  • Program analysis
  • Rewriting logic
  • Term rewriting

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Operational termination of membership equational programs : The order-sorted way. / Lucas, Salvador; Meseguer, José.

In: Electronic Notes in Theoretical Computer Science, 01.12.2008, p. 189-205.

Research output: Contribution to journalConference article

@article{934ca1b9405548b7a1f5bb621f130451,
title = "Operational termination of membership equational programs: The order-sorted way",
abstract = "Our main goal is automating termination proofs for programs in rewriting-based languages with features such as: (i) expressive type structures, (ii) conditional rules, (iii) matching modulo axioms, and (iv) contextsensitive rewriting. Specifically, we present a new operational termination method for membership equational programs with features (i)-(iv) that can be applied to programs in membership equational logic (MEL). The method first transforms a MEL program into a simpler, yet semantically equivalent, conditional order-sorted (OS) program. Subsequent trasformations make the OS-program unconditonal, and, finally, unsorted. In particular, we extend and generalize to this richer setting an order-sorted termination technique for unconditional OS programs proposed by {\"O}lveczky and Lysne. An important advantage of our method is that it minimizes the use of conditional rules and produces simpler transformed programs whose termination is often easier to prove automatically.",
keywords = "Membership equational logic, Operational termination, Order-sorted equational logic, Program analysis, Rewriting logic, Term rewriting",
author = "Salvador Lucas and Jos{\'e} Meseguer",
year = "2008",
month = "12",
day = "1",
language = "English (US)",
pages = "189--205",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - Operational termination of membership equational programs

T2 - The order-sorted way

AU - Lucas, Salvador

AU - Meseguer, José

PY - 2008/12/1

Y1 - 2008/12/1

N2 - Our main goal is automating termination proofs for programs in rewriting-based languages with features such as: (i) expressive type structures, (ii) conditional rules, (iii) matching modulo axioms, and (iv) contextsensitive rewriting. Specifically, we present a new operational termination method for membership equational programs with features (i)-(iv) that can be applied to programs in membership equational logic (MEL). The method first transforms a MEL program into a simpler, yet semantically equivalent, conditional order-sorted (OS) program. Subsequent trasformations make the OS-program unconditonal, and, finally, unsorted. In particular, we extend and generalize to this richer setting an order-sorted termination technique for unconditional OS programs proposed by Ölveczky and Lysne. An important advantage of our method is that it minimizes the use of conditional rules and produces simpler transformed programs whose termination is often easier to prove automatically.

AB - Our main goal is automating termination proofs for programs in rewriting-based languages with features such as: (i) expressive type structures, (ii) conditional rules, (iii) matching modulo axioms, and (iv) contextsensitive rewriting. Specifically, we present a new operational termination method for membership equational programs with features (i)-(iv) that can be applied to programs in membership equational logic (MEL). The method first transforms a MEL program into a simpler, yet semantically equivalent, conditional order-sorted (OS) program. Subsequent trasformations make the OS-program unconditonal, and, finally, unsorted. In particular, we extend and generalize to this richer setting an order-sorted termination technique for unconditional OS programs proposed by Ölveczky and Lysne. An important advantage of our method is that it minimizes the use of conditional rules and produces simpler transformed programs whose termination is often easier to prove automatically.

KW - Membership equational logic

KW - Operational termination

KW - Order-sorted equational logic

KW - Program analysis

KW - Rewriting logic

KW - Term rewriting

UR - http://www.scopus.com/inward/record.url?scp=57549113716&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=57549113716&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:57549113716

SP - 189

EP - 205

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -