{-# OPTIONS -W #-} {-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-} {-# LANGUAGE NoMonomorphismRestriction #-} -- | Philippe de Groote. 2010. Dynamic logic: a type-theoretic view. -- Talk slides at `Le modÃ¨le et l'algorithme', Rocquencourt. -- <http://www.inria.fr/rocquencourt/rendez-vous/modele-et-algo/dynamic-logic-a-type-theoretic-view> -- module Lambda.Dynamics where import Lambda.Semantics import Lambda.CFG import Lambda.QCFG -- | We extend the Lambda language with state (of the type State) type State = [Entity] class (Lambda lrepr) => States lrepr where update :: lrepr Entity -> lrepr State -> lrepr State select :: lrepr State -> lrepr Entity -- | We correspondingly extend our R, C, P intrepreters of Lambda instance States R where update (R x) (R e) = R (x:e) select (R (x:_)) = R x select (R []) = error "who?" instance States C where update (C x) (C e) = C (\i p -> paren (p > 5) (x i 6 ++ "::" ++ e i 5)) select (C e) = C (\i p -> paren (p > 10) ("sel " ++ e i 11)) instance (States lrepr) => States (P lrepr) where update (P x _) (P e _) = unknown (update x e) select (P e _) = unknown (select e) type family Dynamic (a :: *) type instance Dynamic (a -> b) = Dynamic a -> Dynamic b type instance Dynamic Entity = Entity type instance Dynamic Bool = State -> (State -> Bool) -> Bool data D c a = D { unD :: c (Dynamic a) } instance (States c) => Lambda (D c) where app (D f) (D x) = D (app f x) lam f = D (lam (\x -> unD (f (D x)))) john' = D john' mary' = D mary' like' = D (dynamic (\_ -> like')) own' = D (dynamic (\_ -> own')) farmer' = D (dynamic (\_ -> farmer')) donkey' = D (dynamic (\_ -> donkey')) true = D (dynamic (\_ -> true)) neg (D x) = D (dynamic (\e -> neg (static x e))) conj (D x) (D y) = D (lam (\e -> lam (\phi -> app (app x e) (lam (\e -> app (app y e) phi))))) exists = D (lam (\p -> lam (\e -> lam (\phi -> app exists (lam (\x -> app (app (app p x) (update x e)) phi)))))) instance Show (Sem (D C) S) where show = show . unSem instance Show (Sem (D (P C)) S) where show = show . unSem instance Show (D C Bool) where show (D x) = show x instance Show (D (P C) Bool) where show (D x) = show x class Predicate a where dynamic :: (Lambda lrepr) => (lrepr State -> lrepr a) -> lrepr (Dynamic a) static :: (Lambda lrepr) => lrepr (Dynamic a) -> lrepr State -> lrepr a instance Predicate Bool where dynamic f = lam (\e -> lam (\phi -> conj (f e) (app phi e))) static x e = app (app x e) (lam (\_ -> true)) instance (Predicate a) => Predicate (Entity -> a) where dynamic f = lam (\o -> dynamic (\e -> app (f e) o)) static x e = lam (\o -> static (app x o) e) class (Lambda lrepr) => Dynamics lrepr where it' :: lrepr ((Entity -> Bool) -> Bool) instance (States lrepr) => Dynamics (D lrepr) where it' = D (lam (\p -> lam (\e -> lam (\phi -> app (app (app p (select e)) e) phi)))) instance Dynamics C where it' = C (\_ _ -> "it") instance (Dynamics lrepr) => Dynamics (P lrepr) where it' = unknown it' class (Quantifier repr) => Pronoun repr where it_ :: repr QNP instance Pronoun EN where it_ = EN "it" instance (Dynamics lrepr) => Pronoun (Sem lrepr) where it_ = Sem it' sentence = r4 (every (who (r5 own (a donkey)) farmer)) (r5 like it_) sentence_en = sentence :: EN S sentence_sem = sentence :: Sem (D C) S sentence_semp = sentence :: Sem (D (P C)) S