2.6 Definitions

Prev Up Next Page 9 of 800 Search internet

Lines 33 and 34 of combinations.lgs contain a definition:

    33  "[[[ value define (( n , k )) as if k = 0 then 1
    34  else (( n - 1 , k - 1 )) * n div k end define ]]]"

That definition defines the 'value aspect' of the binomial coefficient. Or, stated shorter, it defines the value of the binomial coefficient.

Lines 47-50 of combinations.lgs also contain a definition:

    47  \item "[[ tex show define (( n , k )) as "
    48  \left( \begin{array}{l} "[ n ]"
    49  \\ "[ k ]"
    50  \end{array}\right)" end define ]]"

That definition defines the 'show aspect' of the binomial coefficient. (The 'tex' in Line 47 is a rudiment from the base page; the aspect is the 'show' aspect, not the 'tex show' aspect).

In general, a Logiweb definition has a left hand side which contains the thing being defined, a right hand side which contains the definition, and an 'aspect' which indicates what is being defined. The value aspect defines how the binomial coefficient is computed and the show aspect defines how the binomial coefficient is rendered.

The multzero page contains this definition:

PA lemma 3.2l : all x : 0 * x = 0 end lemma

That definition defines the 'statement/kg' aspect of 3.2l to be

PA infer all x : 0 * x = 0

Logiweb assigns a meaning to certain reserved aspects like 'value' and 'show'. An aspect is reserved if it is identified by a string which contains nothing but small letters a to z and space characters. If you want to introduce your own aspects, include a capital letter or something else which makes it non-reserved. The 'statement/kg' is non-reserved because it contains a slash. That aspect is used by the proof checker defined on the check page.

The combinations page defines two constructs: the binomial coefficient (( x , y )) and a construct named combinations. The latter is the 'page construct'. The page construct is the construct introduced by the ""P escape sequence. The page construct never takes arguments and always has charge zero. The page construct is used whenever there is a need for referring to a Logiweb page as a whole.

The combinations page contains six definitions:

You can see a rendering of the four latter definitions in the chores annex. You can also find a full list of all definitions in the extract generated by the lgc compiler.

Now recall that the source of the combinations page reads:

     1  "";;0143BAB3BC67212340C9406BDB560819F3DCD4E859FC96F7B1C2B2BB0806
     2  ""P combinations
     4  ""R base
     6  ""D 0
     7  (( " , " ))
     9  ""B
    10  page ( ""N , ""C )
    11  title "Combinations"
    53  end page

The lgc compiler expands the quot;quot;N escape sequence into a list of name definitions, one for each construct of the page. Likewise, the lgc compiler expands the quot;quot;C escape sequence into a list of charge definitions (N and C for Name and Charge, respectively). The page ... end page construct puts those lists of name and charge definitions into the chores annex.

Whenever you reference a Logiweb page from your own page, the lgc compiler uses the name and charge definitions of the referenced page to figure out the available grammar. Furthermore, the name definition provides a default when a construct has no show definition.

Prev Up Next Page 9 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05