LogicalSemantics(doesn't compile, extension just for syntax highlighting).gf

-- all code by Aarne Ranta

abstract Logic = {
  cat
    Prop ; Ind ;
  data
    And, Or, If : Prop -> Prop -> Prop ;
    Not         : Prop -> Prop ;
    All, Exist  : (Ind -> Prop) -> Prop ; 
    Past        : Prop -> Prop ;
}

{- 
`Grammar' is the standard miniresource:
 http://www.grammaticalframework.org/gf-book/examples/chapter9/Grammar.gf

You can find the full Semantics.gf at 
 http://www.grammaticalframework.org/gf-book/examples/chapter9/Semantics.gf
 The following is not complete, just shows bits for the example.

Quotes from the GF book.
  "The Semantics module begins with declarations of the interpretation
  functions iC, one for each category C in Grammar. Each of these functions
  takes a tree of type C as its argument, and returns its denotation. 
  One-place verbs (V), adjectives (A), and common nouns (N) are interpreted as 
  one-place propositional functions (Ind -> Prop). [--] Noun phrases (NP) have
  the same type as quantifiers in Logic. This is what is needed to interpret 
  noun phrases like `every man' properly.  
  Determiners are naturally interpreted as functions from CN denotations
  to NP denotations. Their syntax always involves a domain, and this is
  encoded in Logic in the usual way by restricting the quantification
  with `And' in the existential case and `If' in the universal case."
-}

abstract Semantics = Grammar, Logic ** {
fun
  iCl    : Cl    -> Prop ;
  iNP    : NP    -> (Ind -> Prop) -> Prop ;
  iVP    : VP    -> Ind -> Prop ;
  iCN    : CN    -> Ind -> Prop ;
  iDet   : Det   -> (Ind -> Prop) -> (Ind -> Prop) -> Prop ;
  iN     : N     -> Ind -> Prop ;
  iV     : V     -> Ind -> Prop ;
def
  iCl (PredVP np vp)    = iNP np (iVP vp) ;
  iVP (ComplV2 v2 np) i = iNP np (iV2 v2 i) ;
  iVP (UseV v)        i = iV v i ;
  iNP (DetCN det cn)  f = iDet det (iCN cn) f ;
  iCN (UseN n)        i = iN n i ;
  
  iDet a_Det     d f = Exist (\x -> And (d x) (f x)) ;
  iDet every_Det d f = All (\x -> If (d x) (f x)) ;

{- Start by evaluating "every dog sleeps" as a clause. We get the AST 
 
   PredVP (DetCN every_Det (UseN dog_N)) (UseV sleep_V)
   
  Evaluate the AST with iCl.

            let np = DetCN every_Det (UseN dog_N)
                vp = UseV sleep_V
                
               iCl (PredVP np vp)
     iCl def.  iNP np (iVP vp) 
  <expand np>  iNP (DetCN every_Det (UseN dog_N)) (iVP vp)
     iNP def.  iDet every_Det (iCN (UseN dog_N)) (iVP vp)
  <expand vp>  iDet every_Det (iCN (UseN dog_N)) (iVP (UseV sleep_V))
iCN, iVP def.  iDet every_Det (iN dog_N) (iV sleep_V)
    iDet det.  All (\x -> If (iN dog_N x) (iV sleep_V x))
    
So we have translation between "every dog sleeps" and "∀x. dog(x) ⇒ sleeps(x)".

Just to show the `everyone' example, let's add person_N (and a denotation for it) 
and everyone_NP to our lexicon. Then we can just add a def rule for iNP with everyone_NP:
-}
def iNP everyone_NP f =  All (\x -> If (iN person_N x) (f x)) ;

}