1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71

------------------------------------------------------------------------------
--- Library for representation and computation of critical pairs.
---
--- @author Jan-Hendrik Matthes
--- @version February 2020
------------------------------------------------------------------------------

module Rewriting.CriticalPairs
  ( CPair
  , showCPair, showCPairs, cPairs, isOrthogonal, isWeakOrthogonal
  ) where

import Data.List (nub)
import Rewriting.Position (eps, positions, (|>), replaceTerm)
import Rewriting.Rules
import Rewriting.Substitution (applySubst)
import Rewriting.Term (Term, showTerm, isConsTerm)
import Rewriting.Unification (unify)

-- ---------------------------------------------------------------------------
-- Representation of critical pairs
-- ---------------------------------------------------------------------------

--- A critical pair represented as a pair of terms and parameterized over the
--- kind of function symbols, e.g., strings.
type CPair f = (Term f, Term f)

-- ---------------------------------------------------------------------------
-- Pretty-printing of critical pairs
-- ---------------------------------------------------------------------------

-- \x3008 = LEFT ANGLE BRACKET
-- \x3009 = RIGHT ANGLE BRACKET

--- Transforms a critical pair into a string representation.
showCPair :: (f -> String) -> CPair f -> String
showCPair s (l, r) = "\12296" ++ (showTerm s l) ++ ", " ++ (showTerm s r)
                       ++ "\12297"

--- Transforms a list of critical pairs into a string representation.
showCPairs :: (f -> String) -> [CPair f] -> String
showCPairs s = unlines . (map (showCPair s))

-- ---------------------------------------------------------------------------
-- Computation of critical pairs
-- ---------------------------------------------------------------------------

--- Returns the critical pairs of a term rewriting system.
cPairs :: Eq f => TRS f -> [CPair f]
cPairs trs =
  let trs' = maybe trs (\v -> renameTRSVars (v + 1) trs) (maxVarInTRS trs)
   in nub [(applySubst sub r1,
            replaceTerm (applySubst sub l1) p (applySubst sub r2)) |
           rule1@(l1, r1) <- trs',
           p <- positions l1,
           let l1p = l1 |> p, isConsTerm l1p,
           rule2@(l2, r2) <- trs,
           Right sub <- [unify [(l1p, l2)]],
           p /= eps || not (rule1 `isVariantOf` rule2)]

-- ---------------------------------------------------------------------------
-- Functions for term rewriting systems and critical pairs
-- ---------------------------------------------------------------------------

--- Checks whether a term rewriting system is orthogonal.
isOrthogonal :: Eq f => TRS f -> Bool
isOrthogonal trs = isLeftLinear trs && null (cPairs trs)

--- Checks whether a term rewriting system is weak-orthogonal.
isWeakOrthogonal :: Eq f => TRS f -> Bool
isWeakOrthogonal trs = isLeftLinear trs && all (uncurry (==)) (cPairs trs)