diff options
| author | aarne <aarne@cs.chalmers.se> | 2006-06-16 15:29:01 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2006-06-16 15:29:01 +0000 |
| commit | df3b453f3b5697f4c29d2fa394799564a3d2bb90 (patch) | |
| tree | a85d4e60eb54123031832e900b8b431bb6c5c19a | |
| parent | c84e19b21d782404b842da738706c86816a68b27 (diff) | |
tutorial edited
| -rw-r--r-- | doc/tutorial/gf-tutorial2.html | 236 | ||||
| -rw-r--r-- | 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 @@ <P ALIGN="center"><CENTER><H1>Grammatical Framework Tutorial</H1> <FONT SIZE="4"> <I>Author: Aarne Ranta <aarne (at) cs.chalmers.se></I><BR> -Last update: Fri Jun 16 10:32:52 2006 +Last update: Fri Jun 16 17:28:39 2006 </FONT></CENTER> <P></P> @@ -100,40 +100,39 @@ Last update: Fri Jun 16 10:32:52 2006 <UL> <LI><A HREF="#toc66">GF as a logical framework</A> <LI><A HREF="#toc67">Dependent types</A> - <LI><A HREF="#toc68">Dependent types in syntax editing</A> - <LI><A HREF="#toc69">Dependent types in concrete syntax</A> - <LI><A HREF="#toc70">Expressing selectional restrictions</A> - <LI><A HREF="#toc71">Proof objects</A> - <LI><A HREF="#toc72">Variable bindings</A> - <LI><A HREF="#toc73">Semantic definitions</A> + <LI><A HREF="#toc68">Dependent types in concrete syntax</A> + <LI><A HREF="#toc69">Expressing selectional restrictions</A> + <LI><A HREF="#toc70">Proof objects</A> + <LI><A HREF="#toc71">Variable bindings</A> + <LI><A HREF="#toc72">Semantic definitions</A> </UL> - <LI><A HREF="#toc74">More features of the module system</A> + <LI><A HREF="#toc73">More features of the module system</A> <UL> - <LI><A HREF="#toc75">Interfaces, instances, and functors</A> - <LI><A HREF="#toc76">Resource grammars and their reuse</A> - <LI><A HREF="#toc77">Restricted inheritance and qualified opening</A> + <LI><A HREF="#toc74">Interfaces, instances, and functors</A> + <LI><A HREF="#toc75">Resource grammars and their reuse</A> + <LI><A HREF="#toc76">Restricted inheritance and qualified opening</A> </UL> - <LI><A HREF="#toc78">Using the standard resource library</A> + <LI><A HREF="#toc77">Using the standard resource library</A> <UL> - <LI><A HREF="#toc79">The simplest way</A> - <LI><A HREF="#toc80">How to find resource functions</A> - <LI><A HREF="#toc81">A functor implementation</A> + <LI><A HREF="#toc78">The simplest way</A> + <LI><A HREF="#toc79">How to find resource functions</A> + <LI><A HREF="#toc80">A functor implementation</A> </UL> - <LI><A HREF="#toc82">Transfer modules</A> - <LI><A HREF="#toc83">Practical issues</A> + <LI><A HREF="#toc81">Transfer modules</A> + <LI><A HREF="#toc82">Practical issues</A> <UL> - <LI><A HREF="#toc84">Lexers and unlexers</A> - <LI><A HREF="#toc85">Efficiency of grammars</A> - <LI><A HREF="#toc86">Speech input and output</A> - <LI><A HREF="#toc87">Multilingual syntax editor</A> - <LI><A HREF="#toc88">Interactive Development Environment (IDE)</A> - <LI><A HREF="#toc89">Communicating with GF</A> - <LI><A HREF="#toc90">Embedded grammars in Haskell, Java, and Prolog</A> - <LI><A HREF="#toc91">Alternative input and output grammar formats</A> + <LI><A HREF="#toc83">Lexers and unlexers</A> + <LI><A HREF="#toc84">Efficiency of grammars</A> + <LI><A HREF="#toc85">Speech input and output</A> + <LI><A HREF="#toc86">Multilingual syntax editor</A> + <LI><A HREF="#toc87">Interactive Development Environment (IDE)</A> + <LI><A HREF="#toc88">Communicating with GF</A> + <LI><A HREF="#toc89">Embedded grammars in Haskell, Java, and Prolog</A> + <LI><A HREF="#toc90">Alternative input and output grammar formats</A> </UL> - <LI><A HREF="#toc92">Case studies</A> + <LI><A HREF="#toc91">Case studies</A> <UL> - <LI><A HREF="#toc93">Interfacing formal and natural languages</A> + <LI><A HREF="#toc92">Interfacing formal and natural languages</A> </UL> </UL> @@ -2273,8 +2272,8 @@ are straightforward, <PRE> 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. </PRE> <P></P> <A NAME="toc68"></A> -<H3>Dependent types in syntax editing</H3> -<P> -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 -</P> -<PRE> - mkAddress : Address - UK : Country - * ?2 : City UK - ?3 : Street UK ?2 -</PRE> -<P> -only the cities of the U.K. are shown in the city menu. -</P> -<P> -What is more, editing in the state -</P> -<PRE> - mkAddress : Address - ?1 : Country - ?2 : City (?1) - * ?3 : Street (?1) (?2) -</PRE> -<P> -<I>starts</I> from the <CODE>Street</CODE> 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. -</P> -<A NAME="toc69"></A> <H3>Dependent types in concrete syntax</H3> <P> The <B>functional fragment</B> of GF @@ -2452,9 +2418,9 @@ the functions </P> <PRE> 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 </PRE> <P> @@ -2467,7 +2433,7 @@ definitions can be written </P> <PRE> 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 <P> 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. </P> -<A NAME="toc70"></A> +<A NAME="toc69"></A> <H3>Expressing selectional restrictions</H3> <P> 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: </P> <PRE> - 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} ; </PRE> <P> It is ill-formed because the predicate "is equilateral" @@ -2719,7 +2685,17 @@ infers the domain arguments: <PRE> PredV1 human (UsePN human John) (ComplV2 human game play (UsePN game Golf)) </PRE> -<P></P> +<P> +To try this out in GF, use <CODE>pt = put_term</CODE> with the <B>tree transformation</B> +that solves the metavariables by type checking: +</P> +<PRE> + > p -tr "John plays golf" | pt -transform=solve + > p -tr "golf plays John" | pt -transform=solve +</PRE> +<P> +In the latter case, no solutions are found. +</P> <P> A known problem with selectional restrictions is that they can be more or less liberal. For instance, @@ -2746,7 +2722,7 @@ a <CODE>man</CODE> and a <CODE>woman</CODE>, but not the other way round) and the <B>extended use</B> of expressions (e.g. a metaphoric use that makes sense of "golf plays John"). </P> -<A NAME="toc71"></A> +<A NAME="toc70"></A> <H3>Proof objects</H3> <P> Perhaps the most well-known feature of constructive type theory is @@ -2777,69 +2753,55 @@ a number <I>y</I>. Our definition is based on two axioms: <UL> <LI><CODE>Zero</CODE> is less than <CODE>Succ y</CODE> for any <CODE>y</CODE>. <LI>If <CODE>x</CODE> is less than <CODE>y</CODE>, then<CODE>Succ x</CODE> is less than <CODE>Succ y</CODE>. -</UL> - -<P> +<P></P> The most straightforward way of expressing these axioms in type theory is as typing judgements that introduce objects of a type <CODE>Less x y</CODE>: -</P> <PRE> 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) ; </PRE> -<P> Objects formed by <CODE>lessZ</CODE> and <CODE>lessS</CODE> are called <B>proof objects</B>: they establish the truth of certain mathematical propositions. For instance, the fact that 2 is less that 4 has the proof object -</P> <PRE> lessS (Succ Zero) (Succ (Succ (Succ Zero))) (lessS Zero (Succ (Succ Zero)) (lessZ (Succ Zero))) </PRE> -<P> whose type is -</P> <PRE> Less (Succ (Succ Zero)) (Succ (Succ (Succ (Succ Zero)))) </PRE> -<P> which is the same thing as the proposition that 2 is less than 4. -</P> -<P> +<P></P> GF grammars can be used to provide a <B>semantic control</B> 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. -</P> -<P> +<P></P> A simple example of the use of proof objects is the definition of well-formed <I>time spans</I>: a time span is expected to be from an earlier to a later time: -</P> <PRE> from 3 to 8 </PRE> -<P> is thus well-formed, whereas -</P> <PRE> from 8 to 3 </PRE> -<P> is not. The following rules for spans impose this condition by using the <CODE>Less</CODE> predicate: -</P> <PRE> cat Span ; fun span : (m,n : Nat) -> Less m n -> Span ; </PRE> -<P></P> -<A NAME="toc72"></A> +</UL> + +<A NAME="toc71"></A> <H3>Variable bindings</H3> <P> 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 </PRE> -<P></P> <P> 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, </P> <PRE> - fun All : (Ind -> Prop) -> Prop. + fun All : (Ind -> Prop) -> Prop </PRE> <P> We write @@ -2921,7 +2882,7 @@ We write </PRE> <P> to obtain the form shown above. -This linearization rule brings in a new GF concept - the <CODE>v</CODE> +This linearization rule brings in a new GF concept - the <CODE>$0</CODE> field of <CODE>B</CODE> containing a bound variable symbol. The general rule is that, if an argument type of a function is itself a function type <CODE>A -> C</CODE>, the linearization type of @@ -3000,19 +2961,18 @@ To be able to <I>parse</I> variable symbols, however, GF needs to know what to look for (instead of e.g. trying to parse <I>any</I> string as a variable). What strings are parsed as variable symbols -is defined in the lexical analysis part of GF parsing (see below). -</P> -<P> -When <I>editing</I> 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> +<PRE> + > p -cat=Prop -lexer=codevars "(All x)(x = x)" + All (\x -> Eq x x) +</PRE> <P> +(see more details on lexers below). If several variables are bound in the same argument, the labels are <CODE>$0, $1, $2</CODE>, etc. </P> -<A NAME="toc73"></A> +<A NAME="toc72"></A> <H3>Semantic definitions</H3> <P> We have seen that, @@ -3060,6 +3020,16 @@ can be applied. For instance, we compute succ (sum (succ zero) zero) --> succ (succ zero) </PRE> +<P> +Computation in GF is performed with the <CODE>pt</CODE> command and the +<CODE>compute</CODE> transformation, e.g. +</P> +<PRE> + > p -tr "1 + 1" | pt -transform=compute -tr | l + sum one one + succ (succ zero) + s(s(0)) +</PRE> <P></P> <P> The <CODE>def</CODE> definitions of a grammar induce a notion of @@ -3106,16 +3076,16 @@ expression, which are definitionally equal. </P> <P> 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 <B>type checking is extensional</B>. 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, </P> <PRE> - Proof (Od one) - Proof (Od (succ zero)) + Proof (Odd one) + Proof (Odd (succ zero)) </PRE> <P> are equal types. Hence, any tree that type checks as a proof that @@ -3154,12 +3124,24 @@ are marked with a flag <CODE>C</CODE>), new constructors can be added to a type with new <CODE>data</CODE> judgements. The type signatures of constructors are given separately, in ordinary <CODE>fun</CODE> judgements. +One can also write directly </P> -<A NAME="toc74"></A> +<PRE> + data succ : Nat -> Nat ; +</PRE> +<P> +which is equivalent to the two judgements +</P> +<PRE> + fun succ : Nat -> Nat ; + data Nat = succ ; +</PRE> +<P></P> +<A NAME="toc73"></A> <H2>More features of the module system</H2> -<A NAME="toc75"></A> +<A NAME="toc74"></A> <H3>Interfaces, instances, and functors</H3> -<A NAME="toc76"></A> +<A NAME="toc75"></A> <H3>Resource grammars and their reuse</H3> <P> A resource grammar is a grammar built on linguistic grounds, @@ -3232,15 +3214,15 @@ The rest of the modules (black) come from the resource. <P> <IMG ALIGN="middle" SRC="Multi.png" BORDER="0" ALT=""> </P> -<A NAME="toc77"></A> +<A NAME="toc76"></A> <H3>Restricted inheritance and qualified opening</H3> -<A NAME="toc78"></A> +<A NAME="toc77"></A> <H2>Using the standard resource library</H2> <P> The example files of this chapter can be found in the directory <A HREF="./arithm"><CODE>arithm</CODE></A>. </P> -<A NAME="toc79"></A> +<A NAME="toc78"></A> <H3>The simplest way</H3> <P> The simplest way is to <CODE>open</CODE> a top-level <CODE>Lang</CODE> module @@ -3307,7 +3289,7 @@ Here is an example. } </PRE> <P></P> -<A NAME="toc80"></A> +<A NAME="toc79"></A> <H3>How to find resource functions</H3> <P> 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 <B>example-based grammar writing</B>, to which we will return later. </P> -<A NAME="toc81"></A> +<A NAME="toc80"></A> <H3>A functor implementation</H3> <P> The interesting thing now is that the @@ -3406,7 +3388,7 @@ Here, again, a complete example (<CODE>abstract Arithm</CODE> is as above): } </PRE> <P></P> -<A NAME="toc82"></A> +<A NAME="toc81"></A> <H2>Transfer modules</H2> <P> Transfer means noncompositional tree-transforming operations. @@ -3425,9 +3407,9 @@ See the <A HREF="../transfer.html">transfer language documentation</A> for more information. </P> -<A NAME="toc83"></A> +<A NAME="toc82"></A> <H2>Practical issues</H2> -<A NAME="toc84"></A> +<A NAME="toc83"></A> <H3>Lexers and unlexers</H3> <P> Lexers and unlexers can be chosen from @@ -3463,7 +3445,7 @@ Given by <CODE>help -lexer</CODE>, <CODE>help -unlexer</CODE>: </PRE> <P></P> -<A NAME="toc85"></A> +<A NAME="toc84"></A> <H3>Efficiency of grammars</H3> <P> Issues: @@ -3471,10 +3453,10 @@ Issues: <UL> <LI>the choice of datastructures in <CODE>lincat</CODE>s <LI>the value of the <CODE>optimize</CODE> flag -<LI>parsing efficiency: <CODE>-mcfg</CODE> vs. others +<LI>parsing efficiency: <CODE>-fcfg</CODE> vs. others </UL> -<A NAME="toc86"></A> +<A NAME="toc85"></A> <H3>Speech input and output</H3> <P> The<CODE>speak_aloud = sa</CODE> 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. </P> -<A NAME="toc87"></A> +<A NAME="toc86"></A> <H3>Multilingual syntax editor</H3> <P> The @@ -3521,12 +3503,12 @@ Here is a snapshot of the editor: The grammars of the snapshot are from the <A HREF="http://www.cs.chalmers.se/~aarne/GF/examples/letter">Letter grammar package</A>. </P> -<A NAME="toc88"></A> +<A NAME="toc87"></A> <H3>Interactive Development Environment (IDE)</H3> <P> Forthcoming. </P> -<A NAME="toc89"></A> +<A NAME="toc88"></A> <H3>Communicating with GF</H3> <P> Other processes can communicate with the GF command interpreter, @@ -3543,7 +3525,7 @@ Thus the most silent way to invoke GF is </PRE> </UL> -<A NAME="toc90"></A> +<A NAME="toc89"></A> <H3>Embedded grammars in Haskell, Java, and Prolog</H3> <P> GF grammars can be used as parts of programs written in the @@ -3555,15 +3537,15 @@ following languages. The links give more documentation. <LI><A HREF="http://www.cs.chalmers.se/~peb/software.html">Prolog</A> </UL> -<A NAME="toc91"></A> +<A NAME="toc90"></A> <H3>Alternative input and output grammar formats</H3> <P> A summary is given in the following chart of GF grammar compiler phases: <IMG ALIGN="middle" SRC="../gf-compiler.png" BORDER="0" ALT=""> </P> -<A NAME="toc92"></A> +<A NAME="toc91"></A> <H2>Case studies</H2> -<A NAME="toc93"></A> +<A NAME="toc92"></A> <H3>Interfacing formal and natural languages</H3> <P> <A HREF="http://www.cs.chalmers.se/~krijo/thesis/thesisA4.pdf">Formal and Informal Software Specifications</A>, 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=== |