TY - GEN

T1 - Proving ground confluence of equational specifications modulo axioms

AU - Durán, Francisco

AU - Meseguer, José

AU - Rocha, Camilo

N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2018.

PY - 2018

Y1 - 2018

N2 - Terminating functional programs should be deterministic, i.e., should evaluate to a unique result, regardless of the evaluation order. For equational functional programs such determinism is exactly captured by the ground confluence property. For terminating equations this is equivalent to ground local confluence, which follows from local confluence. Checking local confluence by computing critical pairs is the standard way to check ground confluence. The problem is that some perfectly reasonable equational programs are not locally confluent and it can be very hard or even impossible to make them so by adding more equations. We propose a three-step strategy to prove that an equational program as is is ground confluent: First: apply the strategy proposed in [9] to use non-joinable critical pairs as completion hints to either achieve local confluence or reduce the number of critical pairs. Second: use the inductive inference system proposed in this paper to prove the remaining critical pairs ground joinable. Third: to show ground confluence of the original specification, prove also ground joinable the equations added. These methods apply to order-sorted and possibly conditional equational programs modulo axioms such as, e.g., Maude functional modules.

AB - Terminating functional programs should be deterministic, i.e., should evaluate to a unique result, regardless of the evaluation order. For equational functional programs such determinism is exactly captured by the ground confluence property. For terminating equations this is equivalent to ground local confluence, which follows from local confluence. Checking local confluence by computing critical pairs is the standard way to check ground confluence. The problem is that some perfectly reasonable equational programs are not locally confluent and it can be very hard or even impossible to make them so by adding more equations. We propose a three-step strategy to prove that an equational program as is is ground confluent: First: apply the strategy proposed in [9] to use non-joinable critical pairs as completion hints to either achieve local confluence or reduce the number of critical pairs. Second: use the inductive inference system proposed in this paper to prove the remaining critical pairs ground joinable. Third: to show ground confluence of the original specification, prove also ground joinable the equations added. These methods apply to order-sorted and possibly conditional equational programs modulo axioms such as, e.g., Maude functional modules.

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

U2 - 10.1007/978-3-319-99840-4_11

DO - 10.1007/978-3-319-99840-4_11

M3 - Conference contribution

AN - SCOPUS:85053865455

SN - 9783319998398

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 184

EP - 204

BT - Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings

A2 - Rusu, Vlad

PB - Springer Verlag

T2 - 12th International Workshop on Rewriting Logic and its Applications, WRLA 2018

Y2 - 14 June 2018 through 15 June 2018

ER -