Ground confluence of order-sorted conditional specifications modulo axioms

摘要: Abstract Terminating functional programs should be deterministic, i.e., evaluate to a unique result, regardless of the evaluation order. For equational such determinism is exactly captured by ground confluence property. operationally terminating conditional equations this equivalent local confluence, which follows from confluence. Checking computing critical pairs standard way check [33] . The problem that some perfectly reasonable are not locally confluent and it can very hard or even impossible make them so adding more equations. We propose three methods, called Methods 1–3, synergistically combined prove an order-sorted specification modulo axioms B confluent. Method 1 applies strategy proposed in [14] use non-joinable as completion hints either achieve reduce number pairs. 2 uses inductive joinability inference system paper try remaining after applying joinable. It furthermore show original specification. 3 hierarchical nature: used whose conditions belong subspecification has already been proved terminating, conservatively extended overall appropriate sense. These methods apply possibly as, e.g., Maude modules. their effectiveness proving non-trivial examples have eluded previous proof attempts.