The objects at stake

• Computational objects

• Logical statements

• Relations between them

Logical validity

What does it mean for a logical statement to be valid?

The content of proofs

Intuitively, there can be different proofs of a given statement.

But what makes two proofs different, and why does it matter?

• Different syntax — but this is not satisfactory unless one postulates a useful notion of equivalence
• Different normal forms — a particular kind of equivalence, internal to the proof language
• Different behaviours — produces different dialogues or experiments

This induces different forms of constructivism in logic

• From a proof of ∃x, P(x), one can compute an a such that P(a) is valid
• From a proof of a statement, one can compute an effective argument strategy

Computational consistency

What does it mean for a program to be valid?

Universality and decidability

There is no perfect approach to program correctness.

• Any Turing-complete language must have space for invalid programs (cf. halting problem).
• Any meaningful computational property is undecidable (cf. Rice’s theorem).
• A type system is useful for practical purposes if type checking is decidable.

So there has to be cases where correctness for a type is established by ad-hoc semantic means (e.g. unsafe chunks in statically typed code).

Analytic vs synthetic, a priori vs a posteriori

Two useful categorisations of concepts :

• Synthetic notions rely on the meaning of objects while analytic notions rely on their intrinsic structure,
• A priori notions rely on the potential consequences while a posteriori notions rely on explicit facts

Realisability as a method

Choose :

• a computational model
• a language of formulas
• a relation of realisation : p ⊩ P means that
  • p is a witness of P (as a logical statement)
  • p respects P (as a specification)

The kinds of results we are after :

• adequacy : if P is provable, then P has a realiser
• consistency : the set of realised formulas is consistent
• specification : describe the behaviour of the realisers of P
• identify logical principles that a class of models realise

Formulas and proofs

Start from a minimal propositional language : P, Q, … ⩴ α ∣ P → Q

Can be extended to a full-fledged logic with

• additional connectives ∧, ∨, ⊥, ¬
• predicates and first-order quantification
• quantification at higher order

The minimal fragment is enough to illustrate the mechanics.

Hilbert-style proofs

We start with an explicit notion of proof (so-called “synthetic” and “a priori”), in the style of Hilbert.

Proofs derive sequents of the shape 𝒯 ⊢ P where 𝒯 is a set of formulas (seen as a theory) and P is a formula (the conclusion).

• axiom : if P ∈ 𝒯 then 𝒯 ⊢ P
• modus ponens : if 𝒯 ⊢ P → Q and 𝒯 ⊢ P then 𝒯 ⊢ Q
• logical axiom schemes :
  • 𝐊 : P → Q → P
  • 𝐒 : (P → Q → R) → (P → Q) → P → R

Enjoys deduction : 𝒯, P ⊢ Q if and only if 𝒯 ⊢ P → Q.

Heyting algebras – basic structure

A notion of “truth value” for minimal logic.

Definition

A Heyting algebra is a lattice H with ⊤ and ⊥, with an operator → that is adjoint to the meet ∧ : a ∧ b ≤ c ⇔ a ≤ b → c

Properties

• For all a and b, a ≤ b if and only if a → b = ⊤.
• Soundness : if  ⊢ P is provable then its interpretation ⟦P⟧ is ⊤ in all Heyting algebras (by induction on proofs)
• Completeness : if ⟦P⟧ = ⊤ in all interpretation in Heyting algebras, then  ⊢ P is provable (using a syntactic model)

Heyting algebras – more connectives

Absurdity ⊥

• characterised by the axiom scheme ⊥ → P
• naturally interpreted by the minimum in a HA

Conjunction P ∧ Q and disjunction P ∨ Q

• interpreted by the meet and join in a HA
• axiom schemes for conjunction : P → Q → P ∧ Q, P ∧ Q → P, P ∧ Q → Q
• axiom schemes for disjunction : P → P ∨ Q, Q → P ∨ Q, (P → R) → (Q → R) → P ∨ Q → R
• disjunction property : if  ⊢ P ∨ Q then  ⊢ P or  ⊢ Q

Negation ¬P

• defined as ¬P := P → ⊥
• enjoys non-contradiction :  ⊢ ¬(P ∧ ¬P)
• does not enjoy excluded middle : P ∨ ¬P is not provable

Heyting algebras – quantifiers

Proof rules

• generalisation : if 𝒯 ⊢ P and α does not occur in 𝒯 then 𝒯 ⊢ ∀α.P
• specialisation : if 𝒯 ⊢ ∀α.P then 𝒯 ⊢ P[α := t]

Interpretation

• ⟦∀α.P⟧ = ⋀_v⟦P[α := v]⟧ (assuming the algebra has arbitrary meets)
• predicates are functions with values in H
• first order quantifies over a given structure
• second order quantifies over H

Exercise : minimal logic is weaker than classical

• Prove that anything provable in minimal logic is true in classical logic.

• Prove that ∀P.(¬¬P → P) is not provable.

Interpreting formulas or proofs

Heyting algebras provide an interpretation of formulas and provability.

The constructivist approach of Brouwer refuses validity as an absolute property of statements but requires effective means of justification, which implies interpreting proofs.

• Initially, this is an epistemological standpoint (intuitionism vs platonism)
• It does have meaningful technical developments, even without adhering to Brouwer’s radical views

The Brouwer-Heyting-Kolmogorov interpretation

• A proof of P ∧ Q consists of a proof of P and a proof of Q
• A proof of P ∨ Q consists of the information of left or right and a proof of that side
• A proof of P → Q is a way to turn a proof of P into a proof of Q
• A proof of ∃x ∈ S, P(x) consists of an element e ∈ S and a proof of P(e).
• A proof of ∀x ∈ S, P(x) is a way to turn each element e ∈ S into a proof of P(e).
• There is no proof of ⊥.

BHK : explicit and implicit requirements

The BHK interpretation does not prescribe a particular mathematical structure, nor a general interpretation of atomic statements.

• Functions should be effective (computable).
• Quantification requires the domain to be suitable to computation.
• The interpretation of atomic formulas depends on the context
  • basic arithmetical equalities may be interpreted as computations
  • decidable predicates can be justified by proof certificates of some kind
  • or consider that true atomic statements need no further justification

It does interpret proofs :

• The disjunction property is explicit in the interpretation of ∨.
• The identity function is a generic proof of P → P.
• There are two simple proofs of P → P ∨ P (left and right injections).

BHK : some observations

• Synthetic approach : interpret each statement in a domain that depends on the shape of the formula

  connective	structure
  conjunction	cartesian product
  disjunction	disjoint union
  implication	function space
  existential	dependent sum
  universal	dependent product

  The basis of denotational semantics, requires suitable restrictions on function spaces to get good properties. Requires subtle constructs to handle quantification.

• Analytic approach : define a common structure, independent of formulas, to interpret everything.

  The basis of realisability, requires some coding and a form of effectiveness for functions. Supports higher-order quantification through uniformity.

Kleene’s realisability

An implementation of the BHK principles for intuitionistic arithmetic.

Defines the statement n ⊩ P (n realises P) by induction on P :

• ⟨m, n⟩ ⊩ P ∧ Q if m ⊩ P and n ⊩ Q
• ⟨0, m⟩ ⊩ P ∨ Q if m ⊩ P
• ⟨1, m⟩ ⊩ P ∨ Q if m ⊩ Q
• m ⊩ P → Q if for all n, if n ⊩ P then φ_m(n) ⊩ Q
• ⟨m, n⟩ ⊩ ∃x.P if n ⊩ P[x := m]
• m ⊩ ∀x.P if for all n, φ_m(n) ⊩ P[x := n]
• m ⊩ s = t if ℕ ⊨ s = t (with s and t closed)

where ⟨⋅, ⋅⟩ is a bijection of ℕ² to ℕ and φ is en enumeration of recursive functions.

The strength of Kleene’s realisability

Heyting arithmetic HA is intuitionistic logic with first-order quantification and Peano’s axioms for basic arithmetic.

• Anything provable in HA is realisable.

• The following statement (known as Markov’s principle) is realisable, given a total decidable predicate P : ¬¬∃n, P(n) → ∃n, P(n)

• The statement ∀x.(H(x) ∨ ¬H(x)), where H(n) means that φ_n(n) is defined, is classically true but not realisable.

• Hence its negation is realisable but classically false!

Abstracting the computation model

Kleene’s construction relies on an enumeration of recursive functions in natural numbers, but this is nothing deeper that a coding trick.

Definition

A partial combinatory structure is a set A equipped with a partial binary operation ⋅ : A × A ⇀ A.

• ⋅ associates to the left and is implicit : abcd means ((a ⋅ b) ⋅ c) ⋅ d,
• e↓ means that the value of expression e is defined,
• e₁ ≃ e₂ means that e₁ and e₂ are either both undefined or both defined and equal.

A partial combinatory algebra (PCA) is a partial combinatory structure that is combinatorially complete :

• for every applicative expression e over A with variables x₁, …, x_n there is an a ∈ A such that ab₁⋯b_n ≃ e[x₁ := b₁, …, x_n := b_n] for all b₁, …, b_n ∈ A. This element a is written λx₁…x_n.e.

Facts about PCAs

Completeness

Combinatorial completeness is equivalent to the existence of 𝐊 and 𝐒 such that

• for all x, y ∈ A, 𝐊x↓ and 𝐊xy = x
• for all x, y, z ∈ A, 𝐒xy↓ and 𝐒xyz = xz(yz)

Examples

• Given an enumeration φ of recursive functions, the operation a ⋅ b = φ_a(b) makes ℕ a PCA (the so-called first Kleene algebra)

• The set of closed normal λ-terms, with M ⋅ N defined as the normal form of the term (M)N is a PCA.

• The set of closed λ-terms quotiented by β-equivalence is a PCA (where application is actually total).

Adequacy : typing implies realisation. Formally, if M is a λ-term and P is a type, then  ⊢ M : P implies M ⊩ P.

Heyting arithmetic in a PCA

Kleene’s construction can be carried out in any PCA, with some encoding of data :

• pairs can be represented as ⟨a, b⟩ = λp.(p)ab, projectors are π₁ = λxy.x and π₂ = λxy.y,
• natural numbers can be represented as Church numerals ⌜n⌝ = λfx.fⁿx.

Hence the definition :

• a ⊩ P ∧ Q if π₁a ⊩ P and π₂a ⊩ Q
• a ⊩ P → Q if for all b such that b ⊩ P we have ab ⊩ Q
• a ⊩ ∃x.P if there is an n ∈ ℕ such that π₁a = ⌜n⌝ and π₂a ⊩ P[x := n]
• a ⊩ ∀x.P if for all n ∈ ℕ, a⌜n⌝ ⊩ P[x := n]
• a ⊩ s = t if ℕ ⊨ s = t (with s and t closed)

Second order and encoding of data

The interpretation of arithmetic in a PCA relies on ad-hoc encodings of data types (pairs, natural numbers).

These can be specified using second-order quantification :

• Consider a PCA A and formulas on → and ∀ with parameters in subsets of A.
• Define a ⊩ s if a ∈ s for s ⊆ A —parameters specify a realisation predicate explicitly.
• Define a ⊩ ∀α.P as a ⊩ P[α := v] for all sets v ⊆ A — realising a second-order universal means realizing all instances uniformly.

We can prove some specification results :

• t ⊩ ∀α.(α → α) iff t is the identity function, i.e. for all a ∈ A, t ⋅ a = a.
• ∀α.(α → α → α) has two generic realisers, λxy.x and λxy.y.
• ∀α.((α → α) → α → α) has Church numerals as generic realisers.

We keep this fuzzy for now.

Plan

The situation so far :

• PCAs as a generic presentation of models of purely functional computation,
• an implementation of the BHK principles, modulo an encoding of first-order structures as computational objects.

What comes next :

• why full classical logic does nothing interesting in PCAs,
• how we can extend the technique to get constructive content for classical logic.

Intuitionistic negation

By definition, there can be no witness for absurdity ⊥.

This makes negation ¬P (defined as P → ⊥) degenerate :

• If P is realisable, then there can be no realiser of ¬P.
• If P is not realisable, then anything realises ¬P.

The set of realisers of ¬P is either empty or full, so one cannot extract any information from a proof of a negation, apart from its existence.

Classical negation and disjunction

In classical logic, negation is considered involutive :

• ¬¬P is equivalent to P — elimination of double negation
• P ∨ ¬P holds for all P — excluded middle
• ((P → Q) → P) → P holds for all P and Q — Peirce’s law

Fact : classical disjunction is incompatible with an effective intuitionistic disjunction property.

• If P ∨ ¬P was uniformly realised, then the realiser would have to always choose the same side independently of P, which is nonsense.
• If P ∨ ¬P was realised for all P as a function of P, it would imply that all predicates are decidable, which cannot be effective.

The Devil’s interpretation

Computing with continuations

The Devil’s interpretation involves answering the same question several times, that is returning several times from a given computation.

Formally, we now work in a λ-calculus extended with extra constants to handle control :

• terms : M, N, … := x ∣ λx.M ∣ (M)N ∣ 𝐜 ∣ 𝐤_π
• stacks : π, ρ, … := M ⋅ M ⋯ M

Execution now concerns closed terms applied to closed stacks :

An abstract formulation of call with current continuation (from Scheme), which can be used to implement various control structures : exceptions etc.

Typing continuations

A few observations on (𝐜)M ∗ π ≻ M ∗ 𝐤_π ⋅ π :

• (𝐜)M can return several times in its context π, by calling the continuations 𝐤_π that 𝐜 creates.
• A term 𝐤_π discards the context in which it is called, so it never returns.

If (𝐜)M behaves well for a type A, then the 𝐤_π that it creates expects values of type A and do not return at all, so it behaves well for any type.

• k_π respects the type A → B for any B
• M respects the type (A → B) → A
• 𝐜 respects the type ((A → B) → A) → A

The control operator 𝐜 realises Peirce’s law.

Realisability in interactive context

Execution is an interaction between a program and an environment, witnessing a given type means interacting correctly with opponents for that type.

• Pick a pole ⫫
  — a set of states M ∗ π such that s ≻ t ∈ ⫫ implies s ∈ ⫫

• Define orthogonality as M ⫫ π when M ∗ π ∈ ⫫
  — M and π are orthogonal when they interact correctly for ⫫

• Induces an observation equivalence : M ≃ N if {M}^⫫ = {N}^⫫
  — M and N are equivalent when the pass the same tests

• A behaviour is a set of terms A such that A^⫫ ⫫ = A

Remark that, if ⫫ is empty, there are two behaviours : empty and full.

Realisability through falsity values

The realisability structure relies on defining characteristic tests for logical formulas.

• M ⊩ P means that for all π ∈ ⟦P⟧ we have M ⫫ π

• ⟦P⟧ is the falsity value of P, defined inductively on P

  ⟦P → Q⟧	=	{M ⋅ π ∣ M ⊩ P, π ∈ ⟦Q⟧}
  ⟦∀x.P⟧	=	⋃v⟦P[x := v]⟧

  Quantification is interpreted uniformly,

  • in a particular structure for first order (as in model theory),
  • in sets of stacks for second order.

• This is compatible with the previous approach :

  • M ⊩ P → Q implies (M)N ⊩ Q for all N ⊩ P
  • M ⊩ ∀x.P when M ⊩ P[x := v] for all values v

• Adequacy : if the typing judgement  ⊢ M : P is provable then M ⊩ P for any choice of ⫫.

Realising classical principles

• The formula ⊥ is ∀α.α, so ⟦⊥⟧ is the set of all stacks,
  M ⊩ ⊥ means that M ∗ π is in ⫫ whatever π is.

• Consider a formula P and a stack π ∈ ⟦P⟧, then

  • for all M ⊩ P we have M ∗ π ∈ ⫫ by definition
  • for all stack ρ, we have 𝐤_π ∗ M ⋅ ρ ≻ M ∗ π ∈ ⫫
    so 𝐤_π ⊩ P → Q and (𝐤_π)M ⊩ Q for whatever type Q
  • for all N ⊩ (P → Q) → P we have 𝐜 ∗ N ⋅ π ≻ N ∗ 𝐤_π ⋅ π ∈ ⫫
  • hence 𝐜 ⊩ ((P → Q) → P) → P

  Finally, we have 𝐜 ⊩ ∀α.∀β.((α → β) → α) → α, as expected.

If we extend the typing rules with a schema  ⊢ 𝐜 : ((α → β) → α) → α, then adequacy remains and we get proof language for all classical logic.

Proof-like terms

Assume ⫫ is not empty and take an arbitrary M ∗ π ∈ ⫫.
Then (𝐤_π)M is a realiser for ⊥.

Wait… What?

We need a criterion to distinguish “actual” realisers in the set of computational objects.

Definition

A proof-like term (or quasi-proof) is a closed term that has no occurrence of a 𝐤_π.

Now we can make more precise statements :

• A formula P is realisable given pole ⫫ if it is realised by a proof-like term.
• A formula is universally realisable if there is a proof-like term that realises it for any choice of ⫫.

Specification of data types

Using second order quantification, we can characterise behaviours :

Excluded middle

Define T := λf.λg.𝐜(λk.f(λa.k(ga))).

Then T has type ∀α.∀β.(¬α → β) → (α → β) → β, that is ∀α.¬α ∨ α.

It implements a kind of exception handler :

It can be generalised to more complex structures.

First order in realisability

General structure

The logical language can be extended to include first order :

• pick a first-order language (common choices : arithmetic, set theory)
• atomic formulas have the shape α(t₁, …, t_n) where α is a predicate symbol or variable of arity n
• interpret first-order terms and quantifiers in a structure ℳ
• a predicate of arity n is interpreted as a function in ℳⁿ → 𝒫(Π)

Equality

• Definable à la Leibniz : (s = t) := ∀α.(α(t) → α(u))
• When s = t holds in the interpretation structure, λx.x ⊩ s = t.

Realisability models

Pick a language and an interpretation structure ℳ.

Consistency

Given a first-order language and interpretation, each pole ⫫ induces a theory 𝒯_⫫ : the set of formulas realised by proof-like terms.

• A pole ⫫ is consistent if 𝒯_⫫ is, that is ⊥ ∉ 𝒯_⫫

On falsity values, define the relation a ≲ b when a → b is realised by a proof-like term.

• The relation ≲ is a preorder.
• It extends ⊇ (is a ⊇ b then λx.x ⊩ a → b).
• It makes the set of falsity values a Boolean algebra.

Then 𝒯_⫫ is the set of formulas interpreted by ⊤ in this Boolean algebra.

Models

Models of 𝒯_⫫ are realisability models induced by ⫫.

• Realisability models satisfy all axioms of second-order logic.
• In the degenerate  ⫫  = ∅, they are equivalent to ℳ.

Arithmetics

Consider the particular case of arithmetic, with ℕ as the interpretation structure.

• Given two closed first-order terms s and t, ⟦s = t⟧ is ⟦∀α.α → α⟧ if ℕ ⊨ s = t, it is ⟦⊤ → ⊥⟧ if ℕ ⊨ s ≠ t.
• Horn clauses ∀x₁⋯∀x_mE₁ → ⋯ → E_n → G (where the E_i and G are equalities or ⊥) which are true in ℕ are universally realised.
• In particular, all axioms of basic arithmetic hold in realisability models.

Define 𝐍(n) := ∀α.((∀x.α(x) → α(x + 1)) → α(0) → α(n)).

• 𝐍(42) specifies a Church numerals that iterates 42 times
• The recurrence axiom ∀x.𝐍(x) generally does not hold — it would be a term that behaves like all numbers at the same time.

Arithmetic statements can be relativised to 𝐍 : define ∀^𝐍x.P as ∀x.𝐍(x) → P.

• Stating that an operation is internal to 𝐍 means computing it : ∀^𝐍m.∀^𝐍n.𝐍(m + n)
• Mathematical statements specify behaviours : ∀^𝐍p.∀^𝐍q.(p × q = n → p = 1 ∨ q = 1)

Realisability models contain models of second-order arithmetic, plus other objects.

Model theoretic axioms

The axiom of choice

∀R.(∀^𝐍n.∃^𝐍m.R(n, m) → ∃F.∀^𝐍n ∈ N.∃!^𝐍p.(F(n, p) ∧ R(n, p)))

Krivine knows how to realise this by extending the language with an extra instruction (essentially memoizing calls to R to make sure that F is properly functional), yet most realisability models do not satisfy it.

For each n ∈ ℕ, define ∇_n(x) as the formula x + 1 ≤ n (where x ≤ y is ∃t.x + t = y).

• Then ∀x.∇_n(x) → (x = 0 ∨ ⋯ ∨ x = n − 1) is not universally realised.
• Further study of 𝒯_⫫, assuming ∃x.¬𝐍(x) is realised, reveals that the ∇_n cannot be well-ordered, which refutes the axiom of choice.
• Considered as subsets of ℕ, they form a sequence where each element strictly injects into the next. This also contradicts the continuum hypothesis.

The foundation axiom in set theory

On the language of set theory, consider the foundation axiom ∀a.(∀x.(x ∈ a → P(x)) → P(a)) → ∀a.P(a)

• It is the type of a fixed point : Y such that Yφ ≻ φ(Yφ)
• Proving that φ is well typed is equivalent to proving that recursion terminates.

Generalising the construction

The construction of classical realisability is clever but it looks ad-hoc in various ways, we look for cleaner structure.

• Inclusion of falsity values reflects all the basic structure :

  • ⟦Q⟧ ⊇ ⟦P⟧ when Q is a subtype of P
  • {M}^⫫ ⊇ ⟦P⟧ when M is a realiser of P
  • {M}^⫫ ⊇ {N}^⫫ when M somehow reduces to N

• Falsity values form a complete lattice.

• For most purposes, a term M can be identified with the falsity value {M}^⫫ of tests that it passes.

Implicative structures

Definition

• An implicative structure is a complete lattice (A, ≤) equipped with an operator  →  : A × A → A that
  • is contravariant on the left : a ≤ a′ implies a′ → b ≤ a → b
  • commutes to meets on the right : a → ⋀B = ⋀_b ∈ B(a → b)
• Application is defined by adjunction on the arrow :
  a ⋅ b := ⋀{c ∣ a ≤ b → c} so that for all c, a ⋅ b ≤ c iff a ≤ b → c.

Examples

• If ⫫ is a pole, the set ℱ of sets of stacks (falsity values) is an implicative structure with a ≤ b if a ⊇ b and
  a → b := {M ⋅ π ∣ M ⊆ a^⫫, π ∈ b}, and a ⋅ b = {π ∣ ∀M ∈ b^⫫, M ⋅ π ∈ a}.
• If 𝒜 is a complete Heyting algebra, then a → b := ⋁{c ∣ c ∧ a ≤ b} makes it an implicative structure and ⋅ is ∧.
• If 𝒜 is a PCA, then 𝒫(𝒜) with a → b := {p ∣ ∀q ∈ a, pq ∈ b} is (almost) an implicative structure
  and a ⋅ b = {p ⋅ q ∣ p ∈ a, q ∈ b}.

General observations

Elements of an implicative represent behaviours, they can be seen indifferently as types or as programs.

• The structure allows to define combinators by their specification in any structure (but some may be degenerate) :

  • 𝐊 := ⋀_a, b a → b → a
  • 𝐒 := ⋀_a, b, c (a → b → c) → (a → b) → a → c
  • 𝐜 := ⋀_a, b ((a → b) → a) → a

• Any function f : 𝒜 → 𝒜 induces an element λf := ⋀_a(a → f(a)),
  all λ-terms can be interpreted this way.

• Computational properties appear abstractly :

  • (a → b)a ≤ b hence (λf)a ≤ f(a) — β-reduction
  • a ≤ b → ab hence a ≤ λ(b ↦ ab) — η-expansion

• The implicative structure includes uniform and non-uniform constructs :

  • the product A × B := ∀α.(A → B → α) → α is a constructive conjunction
  • the meet A ∧ B is a uniform conjunction (a.k.a. intersection type)
  • A ∧ B → A × B is always realised, the reverse only in degenerate models

Separators and consistency

Definition

A separator of an implicative structure 𝒜 is a subset 𝒮 ⊆ 𝒜 that

• is upwards closed : if b ≥ a ∈ 𝒮 then b ∈ 𝒮,
• contains 𝐊 and 𝐒,
• is stable under modus ponens : if a → b ∈ 𝒮 and a ∈ 𝒮 then b ∈ 𝒮.

A separator 𝒮 is consistent if ⊥ ∉ 𝒮, classical if 𝐜 ∈ 𝒮.

Remarks

• The first condition recalls the one on poles, it accounts for execution dynamics and logical consequence.
• The other two are analogue to provability rules in Hilbert-style proofs.
• Stability under modus ponens implies stability under application, hence all pure λ-terms are representable in all separators.

Entailment in implicative algebras

Given a implicative structure 𝒜 and a separator 𝒮, define entailment as a⊢_𝒮b when (a → b) ∈ 𝒮.

• Entailment is a preorder.
• It extends ≤ (since a ≤ b implies λx.x ≤ a → b).
• The quotient 𝒜/𝒮 of 𝒜 under the associated equivalence is a Heyting algebra.
• It is a Boolean algebra if 𝐜 ∈ 𝒮.

Usual model-theoretic techniques follow :

• If ⊥ ∉ 𝒮 then the theory 𝒯_𝒮 of formulas interpreted by ⊤ in 𝒜/𝒮 is consistent.
• If 𝒮 is maximal among consistent separators, then 𝒜/𝒮 is the 2-element Boolean algebra and 𝒯_𝒮 is complete.

This applies even when 𝒮 is not classical.

Process algebras : CCS

We use a formal language to represent programs that interact by message passing :

One can define the dynamics as a reduction up to structural congruence :

(a.P + P′) ∥ (ā.Q + Q′) ⟶ P ∥ Q

Structural congruence ≡ makes ∥ a commutative monoid law with 1 as neutral and makes name restriction behave right.

Non-determinism is unavoidable :

ā.1 ∥ a.Q ∥ a.R ⟶ 1 ∥ Q ∥ a.R ā.1 ∥ a.Q ∥ a.R ⟶ 1 ∥ a.Q ∥ R

Process algebras : the π-calculus

An extension of CCS where actions can communicate names which can be used themselves for communication.

Notation :

• a(x).P means “receive a name on channel on a, bind it to x then do P”
• ab.P means “send the name b on channel a then do P”

Name passing can reveal new possible interactions

a(x).xc.1 ∥ ab.1 ∥ b(z).P ⟶ bc.1 ∥ 1 ∥ b(z).P ⟶ 1 ∥ 1 ∥ P[z := c]

Name passing represents “mobile” processes, with dynamic connections.

• It is expressive enough to implement the λ-calculus.
• It has variants : polyadic, asynchronous…
• It has various type disciplines

The world of process calculi is a mess

Many languages with various design choices

• more or less higher order
• more or less synchronous
• various restrictions on name passing

Many ways to define equivalence of processes

• various forms of test
• a zoo of notions of bisimilarity

Many encodings with various invariants

• translations between various calculi
• embeddings of λ-calculi

And let us not speak (yet) about type systems.

Models of concurrency, traditionally

Event structures :

• events are points in a partial order
• configurations are particular sets of events (partial runs as histories)
• structures are sets of configurations with consistency conditions

Closely related to Scott’s domains, Girard’s coherence spaces, etc.
More recently exploited in concurrent games.

Operational semantics, CCS as a model :

• use terms of a basic language to interpret programs from other languages
• structure the space using a notion of refinement : (bi)simulation

Blurs the boundary between programs and types :

• specifications are themselves processes :
  program P respects a specification S if P and S are bisimilar;
• a process is identified with the space of its observable behaviours.

The programme

We want a properly logical description of processes behaviours :

• Algebraic structure – for properly composing things
• Semantics – insights on the meaning of process constructs
• Typing – static description of dynamic objects, invariants

We aim for an analytic approach :

• start from a model of interaction with few constraints a priori,
• be agnostic on the notion of refinement at work,
• extract logical principles from the structure.

We look for the minimal logic for concurrency.

Logics for concurrent processes

One assigns types to different elements of the language in order to put constraints on the set of allowed expressions and thus statically ensure properties of terms :

• compatibility between senders and receivers,
• control on name usage,
• guarantees on global good behaviour,
• respect of communication protocols…

Usually guided by computational concerns rather than logical consistency.

We would like to fit all these in a general realisability framework, which has to be linear.

The example of session types

Session types describe the communication discipline on names.

• a : A ⊗ B means “send a name x on a then behave as A on x and as B on a, independently”
• a : A ⊸ B means “receive a name x on a then behave as B on a, assuming the environment behaves as A on x”
• a : 𝟏 means “terminate the session on a”

The logic for these behaviours is linear :

• This can be extended to full linear logic.
• It is very “synthetic” and forces functional behaviours.

Testing as orthogonality

Consider a process algebra and define an observation as a set ⫫ of processes, abstractly considered as well-behaved.

• may testing :  ⫫  = {P ∣ ∃R, P⟶^*ω ∥ R} (where ω is a special action to represent success)
• fair testing :  ⫫  = {P ∣ ∀P⟶^*Q, ∃R, Q⟶^*ω ∥ R}
• termination : ⫫ is the set of terms that have no infinite run
• many other choices

Deduce orthogonality :

• P ⫫ Q if P ∥ Q ∈ ⫫
• P ≃ Q if {P}^⫫ = {Q}^⫫

Orthogonal sets form a complete lattice of behaviours.

Combinations of behaviours

Start with parallel composition of independent behaviours.

• Assume a pair of injections ℓ, r : N → N over names, with disjoint images — split the set of name into independent name spaces
• If P is a term, write P[ℓ] for P renamed by ℓ
• Define multiplicative conjunction by its generators : A ⊗ B := {P[ℓ] ∥ Q[r]; P ∈ A, Q ∈ B}^⫫ ⫫
• Define implication by duality : A ⊸ B := (A ⊗ B^⫫)^⫫ = {P[ℓ] ∥ Q[r]; P ∈ A, Q ∈ B^⫫}^⫫
• Deduce application by adjunction : A ∗ B ≤ C iff A ≤ B ⊸ C, A ∗ B = {(νℓ)(P ∥ Q[ℓ])[r⁻¹]; P ∈ A, Q ∈ B}^⫫ ⫫

This makes A nice structure compatible with multiplicative linear logic.

Other logical constructs can be built on top :

• modalities ⟨a⟩A and [a]A for behaviours that start with an action a
• exponential modalities !A and ?A for replicable processes

Conjunctive structures

Basic structure

A conjunctive structure consists in

• a complete lattice (𝒜, ≤) — behaviours ordered by refinement
• a monotonic binary operator ⊗ — parallel composition of independent behaviours
• a contravariant unary operator (⋅)^⊥ — dual behaviour

Add a few natural conditions.

A conjunctive structure is involutive if a^⊥⊥ = a for all a ∈ 𝒜.

Derived operators

• a ⊸ b := (a ⊗ b^⊥)^⊥ — processes that react well to an offer of a and expectation of b
• a ∗ b := ⋁{c; a ≤ b ⊸ c} — an abstract notion of application among realizers
• By construction, a ∗ b ≤ c iff a ≤ b → c.

Linear conjunctive algebras

This structure allows for defining particular inhabitants of 𝒜, following the ideas of implicative algebras :

Conjunctive algebras

A separator is a subset 𝒮 ⊆ 𝒜 that is upwards closed, stable under modus ponens (for the implication ⊸) and contains 𝐬₁, …, 𝐬₅.

This is essentially equivalent to an implicative algebra.

Linear conjunctive algebras

Removing 𝐬₁ and 𝐬₂ from the requirement on separators yields a linear conjunctive algebra.

• This models multiplicative linear logic.
• Extra constructs and axioms can be included to handle full linear logic.

Instances of linear conjunctive algebras

• Phase spaces (the analogue of Heyting algebras for linear logic) :

  • take a commutative monoid M and a subset ⊥ ⊆ M
  • define orthogonality : x ⊥ y iff xy ∈ M
  • set 𝒜 := {a^⊥; a ⊆ M} and a ⊗ b := {xy; x ∈ a, y ∈ b}^⊥⊥

• Coherence spaces (a standard model for proofs in linear logic) :

  • for x, y ⊆ ℕ, set x⊥y iff ♯(x ∩ y) ≤ 1
  • set 𝒜 := {a^⊥; a ⊆ 𝒫(ℕ)}
  • set a ⊗ b := {x × y; x ∈ a, y ∈ b}^⊥⊥ for some bijection ⟨,⟩ : ℕ² → ℕ

  … up to some details

• Lattices of process behaviours

  • take ⊗ as explained before for a generic composition structure
  • add actions in ⊗ to interpret session types

Open questions

We get a suitable structure to fit process behaviours, but…

• Only deterministic and functional processes are captured by pure linear logic, we need extra principles to describe useful concurrent phenomena

  • Define A ∥ B := {P ∥ Q; P ∈ A, Q ∈ B}^⫫ ⫫, syntactically.
  • Somehow, the ∥ connective is to ⊗ what ∧ is to × in implicative structures.
  • The axioms it should satisfy are yet to be identified.

• Specification techniques for concurrent realisability still have to be developed.

• How does the quantum λ-calculus fit in this framework?

References