Lambda.Dynamics

Philippe de Groote. 2010. Dynamic logic: a type-theoretic view. Talk slides at `Le modle et lalgorithme, Rocquencourt. http://www.inria.fr/rocquencourt/rendez-vous/modele-et-algo/dynamic-logic-a-type-theoretic-view

Documentation

type State = [Entity]

We extend the Lambda language with state (of the type State)

class Lambda lrepr => States lrepr where

Methods

update :: lrepr Entity -> lrepr State -> lrepr State

select :: lrepr State -> lrepr Entity

Instances

States C

States R

We correspondingly extend our R, C, P intrepreters of Lambda

States lrepr => States (P lrepr)

type family Dynamic a

data D c a

Constructors

D

Fields

unD :: c (Dynamic a)

Instances

States c => Lambda (D c)

States lrepr => Dynamics (D lrepr)

Show (Sem (D (P C)) S)

Show (Sem (D C) S)

Show (D (P C) Bool)

Show (D C Bool)

class Predicate a where

Methods

dynamic :: Lambda lrepr => (lrepr State -> lrepr a) -> lrepr (Dynamic a)

static :: Lambda lrepr => lrepr (Dynamic a) -> lrepr State -> lrepr a

Instances

Predicate Bool

Predicate a => Predicate (Entity -> a)

class Lambda lrepr => Dynamics lrepr where

Methods

it' :: lrepr ((Entity -> Bool) -> Bool)

Instances

Dynamics C

Dynamics lrepr => Dynamics (P lrepr)

States lrepr => Dynamics (D lrepr)

class Quantifier repr => Pronoun repr where

Methods

it_ :: repr QNP

Instances

Pronoun EN

Dynamics lrepr => Pronoun (Sem lrepr)