[Logiweb] Larger examples?

[Klaus Ebbe Grue]

Hi Robert,

> Having worked through the tutorials (which are well-written, in my opinion),

Thanks

> I am now looking for other sources of information, guidance, and inspiration 
> as I attempt to improve my working knowledge of Logiweb.

Tutorial T05 covers syntax. I suppose a good next step would be to 
understand the semantics of Logiweb. Unfortunately, I have not yet written 
tutorials on semantics. (But I will give a talk on that in Edinburgh at 
the end of this month - there will probably also be a hands-on session).

At the end of Tutorial T05 it is explained how syntax is converted into a 
"vector" (i.e. "sequence of bytes"). The "semantics" of Logiweb defines 
what such vectors "mean".

I think the most compressed description of what Logiweb does with vectors 
is at http://logiweb.eu/logiweb/doc/browser/loading.html. So, at present,
http://logiweb.eu/logiweb/doc/browser/loading.html is the best available 
description of the semantics of Logiweb.

You probably need a bit of context to get started reading
http://logiweb.eu/logiweb/doc/browser/loading.html:

At the end of Tutorial T05 there is a section entitle "Amnesia" which 
states that once the frontend of the pyk compiler has converted the pyk 
source into a reference and a vector, the pyk compiler forgets the pyk 
source and continues working on the reference and vector.

The relation between reference and vector is as follows: given a vector, 
one can extract the reference from the vector. Once a vector is published 
on Logiweb, one can also convert the other way, i.e. from reference to 
vector. Converting a reference to a vector is called "fetching" in the 
terminology used in http://logiweb.eu/logiweb/doc/browser/loading.html.

http://logiweb.eu/logiweb/doc/browser/loading.html starts from the 
reference, describes how the reference is converted to a vector, and then 
describes what Logiweb does to that vector: it "loads" it, "renders" it, 
and "executes" it.

If you read http://logiweb.eu/logiweb/doc/browser/loading.html right after 
reading Tutorial T05 it may be puzzling that Tutorial T05 leaves you with
a vector but http://logiweb.eu/logiweb/doc/browser/loading.html starts 
with a reference. I hope the explanation above bridges that gap.

Once you are through http://logiweb.eu/logiweb/doc/browser/loading.html 
you will probably have noticed that there are many references to the 
"base" page. In Tutorial T05 you saw that you are the one who defines the 
syntax. It is not forced upon you as it is in e.g. C or Java. After 
reading http://logiweb.eu/logiweb/doc/browser/loading.html you will know 
that the same holds for the semantics: you define the semantics you want 
to use and then publishes it on Logiweb. If you want to use the semantics 
I have defined, fine. Just reference the "base", "check", or "Peano" page 
as first reference. If you want to attach a completely different semantics 
to Logiweb, fine. Just define it, publish it on Logiweb, and reference it 
as first reference in your future work. But before you decide to take 
complete control over Logiweb, I suggest you work with the semantics I 
have published on the "base" page.

The remark above also gives a hint on another source of information: You 
may simply read the "base" page (there are lots of references to it from 
http://logiweb.eu/logiweb/doc/browser/loading.html). The only problem is 
that it is 50 pages long and might give you more details than you want. 
And if the "base" page does not discourage you, you may continue with the 
"check" and "Peano" pages.

> I have found the 
> Peano example, but it is very foundational.  Are there any examples from 
> other parts of mathematics?  Perhaps pages which define things such as 
> groups, polynomials, or graphs?

I agree that Frederiks Ph.D. thesis (which was effectively handed in by 
publishing it on Logiweb) is the most impressive piece of work that has 
been published on Logiweb to date. Unfortunately, it is written in Danish.

And then there are two rather big examples which have *not* been put on 
Logiweb yet, but which were written explicitly with that in mind. They are 
at http://www.diku.dk/~grue/papers/classical/classical.html and
http://www.diku.dk/~grue/papers/mac0102/

> As an exercise for myself, I am attempting to define a bit of ring theory in 
> the system, and would be grateful for pointers to models and other 
> documentation which may exist.  While the tutorials were a good introduction 
> to the flavor of the system, the examples there are quite small.

It *should* be possible to jump directly to such applications. But it is 
probably still a good idea to know a little about the semantics: you will 
probably soon want to program your own side conditions or your own proof 
tactics. And you probably soon want to save yourself a lot of typing by 
defining your own macros. And last, not least, you will need a little 
knowledge of the semantics the moment you need to "debug" a proof.

I hope it helps. I on my part will try to write some more tutorials. And 
don't hesitate to ask again.

Cheers,
Klaus