[TYPES/announce] Logiweb

[Klaus Ebbe Grue]

I am happy to announce the release of the "Logiweb" system.

Logiweb is a system for creating a world wide web of theorems, proofs, and 
much more.

To read more or to try Logiweb in your browser, go to http://logiweb.eu/ 
or http://logiweb.imm.dtu.dk/.

Logiweb is available under the GNU public license.

Have fun,
Klaus Grue

---

Features of Logiweb

User defined grammar. You may decide e.g. to write 'all X : Y' to get a 
universal quantifier.

User defined rendering. You may decide e.g. to render 'all X : Y' as
'\forall X \colon Y'.

User defined proof checker. You may define your own proof checker and 
publish it on Logiweb. Or you may decide to use a proof checker published 
on Logiweb by somebody else. For a sample proof checker and some sample 
proofs go to http://logiweb.eu/logiweb/page/check/fixed/body/index.html 
and click 'PDF'.

User defined logic. You may define your own axiomatic system. Or you may 
decide to use an axiomatic system published on Logiweb by somebody else.
For sample definition of propositional calculus, first order predicate
calculus, and Peano arithmetic, go to
http://logiweb.eu/logiweb/page/check/fixed/body/index.html and click
'PDF'.

Turing complete macro expansion. You may define e.g. that < 1 , 2 , 3 > 
macro expands to 1 :: 2 :: 3 :: <>. Or you may define e.g. that x , y > 5 
macro expands to x > 5 & y > 5. Or you may define e.g. that x , y in Odd , 
Prime macro expands to x in Odd & x in Prime & y in Odd & y in Prime.

Journal quality pages. In analogy to 'web pages', anything published on 
Logiweb is a 'Logiweb page'. Logiweb pages may contain a mixture of 
arbitrary LaTeX and formal, machine verified mathematics. Users may 
utilize this to produce journal quality pages.

Standing on the shoulders of others. Logiweb pages may reference 
previously published Logiweb pages. Definitions, lemmas, proofs, axiomatic 
systems, proof checkers, macros, etc. on referenced pages can be used on 
referencing pages.

Secure publication. Once published, Logiweb pages get a unique identifier 
by the system (base on a RIPEMD-160 global hash key). After publication, 
pages may be mirrored, and pages continue to exist as long as just one 
copy remains on Logiweb. Pages cannot change once published making it 
secure to reference pages published by somebody else.

Automatic loading. When a Logiweb page is machine verified, all 
transitively referenced pages are located, fetched, and verified as well. 
Once verified pages are cached.

Reader friendly. While authors of Logiweb pages must either use a Logiwiki 
or install Logiweb locally, readers can view Logiweb pages using an 
ordinary web browser.

Axiomatic mixture. The demo proof checker which comes with Logiweb allows 
to define arbitrary axiomatic theories and to use several axiomatic 
theories on the same Logiweb page. As an example, it is possible to define 
both ZFC and NBG and to state and prove theorems in both systems on one 
Logiweb page.

Lambda calculus. The programming language of Logiweb is essentially lambda 
calculus. A few twists make the programming language efficient. Using 
lambda calculus makes it easy to formulate theorems about Logiweb 
programs.

Stand alone executables. The notion of a 'Logiweb machine' allows to 
express stand alone executables. A Logiweb machine extends lambda calculus 
with facilities for I/O and interrupt processing. Each Logiweb page can 
define an arbitrary number of Logiweb machines which can be translated to 
stand alone executables when rendering the page.



How you can help

First of all, you can help by helping yourself: publish on Logiweb. After 
years of design, implementation, and local use, Logiweb is ready to 
receive contents. Small contributions of contents will be received with 
appreciation, big ones with greed. If you publish a good Logiweb page, 
please let me know (grue at diku.dk). Then I will review it and announce it 
at the logiweb-notices mailing list.

If you have a spare Linux box with Internet access, it would be very 
helpful for the project if you would download and install the Logiweb 
software. The software includes a server which will connect to other 
Logiweb servers. The more computers Logiweb runs on, the better will the 
distributed aspect of the system be tested. You do not need to install the 
software in order to publish on Logiweb (you may use the Logiwiki at 
http://logiweb.eu/ or http://logiweb.imm.dtu.dk/). But if you publish on 
Logiweb you will probably find it most convenient in the long run to have 
your own copy on your own machine.

If you develop mathematical software yourself then consider interfacing 
with Logiweb. Your system might benefit from version control or web 
distribution or rendering or some other feature of Logiweb. To connect 
your system to Logiweb, install Logiweb on a machine which runs your 
system and enable access to your system in the Logiweb configuration file. 
When the connection is in place you may start exploring how to use it. A 
connection to MIZAR is in place, work on exploring it is in progress, and 
connections to other systems are under consideration.

An "Introduction to Logiweb" is included below.

---

Introduction to Logiweb

Logiweb is a Swiss army knife for mathematicians, software engineers, 
logicians, programmers, computer scientists, conference chairs, editors, 
and others who write or handle text which both has to be read by others 
and has to be processed by machine. Few people will need all of Logiweb. 
But many people can benefit from some of Logiweb.

Logiweb combines literate programming, web publication, and version 
control.

Logiweb supports the writing and editing of programs, operating systems, 
mathematical textbooks, scientific papers, journals, proceedings, lemmas, 
proofs, mathematical libraries, program libraries, program documentation, 
software life-cycle documents, test suites, and other kinds of 
information.

Logiweb offers document production, program compilation, safe linking of 
programs against libraries across the Internet, software integration and 
test, proof checking, interfacing to external tools, and other kinds of 
machine processing of information. Logiweb also offers web publication and 
version control. And in addition to that, Logiweb offers a lot more.

Logiweb is small. When downloading it, the whole download is less than a 
megabyte. And all of Logiweb except its logo is available under the GNU 
public license.

Logiweb is documented. It is feasible to learn all there is to learn about 
it to the level where you could implement it yourself if you wanted.

The following sections explain how Logiweb could be of help to:
- Mathematicians
- Programmers 
- Logicians 
- Computer scientists 
- Software engineers 
- Conference chairs and editors



For mathematicians

As a mathematician, you may use Logiweb as a tool for writing scientific 
papers, lecture notes, and text books. As an example, you can tell Logiweb 
that (( n , m )) denotes the number of combinations in which one can pick 
m elements from a set of n elements. Furthermore, you can tell Logiweb 
that (( n , m )) should be rendered as

    \left(\begin{array}{l} n \\ m \end{array}\right)

Then you may write things like

    \section{The binomial coefficient}

    Define the binomial coefficient "[[ (( n , m )) ]]" thus:

    "[[[ (( n , m )) = n ! over m ! ( n ~V m ) ! ]]]"

    One property of the binomial coefficient reads:

    "[[[ sum m from 0 to n : (( n , m )) = 2 power n ]]]"

With suitable headers, the text above generates nicely typeset text in 
which the binomial coefficient is rendered the way such coefficients are 
usually rendered, the sum is represented as a capital sigma with m=0 
underneath and n above, and so on.

When you are satisfied with the paper, lecture note, or book, then you may 
ask Logiweb to publish it. That way the paper comes under Logiweb version 
control and becomes accessible to anyone with an Internet connection. In 
analogy to the World Wide Web, pieces of work submitted to Logiweb are 
called 'Logiweb pages' even though 'paper' or 'book' or 'document' might 
be more appropriate.

Once the paper is published, your colleagues or students may reference it 
using Logiweb. One benefit of referencing a paper is that all definitions 
on the referenced paper become accessible, so your colleagues or students 
may start writing (( n , m )) for binomial coefficients. And if you were 
lucky, you didn't have to define the binomial coefficient yourself in the 
first place if you could find it on Logiweb.

If you publish exercises for your students then your students may hand in 
their answers through Logiweb. And if you define an algorithm which tells 
whether or not a result is correct (e.g. asking for the inverse of a given 
matrix and checking by comparing the answer with the correct result) then 
you may use Logiweb to check the answers. And if you publish the checking 
algorithm on Logiweb, then the students can check their answers 
themselves.



For programmers

To program using Logiweb, you may either use Logiwebs own programming 
language or use an external one.

The Logiweb programming language is lambda calculus. Due to Logiwebs heavy 
optimization machinery, the Logiweb programming language is suited for 
programming in the large. If you are used to functional programming, you 
should be able to write programs in the Logiweb programming language with 
little instruction. Just do Tutorial T02 and T05 and look into 
http://logiweb.eu/logiweb/page/check/fixed/body/tex/page.pdf to see how 
things are done there. As an example, to define the factorial function you 
would write:

    \section{The factorial function}
    For natural numbers "[[ n ]]" define the factorial "[[ n ! ]]" as the
    product of the numbers between "[[ 1 ]]" and "[[ n ]]", inclusive. A
    definition reads

    "[[[ eager define n ! as if n = 0 then 1 else n * ( n ~V 1 ) ! ]]]"

    As a test case we have "[[ ttst 5 ! = 120 end test ]]".

If suitable headers are added then the text above will define the 
factorial function, will verify that five factorial equals 120, and will 
generate a nicely typeset PDF version of your text. Do tutorial T02 to see 
an example.

If you wonder what 'eager define' above means: It defines an 'eager' 
instead of a 'lazy' function, and it says that if n raises an exception 
then the result of n! is equal to that exception. So e.g. (1/0)! equals 
'division by zero'.

To make stand-alone programs, you need to read about Logiweb machines 
(http://logiweb.eu/logiweb/page/base/fixed/body/tex/page.pdf, Chapter 6) 
which add I/O and interrupt handling to lambda calculus.

A benefit of using the Logiweb programming language is that each and every 
construct of the language are ultimately defined in lambda calculus which 
makes it possible to reason about the programs.

Instead of using the Logiweb programming language, programmers may define 
a 'renderer' which extracts pieces of programs expressed in other 
programming languages from the source text and invokes suitable compilers 
on them. As an example, one may define a renderer which extracts C-code 
from a Logiweb paper, arranges it suitable, and sends it through a 
C-compiler.




For logicians

To arrange that Logiweb checks proofs, you must publish a proof checker on 
Logiweb or reference one published by somebody else. A proof checker is no 
more than a program and it can be published and version controlled by 
Logiweb like any other program. Once somebody has published a proof 
checker, anyone can get their proofs checked by that proof checker just by 
referencing it across the Internet. On Logiweb, a lemma typically states 
that a particular statement holds in a particular theory where the theory 
itself is published on Logiweb. A proof typically proves that a lemma is 
correct and typically indicates that the proof has been checked by a 
particular version of a particular proof checker.

You can find a proof checker in [1] and a definition of propositional 
calculus, first order predicate calculus, and Peano arithmetic in [2]. To 
try making your own proof, run Tutorial T03. Tutorials on defining your 
own theories are under preparation.

[1] http://logiweb.eu/logiweb/page/check/fixed/body/tex/page.pdf
[2] http://logiweb.eu/logiweb/page/Peano/fixed/body/tex/page.pdf



For computer scientists

If you write scientific papers which contain computer programs, then 
Logiweb allows you to write it in such a way that the programs can be 
extracted from it (c.f. the section "For programmers" above) and you may 
publish you paper on Logiweb (c.f. the section "For mathematicians" 
above). If you reason about programs, then Logiweb will typeset both your 
programs and your proofs. And if your proofs are formal, then Logiweb will 
check them as well (c.f. the section "For logicians" above). If you want 
to attack e.g. the POPLMARK challenge, Logiweb should be your weapon of 
choice (some time in the far future I may do it myself, but if you work 
on it and get stuck, don't hesitate to contact me).



For software engineers

If you write Technical Specifications (TSs), Interface Control Documents 
(ICDs), Architectural Design Documents (ADDs), Detailed Design Documents 
(DDDs), Code, Unit Test Plans and Reports, Integration Test Plans and 
Reports, Acceptance Test Plans and Reports, and so on, then you may 
benefit from putting those documents on Logiweb.

On Logiweb, each document published can reference previously published 
documents in which case all definitions present in the referenced document 
become available. As an example one could treat each requirement in the TS 
as a definition which can then be referenced from the ADD and on.

Likewise, each object definition in the ADD could be treated as a 
definition. Such object definitions could be referenced e.g. from 
traceability matrices, or one could arrange that Logiweb generates stubs 
for each object automatically.

The DDD could reference the objects in the ADD and define the contents of 
the objects such that, if sufficient detail is given, then Logiweb can 
auto-generate the final code from the DDD. Furthermore, one can tell 
Logiweb what to do with the code such as sending it through compilers and 
linkers.

The Unit Test Plans and Reports could reference the DDD. Then one can 
arrange that Logiweb builds the software system as specified in the DDD 
and then executes the test suites defined in the Unit Test Plan.

The Integration Test Plan and Report could also reference the DDD. Then 
one can arrange that Logiweb builds the software units as specified in the 
DDD and then integrates and tests the system according to procedures 
defined in the Integration Test Plan and Report.

The Acceptance Test Plan and Report could also reference the DDD but 
possibly specify modified integration procedures and new tests.

And just in case you don't want complete strangers to read your documents, 
you can encrypt them and ask Logiweb to 'unpack' (i.e. decrypt) them when 
fetching them from the Internet.



For conference chairs and editors

If you want your contributers to use a particular style (e.g. a TeX sty 
file) or particular notation (e.g. for combinations as described earlier) 
then publish it on Logiweb and ask your authors to reference your Logiweb 
page. That will make your style and notation available to your authors.

If you want your authors to conform to some guidelines which can be 
checked automatically, then publish your guideline checker on Logiweb. 
Then your authors can use Logiweb to check their contributions for 
conformance.

Instead of submitting their contributions to you, your authors may publish 
their contributions directly on Logiweb and send you a reference. When you 
have accepted a particular version of a particular paper, you can mirror 
it locally to ensure its continued existence on Logiweb.

When you have a full set of submissions for producing your electronic 
proceedings or an issue of your electronic journal, you submit a small 
Logiweb page which simply references the accepted papers. That small page 
is your proceedings or journal issue. Your references give your seal of 
approval to the selected versions of the selected papers by saying that 
the papers were considered appropriate for your proceedings or journal. 
Back in the paper age, publication and giving the seal of approval was the 
same thing. Nowadays, authors web-publish long before they get the seal of 
approval from a publishing house, so the procedure above just brings 
publication up to date.