-- Unification in a commutative monoid -- -- Copyright (C) 2009 John D. Ramsdell -- -- This program is free software: you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation, either version 3 of the License, or -- (at your option) any later version. -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- You should have received a copy of the GNU General Public License -- along with this program. If not, see <http://www.gnu.org/licenses/>. -- | -- Module : Algebra.CommutativeMonoid.Unification -- Copyright : (C) 2009 John D. Ramsdell -- License : GPL -- -- This module provides unification in a commutative monoid. -- -- In this module, a commutative monoid is a free algebra over a -- signature with two function symbols: -- -- * the binary symbol +, the monoid operator, -- -- * a constant 0, the identity element, and -- -- The algebra is generated by a set of variables. Syntactically, a -- variable is an identifer such as x and y (see 'isVar'). -- -- The axioms associated with the algebra are: -- -- [Communtativity] x + y = y + x -- -- [Associativity] (x + y) + z = x + (y + z) -- -- [Identity Element] x + 0 = x -- -- A substitution maps variables to terms. A substitution s is -- applied to a term as follows. -- -- * s(0) = 0 -- -- * s(t + t\') = s(t) + s(t\') -- -- The unification problem is given the problem statement t =? t\', -- find a most general substitution s such that s(t) = s(t\') modulo -- the axioms of the algebra. Substitition s is more general than s\' -- if there is a substitition s\" such that s\' = s\" o s. module Algebra.CommutativeMonoid.Unification ( -- * Terms Term, ide, isVar, var, mul, add, assocs, -- * Equations and Substitutions Equation(..), Substitution, subst, maplets, apply, -- * Unification unify) where import Data.Char (isSpace, isAlpha, isAlphaNum, isDigit) import Data.List (transpose) import Data.Map (Map) import qualified Data.Map as Map import Algebra.CommutativeMonoid.LinDiaphEq -- Chapter 8, Section 5 of the Handbook of Automated Reasoning by -- Franz Baader and Wayne Snyder describes unification in -- commutative/monoidal theories. This module refines the described -- algorithms for the special case of a commutative monoid. -- In this module, a commutative monoid is a free algebra over a signature -- with two function symbols: -- -- * the binary symbol +, the monoid operator, -- * a constant 0, the identity element, and -- -- The algebra is generated by a set of variables. Syntactically, a -- variable is an identifer such as x and y. -- The axioms associated with the algebra are: -- -- * x + y = y + x Commutativity -- * (x + y) + z = x + (y + z) Associativity -- * x + 0 = x Identity Element -- A substitution maps variables to terms. A substitution s is -- extended to a term as follows. -- -- s(0) = 0 -- s(t + t') = s(t) + s(t') -- The unification problem is given the problem statement t =? t', -- find a most general substitution s such that s(t) = s(t') modulo -- the axioms of the algebra. Substitition s is more general than s' -- if there is a substitition s" such that s' = s" o s. -- A term is represented by the identity element, or as the sum of -- factors. A factor is the product of a positive integer coefficient -- and a variable. In this representation, no variable occurs twice. -- Thus a term is represented by a finite map from variables to -- non-negative integers. -- | A term in a commutative monoid is represented by the -- identity element, or as the sum of factors. A factor is the -- product of a positive integer coefficient and a variable. No -- variable occurs twice in a term. For the show and read methods, -- zero is the identity element, the plus sign is the monoid operation. newtype Term = Term (Map String Int) deriving Eq -- Constructors -- | 'ide' represents the identity element (zero). ide :: Term ide = Term Map.empty -- | A variable is an alphabetic Unicode character followed by a -- sequence of alphabetic or numeric digit Unicode characters. The -- show method for a term works correctly when variables satisfy -- the 'isVar' predicate. isVar :: String -> Bool isVar [] = False isVar (c:s) = isAlpha c && all isAlphaNum s -- | Return a term that consists of a single variable. var :: String -> Term var x = Term $ Map.singleton x 1 -- | Multiply every coefficient in a term by an non-negative integer. mul :: Int -> Term -> Term mul 0 (Term _) = ide mul 1 t = t mul n (Term t) | n < 0 = error "Negative coefficient found" | otherwise = Term $ Map.map (* n) t -- Invert a term by negating its coefficients. neg :: Term -> Term neg (Term t) = Term $ Map.map negate t -- | Add two terms. add :: Term -> Term -> Term add (Term t) (Term t') = Term $ Map.foldrWithKey f t' t -- Fold over the mappings in t where f x c t = -- Alter the mapping of Map.alter (g c) x t -- variable x in t g c Nothing = -- Variable x not currently mapped Just c -- so add a mapping g c (Just c') -- Variable x maps to c' | c + c' == 0 = Nothing -- Delete the mapping | otherwise = Just $ c + c' -- Adjust the mapping -- | Return all variable-coefficient pairs in the term in ascending -- variable order. assocs :: Term -> [(String, Int)] assocs (Term t) = Map.assocs t -- | Convert a list of variable-coefficient pairs into a term. term :: [(String, Int)] -> Term term assoc = foldr f ide assoc where f (x, c) t = add t $ mul c $ var x -- Equations and Substitutions -- | An equation is a pair of terms. For the show and read methods, -- the two terms are separated by an equal sign. newtype Equation = Equation (Term, Term) deriving Eq -- | A substitution maps variables into terms. For the show and read -- methods, the substitution is a list of maplets, and the variable -- and the term in each element of the list are separated by a colon. newtype Substitution = Substitution (Map String Term) deriving Eq -- | Construct a substitution from a list of variable-term pairs. subst :: [(String, Term)] -> Substitution subst assocs = Substitution $ foldl f Map.empty assocs where f t (x, n) = Map.insert x n t -- | Return all variable-term pairs in ascending variable order. maplets :: Substitution -> [(String, Term)] maplets (Substitution s) = Map.assocs s -- | Return the result of applying a substitution to a term. apply :: Substitution -> Term -> Term apply (Substitution s) (Term t) = Map.foldrWithKey f ide t where f x n t = add (mul n (Map.findWithDefault (var x) x s)) t -- Unification -- | Given 'Equation' (t0, t1), return a most general substitution s -- such that s(t0) = s(t1) modulo the equational axioms of a -- commutative monoid. unify :: Equation -> Substitution unify (Equation (t0, t1)) = case assocs (add t0 (neg t1)) of [] -> Substitution Map.empty t -> let basis = linDiaphEq (map snd t) 0 in mgu (map fst t) basis -- Construct a most general unifier the minimal non-negative solutions -- to a linear equation. The function adds the variables back into -- terms, and generates fresh variables as needed. mgu :: [String] -> [[Int]] -> Substitution mgu vars basis = subst (zip vars terms) where terms = map (term . zip genSyms) (transpose basis) genSyms = genSymsAvoiding vars -- Generated variables start with this character. genChar :: Char genChar = 'g' -- Generated symbols are the gen start char followed by a number. genSym :: Int -> String genSym i = genChar : show i -- Produce a stream of generated identifiers avoiding what's in vars. genSymsAvoiding :: [String] -> [String] genSymsAvoiding vars = genSymStream 0 where seen = filter genStr vars genStr (c:_) = c == genChar genStr _ = False genSymStream n | elem (genSym n) seen = genSymStream (n + 1) | otherwise = genSym n : genSymStream (n + 1) -- So why solve linear equations? Consider the matching problem -- -- c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1] =? -- d[0]*a[0] + d[1]*a[1] + ... + d[m-1]*a[m-1] -- -- with n variables and m constants. We seek a most general unifier s -- such that -- -- s(c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1]) = -- d[0]*a[0] + d[1]*a[1] + ... + d[m-1]*a[m-1] -- -- which is the same as -- -- c[0]*s(x[0]) + c[1]*s(x[1]) + ... + c[n-1]*s(x[n-1]) = -- d[0]*a[0] + d[1]*a[1] + ... + d[m-1]*a[m-1] -- -- Notice that the number of occurrences of constant a[0] in s(x[0]) -- plus s(x[1]) ... s(x[n-1]) must equal d[0]. Thus the mappings of -- the unifier that involve constant a[0] respect non-negative integer -- solutions of the following linear equation. -- -- c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1] = d[0] -- -- To compute a most general unifier, the set of minimal non-negative -- integer solutions to a linear equation must be found. See module -- Algebra.CommutativeMonoid.LinDiaphEq. -- Input and Output instance Show Term where showsPrec _ t = case assocs t of [] -> showString "0" (t:ts) -> showFactor t . showl ts where showFactor (x, 1) = showString x showFactor (x, c) = shows c . showString x showl [] = id showl (t:ts) = showString " + " . showFactor t . showl ts instance Read Term where readsPrec _ s0 = [ (t1, s2) | (t0, s1) <- readFactor s0, (t1, s2) <- readRest t0 s1 ] where readPrimary s0 = [ (t0, s1) | (x, s1) <- scan s0, isVarToken x, let t0 = var x ] ++ [ (t0, s1) | ("0", s1) <- scan s0, let t0 = ide ] ++ [ (t0, s3) | ("(", s1) <- scan s0, (t0, s2) <- reads s1, (")", s3) <- scan s2 ] readFactor s0 = [ (t0, s1) | (t0, s1) <- readPrimary s0 ] ++ [ (t1, s2) | (n, s1) <- scan s0, isNumToken n, (t0, s2) <- readPrimary s1, let t1 = mul (read n) t0 ] readRest t0 s0 = [ (t2, s3) | ("+", s1) <- scan s0, (t1, s2) <- readFactor s1, (t2, s3) <- readRest (add t0 t1) s2 ] ++ [ (t0, s0) | (s, _) <- scan s0, s /= "+" ] isNumToken :: String -> Bool isNumToken (c:_) = isDigit c isNumToken _ = False isVarToken :: String -> Bool isVarToken (c:_) = isAlpha c isVarToken _ = False scan :: ReadS String scan "" = [("", "")] scan (c:s) | isSpace c = scan s | isAlpha c = [ (c:part, t) | (part,t) <- [span isAlphaNum s] ] | isDigit c = [ (c:part, t) | (part,t) <- [span isDigit s] ] | otherwise = [([c], s)] instance Show Equation where showsPrec _ (Equation (t0, t1)) = shows t0 . showString " = " . shows t1 instance Read Equation where readsPrec _ s0 = [ (Equation (t0, t1), s3) | (t0, s1) <- reads s0, ("=", s2) <- scan s1, (t1, s3) <- reads s2 ] -- This datatype is used only in the read and show methods for -- substitutions. newtype Maplet = Maplet (String, Term) deriving Eq instance Show Maplet where showsPrec _ (Maplet (x, t)) = showString x . showString " : " . shows t instance Read Maplet where readsPrec _ s0 = [ (Maplet (x, t), s3) | (x, s1) <- scan s0, isVarToken x, (":", s2) <- scan s1, (t, s3) <- reads s2 ] instance Show Substitution where showsPrec _ s = shows $ map Maplet $ maplets s instance Read Substitution where readsPrec _ s0 = [ (subst $ map pair ms, s1) | (ms, s1) <- reads s0 ] where pair (Maplet (x, t)) = (x, t)