liboleg 2010.1.6.1 → 2010.1.7.0
raw patch · 4 files changed
+802/−2 lines, 4 files
Files
- Control/Fix.hs +103/−0
- Language/DefinitionTree.hs +383/−0
- Logic/DynEpistemology.hs +290/−0
- liboleg.cabal +26/−2
+ Control/Fix.hs view
@@ -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+--+-- <http://okmij.org/ftp/Computation/fixed-point-combinators.html#Self->+--+-- 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+
+ Language/DefinitionTree.hs view
@@ -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)+-}
+ Logic/DynEpistemology.hs view
@@ -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+-- <http://www.csc.liv.ac.uk/~wiebe/pubs/Documents/iccs.pdf>+--+-- Epistemic Puzzles+-- Hans van Ditmarsch+-- <http://www.cs.otago.ac.nz/staffpriv/hans/cosc462/logicpuzzlesB.pdf>+--+--+-- 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.+--+-- <http://okmij.org/ftp/Algorithms.html#dyn-epistemology>+--+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
liboleg.cabal view
@@ -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 <http://okmij.org/ftp/>+ . 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