module Decide_Termination where
import Prelude hiding (sequence)
import Data.Monoid (mempty)
import Data.Traversable (sequence)
import Data.Map (Map, (!), unionWith)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe, mapMaybe)
data Term = App String [Term]
| Var String
deriving (Eq, Show, Read)
type Subst = Map String Term
subst :: Subst -> Term -> Term
subst sigma (App c ts) = App c (map (subst sigma) ts)
subst sigma (Var n) = fromMaybe (Var n) (Map.lookup n sigma)
{-- MATCHING
If
match t1 t2 = Just sigma
holds, then
subst sigma t1 = t2
--}
merge_maybe :: Eq a => Maybe a -> Maybe a -> Maybe a
merge_maybe (Just a) (Just b)
| a == b = Just a
| otherwise = Nothing
merge_maybe _ _ = Nothing
merge_map :: (Ord k, Eq v) => Map k v -> Map k v -> Maybe (Map k v)
merge_map s t = sequence (unionWith merge_maybe (Map.map Just s) (Map.map Just t))
match :: Term -> Term -> Maybe Subst
match (Var n) t = Just (Map.singleton n t)
match (App f c) (App g d) = if f == g then match_list c d else Nothing
match (App f c) (Var _) = Nothing
match_list :: [Term] -> [Term] -> Maybe Subst
match_list [] [] = Just mempty
match_list (c:cs) (d:ds) =
do
s <- match c d
t <- match_list cs ds
merge_map s t
match_list _ _ = Nothing
subterms :: Term -> [Term]
subterms (Var n) = []
subterms (App f ps) = App f ps : concatMap subterms ps
{-- SOLUTION --}
{--
Check if the equation system is
a) right-ground, i.e. there are no variables at the right sides , and, if it is right-ground,
b) terminating.
Implement the method described in TRaAT:
* start with a term from the right side of an equation
* perform reduction until you either
- find a loop (the original term is a subterm), -> return False
- or there are no possible reductions -> return True
Of course, you need to remember the starting term, and it needs to be done simultaneously, otherwise
the decision method might not terminate.
--}
decide_termination :: [(Term, Term)] -> Bool
decide_termination = ...
{-- EXAMPLES --}
f x y = App "f" [x, y]
g x = App "g" [x]
h x = App "h" [x]
a = App "a" []
b = App "b" []
c = App "c" []
x = Var "x"
y = Var "y"
z = Var "z"
eqs1 = [(f x x, f a b), (a, b)]
eqs2 = [(f x x, f a b), (b, c)]
eqs3 = [(f x y, f a b)]