{-# 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.
--
--
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