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
July 12, 2007
---
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@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.