On the Values of Reducibility Candidates

Colin Riba

Laboratoire de l’Informatique du Parallélisme^{} ENS Lyon – Université de Lyon

                          colin.riba@ens-lyon.fr
                   http://perso.ens-lyon.fr/colin.riba/

Abstract. The straightforward elimination of union types is known to break subject reduction, and for some extensions of the lambda-calculus, to break strong normalization as well. Similarly, the straightforward elimination of implicit existential types breaks subject reduction. We propose elimination rules for union types and implicit existential quantification which use a form call-by-value issued from Girard’s reducibility candidates. We show that these rules remedy the above mentioned difficulties, for strong normalization and, for the existential quantification, for subject reduction as well. Moreover, for extensions of the lambda-calculus based on intuitionistic logic, we show that the obtained existential quantification is equivalent to its usual impredicative encoding w.r.t. provability in realizability models built from reducibility candidates and biorthogonals.

1 Introduction

Although useful in some type systems [2, 12], implicit existential types can be problematic because of their elimination rule. Some of these problems seem related to similar issues with union types.

The straightforward elimination of union types is known to break subject reduction [1], and for some extensions of the -calculus, to break strong normalization as well [14]. The counter example for subject reduction given in [1] has been adapted to implicit existential types in [18]. Concerning strong normalization, the difficulties are related to type interpretations in reducibility. Usually, types are interpreted by closure operators. Union types and implicit existential types are both interpreted by the closure of the union. When no further assumption is made, the validity of their elimination rules follows from the closure under unions of the interpretations (i.e. when closure preserves unions). But results of [14] on failures of strong normalization with elimination of union types show that some rewrite systems are not compatible with type interpretations which are closed under unions.

These problems with elimination are caused by possibly bad cohabitations between the rules of elimination and the reductions of some calculi. This suggests

UMR 5668 CNRS ENS-Lyon UCBL INRIA, 46 allée d’Italie, 69364 Lyon Cedex 7, France

either to adapt the elimination rules to the calculus, or to adapt the calculus to the elimination rules. In call-by-value settings, the first solution is studied in [6, 19] for systems with union and implicit existential quantification. Both works propose elimination rules restricted to call-by-value evaluation contexts. The second solution is studied in [8] for a call-by-value -calculus. On a related subject, a reducibility interpretation of Moggi’s computational calculus based on a combination of reducibility candidates and biorthogonals is given in [11].

In this paper, working on rewriting-based extensions of the -calculus, we propose to eliminate union and implicit existential types by a let in which is reduced according to a form call-by-value issued from Girard’s reducibility candidates [7]. In contrast with [8, 6, 19], this does not force the whole calculus to be call-by-value. We build on [15, 16], where a general notion of Girard’s candidates is proposed. This framework assumes only a rewrite relation and a set of contexts, called elimination contexts, subject to some axioms. The basic ingredient is an interaction property between terms and elimination contexts. Terms which interact with elimination contexts are called values since they are observable. They are the values that we use in the reduction of the let. Our notion of call-by-value is not the usual one (considered for instance in [8]) since in our case variables are not values. From a theoretical point of view, this allows to define the reduction of let in by a rewrite relation. This would have been impossible if variables were values.

We present the basic tools in Sect. 2. The axiomatization of reducibility candidates is presented in Sect. 3. In Sect. 4, we show how to extend modularly our framework with the let and prove that the axioms for reducibility are preserved. Section 5 presents three applications. First, strong normalization with union types and possibly non-deterministic simple rewriting in Sect. 5.1. Second, strong normalization and subject reduction with existential, product and sum types in Sect. 5.2. Third, concerning extensions of the -calculus based on intuitionistic logic, we show in Sect. 5.3 that the obtained existential quantification is equivalent to the usual impredicative encoding w.r.t. provability in realizability models built from reducibility candidates and biorthogonals.

A version of this paper with full proofs is available from the webpage of the author.

2 Preliminaries

Terms. A signature is a family of sets _{}_{ℕ} such that _{}contains algebraic symbols of arity . We consider -terms with uncurryied symbols f in a signature and variables :

f _{}_{}

where f _{}. Let be the set of pure -terms . A substitution is a function of finite domain. The capture-avoiding application of to a term is written or _{}_{}_{}_{}if _{}_{}. We let be the substitution which maps to and is equal to on .

Reductions. A rewrite relation is a binary relation _{} which is closed under contexts and substitutions. Write _{}for _{}_{}and let _{}_{def} _{}. Define the product extension of _{}as _{}_{}_{} when there is such that _{}_{}_{}and _{}_{}for all . We denote by _{}the set of strongly normalizing terms for _{}, which is the smallest set such that _{}_{}_{}. Let _{}

be the smallest rewrite relation on  such that  _{}.

The Polymorphic -Calculus _{}. Our core language is the Curry-style polymorphic -calculus _{}. Its types are the formulas of second-order minimal logic, with variables _{}:

Its typing rules are the following:

\begin{matrix}Ax \overline{}I \frac{}{}E \frac{}{} \\ I \frac{}{}E \frac{}{} \end{matrix}

Types without are called simple types, denoted by . The simply typed -calculus is _{}restricted to (hence without the rules I and E ).

Implicit Existential Types. We add to _{}implicit existential types. Let _{} be the extension of _{}with the second-order existential quantification . The usual implicit rules for are

I \frac{}{}E \frac{}{}

As for universal quantification, they are not reflected at the term level by corresponding constructors and eliminators. The rule E does not satisfy subject reduction [18].

Example 2.1 ([18]). Let , _{}, _{}and let be the context . Using E we have _{}. But _{}_{}_{}and _{}is not of type in .

Moreover, E causes difficulties with strong normalization. To explain them, we introduce some basic notions on reducibility.

Reducibility. Let _{}be a rewrite relation on . In strong normalization proofs based on reducibility, types are interpreted by sets of strongly normalizing terms ⟦ ⟧. Strong normalization of typable terms follows from the adequacy of the interpretation: typable terms must belong to the interpretation of their type. However, not every type interpretation is adequate. Usually, an adequate interpretation can be described by a closure operator on _{}, i.e. by a func-

tion ed  _{}_{}which is idempotent ( ed ed  ed ),
extensive ( ed ) and monotone (  ed  ed ). It is well-

known that the set of closed elements ed _{def} ed _{}is a complete lattice whose g.l.b.’s are given by intersections. We say that ed is a reducibility family if for all ed . There are essentially three kinds of reducibility families: Tait’s saturated sets [17], Girard’s reducibility candidates [7] and biorthogonals [13]. In this paper we focus on the last two.

Assume that ed is closed under the function space , which is defined as _{def} where . Given an assignment _{}ed , the interpretation ⟦ ⟧_{}^{ed} ed of polymorphic types is inductively defined as ⟦ ⟧_{}^{ed} _{def} ,

⟦  ⟧_{}^{ed}  _{def} ⟦ ⟧_{}^{ed} ⟦ ⟧_{}^{ed}  and ⟦ ⟧_{}^{ed}  _{def} _{ed} ⟦ ⟧_{}^{ed}

We say that ⟦ ⟧^{ed} is adequate if (  and  _{ed} ) implies  ⟦ ⟧_{}^{ed} ,
where  _{ed} if  ⟦ ⟧_{}^{ed} for all  . If ⟦ ⟧^{ed} is adequate
then  implies  _{}.

Adequacy and Existential Quantification. Adequacy w.r.t. the rules I and E is ensured by the definition of ⟦ ⟧_{}^{ed} . Dually, one might expect adequacy w.r.t. I and E for the extension of ⟦ ⟧_{}^{ed} to _{}defined as

⟦ ⟧_{}^{ed} _{def} ed _{ed} ⟦ ⟧_{}^{ed}

Since ⟦ ⟧_{}^{ed} ed _{ed} ⟦ ⟧_{}^{ed} , every reducibility family validates the rule I . This is less clear for E . We only know that it is validated by reducibility families which are closed under unions, i.e. such that ed for all ed . But closure under unions is not possible for all rewrite relations _{}. This is related to strong normalization problems with union types.

Union Types. Let _{}be the extension of simple types with intersection types and union types . _{}is equipped with a binary relation such that _{}is a preorder with all finite l.u.b.’s and g.l.b.’s and satisfying usual additional axioms for the arrow (see Sect. 5.1). The typing rules are those of extended with Sub and I (see Sect. 5.1). Intersections and unions are interpreted in ed similarly as quantifications: ⟦ ⟧_{}^{ed} _{def} ⟦ ⟧_{}^{ed} ⟦ ⟧_{}^{ed} and ⟦ ⟧_{}^{ed} _{def} ed ⟦ ⟧_{}^{ed} ⟦ ⟧_{}^{ed} . As with E , if ed is closed under unions, then ⟦ ⟧_{}^{ed} is adequate for the elimination of union:

E \frac{_{}_{}_{}_{}}{}

As E , the rule E does not satisfy subject reduction [1, 18].

Problems with Strong Normalization. There are extensions of -reduction with which the rule E allows to type non-strongly normalizing terms. We consider simple rewrite systems , that are finite sets of rewrite rules of the form f _{}_{}_{}, where f _{}, and _{}_{}are distinct variables. Algebraic symbols are typed using a rule inspired from [3]:

Fun_{}\frac{f _{}}{f}

For instance, with the non-deterministic simple rewrite system _{}_{}_{}_{} ( ), we have _{}_{}_{}_{}_{}_{}_{}_{}. By combining Fun_{} and E , we can type non-strongly normalizing terms, while the type system with Fun_{}but without E is strongly normalizing [14].

Example 2.2 ([14]). Let , _{}and _{}. There are types such that _{}_{}and _{}(note that ). Using E and Fun_{}we get _{}_{}_{}_{}. But _{}^{}_{}_{}_{}^{}_{}.

Call-by-Value Eliminations. In this paper, we propose and study a modified version of E and E which uses a call-by-value let in . We consider the extended set of terms

let  f _{}_{}let  in

and we replace E and E by the following rules:

E_{let} \frac{\begin{aligned}& _{} \\ _{}_{} & _{} \end{aligned}}{let  in}  E_{let} \frac{}{let  in}

The let is reduced according to a notion of value issued from Girard’s reducibility candidates (to be defined in Sect. 3). Given a rewrite relation _{}and a set of values , we extend _{}with the smallest rewrite relation _{}on _{let} s.t.

let  in  _{}if

We show that the rules E_{let} and E_{let} lead to strongly normalizing systems regardless of closure under unions. We moreover show that this may allow to recover subject reduction with implicit existential quantification.

Remark 2.3. The subtyping rule _{}_{}_{}_{}causes strong normalization problems similar to those of E [14]. Our solution does not handle it because it would imply to have a call-by-value arrow, while we want to force call-by-value only locally in E_{let} .

3 Reducibility Candidates

Reducibility candidates, denoted by _{}, form a reducibility family depending only on a rewrite relation _{}and a set of elimination contexts [15, 16]. They come with an inherent notion of values _{}, which are the terms that interact with elimination contexts (see Def. 3.4 below).

An Axiomatization. Our axiomatization of reducibility has been first presented in [15]. We use the version of [16] where details and proofs can be found.

Let  be a distinguished variable and _{}be a rewrite relation on  .

Definition 3.1 (Evaluation Contexts). A set of evaluation contexts for _{} is a set of terms containing exactly one occurrence of , and which is

closed under reduction: if  and  _{}then  .
If  and  then we let  _{def}  .

Values and neutral terms are defined by an interaction property between terms and evaluation contexts.

Definition 3.2 (Interacton, Values and Neutral Terms). Let be a set of evaluation contexts for _{}.

– A term interacts with for _{}, notation ⋈_{}, if there is a term such that _{}and which is not of the form ^{}^{}with .

– A value for _{}in is a term s.t. ⋈_{}for some . We denote by _{}the set of values for _{}in . Given , the set of values of is _{}_{def} _{}_{}^{}for some . We write _{}for .

– A term is neutral for _{}in if it is not a value. We denote by _{}the set of neutral terms for _{}in .

Values are observable terms, since they interact with evaluation contexts. For instance, the values for -reduction in evaluation contexts _{} are the -abstractions . Note that non-interaction is compositional:

Lemma 3.3. If ⋈_{}and ⋈_{}then ⋈_{}.

Reducibility candidates are defined from a rewrite relation and a set of evaluation contexts satisfying some axioms. These axioms define elimination contexts. The modular extension of this framework with let, presented in Sect. 4, requires to introduces new axioms of closure under substitutions.

Definition 3.4 (Elimination Contexts). Let be a set of evaluation contexts for _{}. Then is a set of elimination contexts for _{}if

– ,

– variables are neutral: _{},

– _{}is closed under composition with : if _{}and then .

– _{}is closed under substitution: if  _{}, then  _{}.
– _{}is closed under substitution: if  _{}, then  _{}.
– is closed under substitution: if  and  then

.

For instance, the contexts _{}are elimination contexts for -reduction. We assume given a set of elimination contexts for _{}.

Definition 3.5 (Reducibility Candidates). The set of reducibility candidates for _{}in , written _{}, is the set of all _{}such that

if  and _{}then  ,
if  _{}and  _{}then  .

There is a closure operator _{}_{}_{}such that _{} is the smallest reducibility candidate containing if _{}. The closure of the empty set is the set of hereditary neutral terms, i.e. the set of strongly normalizing neutral terms which never reduce to a value. Since variables are neutral terms in normal form (recall that _{}), we get for all candidate . It follows that reducibility candidates form a reducibility family. Note that the greatest element of _{}is _{}.

The axioms defining elimination contexts allow to show the following basic property of reducibility candidates. We use it to prove that elimination-based type interpretations (such as the function space ) preserve _{}.

Lemma 3.6 ([16]). Let  _{},  _{}and  _{}. If
for all  _{}, then  .
Proof. By induction on  _{}. Since  is neutral, it is sufficient to
show that  _{}. Let  _{}. Since is neutral  ^{}^{}with
. If _{}^{}then  by assumption. Otherwise  _{}
, and for all  _{}we have  _{}^{}, hence ^{}by  .

Thus ^{}by induction hypothesis.

The Values of Reducibility Candidates. An important property of reducibility candidates is that they are uniquely determined by their values:

Lemma 3.7 ([16]). Given  _{}and  _{}, we have  _{}if and

only if _{}_{}.

This paper builds on the following consequences of Lem. 3.7. Write ^{} when is a non-empty subset of .

Corollary 3.8.

\begin{matrix}_{}_{} &  & _{}_{} & _{} \\ _{}_{} &  & _{} & ^{}_{} \\ _{}_{}_{} &  & _{}_{}_{}_{} & _{}_{}_{} \\ _{}_{}_{} &  & _{}_{}_{} & _{}_{}_{} \end{matrix}

The first equality says that _{}is in some sense closed under union w.r.t. values. It will justify the typing rules E_{let} and E_{let} (Sect. 4.2). The last two ones state the distributivity of the candidate lattice, which is used in Sect. 5.1. All these properties are independent from the closure under unions of _{}.

Orthogonality. We now briefly discuss biorthogonality. See [16] for details on biorthogonality in our framework. Let _{}be a rewrite relation on and

be a set of elimination contexts for _{}. Define  as  if and
only if  _{}. Define the orthogonal of  (resp.  ) as
def
resp. ^{}_{def}

The induced map ^{}on _{}is a closure operator [16]. Write _{}^{}for . It is a reducibility family thanks to:

Lemma 3.9 ([16]). _{}^{}_{}.

4 A Call-by-Value Extension of Reducibility

We now insert the let presented in Sect. 2 into the reducibility candidates issued from a rewrite relation _{}on and a set of elimination contexts for _{}.

We first extend the set of terms from to _{let} (defined in Sect. 2). We then extend _{}to the smallest rewrite relation on _{let} containing the original relation _{}(which was defined on ). Now, let _{}be the smallest rewrite relation on _{let} such that let in _{}if _{}.

The delicate operation is to extend the set of elimination contexts. We need to extend both with contexts of the form let in and with contexts having the same shape as those in , but built on _{let} rather than on . This second operation is easy to express in the usual cases where is defined by a grammar (see Sect. 5.1 and Sect. 5.2). However, performing this operation on an arbitrary set while preserving the axioms of Def. 3.4 leads us to some technicalities. We chose to close by _{let}-substitution, but this causes difficulties w.r.t. stability by reduction. A solution is to close by substitution only the contexts which are linear in , but they need not to be stable by reduction. We therefore work with the set ^{lin} , defined as the set of -normal linear .

Definition 4.1. Let _{let} be the smallest set such that

lin  _{let}  _{let}
let  _{let}  let  in  _{let}

We now show that _{let} is a set of elimination contexts for _{}. This allows to define reducibility candidates and biorthogonals. We then show that this turns the closure of an union into an elimination-based interpretation.

4.1 Values, Neutral Terms and Elimination Contexts

In this section, we give the main steps of the proof that _{let} is a set of elimination contexts for _{}. We first give a characterization of the values and neutral terms for _{}in _{let} in terms of those for _{}in . Note that the let ensures that values for _{}in are values for _{}in _{let}. The characterization of neutral terms relies on the fact that values and non-variable neutral terms are not unifiable in let, which follows from the substitution axioms of Def. 3.4.

Proposition 4.2 (Values and Neutral Terms).

let  _{}_{let}
let  let  in  _{let}
let

In order to show that _{let} is a set of elimination contexts for _{}, we have to check the axioms of Defs. 3.1 and 3.4. Concerning Def. 3.1, linearity in follows from an easy induction on _{let}, using linearity in of in the base case. Stability by reduction is a consequence of the condition ^{lin} in the first clause of the definition of _{let}.

Concerning Def. 3.4, stability by substitution for values and non-variable neutral terms follows directly from Prop. 4.2. Stability by substitution for contexts follows from an easy induction on _{let}. Moreover, variables are neutral by Prop. 4.2, and the preservation of neutral terms by composition with elimination contexts is a consequence of Prop. 4.2 shown by induction on _{let}. Hence we have

Theorem 4.3. _{let} is a set of elimination contexts for _{}.

We thus obtain reducibility candidates _{_{let}} and biorthogonals _{_{let}}^{} directly from a rewrite relation _{}on and a set of elimination contexts .

4.2 An Elimination-Based Interpretation of Unions

In this section, we show that for reducibility candidates and biorthogonals, the let turns ed into the elimination-based interpretation _{ed} defined as

ed  s.t.  let  in

Hence, we get elimination-based interpretations of union and implicit existential types. This ensures the adequacy of reducibility candidates and biorthogonals w.r.t. E_{let} and E_{let} , but does not change the definition of the type interpretation using the closure of unions (see Sect. 5).

Write for _{_{let}} , ^{}for _{_{let}}^{}, for _{_{let}} , for _{_{let}} and for _{}. We begin by showing that _{}(resp. _{}^{}) is a reducibility candidate (resp. a biorthogonal).

Lemma 4.4. If ^{}then _{}.

Proof. Write  for _{}. We first show that  . Let  and
take _{def}  . Since  , we get let  in  ,
hence  . Stability by reduction  is immediate. For the clause  ,
take  such that _{}. Let  and such that  implies
. Since let  in  _{let}  and let  ^{}in  for all
, we have let  in  by Lem. 3.3.

Lemma 4.5. If ^{}^{}then _{}^{}^{}.

Proof. Since _{}^{}is the orthogonal of the non-empty subset of

let  in  ^{}^{}

We now show that _{ed} is the closure of the union when ed ^{}.

Theorem 4.6. If ed  ^{}and ^{}ed then _{ed}  ed  .

Proof. . Since ed is defined by a closure operator, by Lem. 4.4 and 4.5

it is sufficient to show that  _{ed} . Let  ,  ed and
s.t.  implies  . Note that  since  is not
empty. By Lem. 3.9, we have  . Since let  in is neutral, it

is sufficient to show that let in _{}. We reason by induction on pairs ordered by the product extension of _{}. Let such that let in _{}. There are two cases.

&  . Since  , we get  by assumption on .
let  ^{}in ^{}&  _{}^{}^{}. By  , we have ^{}and
that  ^{}. We get  by induction hypothesis.

. We have _{ed} ed by Lem. 4.4 and Lem. 4.5. Since ^{}we have ed ed . Therefore, by Cor. 3.8 it is sufficient to show that

ed  ed  . Let  _{ed} and take _{def} ed  . Since
, we obtain that let  in  . But let  in  _{}
since  . Hence  ed  by  .

5 Applications

We now discuss three applications. Our approach is to start from a given calculus made of a type system and a rewrite relation _{}. We provide a set of elimination contexts . This gives reducibility candidates (and biorthogonals) as in Sect. 3. We then apply the method of Sect. 4. Terms are extended with let, the rewrite relation _{}is extended with _{}, and we obtain elimination contexts _{let} by Def. 4.1. Using Thm. 4.3, we obtain reducibility candidates (and biorthogonals ^{}) for _{}in _{let}. We then extend the type system with E_{let} or E_{let} . Adequacy w.r.t. these rules is ensured by Thm. 4.6.

The first application concerns union types, the second one existential types and the third one deals with existential quantification in realizability models based on reducibility candidates and biorthogonals.

5.1 Union Types

We apply the framework presented in Sect. 4 to a calculus with union types, intersection types and (possibly non-deterministic) simple rewrite rules. We focus on reducibility candidates and do not consider biorthogonals since their lattice is not distributive. Some proofs are postponed until Sect. 5.2.

We consider simple types with unions and intersections _{}. As in [5], they are equipped with a preorder so that is a distributive lattice satisfying the additional axioms

and \frac{_{}_{}_{}_{}}{_{}_{}_{}_{}}

Given a simple rewrite system , we add to the rule Fun_{}and

I \frac{}{}Sub \frac{}{}

We consider reducibility candidates for _{}in elimination contexts _{}. By Thm. 4.3, we thus obtain reducibility candidates for _{}in the elimination

contexts _{let} . Note that let  in  _{}if and only if  .
Therefore, continuing Ex. 2.2, we have  let  _{}_{}in  , but
let  _{}_{}in  does not reduce to _{}_{}: since _{}_{}is not a value, we

must choose between _{}and _{}before performing the substitution.

Note that _{let} is the following set of contexts (see Lem. 5.2):

let in

We now add the rule E_{let} to the system.

Types are interpreted as in Sect. 2. Write ⟦ ⟧_{}for ⟦ ⟧_{}^{}. The correctness of the subtyping relation is standard [14], excepted that distributivity is ensured by Cor. 3.8. We get ⟦ ⟧_{}_{}since ^{}(Lem. 5.3).

Theorem 5.1. If  and  then  ⟦ ⟧_{}.

Proof. By induction on . The case of E_{let} follows from Thm. 4.6, which entails that ⟦ ⟧_{}⟦ ⟧_{}_{}⟦ ⟧_{}(see the proof of Thm. 5.5). Adequacy w.r.t. the other rules is standard [14].

5.2 Implicit Existential Types

We apply the framework of Sect. 4 to a calculus with existential, product and sum types. We show that it enjoys strong normalization and subject reduction.

The System. We let _{}be the extension of _{}with the binary product and the binary sum . Terms are built on the signature

def _{}_{}inj_{}inj_{}case

We extend -reduction with _{}_{}_{}_{}_{}and case inj_{}_{}_{}_{}_{}. The type system is that of _{}enriched with I and the following rules:

I \frac{_{}_{}_{}_{}}{_{}_{}_{}_{}}E \frac{_{}_{}}{_{}_{}}

I \frac{_{}}{inj_{}_{}_{}}E \frac{\begin{aligned}& _{}_{} \\ _{}_{} & _{}_{} \end{aligned}}{case _{}_{}} Reducibility. We consider the elimination contexts

case

The values are the terms of the form or inj_{}. We consider reducibility candidates for _{}in . By Thm. 4.3, we thus obtain reducibility candidates and biorthogonals ^{}for _{}in the elimination contexts _{let}.

Lemma 5.2. _{let} is the set of contexts

case  let  in

We add the rule E_{let} to the system. In the remaining of this section, we assume that ed ^{}. We extend the interpretation of Sect. 2 as follows:

⟦ ⟧_{}^{ed}  _{def}  _{}⟦ ⟧_{}^{ed}  _{}⟦ ⟧_{}^{ed}
⟦ ⟧_{}^{ed}  _{def}  ed  ⟦ ⟧_{}^{ed}  ⟦ ⟧_{}^{ed}

case

The correctness of the definition relies on the fact that the shape of elimination contexts has not been destroyed by their extension with let (Lem. 5.2).

Lemma 5.3. If  _{}_{}and  _{}then ⟦ ⟧_{}^{ed} ed .

Proof. In both cases for ed , we reason by induction on . The result is trivial if is a variable. The cases of and follow from the fact that ed is defined by a closure operator. We detail the case of . Write ⟦ ⟧ for ⟦ ⟧_{}^{ed} .

ed  . We have ⟦ ⟧ ⟦ ⟧  _{}since ⟦ ⟧ is not empty and ⟦ ⟧  _{}.
Stability by reduction follows from  on ⟦ ⟧. We get  by Lem. 3.6,
using that  _{let} for all  _{let} thanks to Lem. 5.2.
ed  ^{}. Since ⟦ ⟧ ⟦ ⟧ is orthogonal to  ⟦ ⟧  ⟦ ⟧^{}

which is a non-empty subset of _{}.

Since type constructors are interpreted by eliminations, Lem. 5.3 implies adequacy w.r.t. the elimination rules E , E and E . Adequacy w.r.t. the rules I , I and I follows from the following saturation lemma (recall that _{}and _{let}).

Lemma 5.4. For all  _{}, all  _{let} and all  ,

if

if_{_{}if}

case inj_{}if
case inj_{}if
Proof. Note that  _{}since  _{}. We detail the case of

. Since is neutral, by Lem. 3.6 it is sufficient to show that

if  _{}. We reason by induction on  ordered by the
product extension of _{}. Let such that  _{}. If  then we
are done by assumption. Otherwise,  ^{}^{}with  _{}^{}^{}and

we conclude by induction hypothesis, using that is closed under reduction.

Using Thm. 4.6 for the existential quantification, adequacy follows as usual.

Theorem 5.5. If  and  _{ed} then  ⟦ ⟧_{}^{ed} .
Proof. By induction on  . We detail the case of E_{let} . Let  .
By induction hypothesis we have  ⟦ ⟧_{}^{ed} . Since , if  ed
and ⟦ ⟧_{}^{ed} then  _{ed}  . By induction hypothesis
again, we deduce that  ⟦ ⟧_{}^{ed} for all  _{ed} ⟦ ⟧_{}^{ed} . We obtain
let  in  ⟦ ⟧_{}^{ed} since ⟦ ⟧_{}^{ed}  _{ed} ⟦ ⟧_{}^{ed} by Thm. 4.6.

Subject Reduction. We sketch the proof that let allows to recover subject reduction for implicit existential types. The key-point is that the reduction of a let in obtained from E_{let} is only made when is a value, in which case we know that its type has been obtained by a I rule (Prop. 5.6). This prevents us from the counter example of [18] (Ex. 2.1): we can type let in but this term does not reduce to _{}since is not a value.

Proposition 5.6 (Determinacy of Typing). Let _{_{let}} . If then there is such that .

The remaining of the proof directly follows that of [9] for _{}. It relies on usual substitution and inversion properties.

Substitution. (i) If  and  then  .
(ii) If  then  .
Inversion. (i) If  then  .
(ii) If  _{}_{}_{}_{}then  _{}_{}for all  .

(iii) If inj_{}_{}_{}then _{}.

Theorem 5.7 (Subject Reduction). If  and _{}then  .

5.3 Realizability Semantics of Existential Quantification

We now discuss the realizability interpretation of existential quantification in presence of the let. Realizability with implicit existential types is used e.g. in [12].

Given a reducibility family ed , write ⊩_{ed} (read realizes ) if is a closed term such that ⟦ ⟧_{}^{ed} for all _{}ed . In realizability models based on _{}, the existential quantification is usually encoded as ˜ def where . Using Thm 4.6, we define terms such that for reducibility candidates and biorthogonals, we have ⊩ ˜ and ⊩ ˜ (Thm. 5.9). This means that in the corresponding realizability models, the let makes the two existential quantifications equivalent w.r.t. provability.

We assume given a rewrite relation _{}on , which contains _{}and which is compatible with _{}in the following sense: if _{}and

is not of the form  ^{}^{}with  _{}^{}^{}, then  . We also

assume given a set of elimination contexts for _{}such that for all and such that is neutral for all . Note that this include the reduction systems presented in Sect. 5.1 and Sect. 5.2.

We obtain -terms with let and extend _{}with _{}. Elimination contexts are extended to _{let}. We thus obtain reducibility families _{_{let}} and _{_{let}}^{}, that we write and ^{}respectively. Note that compatibility with _{}is preserved: if _{}then either or ^{}^{}with . This ensures that if ⟦ ⟧_{}^{ed} for all ⟦ ⟧_{}^{ed} then ⟦ ⟧_{}^{ed} . Moreover, we still have _{let} for all _{let}

The formulas we consider are the types _{}. They are interpreted as in

Sect. 5.2, using Thm. 4.6. In particular ⟦ ⟧_{}^{ed}  _{ed} ⟦ ⟧_{}^{ed}  ed .
Definition 5.8. Given a type , let □  _{def}  , where .

Note that the boxed type □ is not the double-negation of . Boxed types are useful because of the following intermediate properties: given ed ^{},

⊩_{ed}  ˜  □
⊩_{ed}  □
⊩_{ed} □
let  in  ⊩_{ed} □  ˜

Theorem 5.9. Let ed ^{}.

(i)  let  in ⊩_{ed}  ˜

(ii) ⊩_{ed} ˜

6 Conclusion

We proposed a let-elimination of union types and implicit existential quantifications. This provides a way to obtain strongly normalizing systems, and for the existential quantification, to get subject reduction as well. We also have shown that the obtained existential quantification coincides with its usual encoding w.r.t. provability in realizability models built from reducibility candidates.

Further Work. There are different way in which this work can be extended. First, to study subject reduction of union types with let. Second, to extend the reduction of let with usual permutative conversions. Third, to study the obtained existential quantification in Krivine’s realizability [10]. Another direction is to explore links with classical logic: the obtained let seems to correspond to a form of ˜ in the sequent-based -calculus of [4]. The elimination rules with let would be seen as the translation on terms of implicit right-introduction rules on contexts.

Acknowledgments. We thank Alexandre Miquel for suggesting the study of realizability models and the use of boxed types.

References

[1] F. Barbanera, M. Dezani-Ciancaglini, and U. de’ Liguoro. Intersection and Union Types: Syntax and Semantics. Information and Computation, 119:202–230, 1995.

[2] F. Blanqui and C. Riba. Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems. In Proceedings of LPAR’06, volume 4246 of LNAI, 2006.

[3] T. Coquand and A. Spiwack. A Proof of Strong Normalisation using Domain Theory. In Proceedings of LiCS’06, pages 307–316. IEEE Computer Society, 2006.

[4] P.-L. Curien and H. Herbelin. The Duality of Computation. In Proceedings of ICFP’00, pages 233–243. ACM, 2000.

[5] M. Dezani-Ciancaglini, U. de’ Liguoro, and P. Piperno. A Filter Model for Concurrent Lambda-Calculus. Siam Journal on Computing, 27(5):1376–1419, 1998.

[6] J. Dunfield and F. Pfenning. Tridirectional Typechecking. In Proceedings of POPL’04, pages 281–292. ACM, 2004.

[7] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[8] H. Ishihara and T. Kurata. Completeness of Intersection and Union Type Assignment Systems for Call-by-Value -Models. Theoretical Computer Science, 272:197–221, 2002.

[9] J.-L. Krivine. Lambda-Calculus, Types and Models. Ellis Horwood, 1993.

[10] J.-L. Krivine. Realizability in Classical Logic. To appear in Panoramas et synthèses, Société Mathématique de France, disponible sur HAL, 2004.

[11] S. Lindley and I. Stark. Reducibility and TT-Lifting for Computation Types. In TLCA, volume 3461 of LNCS, pages 262–277. Springer, 2005.

[12] P. Oliva and T. Streicher. On Krivine’s Realizability Interpretation of Classical Second-Order Arithmetic. Fundameta Informaticae, 84(2):207–220, 2008.

[13] M. Parigot. Proofs of Strong Normalization for Second Order Classical Natural Deduction. Journal of Symbolic Logic, 62(4):1461–1479, 1997.

[14] C. Riba. Strong Normalization as Safe Interaction. In Proceedings of LiCS’07, pages 13–22. IEEE Computer Society, 2007.

[15] C. Riba. Stability by Union of Reducibility Candidates for Orthogonal Constructor Rewriting. In Proceedings of CiE’08, volume 5028 of LNCS, pages 498–510. Springer, 2008.

[16] C. Riba. Toward a General Rewriting-Based Framework for Reducibility. Submitted (available from the author’s homepage), 2008.

[17] W. W. Tait. A Realizability Interpretation of the Theory of Species. In R. Parikh, editor, Logic Colloquium, volume 453 of LNCS, pages 240–251, 1975.

[18] M. Tatsuta. Simple Saturated Sets for Disjunction and Second-Order Existential Quantification. In Proceedings of TLCA’07, volume 4583 of LNCS, pages 366–380. Springer, 2007.

[19] J. Vouillon and P.-A. Melliès. Semantic Types: A Fresh Look at the Ideal Model for Types. In Proceedings of POPL’04. ACM, 2004.