Lambda.Semantics
- data Entity
- class Lambda lrepr where
- john' :: lrepr Entity
- mary' :: lrepr Entity
- like' :: lrepr (Entity -> Entity -> Bool)
- own' :: lrepr (Entity -> Entity -> Bool)
- farmer' :: lrepr (Entity -> Bool)
- donkey' :: lrepr (Entity -> Bool)
- true :: lrepr Bool
- neg :: lrepr Bool -> lrepr Bool
- conj :: lrepr Bool -> lrepr Bool -> lrepr Bool
- exists :: lrepr ((Entity -> Bool) -> Bool)
- app :: lrepr (a -> b) -> lrepr a -> lrepr b
- lam :: (lrepr a -> lrepr b) -> lrepr (a -> b)
- data R a = R {
- unR :: a
- data C a = C {}
- type family Known lrepr a
- data P lrepr a = P {}
Documentation
Here we encode the target language, the language to express denotations (or, meanings) Following Montague, our language for denotations is essentially Church's Simple Theory of Types also known as simply-typed lambda-calculus It is a form of a higher-order predicate logic.
class Lambda lrepr whereSource
We define the grammar of the target language the same way we have defined the grammar for (source) fragment
Methods
like' :: lrepr (Entity -> Entity -> Bool)Source
own' :: lrepr (Entity -> Entity -> Bool)Source
farmer' :: lrepr (Entity -> Bool)Source
donkey' :: lrepr (Entity -> Bool)Source
neg :: lrepr Bool -> lrepr BoolSource
conj :: lrepr Bool -> lrepr Bool -> lrepr BoolSource
exists :: lrepr ((Entity -> Bool) -> Bool)Source
Syntactic sugar
The first interpretation: evaluating in the world with John, Mary, and Bool as truth values. Lambda functions are interpreted as Haskell functions and Lambda applications are interpreted as Haskell applications. The interpreter R is metacircular (and so, efficient).
Running the examples
We now interpret Lambda terms as Strings, so we can show our formulas. Actually, not quite strings: we need a bit of _context_: the precedence and the number of variables already bound in the context. The latter number lets us generate unique variable names.
type family Known lrepr a Source
We can now see the examples
The displayed difference between lsen4 and lsen4' shows that beta-redices have been reduced. NBE.
Normalizing the terms: performing the apparent redices