Project

Back to overview

Computational Structure of Classical Duality

Applicant McKinley Richard
Number 126422
Funding scheme Ambizione
Research institution Institut für Informatik Universität Bern
Institution of higher education University of Berne - BE
Main discipline Information Technology
Start/End 01.03.2010 - 28.02.2013
Approved amount 434'641.00
Show all

All Disciplines (2)

Discipline
Information Technology
Mathematics

Keywords (5)

Proof theory; Logic; Computer Science; Category Theory; Process Algebra

Lay Summary (English)

Lead
Lay summary
The Curry-Howard correspondence, also known as the proofs-as-programs correspondence, is the observation that logical proofs and computer programs are two ways of presenting the same mathematical objects. This project aims to extend the scope of the correspondence in two important directions: on the logical side, towards capturing classical logic, the logic used in natural and mathematical reasoning, and on the computational side to the idea of a "process"; a program which interacts with many other programs by passing messages.

Background: In the 1930s, Alonzo Church developed a calculus (the lambda calculus) a language for writing down what we now call computable functions. At the same time Gerhard Gentzen was developing natural deduction; a language for writing down formal proofs. Both these languages were conceived as tools for exploring the foundations of mathematics, with the advent of computer science, representations of computable functions became a more practicle concern. Lambda calculus was the inspiration for Lisp, the first functional programming language. Meanwhile, William Alvin Howard discovered a link between logic and functional programming: natural deduction proofs could be seen themselves as terms of the lambda calculus. In other words, a proof is a kind of computation, and a very well-behaved kind at that. This observation, known as the Curry-Howard correspondence, has led and continues to lead to an enormous body of theoretical and practical work in computer science and logic.

Goals of the project: Computer science has developed much since its inception, and we no longer think of computer problems as simply calculating a function, but more as interacting with a complex, varying environment comprised of users and other programs. The lambda calculus is unsuited for representing such programs, and other calculi (called process calculi) are used instead to reason about them. These calculi lack the elegant theoretic underpinning enjoyed by the lambda calculus. On the other hand, natural deduction fails to faithfully represent a fundamental reasoning mode: the ability to recognise that a statement is the same as its double negation. This property of logic is called "Duality". A much better calculus for reasoning under duality, called the sequent calculus, was also developed by Gentzen, but its computational meaning has been difficult to discern.

This project aims to extend the proofs as programs correspondence by representing proofs using duality within a new, theoretically inspired language of processes.
Direct link to Lay Summary Last update: 21.02.2013

Responsible applicant and co-applicants

Employees

Publications

Publication
Canonical Proof Nets for Classical Logic
McKinley Richard (2013), Canonical Proof Nets for Classical Logic, in Annals of Pure and Applied Mathematics, 164(6), 702-732.
Proof Nets for Herbrand's Theorem
McKinley Richard (2013), Proof Nets for Herbrand's Theorem, in ACM Transactions on Computational Logic, 14(1), 5.
Expansion nets: Proof nets for for propositional classical logic
McKinley Richard (2010), Expansion nets: Proof nets for for propositional classical logic, in Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR, Yogyakarta, IndonesiaSpringer, BERLIN/HEIDELBERG.

Scientific events

Active participation

Title Type of contribution Title of article or contribution Date Place Persons involved


Self-organised

Title Date Place
Gentzen Systems and Beyond 04.07.2011 Bern

Associated projects

Number Title Start Funding scheme
145747 Computational structure of higher-order sequent calculi 01.03.2013 Ambizione

Abstract

The Curry-Howard correspondence, also known as the proofs-as-programs correspondence, is the observation that proofs and programs are two ways of presenting the same mathematical objects. The most fully developed correspondence of this kind is between intuitionistic logic (roughly, logic without the law of excluded middle) and typed lambda calculus, where proofs in natural deduction correspond to prototypic functional programs. A proof deriving a formula A from a set of assumptions G can be viewed as a program with parameters G, deriving data of type A. In this setting, computation is normalization: a process of removing “detours” from a proof which simpli?es its logical structure. The correspondence applies for propositional, ?rst-order and higher-order logics/type theories, and has been the source of numerous useful insights in both proof theory and programming language design. In particular, the uni?ed semantical theory of proofs/programms in this setting (interpretation in a cartesian-closed category) gives a way to say when two proofs (or two programs) are essentially the same.This project will make contributions to the proofs-as-programs correspondence for classical logic, which is the underlying logic of mathematical practice, and also underpins mant important applications in computer science (speci?cation, veri?cation, circuit design, etc). There have been many attempts to give such a correspondence, but (unlike for intuitionistic logic) there is no general theory of correspondence. This is perhaps unsurprising, as the nature of classical proof itself is poorly understood.The project I propose has two goals:1: To increase our understanding of proving as dialogue (a proof is a strategy for playing a game) by developing formal calculi of strategies and by relating existing notions of proof to game notions of proof. 2: to develop, via the above game theoretic understanding, a theory of classical proofs as processes.
-