Chuck Liang (Prof, Hofstra University, NY, USA) will be visiting the Parsifal team the week of 17 Dec 2012. He will give the following talk in Salle Philippe Flajolet (2017) of LIX on Wednesday 19 December at 11h. -Dale
Extending Intuitionistic Logic for Control
From a relatively practical perspective, our goal is to achieve a computationally meaningful interpretation of disjunctive types, including the throwing and catching of exceptions, using a form of non-additive disjunction. Most of the work on extending the Curry-Howard isomorphism and lambda calculus are based on replacing intuitionistic logic with classical logic. In such a context “classical implication” is given the same computational interpretation as intuitionistic implication, i.e., as lambda abstraction. With this interpretation, the body of a lambda term, of *classical* type A->B, may not actually *compute* B in the sense that B is the result of introductions and eliminations. Instead, B may be the result of weakening. This loss of constructivity becomes especially acute in the presense of disjunction: a particular example is found in the classical equivalence between (A->B)vC and (A->C)vB. This equivalence is not consistent with the concept of localized scope that’s expected in programs.
Our solution to this problem is to introduce a *unified logic* in which classical and intuitionistic logics can co-exist without one subsuming the other. We introduce “Polarized Intuitionistic Control Logic” (PICL). This logic is a synthesis of our earliear works PIL and ICL. In particular, it contains as a natural fragment (ICL) that simply extends intuitionistic logic with an additional logic constant. This simplified fragment is already capable of encoding control operators such as call/cc while preserving intuitionistic implication. However, for a richer type system, we extend ICL with an additional class of formulas. We use polarity information encoded in the formulas to control the availability of certain structural rules, which allows us to unify classical and intuitionistic reasoning. We define a simple but useful Kripke semantics, a tableau/sequent calculus proof system and, most importantly, a natural deduction system with a term calculus. We also discuss the role of polarization in sequent calculus versus natural deduction systems.
Part of this talk will consist of ongoing work and some non-finalized alternatives will also be discussed.
