=> 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.
==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]