From df3b453f3b5697f4c29d2fa394799564a3d2bb90 Mon Sep 17 00:00:00 2001 From: aarne Date: Fri, 16 Jun 2006 15:29:01 +0000 Subject: [PATCH] tutorial edited --- doc/tutorial/gf-tutorial2.html | 236 +++++++++++++++------------------ doc/tutorial/gf-tutorial2.txt | 119 +++++++---------- 2 files changed, 156 insertions(+), 199 deletions(-) diff --git a/doc/tutorial/gf-tutorial2.html b/doc/tutorial/gf-tutorial2.html index de2d63dcb..804ed1969 100644 --- a/doc/tutorial/gf-tutorial2.html +++ b/doc/tutorial/gf-tutorial2.html @@ -7,7 +7,7 @@

Grammatical Framework Tutorial

Author: Aarne Ranta <aarne (at) cs.chalmers.se>
-Last update: Fri Jun 16 10:32:52 2006 +Last update: Fri Jun 16 17:28:39 2006

@@ -100,40 +100,39 @@ Last update: Fri Jun 16 10:32:52 2006 -
  • More features of the module system +
  • More features of the module system -
  • Using the standard resource library +
  • Using the standard resource library -
  • Transfer modules -
  • Practical issues +
  • Transfer modules +
  • Practical issues -
  • Case studies +
  • Case studies @@ -2273,8 +2272,8 @@ are straightforward, 
         lin
   
-      mkAddress country city street = ss (street ++ "," ++ city ++ "," ++ country) ;
-  
+      mkAddress country city street = 
+        ss (street.s ++ "," ++ city.s ++ "," ++ country.s) ;
       UK = ss ("U.K.") ;
       France = ss ("France") ;
       Paris = ss ("Paris") ;
@@ -2400,39 +2399,6 @@ sometimes shortens the code, since we can write e.g.

    -

    Dependent types in syntax editing

    -

    -An extra advantage of dependent types is seen in -syntax editing: -when menus with possible refinements are created, -only those functions are shown that are type-correct. -For instance, if the editor state is -

    -
    -    mkAddress : Address  
-       UK : Country  
-    *  ?2 : City UK  
-       ?3 : Street UK ?2
-
    -

    -only the cities of the U.K. are shown in the city menu. -

    -

    -What is more, editing in the state -

    -
    -    mkAddress : Address  
-       ?1 : Country  
-       ?2 : City (?1)  
-    *  ?3 : Street (?1) (?2)  
-
    -

    -starts from the Street argument, -which enables GF automatically to infer the city and the country. -Thus, in addition to guaranteeing the meaningfulness of the results, -dependent types can shorten editing sessions considerably. -

    -

    Dependent types in concrete syntax

    The functional fragment of GF @@ -2452,9 +2418,9 @@ the functions 

         const :: a -> b -> a
-    const c x = c
+    const c _ = c
   
-    flip :: (a -> b ->c) -> b -> a -> c
+    flip :: (a -> b -> c) -> b -> a -> c
     flip f y x = f x y

    @@ -2467,7 +2433,7 @@ definitions can be written 

         oper const :(a,b : Type) -> a -> b -> a =
-      \_,_,c,x -> c ;
+      \_,_,c,_ -> c ;
   
     oper flip : (a,b,c : Type) -> (a -> b ->c) -> b -> a -> c =
       \_,_,_,f,x,y -> f y x ;
@@ -2475,9 +2441,9 @@ definitions can be written
 
    
 When the operations are used, the type checker requires
 them to be equipped with all their arguments; this may be a nuisance
-for the Haskell or ML programmer. 
+for a Haskell or ML programmer. 
 
    
-
+
 
    Expressing selectional restrictions
    
 
    
 This section introduces a way of using dependent types to
@@ -2506,8 +2472,8 @@ rule that the verb phrase is inflected in the
 number of the noun phrase:
 
    
 
    -    fun PredV1 : NP -> V1 -> S ;
-    lin PredV1 np v1 = {s = np.s ++ v1.s ! np.n} ;
+    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"
@@ -2719,7 +2685,17 @@ infers the domain arguments:
 
         PredV1 human (UsePN human John) (ComplV2 human game play (UsePN game 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,
@@ -2746,7 +2722,7 @@ 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"). 
 
    
-
+
 
    Proof objects
    
 
    
 Perhaps the most well-known feature of constructive type theory is
@@ -2777,69 +2753,55 @@ 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, thenSucc 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 same thing as 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 ;
 
    
-
    
-
+
+
+
 
    Variable bindings
    
 
    
 Mathematical notation and programming languages have lots of
@@ -2864,7 +2826,6 @@ instance,
     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 @@ -2911,7 +2872,7 @@ for variable-binding expressions? Let us first consider universal quantification, 

    -    fun All : (Ind -> Prop) -> Prop.
+    fun All : (Ind -> Prop) -> Prop

    We write @@ -2921,7 +2882,7 @@ We write

    to obtain the form shown above. -This linearization rule brings in a new GF concept - the v +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 @@ -3000,19 +2961,18 @@ 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 (see below). -

    -

    -When editing with grammars that have -bound variables, the names of bound variables are -selected automatically, but can be changed at any time by -using an Alpha Conversion command. +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, @@ -3060,6 +3020,16 @@ can be applied. For instance, we compute 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 @@ -3106,16 +3076,16 @@ 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 intentional. -In the abstract syntax itself, the reference is always extensional, since +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 (Od one)
-    Proof (Od (succ zero))
+    Proof (Odd one)
+    Proof (Odd (succ zero))

    are equal types. Hence, any tree that type checks as a proof that @@ -3154,12 +3124,24 @@ 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 ;
+
    +

    +

    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, @@ -3232,15 +3214,15 @@ The rest of the modules (black) come from the resource.

    - +

    Restricted inheritance and qualified opening

    - +

    Using the standard resource library

    The example files of this chapter can be found in the directory arithm.

    - +

    The simplest way

    The simplest way is to open a top-level Lang module @@ -3307,7 +3289,7 @@ Here is an example. }

    - +

    How to find resource functions

    The definitions in this example were found by parsing: @@ -3328,7 +3310,7 @@ The definitions in this example were found by parsing: 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 @@ -3406,7 +3388,7 @@ Here, again, a complete example (abstract Arithm is as above): }

    - +

    Transfer modules

    Transfer means noncompositional tree-transforming operations. @@ -3425,9 +3407,9 @@ See the transfer language documentation for more information.

    - +

    Practical issues

    - +

    Lexers and unlexers

    Lexers and unlexers can be chosen from @@ -3463,7 +3445,7 @@ Given by help -lexer, help -unlexer:

    - +

    Efficiency of grammars

    Issues: @@ -3471,10 +3453,10 @@ Issues:

    - +

    Speech input and output

    Thespeak_aloud = sa command sends a string to the speech @@ -3504,7 +3486,7 @@ 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 @@ -3521,12 +3503,12 @@ Here is a snapshot of the editor: The grammars of the snapshot are from the Letter grammar package.

    - +

    Interactive Development Environment (IDE)

    Forthcoming.

    - +

    Communicating with GF

    Other processes can communicate with the GF command interpreter, @@ -3543,7 +3525,7 @@ Thus the most silent way to invoke GF is - +

    Embedded grammars in Haskell, Java, and Prolog

    GF grammars can be used as parts of programs written in the @@ -3555,15 +3537,15 @@ following languages. The links give more documentation.

  • Prolog - +

    Alternative input and output grammar formats

    A summary is given in the following chart of GF grammar compiler phases:

    - +

    Case studies

    - +

    Interfacing formal and natural languages

    Formal and Informal Software Specifications, diff --git a/doc/tutorial/gf-tutorial2.txt b/doc/tutorial/gf-tutorial2.txt index 3df55e1e7..d348af0a7 100644 --- a/doc/tutorial/gf-tutorial2.txt +++ b/doc/tutorial/gf-tutorial2.txt @@ -1930,8 +1930,8 @@ are straightforward, ``` lin - mkAddress country city street = ss (street ++ "," ++ city ++ "," ++ country) ; - + mkAddress country city street = + ss (street.s ++ "," ++ city.s ++ "," ++ country.s) ; UK = ss ("U.K.") ; France = ss ("France") ; Paris = ss ("Paris") ; @@ -2013,8 +2013,6 @@ the context of ``Street`` above. What we claimed to be the 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) @@ -2043,36 +2041,6 @@ sometimes shortens the code, since we can write e.g. ``` - -===Dependent types in syntax editing=== - -An extra advantage of dependent types is seen in -syntax editing: -when menus with possible refinements are created, -only those functions are shown that are type-correct. -For instance, if the editor state is -``` - mkAddress : Address - UK : Country - * ?2 : City UK - ?3 : Street UK ?2 -``` -only the cities of the U.K. are shown in the city menu. - -What is more, editing in the state -``` - mkAddress : Address - ?1 : Country - ?2 : City (?1) - * ?3 : Street (?1) (?2) -``` -//starts// from the ``Street`` argument, -which enables GF automatically to infer the city and the country. -Thus, in addition to guaranteeing the meaningfulness of the results, -dependent types can shorten editing sessions considerably. - - - ===Dependent types in concrete syntax=== The **functional fragment** of GF @@ -2090,28 +2058,26 @@ functions. For instance, Haskell programmers have access to the functions ``` const :: a -> b -> a - const c x = c + const c _ = c - flip :: (a -> b ->c) -> b -> a -> 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,x -> c ; + \_,_,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 the Haskell or ML programmer. - +for a Haskell or ML programmer. @@ -2139,14 +2105,12 @@ verb phrase ("is equilateral") in accordance with the rule that the verb phrase is inflected in the number of the noun phrase: ``` - fun PredV1 : NP -> V1 -> S ; - lin PredV1 np v1 = {s = np.s ++ v1.s ! np.n} ; + 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 @@ -2181,7 +2145,6 @@ but no proposition linearized to ``` since ``Equilateral two`` is not a well-formed type-theoretical object. - 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 @@ -2192,8 +2155,6 @@ is guaranteed in various proof systems based on type theory. 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 @@ -2313,6 +2274,13 @@ infers the domain arguments: ``` PredV1 human (UsePN human John) (ComplV2 human game play (UsePN game 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, @@ -2359,14 +2327,11 @@ 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 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``: ``` @@ -2389,8 +2354,6 @@ whose type is ``` which is the same thing as 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 @@ -2398,8 +2361,6 @@ 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: @@ -2440,7 +2401,6 @@ instance, 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 @@ -2477,14 +2437,14 @@ The question now arises: how to define linearization rules for variable-binding expressions? Let us first consider universal quantification, ``` - fun All : (Ind -> Prop) -> Prop. + 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 ``v`` +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 @@ -2536,7 +2496,6 @@ 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 @@ -2548,13 +2507,12 @@ 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 (see below). - -When //editing// with grammars that have -bound variables, the names of bound variables are -selected automatically, but can be changed at any time by -using an Alpha Conversion command. - +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. @@ -2600,6 +2558,14 @@ can be applied. For instance, we compute 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 @@ -2614,8 +2580,6 @@ are definitionally equal to each other. So are the trees ``` 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 @@ -2641,15 +2605,15 @@ 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 intentional. -In the abstract syntax itself, the reference is always extensional, since +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 (Od one) - Proof (Od (succ zero)) + 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. @@ -2684,6 +2648,17 @@ 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 ; +``` + + %--! @@ -2974,7 +2949,7 @@ Issues: - the choice of datastructures in ``lincat``s - the value of the ``optimize`` flag -- parsing efficiency: ``-mcfg`` vs. others +- parsing efficiency: ``-fcfg`` vs. others ===Speech input and output===