logic-classes-1.1: Data/Logic/Tests/Harrison/Equal.hs
{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TypeSynonymInstances #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Logic.Tests.Harrison.Equal where
-- =========================================================================
-- First order logic with equality.
--
-- Copyright (co) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
-- =========================================================================
import Control.Applicative.Error (Failing(..))
import Data.Logic.Classes.Combine (Combinable(..), (∧), (⇒))
import Data.Logic.Classes.Equals ((.=.), pApp)
import Data.Logic.Classes.FirstOrder ((∃), (∀))
import Data.Logic.Classes.Skolem (Skolem(..))
import Data.Logic.Classes.Term (Term(..))
import Data.Logic.Harrison.Equal (equalitize, function_congruence)
import Data.Logic.Harrison.Meson (meson)
import Data.Logic.Harrison.Skolem (runSkolem)
import Data.Logic.Types.Harrison.FOL (TermType(..))
import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula(..))
import Data.Logic.Types.Harrison.Equal (FOLEQ(..), PredName)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.String (IsString(fromString))
-- import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual)
import Data.Logic.Tests.Harrison.HUnit
-- type TF = TestFormula (Formula FOL) FOL TermType String String Function
-- type TFE = TestFormulaEq (Formula FOLEQ) FOLEQ TermType String String Function
tests :: Test (Formula FOLEQ)
tests = TestLabel "Data.Logic.Tests.Harrison.Equal" $ TestList [test01, test02, test03, test04]
-- -------------------------------------------------------------------------
-- Example.
-- -------------------------------------------------------------------------
test01 :: Test (Formula FOLEQ)
test01 = TestCase $ assertEqual "function_congruence" expected input
where input = map function_congruence [(fromString "f", 3 :: Int), (fromString "+",2)]
expected :: [Set.Set (Formula FOLEQ)]
expected = [Set.fromList
[(∀) x1
((∀) x2
((∀) x3
((∀) y1
((∀) y2
((∀) y3 ((((vt x1) .=. (vt y1)) ∧ (((vt x2) .=. (vt y2)) ∧ ((vt x3) .=. (vt y3)))) ⇒
((fApp (fromString "f") [vt x1,vt x2,vt x3]) .=. (fApp (fromString "f") [vt y1,vt y2,vt y3]))))))))],
Set.fromList
[(∀) x1
((∀) x2
((∀) y1
((∀) y2 ((((vt x1) .=. (vt y1)) ∧ ((vt x2) .=. (vt y2))) ⇒
((fApp (fromString "+") [vt x1,vt x2]) .=. (fApp (fromString "+") [vt y1,vt y2]))))))]]
x1 = fromString "x1"
x2 = fromString "x2"
x3 = fromString "x3"
y1 = fromString "y1"
y2 = fromString "y2"
y3 = fromString "y3"
-- -------------------------------------------------------------------------
-- A simple example (see EWD1266a and the application to Morley's theorem).
-- -------------------------------------------------------------------------
test :: (Show a, Eq a) => String -> a -> a -> Test (Formula FOLEQ)
test label expected input = TestLabel label $ TestCase $ assertEqual label expected input
test02 :: Test (Formula FOLEQ)
test02 = test "equalitize 1 (p. 241)" expected input
where input = runSkolem (meson (Just 5) ewd)
ewd :: Formula FOLEQ
ewd = equalitize fm
fm :: Formula FOLEQ
fm = ((∀) x (fx ⇒ gx)) ∧ ((∃) x fx) ∧ ((∀) x ((∀) y (gx ∧ gy ⇒ vt x .=. vt y))) ⇒
(∀) y gy ⇒ fy
fx = pApp' "f" [vt x]
gx = pApp' "g" [vt x]
fy = pApp' "f" [vt y]
gy = pApp' "g" [vt y]
x = fromString "x"
y = fromString "y"
-- y1 = fromString "y1"
-- z = fromString "z"
expected =
Set.singleton (Success ((Map.fromList [(fromString "_0",vt' "_2"),
(fromString "_1",fApp (toSkolem 1) []),
(fromString "_2",vt' "_4"),
(fromString "_3",fApp (toSkolem 1) []),
(fromString "_4",fApp (toSkolem 2) []),
(fromString "_5",fApp (toSkolem 1) [])], 0, 6), 5))
{-
fApp' :: String -> [term] -> term
fApp' s ts = fApp (fromString s) ts
for_all' s = for_all (fromString s)
exists' s = exists (fromString s)
-}
pApp' :: String -> [TermType] -> Formula FOLEQ
pApp' s ts = pApp (fromString s :: PredName) ts
vt' :: String -> TermType
vt' s = vt (fromString s)
-- -------------------------------------------------------------------------
-- Wishnu Prasetya's example (even nicer with an "exists unique" primitive).
-- -------------------------------------------------------------------------
test03 :: Test (Formula FOLEQ)
test03 = TestLabel "equalitize 2" $ TestCase $ assertEqual "equalitize 2 (p. 241)" expected input
where input = runSkolem (meson (Just 1) wishnu)
wishnu = equalitize fm
fm :: Formula FOLEQ
fm = ((∃) (fromString "x") ((x .=. f[g[x]]) ∧ (∀) (fromString "x'") ((x' .=. f[g[x']]) ⇒ (x .=. x')))) .<=>.
((∃) (fromString "y") ((y .=. g[f[y]]) ∧ (∀) (fromString "y'") ((y' .=. g[f[y']]) ⇒ (y .=. y'))))
x = vt (fromString "x")
y = vt (fromString "y")
x' = vt (fromString "x'")
y' = vt (fromString "y")
f terms = fApp (fromString "f") terms
g terms = fApp (fromString "g") terms
expected = Set.singleton (Failure ["Exceeded maximum depth limit"])
-- -------------------------------------------------------------------------
-- More challenging equational problems. (Size 18, 61814 seconds.)
-- -------------------------------------------------------------------------
test04 :: Test (Formula FOLEQ)
test04 = test "equalitize 3 (p. 248)" expected input
where
input = runSkolem (meson (Just 20) . equalitize $ fm)
fm :: Formula FOLEQ
fm = ((∀) "x" . (∀) "y" . (∀) "z") ((*) [x', (*) [y', z']] .=. (*) [((*) [x', y']), z']) ∧
(∀) "x" ((*) [one, x'] .=. x') ∧
(∀) "x" ((*) [i [x'], x'] .=. one) ⇒
(∀) "x" ((*) [x', i [x']] .=. one)
x' = vt "x" :: TermType
y' = vt "y" :: TermType
z' = vt "z" :: TermType
(*) = fApp (fromString "*")
i = fApp (fromString "i")
one = fApp (fromString "1") []
expected :: Set.Set (Failing ((Map.Map String TermType, Int, Int), Int))
expected =
Set.fromList
[Success ((Map.fromList
[( "_0", (*) [one, vt' "_3"]),
( "_1", (*) [fApp (toSkolem 1) [],i [fApp (toSkolem 1) []]]),
( "_2", one),
( "_3", (*) [fApp (toSkolem 1) [],i [fApp (toSkolem 1) []]]),
( "_4", vt' "_8"),
( "_5", (*) [one, vt' "_3"]),
( "_6", one),
( "_7", vt' "_11"),
( "_8", vt' "_12"),
( "_9", (*) [one, vt' "_3"]),
("_10", (*) [vt' "_13",(*) [vt' "_14", vt' "_15"]]),
("_11", (*) [(*) [vt' "_13", vt' "_14"], vt' "_15"]),
("_12", (*) [vt' "_19", vt' "_18"]),
("_13", vt' "_16"),
("_14", vt' "_21"),
("_15", (*) [vt' "_22", vt' "_23"]),
("_16", vt' "_20"),
("_17", (*) [vt' "_14", vt' "_15"]),
("_18", (*) [(*) [vt' "_21", vt' "_22"], vt' "_23"]),
("_19", vt' "_20"),
("_20", i [vt' "_28"]),
("_21", vt' "_28"),
("_22", fApp (toSkolem 1) []),
("_23", i [fApp (toSkolem 1) []]),
("_24", (*) [vt' "_13", vt' "_14"]),
("_25", (*) [vt' "_22", vt' "_23"]),
("_26", (*) [fApp (toSkolem 1) [],i [fApp (toSkolem 1) []]]),
("_27", one),
("_28", vt' "_30"),
("_29", (*) [vt' "_22", vt' "_23"]),
("_30", (*) [(*) [vt' "_21", vt' "_22"], vt' "_23"])],
0,31),13)]
vt' = vt . fromString