further work on tutorial

1 files changed, 392 insertions, 417 deletions

diff --git a/doc/tutorial/gf-tutorial2.txt b/doc/tutorial/gf-tutorial2.txt
index 4b20f38cd..9c3ae71b2 100644
--- a/doc/tutorial/gf-tutorial2.txt
+++ b/doc/tutorial/gf-tutorial2.txt
@@ -1,5 +1,5 @@
 Grammatical Framework Tutorial
-Author: Aarne Ranta <aarne (at) cs.chalmers.se>
+Author: Aarne Ranta aarne (at) cs.chalmers.se
 Last update: %%date(%c)
 
 % NOTE: this is a txt2tags file.
@@ -20,7 +20,7 @@ Last update: %%date(%c)
 
 
 
-[../gf-logo.gif]
+[../gf-logo.png]
 
 
 
@@ -552,7 +552,7 @@ module forms are
 
 
 %--!
-===Record types, records, and ``Str``s===
+===Records and strings===
 
 The linearization type of a category is a **record type**, with
 zero of more **fields** of different types. The simplest record
@@ -922,7 +922,7 @@ The graph uses
 
 
 %--!
-==System commands==
+===System commands===
 
 To document your grammar, you may want to print the
 graph into a file, e.g. a ``.png`` file that
@@ -1385,7 +1385,8 @@ Why does the command also show the operations that form
 the same as the value of ``Noun``.
 
 
-==Using morphology in concrete syntax==
+
+==Using parameters in concrete syntax==
 
 We can now enrich the concrete syntax definitions to
 comprise morphology. This will involve a more radical
@@ -1596,8 +1597,246 @@ of a grammar application.
 
 
 %--!
+===Free variation===
+
+Sometimes there are many alternative ways to define a concrete syntax.
+For instance, the verb negation in English can be expressed both by
+//does not// and //doesn't//. In linguistic terms, these expressions
+are in **free variation**. The ``variants`` construct of GF can
+be used to give a list of strings in free variation. For example,
+```
+  NegVerb verb = {s = variants {["does not"] ; "doesn't} ++ verb.s ! Pl} ;
+```
+An empty variant list
+```
+  variants {}
+```
+can be used e.g. if a word lacks a certain form.
+
+In general, ``variants`` should be used cautiously. It is not
+recommended for modules aimed to be libraries, because the
+user of the library has no way to choose among the variants.
+
+
+===Overloading of operations===
+
+Large libraries, such as the GF Resource Grammar Library, may define 
+hundreds of names, which can be unpractical
+for both the library writer and the user. The writer has to invent longer 
+and longer names which are not always intuitive,
+and the user has to learn or at least be able to find all these names. 
+A solution to this problem, adopted by languages such as C++, is **overloading**:
+the same name can be used for several functions. When such a name is used, the
+compiler performs **overload resolution** to find out which of the possible functions
+is meant. The resolution is based on the types of the functions: all functions that
+have the same name must have different types.
+
+In C++, functions with the same name can be scattered everywhere in the program.
+In GF, they must be grouped together in ``overload`` groups. Here is an example
+of an overload group, defining four ways to define nouns in Italian:
+```
+  oper mkN = overload {
+    mkN : Str -> N                  = -- regular nouns
+    mkN : Str -> Gender -> N        = -- regular nouns with unexpected gender
+    mkN : Str -> Str -> N           = -- irregular nouns
+    mkN : Str -> Str -> Gender -> N = -- irregular nouns with unexpected gender
+  }
+```
+All of the following uses of ``mkN`` are easy to resolve:
+```
+  lin Pizza = mkN "pizza" ;         -- Str -> N
+  lin Hand  = mkN "mano" Fem ;      -- Str -> Gender -> N
+  lin Man   = mkN "uomo" "uomini" ; -- Str -> Str -> N
+```
+
+
+
+
+
+
+
+%--!
+==Using the resource grammar library TODO==
+
+A resource grammar is a grammar built on linguistic grounds,
+to describe a language rather than a domain.
+The GF resource grammar library, which contains resource grammars for
+10 languages, is described more closely in the following
+documents:
+- [Resource library API documentation ../../lib/resource-1.0/doc/]:
+  for application grammarians using the resource.
+- [Resource writing HOWTO ../../lib/resource-1.0/doc/Resource-HOWTO.html]:
+  for resource grammarians developing the resource.
+
+
+===Interfaces, instances, and functors===
+
+===The simplest way===
+
+The simplest way is to ``open`` a top-level ``Lang`` module
+and a ``Paradigms`` module: 
+```
+  abstract Foo = ...
+
+  concrete FooEng = open LangEng, ParadigmsEng in ...
+  concrete FooSwe = open LangSwe, ParadigmsSwe in ...
+```
+Here is an example.
+```
+abstract Arithm = {
+  cat
+    Prop ;
+    Nat ;
+  fun
+    Zero : Nat ;
+    Succ : Nat -> Nat ;
+    Even : Nat -> Prop ;
+    And  : Prop -> Prop -> Prop ;
+}
+
+--# -path=.:alltenses:prelude
+
+concrete ArithmEng of Arithm = open LangEng, ParadigmsEng in {
+  lincat
+    Prop = S ;
+    Nat  = NP ;
+  lin
+    Zero = 
+      UsePN (regPN "zero" nonhuman) ;
+    Succ n = 
+      DetCN (DetSg (SgQuant DefArt) NoOrd) (ComplN2 (regN2 "successor") n) ;
+    Even n = 
+      UseCl TPres ASimul PPos 
+        (PredVP n (UseComp (CompAP (PositA (regA "even"))))) ;
+    And x y = 
+      ConjS and_Conj (BaseS x y) ;
+
+}
+
+--# -path=.:alltenses:prelude
+
+concrete ArithmSwe of Arithm = open LangSwe, ParadigmsSwe in {
+  lincat
+    Prop = S ;
+    Nat  = NP ;
+  lin
+    Zero = 
+      UsePN (regPN "noll" neutrum) ;
+    Succ n = 
+      DetCN (DetSg (SgQuant DefArt) NoOrd) 
+        (ComplN2 (mkN2 (mk2N "efterföljare" "efterföljare") 
+           (mkPreposition "till")) n) ;
+    Even n = 
+      UseCl TPres ASimul PPos 
+        (PredVP n (UseComp (CompAP (PositA (regA "jämn"))))) ;
+    And x y = 
+      ConjS and_Conj (BaseS x y) ;
+}
+```
+
+
+===How to find resource functions===
+
+The definitions in this example were found by parsing:
+```
+  > i LangEng.gf
+
+  -- for Successor:
+  > p -cat=NP -mcfg -parser=topdown "the mother of Paris"
+
+  -- for Even:
+  > p -cat=S -mcfg -parser=topdown "Paris is old"
+
+  -- for And:
+  > p -cat=S -mcfg -parser=topdown "Paris is old and I am old"
+```
+The use of parsing can be systematized by **example-based grammar writing**,
+to which we will return later. 
+
+
+===A functor implementation===
+
+The interesting thing now is that the
+code in ``ArithmSwe`` is similar to the code in ``ArithmEng``, except for
+some lexical items ("noll" vs. "zero", "efterföljare" vs. "successor",
+"jämn" vs. "even").  How can we exploit the similarities and
+actually share code between the languages?
+
+The solution is to use a functor: an ``incomplete`` module that opens
+an ``abstract`` as an ``interface``, and then instantiate it to different
+languages that implement the interface. The structure is as follows:
+```
+  abstract Foo ...
+
+  incomplete concrete FooI = open Lang, Lex in ...
+
+  concrete FooEng of Foo = FooI with (Lang=LangEng), (Lex=LexEng) ;
+  concrete FooSwe of Foo = FooI with (Lang=LangSwe), (Lex=LexSwe) ;
+```
+where ``Lex`` is an abstract lexicon that includes the vocabulary
+specific to this application:
+```
+  abstract Lex = Cat ** ...
+
+  concrete LexEng of Lex = CatEng ** open ParadigmsEng in ...
+  concrete LexSwe of Lex = CatSwe ** open ParadigmsSwe in ...  
+```
+Here, again, a complete example (``abstract Arithm`` is as above):
+```
+incomplete concrete ArithmI of Arithm = open Lang, Lex in {
+  lincat
+    Prop = S ;
+    Nat  = NP ;
+  lin
+    Zero = 
+      UsePN zero_PN ;
+    Succ n = 
+      DetCN (DetSg (SgQuant DefArt) NoOrd) (ComplN2 successor_N2 n) ;
+    Even n = 
+      UseCl TPres ASimul PPos 
+        (PredVP n (UseComp (CompAP (PositA even_A)))) ;
+    And x y = 
+      ConjS and_Conj (BaseS x y) ;
+}
+
+--# -path=.:alltenses:prelude
+concrete ArithmEng of Arithm = ArithmI with
+  (Lang = LangEng),
+  (Lex = LexEng) ;
+
+--# -path=.:alltenses:prelude
+concrete ArithmSwe of Arithm = ArithmI with
+  (Lang = LangSwe),
+  (Lex = LexSwe) ;
+
+abstract Lex = Cat ** {
+  fun
+    zero_PN : PN ;
+    successor_N2 : N2 ;  
+    even_A : A ;
+}
+
+concrete LexSwe of Lex = CatSwe ** open ParadigmsSwe in {
+  lin 
+    zero_PN = regPN "noll" neutrum ;
+    successor_N2 = 
+      mkN2 (mk2N "efterföljare" "efterföljare") (mkPreposition "till") ;
+    even_A = regA "jämn" ;
+}
+```
+
+===Restricted inheritance and qualified opening===
+
+
+
+
+%--!
 ==More constructs for concrete syntax==
 
+In this chapter, we go through constructs that are not necessary in simple grammars
+or when the concrete syntax relies on libraries, but very useful when writing advanced
+concrete syntax implementations, such as resource grammar libraries.
+
 
 %--!
 ===Local definitions===
@@ -1621,48 +1860,6 @@ the same expression. Here is an example, from
 ```
 
 
-
-
-%--!
-===Free variation===
-
-Sometimes there are many alternative ways to define a concrete syntax.
-For instance, the verb negation in English can be expressed both by
-//does not// and //doesn't//. In linguistic terms, these expressions
-are in **free variation**. The ``variants`` construct of GF can
-be used to give a list of strings in free variation. For example,
-```
-  NegVerb verb = {s = variants {["does not"] ; "doesn't} ++ verb.s ! Pl} ;
-```
-An empty variant list
-```
-  variants {}
-```
-can be used e.g. if a word lacks a certain form.
-
-In general, ``variants`` should be used cautiously. It is not
-recommended for modules aimed to be libraries, because the
-user of the library has no way to choose among the variants.
-
-%Moreover, ``variants`` is only defined for basic types (``Str``
-%and parameter types). The grammar compiler will admit
-%``variants`` for any types, but it will push it to the
-%level of basic types in a way that may be unwanted.
-%For instance, German has two words meaning "car", 
-%//Wagen//, which is Masculine, and //Auto//, which is Neuter.
-%However, if one writes
-%```
-%  variants {{s = "Wagen" ; g = Masc} ; {s = "Auto" ; g = Neutr}}
-%```
-%this will compute to
-%```
-%  {s = variants {"Wagen" ; "Auto"} ; g = variants {Masc ; Neutr}}
-%```
-%which will also accept erroneous combinations of strings and genders.
-
-
-
-
 ===Record extension and subtyping===
 
 Record types and records can be **extended** with new fields. For instance,
@@ -1707,7 +1904,7 @@ A typical example is a record of agreement features, e.g. French
   oper Agr : PType = {g : Gender ; n : Number ; p : Person} ;
 ```
 Notice the term ``PType`` rather than just ``Type`` referring to
-parameter types. Every ``PType`` is also a ``Type``.
+parameter types. Every ``PType`` is also a ``Type``, but not vice-versa.
 
 Pattern matching is done in the expected way, but it can moreover
 utilize partial records: the branch
@@ -1728,6 +1925,7 @@ possible to write, slightly surprisingly,
     }
 ```
 
+
 %--!
 ===Regular expression patterns===
 
@@ -1742,8 +1940,22 @@ as in morphology, it is handy to use regular expression patterns:
 
 
 The last three apply to all types of patterns, the first two only to token strings.
-Example: plural formation in Swedish 2nd declension
-(//pojke-pojkar, nyckel-nycklar, seger-segrar, bil-bilar//):
+As an example, we give a rule for the formation of English word forms
+ending with an //s// and used in the formation of both plural nouns and
+third-person present-tense verbs.
+```
+  add_s : Str -> Str = \w -> case w of {
+    _ + "oo"                           => s + "s" ;   -- bamboo
+    _ + ("s" | "z" | "x" | "sh" | "o") => w + "es" ;  -- bus, hero
+    _ + ("a" | "o" | "u" | "e") + "y"  => w + "s" ;   -- boy
+    x + "y"                            => x + "ies" ; -- fly
+    _                                  => w + "s"     -- car
+    } ;
+```
+Here is another example, the plural formation in Swedish 2nd declension.
+The second branch uses a variable binding with ``@`` to cover the cases where an
+unstressed pre-final vowel //e// disappears in the plural
+(//nyckel-nycklar, seger-segrar, bil-bilar//):
 ```
   plural2 : Str -> Str = \w -> case w of {
     pojk + "e"                       => pojk + "ar" ;
@@ -1751,15 +1963,8 @@ Example: plural formation in Swedish 2nd declension
     bil                              => bil + "ar"
     } ;
 ```
-Another example: English noun plural formation.
-```
-  plural : Str -> Str = \w -> case w of {
-    _ + ("s" | "z" | "x" | "sh")      => w + "es" ;
-    _ + ("a" | "o" | "u" | "e") + "y" => w + "s" ;
-    x + "y"                           => x + "ies" ;
-    _                                 => w + "s"
-    } ;
-```
+
+
 Semantics: variables are always bound to the **first match**, which is the first
 in the sequence of binding lists ``Match p v`` defined as follows. In the definition,
 ``p`` is a pattern and ``v`` is a value.
@@ -1834,8 +2039,15 @@ FIXME: The linearization type is ``{s : Str}`` for all these categories.
 
 
 
+
 ==More concepts of abstract syntax==
 
+This section is about the use of the type theory part of GF for 
+including more semantics in grammars. Some of the subsections present
+ideas that have not yet been used in real-world applications, and whose
+tool support outside the GF program is not complete.
+
+
 ===GF as a logical framework===
 
 In this section, we will show how 
@@ -1852,8 +2064,8 @@ of such a theory, represented as an ``abstract`` module in GF.
 ```
 abstract Arithm = {
   cat
-    Prop ;    -- proposition
-    Nat ;     -- natural number
+    Prop ;                        -- proposition
+    Nat ;                         -- natural number
   fun
     Zero : Nat ;                  -- 0
     Succ : Nat -> Nat ;           -- successor of x
@@ -1899,11 +2111,9 @@ abstract Address = {
     OxfordSt, ShaftesburyAve, BdRaspail, RueBlondel, AvAlsaceLorraine : Street ;
   }
 ```
-The linearization rules
-are straightforward,
+The linearization rules are straightforward,
 ```
   lin
-
     mkAddress country city street = 
       ss (street.s ++ "," ++ city.s ++ "," ++ country.s) ;
     UK = ss ("U.K.") ;
@@ -1917,13 +2127,11 @@ are straightforward,
     RueBlondel = ss ("rue" ++ "Blondel") ;
     AvAlsaceLorraine = ss ("avenue" ++ "Alsace-Lorraine") ;
 ```
-with the exception of ``mkAddress``, where we have
+Notice that, in ``mkAddress``, we have
 reversed the order of the constituents. The type of ``mkAddress``
 in the abstract syntax takes its arguments in a "logical" order,
-with increasing precision. (This order is sometimes even used in the concrete
-syntax of addresses, e.g. in Russia).
-
-
+with increasing precision. (This order is sometimes even used in the 
+concrete syntax of addresses, e.g. in Russia).
 
 Both existing and non-existing addresses are recognized by this
 grammar. The non-existing ones in the following randomly generated
@@ -1943,10 +2151,11 @@ Dependent types provide a way to guarantee that addresses are
 well-formed. What we do is to include **contexts** in
 ``cat`` judgements:
 ```
-  cat Address ; 
-  cat Country ; 
-  cat City Country ; 
-  cat Street (x : Country)(y : City x) ;
+  cat 
+    Address ; 
+    Country ; 
+    City Country ; 
+    Street (x : Country)(City x) ;
 ```
 The first two judgements are as before, but the third one makes
 ``City`` dependent on ``Country``: there are no longer just cities,
@@ -1966,19 +2175,18 @@ which is only possible if the subsequent context does not depend on ``x``.
 The ``fun`` judgements of the grammar are modified accordingly:
 ```
   fun
+    mkAddress : (x : Country) -> (y : City x) -> Street x y -> Address ;
   
-  mkAddress : (x : Country) -> (y : City x) -> Street x y -> Address ;
-  
-  UK : Country ;
-  France : Country ;
-  Paris : City France ; 
-  London : City UK ; 
-  Grenoble : City France ;
-  OxfordSt : Street UK London ; 
-  ShaftesburyAve : Street UK London ;
-  BdRaspail : Street France Paris ; 
-  RueBlondel : Street France Paris ; 
-  AvAlsaceLorraine : Street France Grenoble ;
+    UK : Country ;
+    France : Country ;
+    Paris : City France ; 
+    London : City UK ; 
+    Grenoble : City France ;
+    OxfordSt : Street UK London ; 
+    ShaftesburyAve : Street UK London ;
+    BdRaspail : Street France Paris ; 
+    RueBlondel : Street France Paris ; 
+    AvAlsaceLorraine : Street France Grenoble ;
 ```
 Since the type of ``mkAddress`` now has dependencies among
 its argument types, we have to use variables just like we used in
@@ -2012,6 +2220,12 @@ sometimes shortens the code, since we can write e.g.
 ```
   oper triple : (x,y,z : Str) -> Str = ...
 ```
+If a bound variable is not used, it can here, as elswhere in GF, be replaced by
+a wildcard:
+```
+  oper triple : (_,_,_ : Str) -> Str = ...
+```
+
 
 
 ===Dependent types in concrete syntax===
@@ -2074,8 +2288,8 @@ For instance, the sentence
 is syntactically well-formed but semantically ill-formed.
 It is well-formed because it combines a well-formed
 noun phrase ("the number 2") with a well-formed
-verb phrase ("is equilateral") in accordance with the
-rule that the verb phrase is inflected in the
+verb phrase ("is equilateral") and satisfies the agreement 
+rule saying that the verb phrase is inflected in the
 number of the noun phrase:
 ```
   fun PredVP : NP -> VP -> S ;
@@ -2117,6 +2331,7 @@ but no proposition linearized to
   the number 2 is equilateral
 ```
 since ``Equilateral two`` is not a well-formed type-theoretical object.
+It is not even accepted by the context-free parser.
 
 When formalizing mathematics, e.g. in the purpose of
 computer-assisted theorem proving, we are certainly interested
@@ -2147,70 +2362,32 @@ and dependencies of other categories on this:
 ```
   cat 
     S ;            -- sentence
-    V1 Dom ;       -- one-place verb
-    V2 Dom Dom ;   -- two-place verb
+    V1 Dom ;       -- one-place verb with specific subject type
+    V2 Dom Dom ;   -- two-place verb with specific subject and object types
     A1 Dom ;       -- one-place adjective
     A2 Dom Dom ;   -- two-place adjective
-    PN Dom ;       -- proper name
-    NP Dom ;       -- noun phrase
+    NP Dom ;       -- noun phrase for an object of specific type
     Conj ;         -- conjunction
     Det ;          -- determiner
 ```
-The number of ``Dom`` arguments depends on the semantic type
-corresponding to the category: one-place verbs and adjectives
-correspond to types of the form
-```
-  A -> Prop
-```
-whereas two-place verbs and adjectives correspond to types of the form
-```
-  A -> B -> Prop
-```
-where the domains ``A`` and ``B`` can be distinct.
-Proper names correspond to types of the form
-```
-  A
-```
-that is, individual objects of the domain ``A``. Noun phrases
-correspond to
-```
-  (A -> Prop) -> Prop
-```
-that is, **quantifiers** over the domain ``A``.
-Sentences, conjunctions, and determiners correspond to
-```
-  Prop
-  Prop -> Prop -> Prop
-  (A : Dom) -> (A -> Prop) -> Prop
-```
-respectively,
-and are thus independent of domain. As for common nouns ``CN``,
-the simplest semantics is that they correspond to
-```
-  Dom
-```
-In this section, we will, in fact, write ``Dom`` instead of ``CN``. 
-
 Having thus parametrized categories on domains, we have to reformulate
 the rules of predication, etc, accordingly. This is straightforward:
 ```
   fun
     PredV1  : (A   : Dom) -> NP A -> V1 A -> S ;
     ComplV2 : (A,B : Dom) -> V2 A B -> NP B -> V1 A ;
-    UsePN   : (A   : Dom) -> PN A -> NP A ;
     DetCN   :                Det -> (A : Dom) -> NP A ;
     ModA1   :                (A : Dom) -> A1 A -> Dom ;
     ConjS   :                Conj -> S -> S -> S ;
     ConjV1  : (A   : Dom) -> Conj -> V1 A -> V1 A -> V1 A ;
 ```
 In linearization rules,
-we typically use wildcards for the domain arguments,
-to get arities right:
+we use wildcards for the domain arguments,
+because they don't affect linearization:
 ```
   lin
     PredV1 _ np vp = ss (np.s ++ vp.s) ;
     ComplV2 _ _ v2 np = ss (v2.s ++ np.s) ;
-    UsePN _ pn = pn ;
     DetCN det cn = ss (det.s ++ cn.s) ;
     ModA1 cn a1 = ss (a1.s ++ cn.s) ;
     ConjS conj s1 s2 = ss (s1.s ++ conj.s ++ s2.s) ;
@@ -2232,20 +2409,19 @@ To explain the contrast, we introduce the functions
   human : Dom ; 
   game : Dom ;
   play : V2 human game ;
-  John : PN human ;
-  Golf : PN game ;
+  John : NP human ;
+  Golf : NP game ;
 ```
 Both sentences still pass the context-free parser,
 returning trees with lots of metavariables of type ``Dom``:
 ```
-  PredV1 ?0 (UsePN ?1 John) (ComplV2 ?2 ?3 play (UsePN ?4 Golf))
-
-  PredV1 ?0 (UsePN ?1 Golf) (ComplV2 ?2 ?3 play (UsePN ?4 John))
+  PredV1 ?0 John (ComplV2 ?1 ?2 play Golf)
+  PredV1 ?0 Golf (ComplV2 ?1 ?2 play John)
 ```
 But only the former sentence passes the type checker, which moreover
 infers the domain arguments:
 ```
-  PredV1 human (UsePN human John) (ComplV2 human game play (UsePN game Golf))
+  PredV1 human John (ComplV2 human game play Golf)
 ```
 To try this out in GF, use ``pt = put_term`` with the **tree transformation**
 that solves the metavariables by type checking:
@@ -2261,7 +2437,7 @@ or less liberal. For instance,
   John loves Mary
   John loves golf
 ```
-both make sense, even though ``Mary`` and ``golf``
+should both make sense, even though ``Mary`` and ``golf``
 are of different types. A natural solution in this case is to
 formalize ``love`` as a **polymorphic** verb, which takes
 a human as its first argument but an object of any type as its second
@@ -2270,19 +2446,21 @@ argument:
   fun love : (A : Dom) -> V2 human A ;
   lin love _ = ss "loves" ;
 ```
-Problems remain, such as **subtyping** (e.g. what
-is meaningful for a ``human`` is also meaningful for
-a ``man`` and a ``woman``, but not the other way round)
-and the **extended use** of expressions (e.g. a metaphoric use that
-makes sense of "golf plays John"). 
+In other words, it is possible for a human to love anything.
 
+A problem related to polymorphism is **subtyping**: what
+is meaningful for a ``human`` is also meaningful for
+a ``man`` and a ``woman``, but not the other way round.
+One solution to this is **coercions**: functions that
+"lift" objects from subtypes to supertypes.
 
 
+===Case study: selectional restrictions and statistical language models TODO===
 
 
 ===Proof objects===
 
-Perhaps the most well-known feature of constructive type theory is
+Perhaps the most well-known idea in constructive type theory is
 the **Curry-Howard isomorphism**, also known as the
 **propositions as types principle**. Its earliest formulations
 were attempts to give semantics to the logical systems of
@@ -2300,14 +2478,14 @@ natural numbers:
 The **successor function** ``Succ`` generates an infinite
 sequence of natural numbers, beginning from ``Zero``.
 
-We then define what it means for a number //x// to be less than
+We then define what it means for a number //x// to be //less than//
 a number //y//. Our definition is based on two axioms:
-- ``Zero`` is less than ``Succ y`` for any ``y``.
-- If ``x`` is less than ``y``, then``Succ x`` is less than ``Succ y``.
+- ``Zero`` is less than ``Succ`` //y// for any //y//.
+- If //x// is less than //y//, then``Succ`` //x// is less than ``Succ`` //y//.
 
 
 The most straightforward way of expressing these axioms in type theory
-is as typing judgements that introduce objects of a type ``Less x y``:
+is as typing judgements that introduce objects of a type ``Less`` //x y //:
 ```
   cat Less Nat Nat ; 
   fun lessZ : (y : Nat) -> Less Zero (Succ y) ;
@@ -2326,14 +2504,13 @@ whose type is
 ```
   Less (Succ (Succ Zero)) (Succ (Succ (Succ (Succ Zero))))
 ```
-which is the same thing as the proposition that 2 is less than 4.
+which is the formalization of the proposition that 2 is less than 4.
 
 GF grammars can be used to provide a **semantic control** of
 well-formedness of expressions. We have already seen examples of this:
 the grammar of well-formed addresses and the grammar with
 selectional restrictions above. By introducing proof objects
-we have now added a very powerful
-technique of expressing semantic conditions.
+we have now added a very powerful technique of expressing semantic conditions.
 
 A simple example of the use of proof objects is the definition of
 well-formed //time spans//: a time span is expected to be from an earlier to
@@ -2351,7 +2528,35 @@ by using the ``Less`` predicate:
   cat Span ;
   fun span : (m,n : Nat) -> Less m n -> Span ;
 ```
+A possible practical application of this idea is **proof-carrying documents**:
+to be semantically well-formed, the abstract syntax of a document must contain a proof
+of some property, although the proof is not shown in the concrete document.
+Think, for instance, of small documents describing flight connections:
 
+//To fly from Gothenburg to Prague, first take LH3043 to Frankfurt, then OK0537 to Prague.//
+
+The well-formedness of this text is partly expressible by dependent typing: 
+```
+  cat
+    City ;
+    Flight City City ;
+  fun
+    Gothenburg, Frankfurt, Prague : City ;
+    LH3043 : Flight Gothenburg Frankfurt ;
+    OK0537 : Flight Frankfurt Prague ;
+```
+This rules out texts saying //take OK0537 from Gothenburg to Prague//. However, there is a
+further condition saying that it must be possible to change from LH3043 to OK0537 in Frankfurt.
+This can be modelled as a proof object of a suitable type, which is required by the constructor
+that connects flights.
+```
+  cat
+    IsPossible (x,y,z : City)(Flight x y)(Flight y z) ;
+  fun
+    Connect : (x,y,z : City) -> 
+      (u : Flight x y) -> (v : Flight y z) -> 
+        IsPossible x y z u v -> Flight x z ;
+```
 
 
 
@@ -2364,8 +2569,8 @@ a universally quantifier proposition
   (All x)B(x)
 ```
 consists of the **binding** ``(All x)`` of the variable ``x``,
-and the **body** ``B(x)``, where the variable ``x`` is
-said to occur bound. 
+and the **body** ``B(x)``, where the variable ``x`` can have
+**bound occurrences**. 
 
 Variable bindings appear in informal mathematical language as well, for
 instance,
@@ -2433,7 +2638,6 @@ since the linearization type of ``Prop`` is
 ```
   {s : Str}
 ```
-(we remind that the order of fields in a record does not matter).
 In other words, the linearization of a function
 consists of a linearization of the body together with a
 field for a linearization of the bound variable.
@@ -2442,13 +2646,13 @@ should notice that GF requires trees to be in
 **eta-expanded** form in order to be linearizable:
 any function of type
 ```
-  A -> C
+  A -> B
 ```
 always has a syntax tree of the form
 ```
-  \x -> c
+  \x -> b
 ```
-where ``c : C`` under the assumption ``x : A``.
+where ``b : B`` under the assumption ``x : A``.
 It is in this form that an expression can be analysed
 as having a bound variable and a body. 
 
@@ -2477,8 +2681,7 @@ linearized into the same strings that represent them in
 the print-out of the abstract syntax. 
 
 
-To be able to
-//parse// variable symbols, however, GF needs to know what
+To be able to //parse// variable symbols, however, GF needs to know what
 to look for (instead of e.g. trying to parse //any//
 string as a variable). What strings are parsed as variable symbols 
 is defined in the lexical analysis part of GF parsing 
@@ -2486,9 +2689,8 @@ is defined in the lexical analysis part of GF parsing
   > p -cat=Prop -lexer=codevars "(All x)(x = x)"
   All (\x -> Eq x x)
 ```
-(see more details on lexers below).
-If several variables are bound in the same argument, the
-labels are ``$0, $1, $2``, etc. 
+(see more details on lexers below). If several variables are bound in the 
+same argument, the labels are ``$0, $1, $2``, etc. 
 
 
 
@@ -2506,12 +2708,11 @@ us very much. As we will see, however, computation does play a role
 even in the well-formedness of expressions when dependent types are
 present.
 
-
 GF has a form of judgement for **semantic definitions**,
 recognized by the key word ``def``. At its simplest, it is just
 the definition of one constant, e.g.
 ```
-  def one = succ zero ;
+  def one = Succ Zero ;
 ```
 We can also define a function with arguments,
 ```
@@ -2520,24 +2721,25 @@ We can also define a function with arguments,
 which is still a special case of the most general notion of
 definition, that of a group of **pattern equations**:
 ```
-  def sum x zero = x ;
-  def sum x (succ y) = succ (sum x y) ;
+  def 
+    sum x Zero = x ;
+    sum x (Succ y) = Succ (Sum x y) ;
 ```
 To compute a term is, as in functional programming languages,
 simply to follow a chain of reductions until no definition
 can be applied. For instance, we compute
 ```
-  sum one one -->
-  sum (succ zero) (succ zero) -->
-  succ (sum (succ zero) zero) -->
-  succ (succ zero)
+  Sum one one -->
+  Sum (Succ Zero) (Succ Zero) -->
+  Succ (sum (Succ Zero) Zero) -->
+  Succ (Succ Zero)
 ```
 Computation in GF is performed with the ``pt`` command and the
 ``compute`` transformation, e.g.
 ```
   > p -tr "1 + 1" | pt -transform=compute -tr | l
   sum one one
-  succ (succ zero)
+  Succ (Succ Zero)
   s(s(0))
 ```
 
@@ -2548,9 +2750,9 @@ Thus, trivially, all trees in a chain of computation
 (such as the one above)
 are definitionally equal to each other. So are the trees
 ```
-  sum zero (succ one)
-  succ one
-  sum (sum zero zero) (sum (succ zero) one)
+  sum Zero (Succ one)
+  Succ one
+  sum (sum Zero Zero) (sum (Succ Zero) one)
 ```
 and infinitely many other trees.
 
@@ -2558,8 +2760,8 @@ A fact that has to be emphasized about ``def`` definitions is that
 they are //not// performed as a first step of linearization.
 We say that **linearization is intensional**, which means that
 the definitional equality of two trees does not imply that
-they have the same linearizations. For instance, the seven terms
-above all have different linearizations in arithmetic notation:
+they have the same linearizations. For instance, each of the seven terms
+shown above has a different linearizations in arithmetic notation:
 ```
   1 + 1
   s(0) + s(0)
@@ -2587,7 +2789,7 @@ Two types depending on terms that are definitionally equal are
 equal types. For instance,
 ```
   Proof (Odd one)
-  Proof (Odd (succ zero))
+  Proof (Odd (Succ Zero))
 ```
 are equal types. Hence, any tree that type checks as a proof that
 1 is odd also type checks as a proof that the successor of 0 is odd.
@@ -2609,13 +2811,12 @@ unidiomatic or ambiguous. In such a case,
 the translation algorithm may be made to consider
 translation by a paraphrase.
 
-
 To stress express the distinction between
 **constructors** (=**canonical** functions)
 and other functions, GF has a judgement form
 ``data`` to tell that certain functions are canonical, e.g.
 ```
-  data Nat = succ | zero ;
+  data Nat = Succ | Zero ;
 ```
 Unlike in Haskell, but similarly to ALF (where constructor functions
 are marked with a flag ``C``), 
@@ -2624,247 +2825,19 @@ a type with new ``data`` judgements. The type signatures of constructors
 are given separately, in ordinary ``fun`` judgements.
 One can also write directly
 ```
-  data succ : Nat -> Nat ;
+  data Succ : Nat -> Nat ;
 ```
 which is equivalent to the two judgements
 ```
-  fun succ : Nat -> Nat ;
-  data Nat = succ ;
-```
-
-
-
-
-%--!
-==More features of the module system==
-
-===Interfaces, instances, and functors===
-
-
-===Resource grammars and their reuse===
-
-A resource grammar is a grammar built on linguistic grounds,
-to describe a language rather than a domain.
-The GF resource grammar library, which contains resource grammars for
-10 languages, is described more closely in the following
-documents:
-- [Resource library API documentation ../../lib/resource-1.0/doc/]:
-  for application grammarians using the resource.
-- [Resource writing HOWTO ../../lib/resource-1.0/doc/Resource-HOWTO.html]:
-  for resource grammarians developing the resource.
-
-
-However, to give a flavour of both using and writing resource grammars,
-we have created a miniature resource, which resides in the
-subdirectory [``resource`` resource]. Its API consists of the following
-three modules:
-
-[Syntax resource/Syntax.gf] - syntactic structures, language-independent:
-```
-
-```
-[LexEng resource/LexEng.gf] - lexical paradigms, English:
-```
-
-```
-[LexIta resource/LexIta.gf] - lexical paradigms, Italian:
-```
-
-```
-
-
-Only these three modules should be ``open``ed in applications.
-The implementations of the resource are given in the following four modules:
-
-[MorphoEng resource/MorphoEng.gf],
-```
-
-```
-[MorphoIta resource/MorphoIta.gf]: low-level morphology
-- [SyntaxEng resource/SyntaxEng.gf].
-  [SyntaxIta resource/SyntaxIta.gf]: definitions of syntactic structures
-
-
-An example use of the resource resides in the
-subdirectory [``applications`` applications].
-It implements the abstract syntax 
-[``FoodComments`` applications/FoodComments.gf] for English and Italian.
-The following diagram shows the module structure, indicating by
-colours which modules are written by the grammarian. The two blue modules
-form the abstract syntax. The three red modules form the concrete syntax.
-The two green modules are trivial instantiations of a functor.
-The rest of the modules (black) come from the resource.
-
-[Multi.png]
-
-
-
-===Restricted inheritance and qualified opening===
-
-
-==Using the standard resource library==
-
-The example files of this chapter can be found in
-the directory [``arithm`` ./arithm].
-
-
-===The simplest way===
-
-The simplest way is to ``open`` a top-level ``Lang`` module
-and a ``Paradigms`` module: 
-```
-  abstract Foo = ...
-
-  concrete FooEng = open LangEng, ParadigmsEng in ...
-  concrete FooSwe = open LangSwe, ParadigmsSwe in ...
-```
-Here is an example.
-```
-abstract Arithm = {
-  cat
-    Prop ;
-    Nat ;
-  fun
-    Zero : Nat ;
-    Succ : Nat -> Nat ;
-    Even : Nat -> Prop ;
-    And  : Prop -> Prop -> Prop ;
-}
-
---# -path=.:alltenses:prelude
-
-concrete ArithmEng of Arithm = open LangEng, ParadigmsEng in {
-  lincat
-    Prop = S ;
-    Nat  = NP ;
-  lin
-    Zero = 
-      UsePN (regPN "zero" nonhuman) ;
-    Succ n = 
-      DetCN (DetSg (SgQuant DefArt) NoOrd) (ComplN2 (regN2 "successor") n) ;
-    Even n = 
-      UseCl TPres ASimul PPos 
-        (PredVP n (UseComp (CompAP (PositA (regA "even"))))) ;
-    And x y = 
-      ConjS and_Conj (BaseS x y) ;
-
-}
-
---# -path=.:alltenses:prelude
-
-concrete ArithmSwe of Arithm = open LangSwe, ParadigmsSwe in {
-  lincat
-    Prop = S ;
-    Nat  = NP ;
-  lin
-    Zero = 
-      UsePN (regPN "noll" neutrum) ;
-    Succ n = 
-      DetCN (DetSg (SgQuant DefArt) NoOrd) 
-        (ComplN2 (mkN2 (mk2N "efterföljare" "efterföljare") 
-           (mkPreposition "till")) n) ;
-    Even n = 
-      UseCl TPres ASimul PPos 
-        (PredVP n (UseComp (CompAP (PositA (regA "jämn"))))) ;
-    And x y = 
-      ConjS and_Conj (BaseS x y) ;
-}
-```
-
-
-===How to find resource functions===
-
-The definitions in this example were found by parsing:
-```
-  > i LangEng.gf
-
-  -- for Successor:
-  > p -cat=NP -mcfg -parser=topdown "the mother of Paris"
-
-  -- for Even:
-  > p -cat=S -mcfg -parser=topdown "Paris is old"
-
-  -- for And:
-  > p -cat=S -mcfg -parser=topdown "Paris is old and I am old"
-```
-The use of parsing can be systematized by **example-based grammar writing**,
-to which we will return later. 
-
-
-===A functor implementation===
-
-The interesting thing now is that the
-code in ``ArithmSwe`` is similar to the code in ``ArithmEng``, except for
-some lexical items ("noll" vs. "zero", "efterföljare" vs. "successor",
-"jämn" vs. "even").  How can we exploit the similarities and
-actually share code between the languages?
-
-The solution is to use a functor: an ``incomplete`` module that opens
-an ``abstract`` as an ``interface``, and then instantiate it to different
-languages that implement the interface. The structure is as follows:
-```
-  abstract Foo ...
-
-  incomplete concrete FooI = open Lang, Lex in ...
-
-  concrete FooEng of Foo = FooI with (Lang=LangEng), (Lex=LexEng) ;
-  concrete FooSwe of Foo = FooI with (Lang=LangSwe), (Lex=LexSwe) ;
-```
-where ``Lex`` is an abstract lexicon that includes the vocabulary
-specific to this application:
+  fun Succ : Nat -> Nat ;
+  data Nat = Succ ;
 ```
-  abstract Lex = Cat ** ...
 
-  concrete LexEng of Lex = CatEng ** open ParadigmsEng in ...
-  concrete LexSwe of Lex = CatSwe ** open ParadigmsSwe in ...  
-```
-Here, again, a complete example (``abstract Arithm`` is as above):
-```
-incomplete concrete ArithmI of Arithm = open Lang, Lex in {
-  lincat
-    Prop = S ;
-    Nat  = NP ;
-  lin
-    Zero = 
-      UsePN zero_PN ;
-    Succ n = 
-      DetCN (DetSg (SgQuant DefArt) NoOrd) (ComplN2 successor_N2 n) ;
-    Even n = 
-      UseCl TPres ASimul PPos 
-        (PredVP n (UseComp (CompAP (PositA even_A)))) ;
-    And x y = 
-      ConjS and_Conj (BaseS x y) ;
-}
 
---# -path=.:alltenses:prelude
-concrete ArithmEng of Arithm = ArithmI with
-  (Lang = LangEng),
-  (Lex = LexEng) ;
-
---# -path=.:alltenses:prelude
-concrete ArithmSwe of Arithm = ArithmI with
-  (Lang = LangSwe),
-  (Lex = LexSwe) ;
-
-abstract Lex = Cat ** {
-  fun
-    zero_PN : PN ;
-    successor_N2 : N2 ;  
-    even_A : A ;
-}
-
-concrete LexSwe of Lex = CatSwe ** open ParadigmsSwe in {
-  lin 
-    zero_PN = regPN "noll" neutrum ;
-    successor_N2 = 
-      mkN2 (mk2N "efterföljare" "efterföljare") (mkPreposition "till") ;
-    even_A = regA "jämn" ;
-}
-```
+===Case study: representing anaphoric reference TODO===
 
 
-
-==Transfer modules==
+==Transfer modules TODO==
 
 Transfer means noncompositional tree-transforming operations.
 The command ``apply_transfer = at`` is typically used in a pipe:
@@ -2880,7 +2853,7 @@ See the
 for more information.
 
 
-==Practical issues==
+==Practical issues TODO==
 
 
 ===Lexers and unlexers===
@@ -2913,7 +2886,6 @@ Given by ``help -lexer``, ``help -unlexer``:
     -unlexer=codelit     like code, but remove string literal quotes
     -unlexer=concat      remove all spaces
     -unlexer=bind        like identity, but bind at "&+"
-
 ```
 
 
@@ -2946,8 +2918,6 @@ Both Flite and ATK are freely available through the links
 above, but they are not distributed together with GF.
 
 
-
-
 ===Multilingual syntax editor===
 
 The 
@@ -2956,7 +2926,7 @@ describes the use of the editor, which works for any multilingual GF grammar.
 
 Here is a snapshot of the editor:
 
-[../quick-editor.gif]
+[../quick-editor.png]
  
 The grammars of the snapshot are from the
 [Letter grammar package http://www.cs.chalmers.se/~aarne/GF/examples/letter].
@@ -2999,7 +2969,7 @@ A summary is given in the following chart of GF grammar compiler phases:
 [../gf-compiler.png]
 
 
-==Case studies==
+==Larger case studies TODO==
 
 ===Interfacing formal and natural languages===
 
@@ -3011,3 +2981,8 @@ English and German.
 
 A simpler example will be explained here.
 
+
+===A multimodal dialogue system===
+
+See TALK project deliverables, [TALK homepage http://www.talk-project.org]
+