=> t
+ ...
+ }
+```
+
+
+%--!
+==Regular expression patterns==
+
+To define string operations computed at compile time, such
+as in morphology, it is handy to use regular expression patterns:
+ - //p// ``+`` //q// : token consisting of //p// followed by //q//
+ - //p// ``*`` : token //p// repeated 0 or more times
+ (max the length of the string to be matched)
+ - ``-`` //p// : matches anything that //p// does not match
+ - //x// ``@`` //p// : bind to //x// what //p// matches
+ - //p// ``|`` //q// : matches what either //p// or //q// matches
+
+
+The last three apply to all types of patterns, the first two only to token strings.
+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" => w + "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" ;
+ nyck + "e" + l@("l" | "r" | "n") => nyck + l + "ar" ;
+ bil => bil + "ar"
+ } ;
+```
+
+
+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.
+```
+ Match (p1|p2) v = Match p1 v ++ Match p2 v
+ Match (p1+p2) s = [Match p1 s1 ++ Match p2 s2 |
+ i <- [0..length s], (s1,s2) = splitAt i s]
+ Match p* s = [[]] if Match "" s ++ Match p s ++ Match (p+p) s ++... /= []
+ Match -p v = [[]] if Match p v = []
+ Match c v = [[]] if c == v -- for constant and literal patterns c
+ Match x v = [[(x,v)]] -- for variable patterns x
+ Match x@p v = [[(x,v)]] + M if M = Match p v /= []
+ Match p v = [] otherwise -- failure
+```
+Examples:
+- ``x + "e" + y`` matches ``"peter"`` with ``x = "p", y = "ter"``
+- ``x + "er"*`` matches ``"burgerer"`` with ``x = "burg"
+
+
+
+
+
+%--!
+==Prefix-dependent choices==
+
+Sometimes a token has different forms depending on the token
+that follows. An example is the English indefinite article,
+which is //an// if a vowel follows, //a// otherwise.
+Which form is chosen can only be decided at run time, i.e.
+when a string is actually build. GF has a special construct for
+such tokens, the ``pre`` construct exemplified in
+```
+ oper artIndef : Str =
+ pre {"a" ; "an" / strs {"a" ; "e" ; "i" ; "o"}} ;
+```
+Thus
+```
+ artIndef ++ "cheese" ---> "a" ++ "cheese"
+ artIndef ++ "apple" ---> "an" ++ "apple"
+```
+This very example does not work in all situations: the prefix
+//u// has no general rules, and some problematic words are
+//euphemism, one-eyed, n-gram//. It is possible to write
+```
+ oper artIndef : Str =
+ pre {"a" ;
+ "a" / strs {"eu" ; "one"} ;
+ "an" / strs {"a" ; "e" ; "i" ; "o" ; "n-"}
+ } ;
+```
+
+
+==Predefined types and operations==
+
+GF has the following predefined categories in abstract syntax:
+```
+ cat Int ; -- integers, e.g. 0, 5, 743145151019
+ cat Float ; -- floats, e.g. 0.0, 3.1415926
+ cat String ; -- strings, e.g. "", "foo", "123"
+```
+The objects of each of these categories are **literals**
+as indicated in the comments above. No ``fun`` definition
+can have a predefined category as its value type, but
+they can be used as arguments. For example:
+```
+ fun StreetAddress : Int -> String -> Address ;
+ lin StreetAddress number street = {s = number.s ++ street.s} ;
+
+ -- e.g. (StreetAddress 10 "Downing Street") : Address
+```
+FIXME: The linearization type is ``{s : Str}`` for all these categories.
+
+
+
+%--!
+=Using the resource grammar library=
+
+%!include: ../intro-resource.txt
+
+
+%--!
+=Overview of the resource grammar library=
+
+%!include: ../overview-resource.txt
+
+
+
+=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
+to encode advanced semantic concepts in an abstract syntax.
+We use concepts inherited from **type theory**. Type theory
+is the basis of many systems known as **logical frameworks**, which are
+used for representing mathematical theorems and their proofs on a computer.
+In fact, GF has a logical framework as its proper part:
+this part is the abstract syntax.
+
+In a logical framework, the formalization of a mathematical theory
+is a set of type and function declarations. The following is an example
+of such a theory, represented as an ``abstract`` module in GF.
+```
+abstract Arithm = {
+ cat
+ Prop ; -- proposition
+ Nat ; -- natural number
+ fun
+ Zero : Nat ; -- 0
+ Succ : Nat -> Nat ; -- successor of x
+ Even : Nat -> Prop ; -- x is even
+ And : Prop -> Prop -> Prop ; -- A and B
+ }
+```
+A concrete syntax is given below, as an example of using the resource grammar
+library.
+
+
+
+==Dependent types==
+
+**Dependent types** are a characteristic feature of GF,
+inherited from the
+**constructive type theory** of Martin-Löf and
+distinguishing GF from most other grammar formalisms and
+functional programming languages.
+The initial main motivation for developing GF was, indeed,
+to have a grammar formalism with dependent types.
+As can be inferred from the fact that we introduce them only now,
+after having written lots of grammars without them,
+dependent types are no longer the only motivation for GF.
+But they are still important and interesting.
+
+
+Dependent types can be used for stating stronger
+**conditions of well-formedness** than non-dependent types.
+A simple example is postal addresses. Ignoring the other details,
+let us take a look at addresses consisting of
+a street, a city, and a country.
+```
+abstract Address = {
+ cat
+ Address ; Country ; City ; Street ;
+
+ fun
+ mkAddress : Country -> City -> Street -> Address ;
+
+ UK, France : Country ;
+ Paris, London, Grenoble : City ;
+ OxfordSt, ShaftesburyAve, BdRaspail, RueBlondel, AvAlsaceLorraine : Street ;
+ }
+```
+The linearization rules are straightforward,
+```
+ lin
+ mkAddress country city street =
+ ss (street.s ++ "," ++ city.s ++ "," ++ country.s) ;
+ UK = ss ("U.K.") ;
+ France = ss ("France") ;
+ Paris = ss ("Paris") ;
+ London = ss ("London") ;
+ Grenoble = ss ("Grenoble") ;
+ OxfordSt = ss ("Oxford" ++ "Street") ;
+ ShaftesburyAve = ss ("Shaftesbury" ++ "Avenue") ;
+ BdRaspail = ss ("boulevard" ++ "Raspail") ;
+ RueBlondel = ss ("rue" ++ "Blondel") ;
+ AvAlsaceLorraine = ss ("avenue" ++ "Alsace-Lorraine") ;
+```
+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).
+
+Both existing and non-existing addresses are recognized by this
+grammar. The non-existing ones in the following randomly generated
+list have afterwards been marked by *:
+```
+ > gr -cat=Address -number=7 | l
+
+ * Oxford Street , Paris , France
+ * Shaftesbury Avenue , Grenoble , U.K.
+ boulevard Raspail , Paris , France
+ * rue Blondel , Grenoble , U.K.
+ * Shaftesbury Avenue , Grenoble , France
+ * Oxford Street , London , France
+ * Shaftesbury Avenue , Grenoble , France
+```
+Dependent types provide a way to guarantee that addresses are
+well-formed. What we do is to include **contexts** in
+``cat`` judgements:
+```
+ 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,
+but cities of the U.K. and cities of France. The fourth judgement
+makes ``Street`` dependent on ``City``; but since
+``City`` is itself dependent on ``Country``, we must
+include them both in the context, moreover guaranteeing that
+the city is one of the given country. Since the context itself
+is built by using a dependent type, we have to use variables
+to indicate the dependencies. The judgement we used for ``City``
+is actually shorthand for
+```
+ cat City (x : Country)
+```
+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 ;
+
+ 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
+the context of ``Street`` above. What we claimed to be the
+"logical" order of the arguments is now forced by the type system
+of GF: a variable must be declared (=bound) before it can be
+referenced (=used).
+
+The effect of dependent types is that the *-marked addresses above are
+no longer well-formed. What the GF parser actually does is that it
+initially accepts them (by using a context-free parsing algorithm)
+and then rejects them (by type checking). The random generator does not produce
+illegal addresses (this could be useful in bulk mailing!).
+The linearization algorithm does not care about type dependencies;
+actually, since the //categories// (ignoring their arguments)
+are the same in both abstract syntaxes,
+we use the same concrete syntax
+for both of them.
+
+**Remark**. Function types //without//
+variables are actually a shorthand notation: writing
+```
+ fun PredV1 : NP -> V1 -> S
+```
+is shorthand for
+```
+ fun PredV1 : (x : NP) -> (y : V1) -> S
+```
+or any other naming of the variables. Actually the use of variables
+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==
+
+The **functional fragment** of GF
+terms and types comprises function types, applications, lambda
+abstracts, constants, and variables. This fragment is similar in
+abstract and concrete syntax. In particular,
+dependent types are also available in concrete syntax.
+We have not made use of them yet,
+but we will now look at one example of how they
+can be used.
+
+Those readers who are familiar with functional programming languages
+like ML and Haskell, may already have missed **polymorphic**
+functions. For instance, Haskell programmers have access to
+the functions
+```
+ const :: a -> b -> a
+ const c _ = c
+
+ flip :: (a -> b -> c) -> b -> a -> c
+ flip f y x = f x y
+```
+which can be used for any given types ``a``,``b``, and ``c``.
+
+The GF counterpart of polymorphic functions are **monomorphic**
+functions with explicit **type variables**. Thus the above
+definitions can be written
+```
+ oper const :(a,b : Type) -> a -> b -> a =
+ \_,_,c,_ -> c ;
+
+ oper flip : (a,b,c : Type) -> (a -> b ->c) -> b -> a -> c =
+ \_,_,_,f,x,y -> f y x ;
+```
+When the operations are used, the type checker requires
+them to be equipped with all their arguments; this may be a nuisance
+for a Haskell or ML programmer.
+
+
+
+==Expressing selectional restrictions==
+
+This section introduces a way of using dependent types to
+formalize a notion known as **selectional restrictions**
+in linguistics. We first present a mathematical model
+of the notion, and then integrate it in a linguistically
+motivated syntax.
+
+In linguistics, a
+grammar is usually thought of as being about **syntactic well-formedness**
+in a rather liberal sense: an expression can be well-formed without
+being meaningful, in other words, without being
+**semantically well-formed**.
+For instance, the sentence
+```
+ the number 2 is equilateral
+```
+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") and satisfies the agreement
+rule saying that the verb phrase is inflected in the
+number of the noun phrase:
+```
+ fun PredVP : NP -> VP -> S ;
+ lin PredVP np v = {s = np.s ++ vp.s ! np.n} ;
+```
+It is ill-formed because the predicate "is equilateral"
+is only defined for triangles, not for numbers.
+
+In a straightforward type-theoretical formalization of
+mathematics, domains of mathematical objects
+are defined as types. In GF, we could write
+```
+ cat Nat ;
+ cat Triangle ;
+ cat Prop ;
+```
+for the types of natural numbers, triangles, and propositions,
+respectively.
+Noun phrases are typed as objects of basic types other than
+``Prop``, whereas verb phrases are functions from basic types
+to ``Prop``. For instance,
+```
+ fun two : Nat ;
+ fun Even : Nat -> Prop ;
+ fun Equilateral : Triangle -> Prop ;
+```
+With these judgements, and the linearization rules
+```
+ lin two = ss ["the number 2"] ;
+ lin Even x = ss (x.s ++ ["is even"]) ;
+ lin Equilateral x = ss (x.s ++ ["is equilateral"]) ;
+```
+we can form the proposition ``Even two``
+```
+ the number 2 is even
+```
+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
+in semantic well-formedness: we want to be sure that a proposition makes
+sense before we make the effort of proving it. The straightforward typing
+of nouns and predicates shown above is the way in which this
+is guaranteed in various proof systems based on type theory.
+(Notice that it is still possible to form //false// propositions,
+e.g. "the number 3 is even".
+False and meaningless are different things.)
+
+As shown by the linearization rules for ``two``, ``Even``,
+etc, it //is// possible to use straightforward mathematical typings
+as the abstract syntax of a grammar. However, this syntax is not very
+expressive linguistically: for instance, there is no distinction between
+adjectives and verbs. It is hard to give rules for structures like
+adjectival modification ("even number") and conjunction of predicates
+("even or odd").
+
+By using dependent types, it is simple to combine a linguistically
+motivated system of categories with mathematically motivated
+type restrictions. What we need is a category of domains of
+individual objects,
+```
+ cat Dom
+```
+and dependencies of other categories on this:
+```
+ cat
+ S ; -- sentence
+ 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
+ NP Dom ; -- noun phrase for an object of specific type
+ Conj ; -- conjunction
+ Det ; -- determiner
+```
+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 ;
+ 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 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) ;
+ 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) ;
+ ConjV1 _ conj v1 v2 = ss (v1.s ++ conj.s ++ v2.s) ;
+```
+The domain arguments thus get suppressed in linearization.
+Parsing initially returns metavariables for them,
+but type checking can usually restore them
+by inference from those arguments that are not suppressed.
+
+One traditional linguistic example of domain restrictions
+(= selectional restrictions) is the contrast between the two sentences
+```
+ John plays golf
+ golf plays John
+```
+To explain the contrast, we introduce the functions
+```
+ human : Dom ;
+ game : Dom ;
+ play : V2 human 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 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 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:
+```
+ > p -tr "John plays golf" | pt -transform=solve
+ > p -tr "golf plays John" | pt -transform=solve
+```
+In the latter case, no solutions are found.
+
+A known problem with selectional restrictions is that they can be more
+or less liberal. For instance,
+```
+ John loves Mary
+ John loves 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
+argument:
+```
+ fun love : (A : Dom) -> V2 human A ;
+ lin love _ = ss "loves" ;
+```
+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 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
+propositional and predicate calculus. In this section, we will consider
+a more elementary example, showing how the notion of proof is useful
+outside mathematics, as well.
+
+We first define the category of unary (also known as Peano-style)
+natural numbers:
+```
+ cat Nat ;
+ fun Zero : Nat ;
+ fun Succ : Nat -> Nat ;
+```
+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//
+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//.
+
+
+The most straightforward way of expressing these axioms in type theory
+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) ;
+ fun lessS : (x,y : Nat) -> Less x y -> Less (Succ x) (Succ y) ;
+```
+Objects formed by ``lessZ`` and ``lessS`` are
+called **proof objects**: they establish the truth of certain
+mathematical propositions.
+For instance, the fact that 2 is less that
+4 has the proof object
+```
+ lessS (Succ Zero) (Succ (Succ (Succ Zero)))
+ (lessS Zero (Succ (Succ Zero)) (lessZ (Succ Zero)))
+```
+whose type is
+```
+ Less (Succ (Succ Zero)) (Succ (Succ (Succ (Succ Zero))))
+```
+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.
+
+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
+a later time:
+```
+ from 3 to 8
+```
+is thus well-formed, whereas
+```
+ from 8 to 3
+```
+is not. The following rules for spans impose this condition
+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 ;
+```
+
+
+
+==Variable bindings==
+
+Mathematical notation and programming languages have lots of
+expressions that **bind** variables. For instance,
+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`` can have
+**bound occurrences**.
+
+Variable bindings appear in informal mathematical language as well, for
+instance,
+```
+ for all x, x is equal to x
+
+ the function that for any numbers x and y returns the maximum of x+y
+ and x*y
+```
+In type theory, variable-binding expression forms can be formalized
+as functions that take functions as arguments. The universal
+quantifier is defined
+```
+ fun All : (Ind -> Prop) -> Prop
+```
+where ``Ind`` is the type of individuals and ``Prop``,
+the type of propositions. If we have, for instance, the equality predicate
+```
+ fun Eq : Ind -> Ind -> Prop
+```
+we may form the tree
+```
+ All (\x -> Eq x x)
+```
+which corresponds to the ordinary notation
+```
+ (All x)(x = x).
+```
+
+
+An abstract syntax where trees have functions as arguments, as in
+the two examples above, has turned out to be precisely the right
+thing for the semantics and computer implementation of
+variable-binding expressions. The advantage lies in the fact that
+only one variable-binding expression form is needed, the lambda abstract
+``\x -> b``, and all other bindings can be reduced to it.
+This makes it easier to implement mathematical theories and reason
+about them, since variable binding is tricky to implement and
+to reason about. The idea of using functions as arguments of
+syntactic constructors is known as **higher-order abstract syntax**.
+
+The question now arises: how to define linearization rules
+for variable-binding expressions?
+Let us first consider universal quantification,
+```
+ fun All : (Ind -> Prop) -> Prop
+```
+We write
+```
+ lin All B = {s = "(" ++ "All" ++ B.$0 ++ ")" ++ B.s}
+```
+to obtain the form shown above.
+This linearization rule brings in a new GF concept - the ``$0``
+field of ``B`` containing a bound variable symbol.
+The general rule is that, if an argument type of a function is
+itself a function type ``A -> C``, the linearization type of
+this argument is the linearization type of ``C``
+together with a new field ``$0 : Str``. In the linearization rule
+for ``All``, the argument ``B`` thus has the linearization
+type
+```
+ {$0 : Str ; s : Str},
+```
+since the linearization type of ``Prop`` is
+```
+ {s : Str}
+```
+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.
+Those familiar with type theory or lambda calculus
+should notice that GF requires trees to be in
+**eta-expanded** form in order to be linearizable:
+any function of type
+```
+ A -> B
+```
+always has a syntax tree of the form
+```
+ \x -> b
+```
+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.
+
+
+Given the linearization rule
+```
+ lin Eq a b = {s = "(" ++ a.s ++ "=" ++ b.s ++ ")"}
+```
+the linearization of
+```
+ \x -> Eq x x
+```
+is the record
+```
+ {$0 = "x", s = ["( x = x )"]}
+```
+Thus we can compute the linearization of the formula,
+```
+ All (\x -> Eq x x) --> {s = "[( All x ) ( x = x )]"}.
+```
+
+How did we get the //linearization// of the variable ``x``
+into the string ``"x"``? GF grammars have no rules for
+this: it is just hard-wired in GF that variable symbols are
+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 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
+```
+ > 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.
+
+
+
+==Semantic definitions==
+
+We have seen that,
+just like functional programming languages, GF has declarations
+of functions, telling what the type of a function is.
+But we have not yet shown how to **compute**
+these functions: all we can do is provide them with arguments
+and linearize the resulting terms.
+Since our main interest is the well-formedness of expressions,
+this has not yet bothered
+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 ;
+```
+We can also define a function with arguments,
+```
+ def Neg A = Impl A Abs ;
+```
+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 ;
+ 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)
+```
+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)
+ s(s(0))
+```
+
+The ``def`` definitions of a grammar induce a notion of
+**definitional equality** among trees: two trees are
+definitionally equal if they compute into the same tree.
+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)
+```
+and infinitely many other trees.
+
+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, each of the seven terms
+shown above has a different linearizations in arithmetic notation:
+```
+ 1 + 1
+ s(0) + s(0)
+ s(s(0) + 0)
+ s(s(0))
+ 0 + s(0)
+ s(1)
+ 0 + 0 + s(0) + 1
+```
+This notion of intensionality is
+no more exotic than the intensionality of any **pretty-printing**
+function of a programming language (function that shows
+the expressions of the language as strings). It is vital for
+pretty-printing to be intensional in this sense - if we want,
+for instance, to trace a chain of computation by pretty-printing each
+intermediate step, what we want to see is a sequence of different
+expression, which are definitionally equal.
+
+What is more exotic is that GF has two ways of referring to the
+abstract syntax objects. In the concrete syntax, the reference is intensional.
+In the abstract syntax, the reference is extensional, since
+**type checking is extensional**. The reason is that,
+in the type theory with dependent types, types may depend on terms.
+Two types depending on terms that are definitionally equal are
+equal types. For instance,
+```
+ Proof (Odd one)
+ 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.
+(Recall, in this connection, that the
+arguments a category depends on never play any role
+in the linearization of trees of that category,
+nor in the definition of the linearization type.)
+
+In addition to computation, definitions impose a
+**paraphrase** relation on expressions:
+two strings are paraphrases if they
+are linearizations of trees that are
+definitionally equal.
+Paraphrases are sometimes interesting for
+translation: the **direct translation**
+of a string, which is the linearization of the same tree
+in the targer language, may be inadequate because it is e.g.
+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 ;
+```
+Unlike in Haskell, but similarly to ALF (where constructor functions
+are marked with a flag ``C``),
+new constructors can be added to
+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 ;
+```
+which is equivalent to the two judgements
+```
+ fun Succ : Nat -> Nat ;
+ data Nat = Succ ;
+```
+
+
+==Case study: representing anaphoric reference TODO==
+
+
+=Transfer modules TODO=
+
+Transfer means noncompositional tree-transforming operations.
+The command ``apply_transfer = at`` is typically used in a pipe:
+```
+ > p "John walks and John runs" | apply_transfer aggregate | l
+ John walks and runs
+```
+See the
+[sources ../../transfer/examples/aggregation] of this example.
+
+See the
+[transfer language documentation ../transfer.html]
+for more information.
+
+
+=Practical issues TODO=
+
+
+==Lexers and unlexers==
+
+Lexers and unlexers can be chosen from
+a list of predefined ones, using the flags``-lexer`` and `` -unlexer`` either
+in the grammar file or on the GF command line.
+
+Given by ``help -lexer``, ``help -unlexer``:
+```
+ The default is words.
+ -lexer=words tokens are separated by spaces or newlines
+ -lexer=literals like words, but GF integer and string literals recognized
+ -lexer=vars like words, but "x","x_...","$...$" as vars, "?..." as meta
+ -lexer=chars each character is a token
+ -lexer=code use Haskell's lex
+ -lexer=codevars like code, but treat unknown words as variables, ?? as meta
+ -lexer=text with conventions on punctuation and capital letters
+ -lexer=codelit like code, but treat unknown words as string literals
+ -lexer=textlit like text, but treat unknown words as string literals
+ -lexer=codeC use a C-like lexer
+ -lexer=ignore like literals, but ignore unknown words
+ -lexer=subseqs like ignore, but then try all subsequences from longest
+
+ The default is unwords.
+ -unlexer=unwords space-separated token list (like unwords)
+ -unlexer=text format as text: punctuation, capitals, paragraph
+ -unlexer=code format as code (spacing, indentation)
+ -unlexer=textlit like text, but remove string literal quotes
+ -unlexer=codelit like code, but remove string literal quotes
+ -unlexer=concat remove all spaces
+ -unlexer=bind like identity, but bind at "&+"
+```
+
+
+==Efficiency of grammars==
+
+Issues:
+
+- the choice of datastructures in ``lincat``s
+- the value of the ``optimize`` flag
+- parsing efficiency: ``-fcfg`` vs. others
+
+
+==Speech input and output==
+
+The``speak_aloud = sa`` command sends a string to the speech
+synthesizer
+[Flite http://www.speech.cs.cmu.edu/flite/doc/].
+It is typically used via a pipe:
+``` generate_random | linearize | speak_aloud
+The result is only satisfactory for English.
+
+The ``speech_input = si`` command receives a string from a
+speech recognizer that requires the installation of
+[ATK http://mi.eng.cam.ac.uk/~sjy/software.htm].
+It is typically used to pipe input to a parser:
+``` speech_input -tr | parse
+The method words only for grammars of English.
+
+Both Flite and ATK are freely available through the links
+above, but they are not distributed together with GF.
+
+
+==Multilingual syntax editor==
+
+The
+[Editor User Manual http://www.cs.chalmers.se/~aarne/GF2.0/doc/javaGUImanual/javaGUImanual.htm]
+describes the use of the editor, which works for any multilingual GF grammar.
+
+Here is a snapshot of the editor:
+
+[../quick-editor.png]
+
+The grammars of the snapshot are from the
+[Letter grammar package http://www.cs.chalmers.se/~aarne/GF/examples/letter].
+
+
+
+==Interactive Development Environment (IDE)==
+
+Forthcoming.
+
+
+==Communicating with GF==
+
+Other processes can communicate with the GF command interpreter,
+and also with the GF syntax editor. Useful flags when invoking GF are
+- ``-batch`` suppresses the promps and structures the communication with XML tags.
+- ``-s`` suppresses non-output non-error messages and XML tags.
+-- ``-nocpu`` suppresses CPU time indication.
+
+Thus the most silent way to invoke GF is
+```
+ gf -batch -s -nocpu
+```
+
+
+
+==Embedded grammars in Haskell, Java, and Prolog==
+
+GF grammars can be used as parts of programs written in the
+following languages. The links give more documentation.
+
+- [Java http://www.cs.chalmers.se/~bringert/gf/gf-java.html]
+- [Haskell http://www.cs.chalmers.se/~aarne/GF/src/GF/Embed/EmbedAPI.hs]
+- [Prolog http://www.cs.chalmers.se/~peb/software.html]
+
+
+==Alternative input and output grammar formats==
+
+A summary is given in the following chart of GF grammar compiler phases:
+[../gf-compiler.png]
+
+
+=Larger case studies TODO=
+
+==Interfacing formal and natural languages==
+
+[Formal and Informal Software Specifications http://www.cs.chalmers.se/~krijo/thesis/thesisA4.pdf],
+PhD Thesis by
+[Kristofer Johannisson http://www.cs.chalmers.se/~krijo], is an extensive example of this.
+The system is based on a multilingual grammar relating the formal language OCL with
+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]
+