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
_______________________________________________
Logiweb mailing list
Logiweb@diku.dk
http://lists.diku.dk/mailman/listinfo/logiweb
(Web access from inside DIKUs LAN only)
