Séminaire, 26 septembre 2013

Programme

10:30 – 12:00

Christophe Raffalli (LAMA, Université de Savoie)

Invited talk: Nullstellensatz and Positivestellensatz from cut-elimination

We give here an effective proof of Hilbert's nullstellensatz and Krivine-Stengle's positivestellensatz using the cut elimination theorem for sequent calculus. The proof is very similar to the current techniques in constructive algebraic geometry by Henri Lombardi, but seems more modular.

In the case of the positive stellensatz, we think we prove a more general result than the original one, thanks to a new notion of justification of positiveness: PBDD (polynomial binary decision diagram). It allows both to recover Krivine-Stengle's justification, but also another one which seems to require lower degree.

We apply the same techniques to the nullstellensatz for differentially closed field and show that the proof is almost unchanged.

Remark: here we do not provide bound, but an effective algorithm (implemented in OCaml) to build the wanted algebraic equality. Nevertheless, we discuss how bound could probably be obtained. We also do not deal effectively with the axiom of algebraic/real closure. Those are eliminated using standard model theory.

• slides

14:00 – 15:00

Michele Basaldella

Invited talk: An interactive semantics for classical proofs

The aim of this talk is to present a semantics for proofs in classical logic.

Classical logic: We use a variant of the proof-system introduced by Tait (1968), a system which is often used for analyzing the proof-theory of classical arithmetic and its fragments. The language of this logic consists of infinitary propositional formulas, and the proof-system for this language is formulated through a sequent calculus with infinitary rules of inference.

Proofs: The target of our analysis is not the derivability predicate “the formula A is derivable”, but the more subtle relation “p is a proof of the formula A”, that we abbreviate as “p der A.” In order to define this relation, we need to formalize the concept of “formula-free proofs”, i.e, proofs that does not depend (too much) on the formulas they prove. To understand the idea behind this concept, consider the untyped λ-calculus. By the Curry-Howard correspondence, λ-terms can be seen as a “formula-free” formalization of natural deduction proofs for the implicational fragment of intuitionistic propositional logic. Hence, “p der A” can be read as “the untyped λ-term p has (simple) type A in the Curry-style type assignment.” Here we use a similar idea: we define a class of objects that we call tests which play the role of the untyped λ-terms, and in order to define p der A, we use Tait’s normal rules as type assignment.

Semantics: Our semantics is deeply inspired by Girard’s ludics (2001). As in untyped λ-calculus β-reduction can be seen as natural deduction normalization “without types”, we similarly define a “formula-free” cut-elimination procedure which works with tests, that we call interaction. By analyzing the properties of interaction, we define another relation “p int A” between tests and formulas with the following meaning: “the result of the interaction between the test p and the counter-tests for A terminates.” We finally show a soundness-and-completeness theorem: “p der A” if and only if “p int A”.

• slides

15:30 – 16:30

Michele Pagani (LIPN, Univ. Paris 13)

Invited talk: Probabilistic Coherence Spaces are Fully Abstract for Probabilistic PCF

Probabilistic coherence spaces PCOH yield a semantics of higher-order probabilistic computation, interpreting types as convex sets and programs as power series. We prove that the equality of interpretations in PCOH characterizes the operational indistinguishability of programs in PCF with a random primitive.

This is the first result of full abstraction for a semantics of probabilistic PCF. The key ingredient relies on the regularity of power series and introduces, in denotational semantics, techniques coming from Calculus.

Along the way to the theorem, we design a weighted intersection type assignment system giving a logical presentation of PCOH.

• slides