README

13/9/2011 by AR

Main files

  Types.gf     -- Martin-Löf's "Intuitionistic Type Theory" (book 1984)
  TypesSymb.gf -- concrete syntax close to the notation of the book

Experimental extension

  Donkey.gf    -- sentences about men and donkeys, with Montague semantics in Types
  DonkeyEng.gf -- quick and dirty English concrete syntax

Example 1: the formula for the "donkey sentence", 
"if a number is equal to a number, it is equal to it"
The parser restores implicit arguments, and linearizing the formula back returns it with
Greek letters (which could also be used in the input):
 
  > import TypesSymb.gf

  Types> p -tr -cat=Set "( Pi z : ( Sigma x : N ) ( Sigma y : N ) I ( N , x , y ) ) I ( N , p ( z ) , p ( q ( z ) ) )" | l -unlexcode

  Pi 
    (Sigma Nat (\x -> 
      Sigma Nat (\y -> Id Nat x y))) 
    (\z -> 
      Id Nat 
        (p {Nat} {\_1 -> Sigma Nat (\v2 -> Id Nat _1 v2)} 
           z) 
        (p {Nat} {\_1 -> Id Nat (p Nat (\v2 -> Sigma Nat (\v3 -> Id Nat v2 v3)) z) _1} (
           q {Nat} {\_1 -> Sigma Nat (\v2 -> Id Nat _1 v2)} 
             z)))

  (Π z : (Σ x : N)(Σ y : N)I (N , x , y))I (N , p (z), p (q (z)))


Example 2: parse and interpret a sentence, also showing the nice formula.

  > import DonkeyEng.gf

  Donkey> p -cat=S -tr "a man owns a donkey " | pt -transfer=iS -tr | l -unlexcode

  PredVP {Man'} (An Man) (ComplV2 {Man'} {Donkey'} Own (An Donkey))

  Sigma Man' (\v0 -> Sigma Donkey' (\v1 -> Own' v0 v1))

  (Σ v0 : man')(Σ v1 : donkey')own' (v0 , v1)


Example 3: (to be revisited) parse of "the donkey sentence" returns some metavariables

  Donkey> dc interpret p ?0 | pt -transfer=iS | l -unlexcode

  Donkey> %interpret "if a man owns a donkey he beats it"

  (Π v0 : (Σ v0 : man')(Σ v1 : donkey')own' (v0 , v1))beat' (?16 , ?22)