|| Second Workshop on Logical and Semantic
Frameworks, with Applications
August 28th 2007, Ouro Preto, Brazil
Gilles Dowek, École Polytechnique, Paris
Truth values algebras and proof normalization
We extend the notion of Heyting algebra to a notion of truth values algebra and prove that a theory is consistent if and only if it has a B-valued model for some non trivial truth values algebra B. A theory that has a B-valued model for all truth values algebras B is said to be super-consistent. We prove that super-consistency is a model-theoretic sufficient condition for strong normalization and discuss the open problem whether the converse is true or not.
Fairouz Kamareddine, Heriot-Watt University, Edinburgh
The MathLang framework for computerizing and checking Mathematics
The MathLang project aims at computerizing mathematical texts according to various degrees of formalisations, and without any prior commitment to a particular logical framework (e.g., having to choose either set theory or category theory or type theory, etc.) or to a particular proof checker (e.g., having to choose Mizar or Isabelle or Coq, etc.). Instead, MathLang keeps the choices of the logical framework and proof checker open depending on the taste and expertise of the user. Furthermore, MathLang allows useful computerizations of mathematical texts at much lower levels where the emphasis is not on full formalization as is done in the foundations of mathematics (e.g., as initiated by Frege and Russell) or on proof checking (e.g., as initiated by de Bruijn's Automath).
During computerization, first, the mathematical text is input into the computer exactly as it was written and then one or more MathLang aspects are applied to the text to provide extended versions of the text that can be checked for different levels of correctness. One basic aspect is to extend the text with categorical information (term, noun, adjective, statement, etc) and to automatically check the correctness of the text at this categorical level. This guarantees coherence of the text (e.g., variables are declared before being used and the text constitutes a well structured book). Another aspect is to divide the text into parts annotated with relations (e.g., Corollary A uses Theorem B) and to automatically derive from these relations a number of structures that represent some dependencies in the text which help explain the logical structure of the text. These dependencies are used in a further aspect where a version of the text is transformed into another which shows the holes in the proofs. Other aspects will transform this version into a fully formalized version (say in Mizar or Isabelle).
MathLang was created as an experience driven project where the computerisation of different texts taken from various branches of mathematics, is the basis for the design and implementation of the MathLang aspects. So far, a number of mathematical texts have been computerised, some of which have been gradually transformed through MathLang aspects into full Mizar. Other proof checkers (e.g., Isabelle and Coq) are envisioned for the near future.
In this talk, the MathLang framework, its developments and its current and future aspects, as well as examples of computerization from original mathematical texts to the fully formalised Mizar versions are given. For each aspect, emphasis will be on its design, formalisation, implementation, the automation available for this aspect and the correctness or trustworthiness of these processes. Then, we discuss how the computerisation path from the original mathematical text to full Mizar will look if Isabelle was the checker chosen instead of Mizar and show that a number of aspects and computerised versions of the original text are common between both path. We also discuss at which stage a commitment to a certain logical framework and a certain proof checker can be made on the path from the original mathematical text to the version fully formalised in that proof checker.
The MathLang project started in 2000 by Fairouz Kamareddine and Joe Wells and has had since 2002 three PhD students (Manuel Maarek, Krzysztof Retel and Robert Lamar) and a number of MSc and BSc students all collaborating and contributing to the design and implementation of the various aspects and to the computerization of mathematical texts.
Simona Ronchi Della Rocca, Università di Torino
SOFT Time and SOFT Space
A recent research field in Theoretical Computer Science is the design of programming languages with bounded complexity, either in time or in space. In fact, guaranteeing and certifying a limited resources usage is of central importance for computer networks constituted of small and mobile devices with bounded computational resources that receive programs to be executed from the network itself. One of the more promising approaches to this problem is based on the use of lambda calculus as paradigmatic programming language, and on the design of type assignment systems for lambda-terms, where types represent the property of having the desired complexity bound. So the complexity can be checked statically at compilation time, in ML style. A useful tool for this aim are the Light Logics, derived from the Linear Logic of Girard, which characterize complexity classes through their cut-elimination procedure. Here I will describe some results obtained starting from the SOFT logic of Lafont, which characterize PTIME. We designed two type assignments systems for lambda-calculus based on this logic, namely STA and STAB. Types in STA are a subset of SOFT logical formulae, in STAB are the same subset plus two boolean constants. The two type assignment systems have all the good properties we expect, namely subject reduction and strong normalization. The key results are the following:
1. A term which can be typed in STA can be reduced to normal form by a number of Beta-reductions which is polynomial in its lenght. Moreover the system is complete for FPTIME, namely all polynomial functions can be computed by terms typable in this system.
2. A term that can be typed in STAB can be reduced to normal form using an amount of space which is polynomial in its lenght. Moreover the system is complete for PSPACE.