[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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 ([EMAIL PROTECTED]). 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.