Logiweb(TM)     Logiweb system pages  
        Tutorial T02: Programming  
 

System pages
Site pages

Introduction...
Showroom
Tutorials
Man pages
Help
Download
Wiki...
Wiki submission
Background
Machine room...
Contact

T01: Hello world
T02: Programming
T03: Proving
T04: Googling
T05: Syntax

   

Up. Submission form.

Introduction

The present tutorial teaches how to write and test a program.

Prerequisites

You must have done Tutorial T01: Hello world.

References

As in Tutorial T01: Hello world, construct a page with the following bibliography:

PAGE my page
BIBLIOGRAPHY
"check" "http:../../../page/check/latest/vector/page.lgw".
"base" "http:../../../page/base/latest/vector/page.lgw".

In case you have forgot, these are the steps to perform:

  • Open the header creation form in a separate window (in most browsers: right click the link and select something like 'open in new window').
  • Enter the text above in the upper text window.
  • Click 'Suggest Header'.
  • Enter some strings in the 'org=' and 'name=' fields.

Introduce a new construct

In the upper window, add a line after the one saying "base" base:

...
PREASSOCIATIVE
"check" check
"base" base
"" (( " , " ))
PREASSOCIATIVE
"base" +"
...

The "" (( " , " )) line above introduces a new, binary construct named (( X , Y )). The first two quotes make up an empty string which signifies that the line introduces a new construct rather than importing one. After the first two quotes, all remaining quotes until the end of the line are placeholders for parameters.

The new construct gets the same priority and associativity as the 'check' and 'base' constructs. The priority and associativity has no effect for the (( X , Y )) construct since the construct is 'closed' (starts and ends with a non-variable). Priority and associativity only has effect for 'open' constructs like 'X + Y' which start and end with variables, for 'prefix' constructs like 'if X then Y else Z' which start with a non-varible and ends with a variable, and for 'suffix' constructs like 'X factorial' which start with a variable and end with a non-varible.

Define the new construct

Put the following in the lower text window:

BODY
page ( Pyk , Priority )
title "Combinations"
bib "
@techreport{appendix,
  author    = {A. U. Thor},
  year      = {2006},
  title     = {Combinations - appendix},
  institution={Logiweb},
  note      = {\href{\lgwrelay/64/\lgwThisBlockBaseSixtyFour/2/body/tex/appendix.pdf}{%
\lgwBreakRelay 64/\lgwThisBreakBaseSixtyFour /2/body/tex/appendix.pdf}}}
"
main text "
\title{Combinations}
\author{A. U. Thor}
\maketitle
\tableofcontents
\section{Combinations}
The number of combinations of size "[[ k ]]" from a set
of size "[[ n ]]" is given by the binomial coefficient
"[[ (( n , k )) = n factorial div k factorial
div ( n - k ) factorial ]]". A recursive definition
of "[[ (( n , k )) ]]" may be stated thus:
"[[[ value define (( n , k )) as if k = 0 then 1
else (( n - 1 , k - 1 )) * n div k end define ]]]"
As an example, we have "[[ ttst (( 4 , 2 )) = 6 end test ]]".
For details on how the binomial coefficient is rendered, see
\cite{appendix}.
\bibliography{./page}
"
appendix "
\title{Combinations - appendix}
\author{A. U. Thor}
\maketitle
\tableofcontents
\section{\TeX\ definitions}
\begin{statements}
\item "[[ tex define (( n , k )) as "
\left( \begin{array}{l} "[ n ]"
\\ "[ k ]"
\end{array}\right)" end define ]]"
\end{statements}
"
end page

The text above is a mixture of free text (like \title{Combinations}) and pyk source. Pyk source must be enclosed in "[ ... ]" as in

bla bla bla "[ x + y ]" bla bla bla

The "[[ X ]]" constructs is like "[ X ]" but also inserts dollar signs around X so that TeX renders X in math mode. In other words, "[[ X ]]" is equivalent to $ "[ X ]" $. The "[[[ X ]]]" is like "[[ X ]]" except that it generates a displayed equation. The 'statements' environment is defined by the 'page' construct. If you are not satisfied with "[ X ]" et al, define your own ones (see the 'tex' definitions of "[ X ]" and "[[ X ]]" on the base page for inspiration). If you are not satisfied with the setup made by the 'page' construct, look at the definitions of 'page' on the base page or see the pyk source of the base page for a different approach where you write everything starting from \documentclass{article} and specify when to run LaTeX et al.

The 'ttst X end test' asks Logiweb to compute X and verify that it equals T (truth). Other tests are 'ftst X end test' which tests that X equals F (falsehood) and 'etst X ; Y end test' which tests that X equals Y. The etst construct is satisfied if X and Y are equal or throw the same exception. The ttst and ftst tests fail if X throws an exception. See the base page for a definition of 'equality', which is really a partial equivalence relation. As an example, if computation of X or Y loops indefinitely, then 'etst X ; Y end test' will never return an answer.

Submit your page

  • Use the 'level' control to change 'level=body' to 'level=all'.
  • Click 'Submit'.

Setting level=all makes the backend of the pyk compiler generate almost all the output it is able to generate. Normally, one will ask for less (e.g. level=body) to save time.

There is one level above level=all, namely level=submit. With level=submit, your page is actually submitted to Logiweb. Once submitted, you may not be able to delete your page again since your page may be mirrorred by mirror sites from which you may not be able to delete your page. So beware what you write before you set level=submit.

Viewing your page

Click to your page (following the here link in the Logiwiki response). Then click 'Body' and 'Pdf' to see your page.

As you can see, the binomial coefficient is rendered the usual way. That is because of your 'tex' definition in your appendix.

Your main text contains a value definition and a test case. The test case verifies that one can take pick two elements from a set with four elements in six ways.

A Logiweb definition consists of a left hand side, a right hand side, and an 'aspect'. Your main text defines the 'value' aspect of the binomial coefficient whereas your appendix defines the 'tex' aspect. It is possible to assign any number of aspects to any construct.

The main text ends with a reference to an appendix. If you click the reference you get a 'Page not found'. That particular reference only works when you choose level=submit since it is a an official Logiweb reference and only works for pages which are really submitted.

In Tutorial T01: Hello world you saw that the 'chores' part of your page contained 'pyk' and 'priority' definitions.

You can see all definitions on your page by navigating to the Codex of your page (follow the here link to the main menu and click 'Codex').

Try navigating to the Codex and open the Pdf version. The priority definition of 'my page' takes up quite a number of pages. So read the last and penultimate pages. There you will find a value, a pyk, and a tex definition of the binomial coefficient and a pyk definition of 'my page'. The 'my page' construct has no tex definition, so the rendering of 'my page' is based on the pyk definition instead.

Pyk inserts a number of understood parentheses when rendering the codex. Pyk uses blue square brackets for understood parentheses.

Also try to go to the page named 'Logiweb codex of my page' and click 'Pyk'. That allows to see the definitions expressed in the pyk language. In the pyk version of the codex, braces are used for understood parentheses.

As another experiment, try to modify the test such that it fails, submit your page again and view the diagnose.

As a third experiment, try to add a test saying 'ttst trace ( (( 4 , 2 )) ) end test''. The 'trace ( X )' construct returns T (truth) but, as a side effect, prints the value of (( 4 , 2 )) to standard output. This may be handy for debugging. There is also a 'spy ( X )' construct which sets an internal variable of the pyk compiler to the value of X for later inspection (see the 'quit', 'spy', 'spydepth', and 'spylength' options of the pyk compiler in man pyk for details). Among other, ttst, ftst, and etst set the spy variable to the construct being tested so that if the test loops indefinitely then the user can find out which test was being conducted when the user lost his patience and killed pyk. The 'trace' and 'spy' constructs can be used in any code executed by the pyk compiler: tests, proof tactics, macro expanders, page unpackers, rendering engines, Logiweb machines, etc. But only use 'trace' and 'spy' for debugging. If you want user interaction, use the IO capabilities of Logiweb machines (c.f. the base page).

Suggestion for further work

Try to submit your 'Combinations' paper (using 'level=submit'). Then try to write a new paper which references your Combinations paper as well as the check and base pages (make sure to reference the 'check' page as your first reference such that 'check' becomes your bed page - otherwise you have no macro expansion or verification machinery at your disposal). Then try to verify e.g. (( 5 , 2 )) = 10 on your new page.

Conclusion

You have now produced your first Logiweb program (the (( x , y )) construct). You have also tested your program using [ ttst (( 4 , 2 )) = 6 end test ].

Up. Submission form.