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)]