Types of Fireballs
The noble art of non-idempotent intersection types in Call-by-Value

Giulio Guerrieri1
1

Beniamino Accattoli2

DISI, Università di Bologna
2

INRIA, Saclay

Crecogi/Elica/GDRI-LL
Paris, October 10, 2018

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

1 / 23

Outline

1

Introduction

2

The rise and the fall of the fireball calculus λfire

3

The split fireball calculus λsplit
fire and multi types

4

Tight type derivations and exact bounds

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

2 / 23

Outline

1

Introduction

2

The rise and the fall of the fireball calculus λfire

3

The split fireball calculus λsplit
fire and multi types

4

Tight type derivations and exact bounds

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

3 / 23

What is a good λ-calculus?
There are many variants of λ-calculus:
Strong or weak (evaluation can fire under λ’s or not);Term may be open or only closed;
Evaluation strategies: call-by-name (CbN), call-by-value (CbV), call-by-need;With or without explicit substitutions, with or without linear substitutions;...
What is a good λ-calculus? Some (non-exhaustive) criteria:
1

Rewriting;2

Logic;

3

Implementation;

4

Cost model;

5

Denotations;

6

Equality.

Meta-principle: The more principles are connected, the better.
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

4 / 23

What is a good λ-calculus?
There are many variants of λ-calculus:
Strong or weak (evaluation can fire under λ’s or not);Term may be open or only closed;
Evaluation strategies: call-by-name (CbN), call-by-value (CbV), call-by-need;With or without explicit substitutions, with or without linear substitutions;...
What is a good λ-calculus? Some (non-exhaustive) criteria:
1

Rewriting;2

Logic;

3

Implementation;

4

Cost model;

5

Denotations;

6

Equality.

Meta-principle: The more principles are connected, the better.
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

4 / 23

Open Call-by-Value
The setting we will study via non-idempotent intersection types: Open CbV, i.e.
evaluation is weak (does not reduce under λ’s),
terms are possibly open.
intermediate setting between Strong CbV (which evaluates under λ’s) andClosed CbV (terms are closed and evaluation is weak).
Motivation: Closed CbV is enough for modeling programming languages, notproof-assistants. Strong CbV is a very tricky setting.
In the literature, there are many equivalent presentations of Open CbV.
The fireball calculus λfire is one of them, with many good properties...
elegant rewrite theory, clear logical understanding;simple implementation in abstract machines, with a reasonable cost model;. . . many inventors with different motivations: Ronchi Della Rocca & Paolini(1999, 2004), Grégoire & Leroy (2002), Accattoli & Sacerdoti Coen (2014);. . . and a big problem: there is no adequate denotational model for it!
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

5 / 23

Open Call-by-Value
The setting we will study via non-idempotent intersection types: Open CbV, i.e.
evaluation is weak (does not reduce under λ’s),
terms are possibly open.
intermediate setting between Strong CbV (which evaluates under λ’s) andClosed CbV (terms are closed and evaluation is weak).
Motivation: Closed CbV is enough for modeling programming languages, notproof-assistants. Strong CbV is a very tricky setting.
In the literature, there are many equivalent presentations of Open CbV.
The fireball calculus λfire is one of them, with many good properties...
elegant rewrite theory, clear logical understanding;simple implementation in abstract machines, with a reasonable cost model;. . . many inventors with different motivations: Ronchi Della Rocca & Paolini(1999, 2004), Grégoire & Leroy (2002), Accattoli & Sacerdoti Coen (2014);. . . and a big problem: there is no adequate denotational model for it!
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

5 / 23

Non-idempotent intersection types
Non-idempotent intersections types (aka multi-types) have many features:qualitative: they characterize normalization for (some strategy of) λ-calculus;
quantitative: they provide bounds on the execution time (i.e. the number of
β-steps) to reach the normal form;
denotational semantics: they can be seen as a syntactic presentation ofrelational semantics, a denotational model of λ-calculus;
linear logic interpretation: they are deeply linked to linear logic.
De Carvalho’s System R (2009) shows all these features for CbN λ-calculus.
Our goal: to show these features in a CbV setting.
Rmk (for LL friends only): The multi-type system used in the λ-calculus depends
on the evaluation mechanism, according the two Girard’s translations.
CbN(A → B) = !An ( B nnG. Guerrieri, B. Accattoli

CbV ("boring")(A → B)v = !Av ( !B v

Types of Fireballs

Elica/GDRI-LL 2018/10/10

6 / 23

Non-idempotent intersection types
Non-idempotent intersections types (aka multi-types) have many features:qualitative: they characterize normalization for (some strategy of) λ-calculus;
quantitative: they provide bounds on the execution time (i.e. the number of
β-steps) to reach the normal form;
denotational semantics: they can be seen as a syntactic presentation ofrelational semantics, a denotational model of λ-calculus;
linear logic interpretation: they are deeply linked to linear logic.
De Carvalho’s System R (2009) shows all these features for CbN λ-calculus.
Our goal: to show these features in a CbV setting.
Rmk (for LL friends only): The multi-type system used in the λ-calculus depends
on the evaluation mechanism, according the two Girard’s translations.
CbN(A → B) = !An ( B nnG. Guerrieri, B. Accattoli

CbV ("boring")(A → B)v = !Av ( !B v

Types of Fireballs

Elica/GDRI-LL 2018/10/10

6 / 23

Non-idempotent intersection types
Non-idempotent intersections types (aka multi-types) have many features:qualitative: they characterize normalization for (some strategy of) λ-calculus;
quantitative: they provide bounds on the execution time (i.e. the number of
β-steps) to reach the normal form;
denotational semantics: they can be seen as a syntactic presentation ofrelational semantics, a denotational model of λ-calculus;
linear logic interpretation: they are deeply linked to linear logic.
De Carvalho’s System R (2009) shows all these features for CbN λ-calculus.
Our goal: to show these features in a CbV setting.
Rmk (for LL friends only): The multi-type system used in the λ-calculus depends
on the evaluation mechanism, according the two Girard’s translations.
CbN(A → B) = !An ( B nnG. Guerrieri, B. Accattoli

CbV ("boring")(A → B)v = !Av ( !B v

Types of Fireballs

Elica/GDRI-LL 2018/10/10

6 / 23

Outline

1

Introduction

2

The rise and the fall of the fireball calculus λfire

3

The split fireball calculus λsplit
fire and multi types

4

Tight type derivations and exact bounds

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

7 / 23

Plotkin’s CbV λ-calculus
x | λx.t | tu
x | λx.th·i | vC | Ct

Terms
ValuesLeft evaluation contexts

t, u, sv, v0CRule at top level(λx.t)v 7→βv t{v /x}Contextual closure
C hti →βv C hui if t 7→βv u

::=
::=
::=

Plotkin’s CbV is well-behaved when evaluation is weak and terms are only closed.
Consider the case of weak evaluation and possibly open terms (Open CbV).
t := (λz.δ)(xx)δ

where δ := λy .yy

t is βv -normal but it "morally" shouldn’t! It should behave like the diverging δδ.
In any denotational model for CbV, t has the same semantics as δδ;for any sensitive notion of observational equivalence, t and δδ are equivalent.

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

8 / 23

The fireball calculus λfire
Restore the good properties of Plotkin’s CbV for Open CbV.
Terms
ValuesFireballs
Inert terms
Right evaluation contexts
Rule at top level(λx.t)v 7→βv t{v /x}(λx.t)i 7→βi t{i/x}Reductiont, u, s, r
v , v 0 , v 00
f , f 0 , f 00
i, i 0 , i 00
C

::=
::=
::=
::=
::=

x | λx.t | tu
x | λx.t
v |i
xf1 . . . fn n > 0
h·i | tC | Cf

Contextual closure
C hti →βv C hui if t 7→βv u
C hti →βi C hui if t 7→βi u→βf := →βv ∪ →βi

Example: (λz.δ)(xx)δ →βi δδ →βv δδ →βv . . .

(where δ := λy .yy )Proposition (Distinctive properties of λfire )1

Open harmony: t is βf -normal if and only if t is a fireball.

2

Conservative open extension: t →βf u if and only if t →βv u, when t is closed.

3

Evaluation and inert substitutions commute t →βf u iff t{i/x} →βf u{i/x}.
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

9 / 23

Non-idempotent intersection types for CbV (Ehrhard, 2012)
Multi types and linear types are defined by mutual induction:
multiset0linear types L, L ::= P ( Qz }| {
multi types P, Q ::= [L1 , . . . , Ln ] (n ≥ 0)

there are no base types: their role is played by the empty multiset [ ] (n = 0);
A multi type [L1 , . . . , Ln ] has to be intended as a conjunction L1 ∧ · · · ∧ Ln ;this conjunction ∧ is commutative and associative, non-idempotent;t : [L1 , L2 , L2 ] intuitively means that t can be used once as data of type L1
and twice as data of type L2 .
x :P ` x :PaxΓ ` t : [P ( Q]∆ ` u :P@Γ ] ∆ ` tu : Qn∈NΓ1 , x : P1 ` t : Q1...
Γn , x : Pn ` t : QnλΓ1 ] · · · ] Γn ` λx.t : [P1 ( Q1 , . . . , Pn ( Qn ]where Γ ] ∆ is the pointwise multiset sum between type contexts.
This nothing but the CbV counterpart of De Carvalho’s System R for CbN.
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

10 / 23

A concrete model for Plotkin’s CbV: relational semantics
The semantics of a term is a the set of its types, together with their type contexts.
If x1 , . . . , xn are pairwise distinct variables, and fv(t) ⊆ {x1 , . . . , xn }, we say that~x = (x1 , . . . , xn ) is suitable for t. Given ~x suitable for t, its semantics is:
JtK~x := {((P1 , . . . , Pn ), Q) | ∃ π B x1 : P1 , . . . , xn : Pn ` t : Q} .
Notation: π B Γ ` t : P means "π is a type derivation with conclusion Γ ` t : P".

Theorem (invariance under →βv , Ehrhard 2012)
Let ~x be a suitable list of variables for t and u. If t →βv u then JtK~x = JuK~x .
Terminology: A denotational model for a λ-calculus is adequate if it characterizes
all and only the normalisable terms.
In relational semantics: JtK = ∅ if and only if t is not normalisable.
CbV relational semantics is not adequate for Plotkin’s CbV:
J(λz.δ)(xx)δKx = ∅G. Guerrieri, B. Accattoli

butTypes of Fireballs(λz.δ)(xx)δ is βv -normal.

Elica/GDRI-LL 2018/10/10

11 / 23

A concrete model for Plotkin’s CbV: relational semantics
The semantics of a term is a the set of its types, together with their type contexts.
If x1 , . . . , xn are pairwise distinct variables, and fv(t) ⊆ {x1 , . . . , xn }, we say that~x = (x1 , . . . , xn ) is suitable for t. Given ~x suitable for t, its semantics is:
JtK~x := {((P1 , . . . , Pn ), Q) | ∃ π B x1 : P1 , . . . , xn : Pn ` t : Q} .
Notation: π B Γ ` t : P means "π is a type derivation with conclusion Γ ` t : P".

Theorem (invariance under →βv , Ehrhard 2012)
Let ~x be a suitable list of variables for t and u. If t →βv u then JtK~x = JuK~x .
Terminology: A denotational model for a λ-calculus is adequate if it characterizes
all and only the normalisable terms.
In relational semantics: JtK = ∅ if and only if t is not normalisable.
CbV relational semantics is not adequate for Plotkin’s CbV:
J(λz.δ)(xx)δKx = ∅G. Guerrieri, B. Accattoli

butTypes of Fireballs(λz.δ)(xx)δ is βv -normal.

Elica/GDRI-LL 2018/10/10

11 / 23

But relational semantics is not a denotational model for λfire !
Relational semantics is not invariant under →βf !
(λz.y )(xx) →βf y(λz.zz)(xx) →βf (xx)(xx)orJ(λz.y )(xx)Kx,y 6= Jy Kx

J(λz.z)(xx)Kx,y 6= J(xx)(xx)Kx

All counterexamples are due to →βi , when an inert term is erased or duplicated.
Relational semantics is not adequate for Plotkin’s CbV;
Relational semantics is not a denotational model for λfire .
Goal: Forcing relational semantics to be an adequate denotational model for λfire .
Rmk: Any denotational model for the CbN λ-calculus is invariant under →βf(since →βf ⊆→β ), but there is no hope that it could be adequate for λfire :in CbN J(λx.y )(δδ)Ky = Jy Kybut

y is βf -normal, (λx.y )(δδ) is βf -diverging.

Ehrhard’s methodological law (what I learned in my PhD)
If there is a mismatch between syntax and semantics, the problem is in the syntax.
Change the syntax!
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

12 / 23

But relational semantics is not a denotational model for λfire !
Relational semantics is not invariant under →βf !
(λz.y )(xx) →βf y(λz.zz)(xx) →βf (xx)(xx)orJ(λz.y )(xx)Kx,y 6= Jy Kx

J(λz.z)(xx)Kx,y 6= J(xx)(xx)Kx

All counterexamples are due to →βi , when an inert term is erased or duplicated.
Relational semantics is not adequate for Plotkin’s CbV;
Relational semantics is not a denotational model for λfire .
Goal: Forcing relational semantics to be an adequate denotational model for λfire .
Rmk: Any denotational model for the CbN λ-calculus is invariant under →βf(since →βf ⊆→β ), but there is no hope that it could be adequate for λfire :in CbN J(λx.y )(δδ)Ky = Jy Kybut

y is βf -normal, (λx.y )(δδ) is βf -diverging.

Ehrhard’s methodological law (what I learned in my PhD)
If there is a mismatch between syntax and semantics, the problem is in the syntax.
Change the syntax!
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

12 / 23

But relational semantics is not a denotational model for λfire !
Relational semantics is not invariant under →βf !
(λz.y )(xx) →βf y(λz.zz)(xx) →βf (xx)(xx)orJ(λz.y )(xx)Kx,y 6= Jy Kx

J(λz.z)(xx)Kx,y 6= J(xx)(xx)Kx

All counterexamples are due to →βi , when an inert term is erased or duplicated.
Relational semantics is not adequate for Plotkin’s CbV;
Relational semantics is not a denotational model for λfire .
Goal: Forcing relational semantics to be an adequate denotational model for λfire .
Rmk: Any denotational model for the CbN λ-calculus is invariant under →βf(since →βf ⊆→β ), but there is no hope that it could be adequate for λfire :in CbN J(λx.y )(δδ)Ky = Jy Kybut

y is βf -normal, (λx.y )(δδ) is βf -diverging.

Ehrhard’s methodological law (what I learned in my PhD)
If there is a mismatch between syntax and semantics, the problem is in the syntax.
Change the syntax!
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

12 / 23

Outline

1

Introduction

2

The rise and the fall of the fireball calculus λfire

3

The split fireball calculus λsplit
fire and multi types

4

Tight type derivations and exact bounds

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

13 / 23

The split fireball calculus λsplit
fire

Goal: A different presentation of λfire that has an adequate denotational model.
Terms, Values, Fireballs,
Inert terms, Right ev. contexts

as for the fireball calculus λfire

Environments
Programs
Rules
Reduction

E
p

::=
::=

(C h(λx.t)v i, E ) →βv(C h(λx.t)ii, E ) →βi→βf :=

 | [i/x] : E(t, E )
(C ht{v /x}i, E )(C ht)i, [i/x] : E )→βv ∪ →βi

Proposition (Harmony for λsplit
fire )A program p is normal iff p = (f , E ).
→(t, E @[i/x]) := (t, E ) {i/x}.
→(t, ) := t→Unfolding (from λsplit
fire to λfire ):Proposition (Strong bisimulation)
Plain to split: if p →βf u then there exists q such that p →βf q and q = u.

→Split to plain: if p →βf q then p →βf q .

2

→

1

→

→

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

14 / 23

The multi type system for λsplit
fire

x :P ` x :PaxΓ ` t : [P ( Q]∆ ` u :P@Γ ] ∆ ` tu : Qn∈NΓ1 , x : P1 ` t : Q1...
Γn , x : Pn ` t : QnλΓ1 ] · · · ] Γn ` λx.t : [P1 ( Q1 , . . . , Pn ( Qn ]Γ ` t :PesΓ ` (t, ) : P

Γ, x : P ` (t, E ) : Q∆ ` i :Pes@Γ ] ∆ ` (t, E @[i/x]) : Q

1

Size |t| of a term t: the number of its applications not in the scope of λ’s.

2Size |p| of a program (t, E ): |t| plus the sizes of the inert terms in E .

3Size |π| of a type derivation π: the number of its @ rules.

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

15 / 23

Examples and intuitions about multi types for CbV
Example:ax

x:[] ` x:[]λλ` I :[]
πII = ` I : [[ ] ( [ ]]@` II : [ ]es` (II , ) : [ ]

λ

πI =

` I :[]es` (I , ) : [ ]where I := λx.x

Note that (II , ) →βf (I , ) (with 1 βf -step) and |πII | = 1 = |πI | + 1.
Idea: [ ] is the type of terms that can be erased.
In multi types for CbN, every term, even a diverging one, is typable with [ ].
in CbN every term can be erased, even the diverging ones;in CbN adequacy is formulated with respect to non-empty types.
In multi-types for CbV, terms have to be evaluated before being erased.
in CbV, normalisable terms and erasable terms coincide;in CbV, a term is typable if and only if it is typable with [ ].

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

16 / 23

Examples and intuitions about multi types for CbV
Example:ax

x:[] ` x:[]λλ` I :[]
πII = ` I : [[ ] ( [ ]]@` II : [ ]es` (II , ) : [ ]

λ

πI =

` I :[]es` (I , ) : [ ]where I := λx.x

Note that (II , ) →βf (I , ) (with 1 βf -step) and |πII | = 1 = |πI | + 1.
Idea: [ ] is the type of terms that can be erased.
In multi types for CbN, every term, even a diverging one, is typable with [ ].
in CbN every term can be erased, even the diverging ones;in CbN adequacy is formulated with respect to non-empty types.
In multi-types for CbV, terms have to be evaluated before being erased.
in CbV, normalisable terms and erasable terms coincide;in CbV, a term is typable if and only if it is typable with [ ].

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

16 / 23

Examples and intuitions about multi types for CbV
Example:ax

x:[] ` x:[]λλ` I :[]
πII = ` I : [[ ] ( [ ]]@` II : [ ]es` (II , ) : [ ]

λ

πI =

` I :[]es` (I , ) : [ ]where I := λx.x

Note that (II , ) →βf (I , ) (with 1 βf -step) and |πII | = 1 = |πI | + 1.
Idea: [ ] is the type of terms that can be erased.
In multi types for CbN, every term, even a diverging one, is typable with [ ].
in CbN every term can be erased, even the diverging ones;in CbN adequacy is formulated with respect to non-empty types.
In multi-types for CbV, terms have to be evaluated before being erased.
in CbV, normalisable terms and erasable terms coincide;in CbV, a term is typable if and only if it is typable with [ ].

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

16 / 23

Examples and intuitions about multi types for CbV
Example:ax

x:[] ` x:[]λλ` I :[]
πII = ` I : [[ ] ( [ ]]@` II : [ ]es` (II , ) : [ ]

λ

πI =

` I :[]es` (I , ) : [ ]where I := λx.x

Note that (II , ) →βf (I , ) (with 1 βf -step) and |πII | = 1 = |πI | + 1.
Idea: [ ] is the type of terms that can be erased.
In multi types for CbN, every term, even a diverging one, is typable with [ ].
in CbN every term can be erased, even the diverging ones;in CbN adequacy is formulated with respect to non-empty types.
In multi-types for CbV, terms have to be evaluated before being erased.
in CbV, normalisable terms and erasable terms coincide;in CbV, a term is typable if and only if it is typable with [ ].

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

16 / 23

Properties of multi types for CbV: correctness
Proposition (Type derivations bound the size of normal forms)
Let π B Γ ` p : P be a type derivation for a normal program p. Then |p| ≤ |π|.

Proposition (quantitative subject reduction)
Let p and q be programs and π B Γ ` p : P be a type derivation. If p →βf q thenthere exists a type derivation σ B Γ ` q : P such that |π| = |σ| + 1.
From propositions above, it follows that typability implies termination:

Theorem (correctness)
Let π B Γ ` p : P be a type derivation. Then there is a normalising evaluationd : p →∗βf q such that |d| + |q| ≤ |π|.

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

17 / 23

Properties of multi types for CbV: correctness
Proposition (Type derivations bound the size of normal forms)
Let π B Γ ` p : P be a type derivation for a normal program p. Then |p| ≤ |π|.

Proposition (quantitative subject reduction)
Let p and q be programs and π B Γ ` p : P be a type derivation. If p →βf q thenthere exists a type derivation σ B Γ ` q : P such that |π| = |σ| + 1.
From propositions above, it follows that typability implies termination:

Theorem (correctness)
Let π B Γ ` p : P be a type derivation. Then there is a normalising evaluationd : p →∗βf q such that |d| + |q| ≤ |π|.

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

17 / 23

Properties of multi types for CbV: completenessProposition (normal forms are typable)
1

Normal program: For any normal program, there exists a type derivation
π B Γ ` p : P for some type context Γ and some multi type P.

2Inert term: For any multi type Q and any inert term i, there exists a typederivation σ B σ ` i : Q for some type context ∆.

Proposition (quantitative subject expansion)
Let p and q be programs and σ B Γ ` q : P be a type derivation. If p →βf q thenthere exists a type derivation π B Γ ` p : P such that |π| = |σ| + 1.
From propositions above, it follows that termination implies typability:

Theorem (completeness)
Let d : p →∗βf q be a normalising evaluation. Then there is a type derivation
π B Γ ` p : P, and it satisfies |d| + |q| ≤ |π|.
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

18 / 23

Properties of multi types for CbV: completenessProposition (normal forms are typable)
1

Normal program: For any normal program, there exists a type derivation
π B Γ ` p : P for some type context Γ and some multi type P.

2Inert term: For any multi type Q and any inert term i, there exists a typederivation σ B σ ` i : Q for some type context ∆.

Proposition (quantitative subject expansion)
Let p and q be programs and σ B Γ ` q : P be a type derivation. If p →βf q thenthere exists a type derivation π B Γ ` p : P such that |π| = |σ| + 1.
From propositions above, it follows that termination implies typability:

Theorem (completeness)
Let d : p →∗βf q be a normalising evaluation. Then there is a type derivation
π B Γ ` p : P, and it satisfies |d| + |q| ≤ |π|.
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

18 / 23

Relational semantics is an adequate model for λsplit
fire
Corollary (invariance)
Let ~x be a suitable list of variables for p and q. If p →βf q then JpK~x = JqK~x .

Corollary (adequacy)
Let ~x be a suitable list of variables for p. The following are equivalent:
1

Termination: p is βf -normalizable;

2

Typability: there is a type derivation π B Γ ` p : P for some Γ and P;

3

Non-empty denotation: JpK~x 6= ∅.

Rmk: λsplit
fire and λfire and Plotkin’s CbV are the same calculus when restricted toclosed terms.
Adequacy theorem above shows also that relational semantics is adequate forclosed Plotkin’s CbV.

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

19 / 23

Relational semantics is an adequate model for λsplit
fire
Corollary (invariance)
Let ~x be a suitable list of variables for p and q. If p →βf q then JpK~x = JqK~x .

Corollary (adequacy)
Let ~x be a suitable list of variables for p. The following are equivalent:
1

Termination: p is βf -normalizable;

2

Typability: there is a type derivation π B Γ ` p : P for some Γ and P;

3

Non-empty denotation: JpK~x 6= ∅.

Rmk: λsplit
fire and λfire and Plotkin’s CbV are the same calculus when restricted toclosed terms.
Adequacy theorem above shows also that relational semantics is adequate forclosed Plotkin’s CbV.

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

19 / 23

Outline

1

Introduction

2

The rise and the fall of the fireball calculus λfire

3

The split fireball calculus λsplit
fire and multi types

4

Tight type derivations and exact bounds

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

20 / 23

Tight type derivations
In CbN, multi-types can provide exact bounds for the evaluation length and forthe size of normal forms.
Can we extract this quantitative information in Open CbV as well? Yes!
We define two subsets of linear types and multi types:
inert linear types Li ::= [ ] ( P iinert multi types P i ::= [Li1 , . . . , Lin ] (n ≥ 0)

A type context Γ is inert if it assigns only inert multi types to variables.
A type derivation π B Γ ` p : P isinert if Γ is a inert type context;tight if π is inert and P = [ ].
Intuition: Any βf -normalisable (i.e. any typable) program is typable with type [ ].
More precisely, with a tight type derivation.

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

21 / 23

Tight type derivations
In CbN, multi-types can provide exact bounds for the evaluation length and forthe size of normal forms.
Can we extract this quantitative information in Open CbV as well? Yes!
We define two subsets of linear types and multi types:
inert linear types Li ::= [ ] ( P iinert multi types P i ::= [Li1 , . . . , Lin ] (n ≥ 0)

A type context Γ is inert if it assigns only inert multi types to variables.
A type derivation π B Γ ` p : P isinert if Γ is a inert type context;tight if π is inert and P = [ ].
Intuition: Any βf -normalisable (i.e. any typable) program is typable with type [ ].
More precisely, with a tight type derivation.

G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

21 / 23

Exact bounds for Open CbV
Tight type derivations have a nice property with respect to normal forms:

Lemma (tight type derivations are minimal)
If π B Γ ` p : [ ] is a tight type derivation and p is βf -normal, then |p| = |π| and|π| is minimal among the type derivations of p.
We can refine correctness and completeness with exact quantitative information:

Theorem (tight correctness)
If π B Γ ` p : [ ] is a tight type derivation, then there is a normalising evaluationd : p →∗βf q such that |d| + |q| = |π|. And if q is a value, then |d| = |π|.

Theorem (tight completeness)
If d : p →∗βf q is a normalizing evaluation, then there is a tight type derivation
π B Γ ` p : [ ], and it satisfies |d| + |q| = |π|. And if q is a value, then |d| = |π|.
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

22 / 23

Exact bounds for Open CbV
Tight type derivations have a nice property with respect to normal forms:

Lemma (tight type derivations are minimal)
If π B Γ ` p : [ ] is a tight type derivation and p is βf -normal, then |p| = |π| and|π| is minimal among the type derivations of p.
We can refine correctness and completeness with exact quantitative information:

Theorem (tight correctness)
If π B Γ ` p : [ ] is a tight type derivation, then there is a normalising evaluationd : p →∗βf q such that |d| + |q| = |π|. And if q is a value, then |d| = |π|.

Theorem (tight completeness)
If d : p →∗βf q is a normalizing evaluation, then there is a tight type derivation
π B Γ ` p : [ ], and it satisfies |d| + |q| = |π|. And if q is a value, then |d| = |π|.
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

22 / 23

What are we counting?
λsplitfire mimics LL proof-nets behavior via "boring" translation A ⇒ B(C h(λx.t)v i, E ) →βv (C ht{v /x}i, E )(·)v!Av ( !B v.

(C h(λx.t)ii, E ) →βi (C hti, [i/x] : E )a βv -step corresponds to a multiplicative followed by an exponential step;a βi -step corresponds to a multiplicative step.
The number of βf -steps is the number of multiplicative steps in LL proof-nets.
Tight derivations count the number of multiplicative steps to reach a normal
form of a LL proof-net.
Rmk: The number of βf -steps is a reasonable cost model (λsplit
fire can be
implemented on a RAM with an overhead that is linear in the number of βf -step).
Summing up: At least in the CbV fragment of LL:
the multiplicative step is the computationally meaningful cut-elimination step;
the exponential step just allows evaluation to go on.
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

23 / 23

What are we counting?
λsplitfire mimics LL proof-nets behavior via "boring" translation A ⇒ B(C h(λx.t)v i, E ) →βv (C ht{v /x}i, E )(·)v!Av ( !B v.

(C h(λx.t)ii, E ) →βi (C hti, [i/x] : E )a βv -step corresponds to a multiplicative followed by an exponential step;a βi -step corresponds to a multiplicative step.
The number of βf -steps is the number of multiplicative steps in LL proof-nets.
Tight derivations count the number of multiplicative steps to reach a normal
form of a LL proof-net.
Rmk: The number of βf -steps is a reasonable cost model (λsplit
fire can be
implemented on a RAM with an overhead that is linear in the number of βf -step).
Summing up: At least in the CbV fragment of LL:
the multiplicative step is the computationally meaningful cut-elimination step;
the exponential step just allows evaluation to go on.
G. Guerrieri, B. Accattoli

Types of Fireballs

Elica/GDRI-LL 2018/10/10

23 / 23