diff --git a/Control/Fix.hs b/Control/Fix.hs new file mode 100644 --- /dev/null +++ b/Control/Fix.hs @@ -0,0 +1,103 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -O0 #-} + +-- | Several ways of expressing the polymorphic fix-point combinator in Haskell +-- without resorting to value recursion or unsafe operations. +-- This present code attempts to translate the OCaml version +-- +-- +-- +-- to Haskell. +-- +module Control.Fix where + +import Control.Monad.ST.Lazy +import Data.STRef.Lazy +import Data.Dynamic + +-- | Factorial written in the `open recursion style', without the use +-- of recursion. +fact self 0 = 1 +fact self n = n * self (pred n) + +-- The first approach: using the iso-recursive algebraic data type +-- The functions Wrap and unwrap witness the isomorphism +-- +-- > r == r -> a +-- +newtype Wrap a = Wrap{unwrap :: Wrap a -> a} +fix1 f = let aux g = g (Wrap g) in + aux (\x -> f (unwrap x x)) + +test1 = fix1 fact 5 +-- 120 + +-- | The 2. approach: using Dynamics for type abstraction. +-- This is the only example where constraints, Typeable in this case, +-- are imposed. +-- The other fixes in this file are fully polymorphic. +fix2 f = + let wrap = toDyn + unwrap x = fromDyn x undefined + aux g = g (wrap g) in + aux (\x -> f (unwrap x x)) + +test2 = fix2 fact (5::Int) +-- 120 + +-- | The third approach: type abstraction, impredicativity +-- and implicit type-level recursion: +-- the data type declaration can refer to a class that refers +-- to the type being declared +-- No spurious constraints are introduced +data W3 a = forall d. C d => W3 (d a -> a) + +class C d where + unwrap3 :: (d a -> a) -> W3 a -> a + +instance C W3 where + unwrap3 = ($) + +fix3 f = let aux g = g (W3 g) in + aux (\x -> f (case x of W3 h -> unwrap3 h x)) + +test3 = fix3 fact 5 +-- 120 + + +-- | Even better example, exploiting the fact that type classes and +-- type families are open. Hence we can define instances afterwards, +-- referring to already defined types. +-- Haskell is inconsistent in yet another way. +-- +type family D a :: * + +newtype W31 a = W31 (D a -> a) + +type instance D a = W31 a + +fix31 f = let aux g = g (W31 g) in + aux (\x -> f (case x of W31 h -> h x)) + + +test31 = fix31 fact 5 +-- 120 + +-- | The fourth approach: using references and laziness +-- Any sort of partiality (partial pattern-match) would work instead +-- of the error call. +-- The example might seem paradoxical: the effect of reading the wrap +-- cell seems to be occurring in the pure code. +-- Lazy ST is indeed quite interesting (for more discussion, see +-- Moggi and Sabry, 2001). +-- +fix4 f = runST (do + wrap <- newSTRef (error "black hole") + let aux = readSTRef wrap >>= (\x -> x >>= return . f) + writeSTRef wrap aux + aux) + +test4 = fix4 fact 5 +-- 120 + diff --git a/Language/DefinitionTree.hs b/Language/DefinitionTree.hs new file mode 100644 --- /dev/null +++ b/Language/DefinitionTree.hs @@ -0,0 +1,383 @@ +{-# LANGUAGE PatternGuards #-} +-- | A model of the evaluation of logic programs (i.e., resolving Horn clauses) +-- +-- The point is not to re-implement Prolog with all the conveniences +-- but to formalize evaluation strategies such as SLD, SLD-interleaving, +-- and others. +-- The formalization is aimed at reasoning about termination and +-- solution sequences. See App A and B of the full FLOPS 2008 paper +-- (the file arithm.pdf in this directory). +-- +module Language.DefinitionTree where + +import Data.Map +import Prelude hiding (lookup) + +-- | A logic var is represented by a pair of an integer +-- and a list of `predicate marks' (which are themselves +-- integers). Such an odd representation is needed to +-- ensure the standardization apart: different instances +-- of a clause must have distinctly renamed variables. +-- Unlike Claessen, we get by without the state monad +-- to generate unique variable names (labels). See the +-- discussion and examples in the `tests' section below. +-- Our main advantage is that we separate the naming of +-- variables from the evaluation strategy. Evaluation +-- no longer cares about generating fresh names, which +-- notably simplifies the analysis of the strategies. +-- Logic vars are typed, albeit phantomly. +type VStack = [Int] +type LogicVar term = (Int,VStack) + +-- | A finite map from vars to terms (parameterized over the domain of terms) +type Subst term = Map (LogicVar term) term + + +-- | Formulas +-- +-- A formula describes a finite or _infinite_ AND-OR tree +-- that encodes the logic-program clauses that may be needed to +-- evaluate a particular goal. +-- We represent a goal g(t1,...,tn) by a combination of the goal +-- g(X1,...,Xn), whose arguments are distinct fresh logic +-- variables, and a substitution {Xi=ti}. For a goal +-- g(X1,...,Xn), a |Formula| encodes all the clauses of the +-- logic program that could possibly prove g, in their order. Each +-- clause +-- +-- > g(t1,...,tn) :- b1(t11,...,t1m), ... +-- +-- is represented by the (guarding) substitution {Xi=ti, Ykj=tkj} +-- and the sequence of the goals bk(Yk1,...,Ykm) in the body. +-- Each of these goals is again encoded as a |Formula|. +-- All variables in the clauses are renamed to ensure the standardization apart. +-- +-- Our trees are similar to Antoy's definitional trees, used to encode +-- rewriting rules and represent control strategies in +-- term-rewriting systems and _functional logic_ programming. +-- However, in definitional trees, function calls can be nested, +-- and patterns are linear. +-- +-- The translation from Prolog is straightforward; the first step +-- is to re-write clauses so that the arguments of each goal are +-- logic variables: +-- A fact +-- +-- > g(term). +-- +-- is converted to +-- +-- > g(X) :- X = term. +-- +-- A clause +-- +-- > g(term) :- g1(term1), g2(term2). +-- +-- is converted to +-- +-- > g(X) :- X = term, _V1 = term1, g1(_V1), _V2=term2, g2(_V2). +-- +-- See the real examples at the end +-- +-- A formula (parameterized by the domain of terms) is an OR-sequence +-- of clauses +data Formula term = Fail | (Clause term) :+: (Formula term) + +-- | A clause is a guarded body; the latter is an AND-sequence of formulas +data Clause term = G (Subst term) (Body term) + +data Body term = Fact | (Formula term) :*: (Body term) + +infixr 6 :+: +infix 7 `G` +infixr 8 :*: + +-- Evaluation of formulas + +-- | The evaluation process starts with a formula and the initial +-- substitution, which together represent a goal. The +-- guarding substitution of the clause conjoins with the current +-- substitution to yield the substitution for the evaluation of the body. +-- The conjunction of substitutions may lead to a contradiction, +-- in which case the clause is skipped (`pruned'). +-- +-- Evaluation as pruning: we traverse a tree and prune away failed branches +prune :: Unifiable term => Formula term -> Subst term -> Formula term +prune Fail _ = Fail +prune (cl :+: f2) s = case prunec cl s of + Nothing -> prune f2 s + Just cl -> cl :+: prune f2 s + +prunec :: Unifiable term => Clause term -> Subst term -> Maybe (Clause term) +prunec (G s' b) s = case unify s s' of + Nothing -> Nothing + Just s -> case pruneb b s of + Nothing -> Nothing + Just b -> Just $ G s b +pruneb Fact s = Just Fact +pruneb (f :*: b) s = case prune f s of + Fail -> Nothing + f -> case pruneb b s of + Nothing -> Nothing + Just b -> Just $ f :*: b + +-- one may also try to push disjunctions up using distributivity... + + +-- | A different evaluator: Evaluate a tree to a stream (lazy list) +-- given the initial substitution s. +-- Here we use the SLD strategy. +eval :: Unifiable term => Formula term -> Subst term -> [Subst term] +eval Fail _ = [] +eval (cl :+: f2) s = evalc cl s ++ eval f2 s +evalc (G s' b) s = maybe [] (evalb b) $ unify s s' +evalb Fact s = [s] +evalb (f :*: b) s = concatMap (evalb b) (eval f s) + +-- | Same as above, using the SLD-interleaving strategy. +-- See Definition 3.1 of the LogicT paper (ICFP05) +evali :: Unifiable term => Formula term -> Subst term -> [Subst term] +evali Fail _ = [] +evali (cl :+: f2) s = evalic cl s `interleave` evali f2 s +evalic (G s' b) s = maybe [] (evalib b) $ unify s s' +evalib Fact s = [s] +evalib (f :*: b) s = fairConcatMap (evalib b) (evali f s) + where fairConcatMap k [] = [] + fairConcatMap k (a:m) = interleave (k a) (fairConcatMap k m) + +interleave [] m = m +interleave (a:m1) m2 = a : (interleave m2 m1) + +-- Terms and substitutions + +-- | Evaluation, substitutions and unification are parametric over terms +-- (term algebra), provided the following two operations are defined. +-- We should be able to examine a term and determine if it is a variable +-- or a constructor (represented by an integer) applied to a sequence of +-- zero or more terms. Conversely, given a constructor (represented by an +-- integer) and a list of terms-children we should be able to build a term. +-- The two operations must satisfy the laws: +-- +-- > either id build . classify === id +-- > classify . build === Right +-- +class Unifiable term where + classify :: term -> Either (LogicVar term) (Int,[term]) + build :: (Int,[term]) -> term + +-- | building substitutions +bv :: LogicVar term -> term -> Subst term +bv x = singleton x + +ins :: Subst term -> (LogicVar term, term) -> Subst term +ins m (v,t) = insert v t m + +-- | Apply a substitution to a term +sapp :: Unifiable term => Subst term -> term -> term +sapp s t = either dov donv $ classify t + where dov v = maybe t id $ lookup v s -- term is a variable + donv (ctr, ts) = build (ctr, Prelude.map (sapp s) ts) -- non-var term + + +-- | Conjoin two substitutions (see Defn 1 of the FLOPS 2008 paper). +-- We merge two substitutions and solve the resulting set of equations, +-- returning Nothing if the two original substitutions are contradictory. +unify :: Unifiable term => Subst term -> Subst term -> Maybe (Subst term) +unify s1 s2 = solve empty $ foldWithKey fld (foldWithKey fld [] s1) s2 + where + fld v t l = (Left v,t) : l + +-- | Solve the equations using the naive realization of the +-- Martelli and Montanari process +solve :: Unifiable term => Subst term -> + [(Either (LogicVar term) term,term)] -> + Maybe (Subst term) +solve s [] = Just s +solve s ((Left v,t):r) = either dov donv $ classify t + where dov v' = if v == v' then solve s r else add'cont + donv _ = add'cont -- skip the occurs check + s' = insert v t s + add'cont = solve s' (Prelude.map (sapp'eq s') r) + sapp'eq s (Left v,t) = (maybe (Left v) Right $ lookup v s, sapp s t) + sapp'eq s (Right t1,t2) = (Right $ sapp s t1, sapp s t2) +solve s ((Right t1,t2):r) = + case (classify t1, classify t2) of + (Left v,_) -> solve s $ (Left v,t2):r + (_,Left v) -> solve s $ (Left v,t1):r + (Right (ctr1,ts1),Right (ctr2,ts2)) + | ctr1 == ctr2, length ts1 == length ts2 -> + solve s $ (zipWith (\x y -> (Right x,y)) ts1 ts2) ++ r + _ -> Nothing + + + +-- Tests and examples + +-- | Unary numerals +-- +data UN = UNv (LogicVar UN) + | UZ + | US UN + deriving (Eq, Show) + +-- | Constructor UZ is represented by 0, and US is represented by 1 +instance Unifiable UN where + classify (UNv v) = Left v + classify UZ = Right (0,[]) + classify (US n) = Right (1,[n]) + + build (0,[]) = UZ + build (1,[n]) = US n + + +-- | Encoding of variable names to ensure standardization apart. +-- A clause such as genu(X) or add(X,Y,Z) may appear in the tree +-- (infinitely) many times. We must ensure that each instance uses distinct +-- logic variables. To this end, we name variables by a pair (Int, VStack) +-- whose first component is the local label of a variable within a clause. +-- VStack is a path from the root of the tree to the current occurrence +-- of the clause in the tree. Each predicate along the path is represented +-- by an integer label (0 for genu, 1 for add, 2 for mul, etc). +-- To `pass' arguments to a clause, we add to the current substitution +-- the bindings for the variables of that clause. See the genu' example +-- below: whereas (0,h) is the label of the variable X in the current +-- instance of genu, (0,genu_mark:h) is X in the callee. +-- +-- A logic program +-- +-- > genu([]). +-- > genu([u|X]) :- genu(X). +-- +-- and the goal genu(X) are encoded as follows. The argument of genu' is +-- the path of the current instance of genu' from the top of the AND-OR +-- tree. +-- +genu :: Formula UN +genu = genu' [] + where + genu' h = (bv x UZ) `G` Fact :+: + (bv x (US (UNv x'))) `G` (genu' h') :*: Fact :+: + Fail + where x = (0,h) + h' = genu_mark:h + x' = (0,h') + genu_mark = 0 + +test1 = take 5 (eval genu empty) +{- +*SLD> test1 + [fromList [((0,[]),UZ)], + fromList [((0,[]),US UZ),((0,[0]),UZ)], + fromList [((0,[]),US (US UZ)),((0,[0]),US UZ),((0,[0,0]),UZ)], + fromList [((0,[]),US (US (US UZ))),((0,[0]),US (US UZ)), + ((0,[0,0]),US UZ),((0,[0,0,0]),UZ)], + fromList [((0,[]),US (US (US (US UZ)))),((0,[0]),US (US (US UZ))), + ((0,[0,0]),US (US UZ)),((0,[0,0,0]),US UZ),((0,[0,0,0,0]),UZ)]] +-} + + +-- A logic program with the goal add(X,Y,Z) +-- add([],X,X). +-- add([u|X],Y,[u|Z]) :- add(X,Y,Z). +-- is encoded as follows. The labels of local variables are: +-- X is 0, Y is 1, Z is 2. + +add :: VStack -> Formula UN +add h = (bv x UZ) `ins` (y,(UNv z)) `G` Fact :+: + (bv x (US (UNv x'))) `ins` (y,UNv y') `ins` (z,US (UNv z')) + `G` add h' :*: Fact :+: + Fail + where + [x,y,z] = Prelude.map (\n->(n,h)) [0..2] -- vars in the current call + h' = add_mark:h + [x',y',z'] = Prelude.map (\n->(n,h')) [0..2] -- vars in the recursive call +add_mark = 1 + +test2 = take 3 (eval (add []) empty) + +{- +*SLD> test2 + [fromList [((0,[]),UZ),((1,[]),UNv (2,[]))], + fromList [((0,[]),US UZ),((0,[1]),UZ),((1,[]),UNv (2,[1])), + ((1,[1]),UNv (2,[1])),((2,[]),US (UNv (2,[1])))], + fromList [((0,[]),US (US UZ)),((0,[1]),US UZ),((0,[1,1]),UZ), + ((1,[]),UNv (2,[1,1])),((1,[1]),UNv (2,[1,1])), + ((1,[1,1]),UNv (2,[1,1])),((2,[]),US (US (UNv (2,[1,1])))), + ((2,[1]),US (UNv (2,[1,1])))]] + +Note that (0,[]) is the top-level X, (1,[]) is teh top-level Y, +(2,[]) is the top-level Z. In the more concise notation, the above +list of substitution reads: + [(X,0), (Y,Z)] + [(X,1), (Y,Z'), (Z, succ(Z'))] + [(X,2), (Y,Z''), (Z,succ (succ (Z'')))] +-} + +test3 = take 3 (evali (add []) empty) +-- the same as test2 + +-- A logic program with the goal mul(X,Y,Z) (Sec 2.3 of the FLOPS paper) +-- mul([],_,[]). +-- mul([u|_],[],[]). +-- mul([u|X],[u|Y],Z) :- add([u|Y],Z1,Z), mul(X,[u|Y],Z1). +-- is converted into +-- mul(X,Y,Z) :- X=[], Z=[]. +-- mul(X,Y,Z) :- X=[u|X1], Y=[], Z=[]. +-- mul(X,Y,Z) :- X=[u|X1], Y=[u|Y1], +-- AddX=Y, AddY=Z1, AddZ=Z, +-- MulX=X1, MulY=Y, MulZ=Z1, +-- add(AddX,AddY,AddZ), mul(MulX,MulY,MulZ). + +-- is encoded as follows. The labels of local variables are: +-- X is 0, Y is 1, Z is 2. + +mul :: VStack -> Formula UN +mul h = (bv x UZ) `ins` (z,UZ) `G` Fact :+: + + (bv x (US (UNv x1))) `ins` (y,UZ) `ins` (z,UZ) `G` Fact :+: + + (bv x (US (UNv x1))) `ins` (y,US (UNv y1)) `ins` + (addx,(UNv y)) `ins` (addy,(UNv z1)) `ins` (addz,(UNv z)) `ins` + (mulx,(UNv x1)) `ins` (muly,(UNv y)) `ins` (mulz,(UNv z1)) + `G` add h'add :*: mul h'mul :*: Fact :+: + Fail + where + [x,y,z,x1,y1,z1] = Prelude.map (\n->(n,h)) [0..5] + h'add = add_mark:h -- frame for the call to add + h'mul = mul_mark:h -- frame for the recursive call to mul + [addx,addy,addz] = Prelude.map (\n->(n,h'add)) [0..2] + [mulx,muly,mulz] = Prelude.map (\n->(n,h'mul)) [0..2] +mul_mark = 2 + +test4 = take 6 . Prelude.map proj_xyz $ (eval (mul []) empty) +test5 = take 8 . Prelude.map proj_xyz $ (evali (mul []) empty) + +proj_xyz s = (pv 0, pv 1, pv 2) + where + pv n = maybe (UNv (n,[])) chase $ lookup (n,[]) s + chase t = let t' = sapp s t in if t == t' then t else chase t' + +{- +*SLD> test4 + [(UZ,UNv (1,[]),UZ), + (US (UNv (3,[])),UZ,UZ), + (US UZ,US UZ,US UZ), + (US (US UZ),US UZ,US (US UZ)), + (US (US (US UZ)),US UZ,US (US (US UZ))), + (US (US (US (US UZ))),US UZ,US (US (US (US UZ))))] + +This result matches the one mentioned on p10 of the paper (mul for SLD +without interleaving). In each solution except the first two, Y is 1. + +For interleaving, the picture is different: + +*SLD> test5 + [(UZ,UNv (1,[]),UZ), + (US (UNv (3,[])),UZ,UZ), + (US UZ,US UZ,US UZ), -- (1,1,1) + (US UZ,US (US UZ),US (US UZ)), -- (1,2,2) + (US (US UZ),US UZ,US (US UZ)), -- (2,1,1) + (US UZ,US (US (US UZ)),US (US (US UZ))), -- (1,3,3) + (US (US (US UZ)),US UZ,US (US (US UZ))), -- (3,1,3) + (US (US UZ),US (US UZ),US (US (US (US UZ))))] -- (2,2,4) +-} diff --git a/Logic/DynEpistemology.hs b/Logic/DynEpistemology.hs new file mode 100644 --- /dev/null +++ b/Logic/DynEpistemology.hs @@ -0,0 +1,290 @@ +-- | Dynamic Epistemic Logic: solving the puzzles from +-- Hans van Ditmarsch's tutorial course on Dynamic Epistemic Logic, +-- NASSLLI 2010, June 20, 2010. +-- See also +-- +-- Dynamic Epistemic Logic and Knowledge Puzzles +-- H.P. van Ditmarsch, W. van der Hoek, and B.P. Kooi +-- +-- +-- Epistemic Puzzles +-- Hans van Ditmarsch +-- +-- +-- +-- We encode the statement of the problem as a filter on +-- possible worlds. +-- The possible worlds consistent with the statement of +-- the problem are the solutions. +-- +-- > "Agent A does not know proposition phi" is interpreted +-- +-- as the statement that for all worlds consistent with the propositions +-- A currently knows, phi is true in some but false in the others. +-- +-- +-- +module Logic.DynEpistemology where + +import qualified Data.Map as M +import Control.Monad +import Data.List (sortBy, groupBy) + +-- ------------------------------------------------------------------------ +-- | Problem 1 +-- Anne and Bill each privately receive a natural number. +-- Their numbers are consecutive. +-- The following truthful conversation takes place: +-- +-- > Anne: I don't know your number +-- > Bill: I don't know your number either +-- > Anne: I know your number. +-- > Bill: I know your number too. +-- +-- If Anne has received the number 2, what was the number +-- received by Bill? +-- This puzzle is also known as `Conway paradox': it appears +-- that Anne and Bill have truthfully made contradictory statements. +-- +-- A possible world for a problem 1: +-- numbers received by Anne and Bill +-- +type P1World = (Int,Int) + +-- | The number Anne received in the world w +p1_anne :: P1World -> Int +p1_anne = fst + +-- | The number Bill received in the world w +p1_bill :: P1World -> Int +p1_bill = snd + +-- | An initial stream of possible worlds for problem 1 +p1worlds :: MonadPlus m => m P1World +p1worlds = do + anne_number <- nat + bill_number <- choose [anne_number + 1, anne_number - 1] + guard (bill_number >= 0) + return (anne_number,bill_number) + +-- | Encoding the statement of the problem: the conversation steps. +-- The remaining possible world gives us the solution. +prob1 :: [P1World] +prob1 = take 1 $ + p1worlds + `andthen` + nonunique (\w -> [p1_anne w]) -- Anne's statement 1 + `andthen` + nonunique (\w -> [p1_bill w]) -- Bill's statement + `andthen` + filter (\w -> p1_anne w == 2) -- Anne's statement 2 +-- Answer: +-- [(2,3)] +-- That is, Bill's number is 3. + + +-- | A variation of the problem: +-- Assuming the numbers don't exceed 100, what +-- are the numbers received by Anne and Bill? +-- Again, the possible worlds consistent with the statement of +-- the problem are the solutions. +prob1a :: [P1World] +prob1a = p1worlds + `andthen` + nonunique (\w -> [p1_anne w]) -- Anne's statement 1 + `andthen` + nonunique (\w -> [p1_bill w]) -- Bill's statement + `andthen` + unique (\w -> [p1_anne w]) (>100) -- Anne's statement 2 +-- Answer +-- [(1,2),(2,3),(100,99)] + +-- | Spelling out the `unique' condition, to demonstrate what it means +prob1a' :: [[P1World]] +prob1a' = p1worlds + `andthen` + nonunique (\w -> [p1_anne w]) -- Anne's statement 1 + `andthen` + nonunique (\w -> [p1_bill w]) -- Bill's statement + `andthen` + takeWhile (\w -> p1_anne w <= 100) + `andthen` + sortBy (\w1 w2 -> compare (p1_anne w1) (p1_anne w2)) + `andthen` + groupBy (\w1 w2 -> p1_anne w1 == p1_anne w2) + `andthen` + filter (\l -> length l == 1) +-- [[(1,2)],[(2,3)],[(100,99)]] + +-- ------------------------------------------------------------------------ +-- | Problem 2 +-- +-- Anne, Bill and Cath each have a positive natural number written on +-- their foreheads. They can only see the foreheads of others. +-- One of the numbers is the sum of the other two. All the previous +-- is common knowledge. The following truthful conversation takes place: +-- +-- > Anne: I don't know my number. +-- > Bill: I don't know my number. +-- > Cath: I don't know my number. +-- > Anne: I now know my number, and it is 50. +-- +-- What are the numbers of Bill and Cath? +-- Math Horizons, November 2004. Problem 182. +-- +-- A possible world for a problem 1: +-- numbers received by Anne, Bill, and Cath +type P2World = (Int,Int,Int) + +-- | The number on Anne's forehead in the world w +p2_anne :: P2World -> Int +p2_anne (x,_,_) = x + +-- | If Anne sees the number x on Bill's forehead and the +-- number y on Cath's forehead, what numbers could be +-- on Anne's forehead? +-- In other words, compute the set of possible worlds +-- that are indistinguishable from the world w as far as +-- Anne is concerned. +p2_anne_keys :: P2World -> [P2World] +p2_anne_keys (_,x,y) = [(abs (x-y),x,y),(x+y,x,y)] + +-- | The number on Bill's forehead in the world w +p2_bill :: P2World -> Int +p2_bill (_,x,_) = x + +-- | Which worlds Bill can't distinguish +p2_bill_keys :: P2World -> [P2World] +p2_bill_keys (x,_,y) = [(x,abs (x-y),y),(x,x+y,y)] + +-- | The number on Cath's forehead in the world w +p2_cath :: P2World -> Int +p2_cath (_,_,x) = x + +-- | Ditto for Cath +p2_cath_keys :: P2World -> [P2World] +p2_cath_keys (x,y,_) = [(x,y,abs (x-y)),(x,y,x+y)] + +-- | An initial stream of possible worlds for problem 2. +-- The code is naive but hopefully obviously correct +-- as it clearly corresponds to the statement of the problem. +p2worlds :: MonadPlus m => m P2World +p2worlds = do + sum <- iota 1 + summand1 <- choose [1..sum] + let summand2 = sum - summand1 + guard $ summand1 >= 1 && summand2 >= 1 + choose [(summand1,summand2,sum), + (sum,summand1,summand2), + (summand2,sum,summand1)] + + +-- | Encoding the statement of the problem: the conversation steps. +-- The remaining possible world gives us the solution. +prob2 :: [P2World] +prob2 = take 1 $ + p2worlds + `andthen` + nonunique p2_anne_keys -- Anne does not know her number + `andthen` + nonunique p2_bill_keys -- Neither does Bill his + `andthen` + nonunique p2_cath_keys -- or Cath her + `andthen` + unique p2_anne_keys (\(x,_,_) -> x > 200) -- Anne now knows her number + `andthen` + filter (\w -> p2_anne w == 50) +-- answer +-- [(50,20,30)] + + +-- ------------------------------------------------------------------------ +-- Utility functions + +-- | Reverse application +infixl 1 `andthen` +andthen = flip ($) + + +choose :: MonadPlus m => [a] -> m a +choose = foldr (mplus . return) mzero + +-- | A stream of naturals +nat :: MonadPlus m => m Int +nat = iota 0 + +-- | A stream of integers starting with n +iota :: MonadPlus m => Int -> m Int +iota n = return n `mplus` iota (succ n) + + + +-- | Filter a set of possible worlds +-- Given a proj function (yielding a set of keys for a world w), +-- return a stream of worlds that are not unique with +-- respect to their keys. That is, there are several +-- worlds with the same key. +-- Our state is a set of quarantined worlds. +-- When we receive a world whose key we have not seen, +-- we quarantine it. We release from the quarantine +-- when we encounter the same key again. +-- Our function is specialized to the List monad. In general, +-- we need MonadMinus (see the LogicT paper), of which List is an instance. +-- +nonunique :: Ord key => (w -> [key]) -> [w] -> [w] +nonunique proj worlds = loop M.empty worlds + where + loop quarantine [] = [] + loop quarantine (w:ws) = + decide quarantine w ws . + map (\key -> (key,M.lookup key quarantine)) $ + proj w + + -- we have not seen that key yet, quarantine + decide q w ws res@((k,_):rest) | all (\ (_,v)-> isNothing v) res = + let q' = M.insert k (Just w) q + q'' = foldr (\ (k,_) -> M.insert k Nothing) q' rest in + loop q'' ws + + -- we have seen a key, one or more times. + -- If a world has been quarantined, release it + decide q w ws res = + let released = foldr (\ (_,v) -> maybe id (maybe id (:)) v) [] res + q' = foldr (\ (k,v) -> maybe id (\_ -> M.insert k Nothing) v) q res + in released ++ w:(loop q' ws) + +isNothing Nothing = True +isNothing _ = False + +-- | Given a proj function (yielding a set of keys for a world w), +-- return a stream of worlds that are unique with +-- respect to their keys. That is, there is only one +-- world for the key. +-- We accept a termination criterion. +-- We terminate the stream once we have received the key +-- for which the criterion returns true. +-- When we receive a world whose key we have not seen, +-- we quarantine it. We release from the quarantine +-- when the stream is terminated. +-- +unique :: Ord key => (w -> [key]) -> (key -> Bool) -> [w] -> [w] +unique proj maxkey worlds = loop M.empty worlds + where + loop quarantine [] = M.fold (\x a -> maybe a (:a) x) [] quarantine + loop quarantine (w:ws) = + let keys = proj w in + if any maxkey keys then loop quarantine [] + else + decide quarantine w ws . + map (\key -> (key,M.lookup key quarantine)) $ keys + + -- we have not seen that key yet, quarantine + decide q w ws res@((k,_):rest) | all (\ (_,v)-> isNothing v) res = + let q' = M.insert k (Just w) q + q'' = foldr (\ (k,_) -> M.insert k Nothing) q' rest in + loop q'' ws + + -- we have seen a key, one or more times. Skip w + decide q w ws res = + let q' = foldr (\ (k,v) -> maybe id (\_ -> M.insert k Nothing) v) q res + in loop q' ws diff --git a/liboleg.cabal b/liboleg.cabal --- a/liboleg.cabal +++ b/liboleg.cabal @@ -1,5 +1,5 @@ name: liboleg -version: 2010.1.6.1 +version: 2010.1.7.0 license: BSD3 license-file: LICENSE author: Oleg Kiselyov @@ -7,7 +7,11 @@ homepage: http://okmij.org/ftp/ category: Text synopsis: An evolving collection of Oleg Kiselyov's Haskell modules -description: An evolving collection of Oleg Kiselyov's Haskell modules (released with his permission) +description: An evolving collection of Oleg Kiselyov's Haskell modules + (released with his permission) + . + See the original articles at + . build-type: Simple stability: experimental cabal-version: >= 1.2 @@ -31,14 +35,32 @@ Control.ShiftResetGenuine Control.VarStateM Control.ExtensibleDS + -- Control.Fix Control.Poly2 Control.StateAlgebra Codec.Image.Tiff + Lambda.CCG + Lambda.CFG1EN + Lambda.CFG1Sem + Lambda.CFG2EN + Lambda.CFG2Sem + Lambda.CFG3EN + Lambda.CFG3Sem + Lambda.CFG4 + Lambda.CFG + Lambda.CFGJ + Lambda.Dynamics + Lambda.QCFG + Lambda.QCFGJ + Lambda.QHCFG + Lambda.Semantics + Language.TypeLC Language.TypeFN + Language.DefinitionTree Language.TEval.EvalN Language.TEval.EvalTaglessF Language.TEval.EvalTaglessI @@ -61,6 +83,8 @@ Language.ToTDPE Language.Typ Language.TypeCheck + + Logic.DynEpistemology Text.PrintScan Text.PrintScanF