Thibaut Balabonski
email: thibaut.balabonski@pps.jussieu.fr

A Unified Approach to Fully Lazy Sharing

We give an axiomatic presentation of sharing-via-labelling for weak λ-calculi, that allows to formally compare many different approaches to fully lazy sharing, and obtain two important results. We prove that the known implementations of full laziness are all equivalent in terms of the number of β-reductions performed, although they behave differently regarding the duplication of terms. We establish a link between the optimality theories of weak λ-calculi and first-order rewriting systems by expressing fully lazy λ-lifting in our framework, thus emphasizing the first-order essence of weak reduction.

This technical report extends [Bal12] with comprehensive proofs.

Introduction

A fundamental problem in the implementation of functional programming languages is the efficient evaluation of β-reduction, which has been studied for a long time. The difficulty of the problem comes from the fact that one has to minimize the number of β-steps as well as control the actual (amortized) cost of single β-reduction steps. The minimization of the number of β-steps requires, in turn, to handle two different issues: avoiding non-needed computations, and minimizing duplications of unfinished work.

In λ-calculus, some reduction strategies [START_REF] Barendregt | Needed reduction and spine strategies for the lambda calculus[END_REF] can completely avoid non-needed computations. However, it is also known that no reduction strategy can completely avoid duplications [START_REF] Lamping | An algorithm for optimal lambda calculus reduction[END_REF]. Hence, in any case, one has to cope with duplications that still occur, and find some appropriate ways to deal with them. This is exactly the point of sharing: building implementations in which the duplicated occurrences of a given original subterm keep a unique shared representation allowing to evaluate all the copies at the same time, as if they were only one. The idea is to make sure that some parts of a program which 1 are logically duplicated (in the term representation of the program) remain physically single pieces (in the memory of the evaluator).

Sharing cannot be achieved using only λ-terms: it requires the use of other technical tools, for instance graphs, closures, or program transformations. The various resulting formalisms may be hardly comparable.

This paper focuses on one particularly rich flavor of sharing called fully lazy sharing (described in section 1.2) and aims at formally relating its various implementations. This is done by defining a framework called sharingvia-labelling systems in which they can all be expressed and compared.

This unified approach provides compiler writers with increased knowledge on the wide panorama of full laziness. In particular, it replaces a series of sometimes informal justifications of equivalence by a central theorem ensuring that all the considered approaches are equivalent with respect to the number of shared β-steps. As a consequence, one can safely restrict any subsequent comparison of two fully lazy models to other parameters of interest such as their space consumption or the actual cost of maintaining sharing. Having a unified framework will also simplify the task of comparing full laziness to the other efficient implementation techniques, such as other degrees of laziness (up to optimality), or partial evaluation.

The rest of the introduction is organized as follows: Section 1.1 presents the various technical tools commonly used to specify sharing, Section 1.2 describes how these tools have been used and combined over the past 40 years to propose different definitions of fully lazy sharing, and Section 1.3 details our approach and the contributions of the paper.

Many tools for sharing

This section reviews several different technical tools that have been used to deal with sharing.

Graphs. The most intuitive way of expressing sharing might be by using graphs. In the following pictures, we denote application by the binary node @, and redexes1 are marked with bold lines. For instance in the center of the following picture, an abstraction λx.t is applied to an argument a. The function body t contains two occurrences of the formal parameter x, and the argument a is thus logically duplicated (on the left). The simplest notion of sharing, which may be referred to as lazy sharing, or just laziness, prevents the previous duplication by keeping a physically unique, with two pointers to its location (right hand side part of the previous picture).

Here the term laziness is to be taken in literal sense: the duplications are postponed as long as it is possible, but some of them will eventually happen. For instance, a shared function has to be copied prior to any instantiation, as shown in the picture below. Extraction of free parameters. The previous pictures feature graphs built with λ-calculus constructs and in particular with binders. This requires either to define variable renaming (α-conversion) or to add some special structure to represent binding. In any case the resulting graph formalism is quite complex. Graph reduction can be made easier by turning λ-terms (that are higher-order terms) to applicative expressions (that are first-order terms). This is the point when compiling the λ-calculus into combinators [START_REF] Turner | A new implementation technique for applicative languages[END_REF] or supercombinators [START_REF] Hughes | Super combinators: A new implementation method for applicative languages[END_REF], techniques that finally led to the λ-lifting program transformation [START_REF] Johnsson | Lambda lifting: Transforming programs to recursive equations[END_REF][START_REF] Jones | The Implementation of Functional Programming Languages[END_REF].

This transformation extracts all the free variables from a function and replaces what remains of the function by a symbol called supercombinator. New reduction rules are added to deal with the new symbols.

Closures and memory heaps. While graphs are a simple and old way to describe lazy sharing, the reference system for the semantics of lazy evaluation is J. Launchbury's natural semantics [START_REF] Launchbury | A natural semantics for lazy evaluation[END_REF]. It introduces let ... in ... constructs to name the arguments of the applications, and then puts these arguments in a heap. Sharing then appears as memoization: when one needs to access the content of a variable, the corresponding expression found in the heap is evaluated, and the heap is updated with the obtained result.

In contrast to the previous big-step approach, a small-step description of lazy evaluation based on terms is the call-by-need λ-calculus of Z. Ariola et al. [AFM + 95]. Here again, sharing is expressed thanks to additional let ... in ... constructs used as closures. Similar effects can also be achieved by expressing sharing using explicit substitutions [START_REF] Yoshida | Optimal reduction in weak-λ-calculus with shared environments[END_REF].

Labels and weak reduction. Finally, laziness is seen in [START_REF] Yoshida | Optimal reduction in weak-λ-calculus with shared environments[END_REF][START_REF] Maranget | Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems[END_REF] as the optimal way of sharing in weak λ-calculi: variants of the λ-calculus where reduction under λ-abstractions is restricted. After J.-J. Lévy described optimal sharing for the plain λ-calculus (unrestricted, untyped, usual λ-calculus) by means of labelled λ-terms [START_REF] Lévy | Optimal reductions in the lambda-calculus[END_REF], L. Maranget [START_REF] Maranget | Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems[END_REF] adapted these ideas for a weak λ-calculus and for first-order rewriting and got an additional result that is not valid for the plain λ-calculus: labelled terms represent graphs implementing optimal sharing.

In [START_REF] Maranget | Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems[END_REF] the link between labelled terms and graphs is made by interpreting the label of a term as its location in memory, or graphically by its coordinate:

@ α λx β @ γ x ι t t δ δ @ λx @ x t
We call this principle sharing-via-labelling. The idea is also explored in [START_REF] Dougherty | Addressed Term Rewriting Systems: Syntax, Semantics, and Pragmatics: Extended Abstract[END_REF]. In this setting the equality of labels corresponds to the physical equality of two terms, which should in turn imply their syntactic equality: two terms stored/drawn at the same place ought to be equal. The reduction of a graph-redex is simulated by the reduction of all the labelled term-redexes with a given label. One then needs to ensure that the sharing property (terms with equal labels are syntactically equal) is preserved by reduction.

Full laziness: State of the art

The main idea. Full laziness is based upon the following remark: the constant parts of a function body are not affected by the instantiation of the function, hence they need not be duplicated.

A similar idea exists in the optimization of imperative programs: a constant expression without effect in the body of a loop need not be evaluated at each iteration, and can be lifted out of the loop by the compiler.

This can be formalized by means of the notion of free expression. We recall the definition given in [START_REF] Jones | The Implementation of Functional Programming Languages[END_REF]. Say a subterm s of t is free in λx.t if all the free variables of s are free in λx.t. A maximal free expression of λx.t is a free expression of λx.t which is not contained into any other free expression of λx.t.

Fully lazy sharings. The various definitions of fully lazy sharing come from a combination of the previous idea with one or more of the technical tools described in section 1.1.

The first description of fully lazy sharing is in the graph evaluation technique presented by C.P. Wadsworth [Wad71]. This graph reduction performs only a partial copy of a duplicated function body, by avoiding the copy of its maximal free expressions (see Example 1a). O. Shivers and M. Wand [START_REF] Shivers | Bottom-up β-reduction: Uplinks and λ-DAGs[END_REF] enrich the graph structure of [START_REF] Wadsworth | Semantics and Pragmatics of the Lambda Calculus[END_REF] to allow a simple and efficient implementation. For this they also use a different characterization of what has to be copied, which we detail in Section 3.1.

Two other approaches combine graphs with other tools. First S. Peyton-Jones [START_REF] Jones | The Implementation of Functional Programming Languages[END_REF] reaches a simple graph formalism thanks to a fully-lazy version of λ-lifting which replaces the extraction of the free variables of a function by the extraction of its maximal free expressions, following [START_REF] Hughes | Super combinators: A new implementation method for applicative languages[END_REF]. Second, T. Blanc, J.-J. Lévy and L. Maranget [START_REF] Blanc | Sharing in the Weak Lambda-Calculus Revisited[END_REF] derive a graph implementation of fully lazy sharing through the sharing-via-labelling principle, using labels that characterize optimal sharing for a weak λ-calculus studied in [C ¸H98]. This approach can copy fewer graph nodes of the duplicated abstractions (see Example 1b).

Finally, Z. Ariola and M. Felleisen [START_REF] Ariola | The call-by-need lambda calculus[END_REF] and P. Sestoft [START_REF] Sestoft | Deriving a lazy abstract machine[END_REF] use the extraction of maximal free expressions to build fully lazy versions of (respectively) the call-by-need λ-calculus [AFM + 95] and Launchbury's natural semantics for laziness [START_REF] Launchbury | A natural semantics for lazy evaluation[END_REF]. Both solutions are based on closures represented by let ... in ... constructs. The former solution [START_REF] Ariola | The call-by-need lambda calculus[END_REF] uses a more restrictive definition of free expressions and hence may in some cases copy more nodes than the others (see Example 1c).

Example 1.

Bold lines identify the parts of the function that are duplicated by the different models. See Section 3.1 for a formal statement.

λx @ λz z λy @ x @ y y λx @ λz z λy @ x @ y y λx @ λz z λy @ x @ y y (a) [Wad71] (b) [BLM07] (c) [AF97]
Summary. The following table sums up how each of the previous works gives its own view on fully lazy sharing, with different interpretations of the same main idea and using various combinations of technical tools that are sometimes hardly comparable. We use the symbol = to mean "as many copied nodes as [START_REF] Wadsworth | Semantics and Pragmatics of the Lambda Calculus[END_REF]".

Tools Dupl. Graphs Extraction Closures Labels

[Wad71] = [Jon87] = [AF97] More [Ses97] = [SW04] = [BLM07] Fewer
This paper proposes a formal setting in which all the approaches mentioned above can be expressed. This allows to formally compare them and leads us to the two following conclusions:

• The previous approaches correspond to at least three different graph implementations. This means that, strictly speaking, they do not all induce the same amount of sharing. Hence, despite the fact that all these approaches intend to implement the same idea their equivalence is not obvious.

• However, all these approaches have the same reduction space, which in turn means that the different implementations of fully lazy sharing perform the same number of β-reductions. In other words, any further comparison of these approaches need not anymore take this parameter into account.

Content of the paper

An axiomatic framework for sharing-via-labelling. To express all the previous approaches, we build in Section 2 an axiomatic framework which generalizes the work of T. Blanc, J.-J. Lévy and L. Maranget [START_REF] Blanc | Sharing in the Weak Lambda-Calculus Revisited[END_REF]. We use labelled terms to describe the graphs realizing optimal sharing for a given notion of weak reduction. Various weak reduction notions are defined thanks to an axiomatic description of the parts of the program where reduction is forbidden. In any case the restrictions concern only evaluation in the body of a non-instantiated function, called partial evaluation. This implies that the call-by-value and call-by-name strategies are always valid. However, the different weak calculi may or may not be confluent (see [C ¸H98] and Example 3). This approach of sharing-via-labelling allows in Section 3 to relate all the definitions of fully lazy sharing that do not rely on supercombinators and λ-lifting. In other words this axiomatic framework, which is designed in higher-order rewriting, covers the definitions of full laziness which directly operate in the higher-order world [Wad71, AF97, Ses97, SW04, BLM07]. The remaining approaches using a translation to first-order rewriting by λlifting [START_REF] Hughes | Super combinators: A new implementation method for applicative languages[END_REF][START_REF] Jones | The Implementation of Functional Programming Languages[END_REF] are studied separately in Section 4. The translation to first-order by means of combinators of D. Turner [START_REF] Turner | A new implementation technique for applicative languages[END_REF] is out of the scope of the present paper, since these combinators simulate explicit substitutions and then introduce additional reduction steps.

Notably due to its axiomatic nature, our framework is not suitable for an immediate implementation. On the other hand, this approach teaches us something about full laziness in general and on its various concrete implementations. The novelty of our framework lies in the fact that it cannot be seen as a straightforward generalization of any of the aforementioned embodiments of full laziness taken in isolation: the axiomatization rather comes from an analysis of the similarities and the differences of all the concrete systems. This yields a new system whose specific properties may be understood as the intersection of the particular properties of the various concrete systems. In other words, our axiomatization tries to grasp the essence of full laziness.

A formal coding of higher order into first order by λ-lifting. The λ-lifting program transformation turns a λ-term into a first-order term. The main feature of λ-lifting is the transformation of λ-abstractions into function symbols, also called supercombinators, over which first-order reduction rules are defined. As emphasized in [START_REF] Lago | On constructor rewrite systems and the lambda-calculus[END_REF], this transformation unveils a tight relation between weak λ-calculus and first-order rewriting.

Usual definitions of λ-liftings [START_REF] Johnsson | Lambda lifting: Transforming programs to recursive equations[END_REF] proceed by first defining the transformation of λ-abstractions, and then iteratively applying the process to a λ-term until it contains no more λ-abstractions. Definitions differ in particular in the way in which a single λ-abstraction is transformed and on the order in which the iteration is applied. For instance, [START_REF] Jones | The Implementation of Functional Programming Languages[END_REF] describes a bottom-up transformation, while [START_REF] Sestoft | Deriving a lazy abstract machine[END_REF] iterates in an unspecified order. We ensure the consistence of these two views by giving a definition of fully-lazy λ-lifting in which the order of the iterative process is irrelevant.

Since λ-lifting is an iterative process that turns progressively a λ-term into a first-order term, none of the intermediate steps is in either of these worlds. Nevertheless, we would like to embody the source, the target, and all the intermediate steps of the transformation into a single formalism. To this aim we use Combinatory Reduction Systems (CRS), a higher-order rewriting framework introduced by J.W. Klop and reviewed in [START_REF] Klop | Combinatory reduction systems: Introduction and survey[END_REF] that mixes abstractions and symbols. The β-reduction as well as the target first-order reduction have a straightforward encoding into CRS rules. Moreover, fully lazy λ-lifting itself can then be seen as a rewriting process: it is expressed in Section 4 as a confluent and strongly normalizing CRS reduction relation.

We provide a new proof of correctness of fully lazy λ-lifting by showing that the transformation preserves reduction sequences: each single reduction step in the source (resp. target) system is simulated by exactly one single step in the target (resp. source) system. The proof is small-step: the reduction sequences are proved to be preserved in every intermediate step of the transformation. Moreover, we prove that the notion of optimal sharing is also preserved, which has two consequences:

• The direct [START_REF] Wadsworth | Semantics and Pragmatics of the Lambda Calculus[END_REF] and the λ-lifting based [START_REF] Jones | The Implementation of Functional Programming Languages[END_REF] approaches of full laziness are reduction-wise equivalent.

• Fully-lazy λ-lifting establishes a link between optimal sharing in the weak λ-calculus [START_REF] Blanc | Sharing in the Weak Lambda-Calculus Revisited[END_REF] and the better known optimality theory of first-order rewriting [START_REF] Maranget | Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems[END_REF][START_REF]Term Rewriting Systems[END_REF]. This emphasizes in a new way the "first-order" nature of weak reduction, without any de Bruijn indices or explicit substitutions (contrary to [START_REF] Maranget | Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems[END_REF]).

A final bonus remark is an incidental point which happens to have some theoretical significance: while β-reduction and λ-lifting considered separately can be seen as orthogonal systems2 , their combination cannot. As far as the author is aware, the system derived in this paper is the first successful optimality-oriented labelling of a non-orthogonal system.

Outline. The paper comprises three main parts: Section 2 presents the abstract notions of prefix, weak reduction, and sharing-via-labelling and gives a proof of the sharing property for the axiomatic framework. Section 3 restricts the axiomatics to enforce full laziness and proves a generic equivalence between several notions of fully lazy sharing. Section 4 focuses on the particular fully lazy system of [START_REF] Wadsworth | Semantics and Pragmatics of the Lambda Calculus[END_REF][START_REF] Shivers | Bottom-up β-reduction: Uplinks and λ-DAGs[END_REF] whose properties allow a clean definition of fully lazy λ-lifting which establishes a strong link between weak β-reduction and first-order rewriting.

Sharing and β-reduction

We define in this section an axiomatic framework in which the higher-order approaches [Wad71, AF97, Ses97, SW04, BLM07] to fully lazy sharing can be expressed. We propose an axiomatic notion of weak β-reduction in Subsection 2.1, whose optimal sharing is characterized by the sharing-via-labelling systems introduced in Section 2.2. Section 2.3 then shows that reduction of labelled terms in sharing-via-labelling systems represents reduction of graphs.

All this is expressed in Combinatory Reduction Systems (CRS). By lack of space we recall only the basic syntax and refer the reader to [START_REF] Klop | Combinatory reduction systems: Introduction and survey[END_REF] for details. The grammar of metaterms in a CRS is:

t ::= x | [x]t | f (t 1 , ..., t n ) | Z(t 1 , ..., t n )
where x is a variable, [x] denotes the binding of a variable, f is an nary function symbol taken in a signature Σ, and Z is an n-ary metavariable. A term is a metaterm without meta-variable, and a reduction rule is a pair L → R of closed metaterms satisfying the following conditions: the meta-variables in L appear as Z(x 1 , ..., x n ) with x 1 , ..., x n distinct bound variables, and all the meta-variables of R also appear in L. A rule matches a term by application of a valuation σ that maps n-ary meta-variables to n-ary contexts avoiding variable capture. Reduction by a rule

L → R with valuation σ in a context c is c[L σ ] → c[R σ ].

Weak β-reduction systems

This section gives an abstract definition of weak reduction in the λ-calculus and states one of its crucial properties: disjoint redexes remain disjoint along any reduction (Lemma 1). This lemma serves in particular in the definition of graph reduction in Section 2.3.

Weak reduction forbids the reduction of so-called frozen redexes, which are identified by their belonging to the prefix of some λ-abstraction. Prefixes are parts of λ-abstractions defined by a prefix function satisfying the axioms of a weak β-reduction system.

Weak β-reduction systems are CRS over the signature Σ comprising:

• a binary symbol @ for application,

• a unary symbol λ for λ-abstraction,

• a unary dummy symbol ,

• for all n ∈ N, a countable set F n of n-ary symbols.

From now on, by term we mean a CRS term over the signature Σ (notation t, u, v, w, a). We use the usual notion of positions of terms (notation q), contexts and free variables [START_REF] Klop | Combinatory reduction systems: Introduction and survey[END_REF]. We write t {x:=u} the substitution by u of all the free occurrences of the variable x in t.

Application and λ-abstraction symbols are used to embody λ-terms in this signature, which is made in the usual way: the λ-term (λx.x)y for instance is encoded in the CRS term @(λ([x]x), y). We write λx.t as a shorthand for λ([x]t). Hence the encoding of (λx.x)y is simply written @(λx.x, y), and the usual β-reduction is represented by the CRS rule @(λx.Z(x), Z ) → Z(Z ).

The symbols in the sets F n are used in Section 4 to represent supercombinators. Until then they play no role and may be ignored.

The dummy symbol has no meaning in itself. It is needed for labelling (Subsection 2.2), and serves in particular as a container for dynamically created labels. In the graphical interpretation of labelled terms, the occurrences of will represent indirections (see Subsection 3.1). As a consequence, occurrences of should not interfere with β-reduction. This leads to the following countable set of rules to simulate β-reduction by allowing any number of 's between the application and the λ-abstraction: Write ρ : t → t a reduction ρ of a term t to a term t . The usual notions of ancestors and descendants, which allow to track subterms along reduction in the λ-calculus are straightforwardly adapted, as illustrated in Example 2. A residual of a redex r is a descendant of r which is still a redex.

β 0 : @(λx.Z(x), Z ) → β (Z( (Z ))) β 1 : @( (λx.Z(x)), Z ) → β (Z( (Z ))) β 2 : @( ( (λx.Z(x))), Z ) → β (Z( (Z ))) ...

Example 2.

The term t = @( (λx.@(x, x)), y) reduces by rule β 1 to t = (@( (y), (y))). The two occurrences of y in t are the descendants of the y in t, and the latter is the ancestor of the formers. The in t has no descendant and the 's in t have no ancestor.

We call plain λ-calculus the usual reduction relation where the previous rules can be applied in any context. Weak reduction consists in restricting this reduction relation. Particularly, it affects the reduction under λabstractions. Before introducing the formal definition, let us present two different well-known examples:

Example 3.

1. The naive weak reduction simply forbids any reduction under λabstractions.

2. A more refined version, studied in particular in [C ¸H98], allows no reduction between an occurrence of a bound variable and its binder. Formally, if r is a redex of contractum r , then the reduction

C[r] → C[r ]
is allowed if and only if the context C binds no variable that appears free in r. We call this version CH-weak reduction.

It is known that CH-weak reduction yields a confluent weak calculus while naive weak reduction does not [C ¸H98].

To specify the previous notions, we introduce a notion of prefix: call a nary closed prefix of a term t a n-ary context p which does not contain any free variable and such that there are terms t 1 , ..., t n satisfying t = p[t 1 , ..., t n ]. Example 4 gives two closed prefixes of the same term. Call a prefix function a function that takes a term t as input and returns a closed prefix of t.

Example 4. Let t = λx.@(@(z 1 , z 2 ), λy.@(@(y, z 3 ), x)). The two contexts λx.@([], λy.@([], x)) and λx.@([], λy.@(@(y, []), x)) are two closed prefixes of t, called respectively spine and skeleton (see Section 3.1). These two prefixes are marked with bold lines in the two following pictures.

λx @ @ z 1 z 2 λy @ x @ y z 3 λx @ @ z 1 z 2 λy @ x @ y z 3

Spine Skeleton

A weak β-reduction system is defined below by a prefix function P satisfying some conditions. The first condition is a simple restriction linked to bound variables. The second condition controls the evolution of P(t) when free variables of t are substituted by terms. In particular, P(t {x:=u} ) is required to contain P(t), and the extension from P(t) to P(t {x:=u} ) has to be uniform. This uniformity is enforced by the use of an auxiliairy function P .

Call a weak β-reduction system a prefix function P such that:

• For any term λx.t such that P(λx.t) = p and λx.t = p[t 1 , ..., t n ], the variable x does not appear free in any of the t i 's (which are called the parameters of λx.t). In other words, P(λx.t) contains all the occurrences of x that are free in t.

• There is an auxiliary prefix function P such that for any p in the codomain of P and for any terms t 1 , ..., t n where no free variable of a t i is bound in p, the equation

P(p[t 1 , ..., t n ]) = p[P (t 1 ), ..., P (t n )] holds.
A weak β-reduction system defines a notion of weak reduction as follows: β-reduction is forbidden in the prefix of any λ-abstraction. Call a frozen position of a term t a position that is in the prefix of some λabstraction of t. Call a frozen β-redex a redex whose main @ symbol occurs at a frozen position.

Example 5. The two weak reductions of Example 3 can be captured by our axiomatic definition:

1. Naive weak reduction is given by P n such that P n (t) = p where t = p[x 1 , ..., x n ] and x 1 , ..., x n are all the free variable occurrences of t. The auxiliary function is P n = P n (the whole substituted term is included into the prefix).

2. CH-weak reduction can be given by P ch such that P ch (t) = p where t = p[t 1 , ..., t n ] and t 1 , ..., t n are all the maximal free expressions of t. The auxiliary function P ch is the constant mapping returning the empty unary context [] (the prefix is stable by substitution). We will see in Section 3.2 that P ch is not the unique representation of CH-weak reduction.

A weak β-reduction system is said to be safe when the descendants of a non frozen redex are not frozen.

Example 6. CH-weak reduction is safe, while naive weak reduction is not: let t = @(λx.λy.x, @(λz.u, v)), where the redex @(λz.u, v) is not frozen in t. We have the reduction t → β (λy. (@(λz.u, v))) = t .

@ λx λy x @ λz u v λy @ λz u v
In the case of naive weak reduction @(λz.u, v) is frozen in t , which is not the case in CH-weak reduction since y does not appear in @(λz.u, v). This example also suggests why naive weak reduction is not confluent.

An important feature of weak reduction is that it cannot nest the residuals of disjoint redexes. This fact is formalized in Lemma 1, and will be useful in Section 2.3 to ground the notion of parallel reduction.

Lemma 1 (Disjoint residuals). Let ρ : t → t be a reduction and r 1 , ..., r n (non frozen) redexes of t occurring at disjoint positions. Then the descendants of r 1 , ..., r n also occur at disjoint positions.

Proof. If a descendant r i of r i is below a descendant r j of r j then r i has been substituted into r j , which means that r j contains an occurrence of a variable bound above r j . Hence r j is frozen, contradiction.

Example 7 shows why Lemma 1 is a feature of weak reduction which is not valid in the plain λ-calculus.

Example 7. Suppose r 1 and r 2 are two redexes. In the left term r 1 is frozen for any weak β-reduction system. @

r 1 λx x r 2 r 1 r 2
To prepare the implementation of optimal sharing for weak β-reduction systems in next section (2.2), we give a characterization of redex creation in these systems. Suppose ρ : t → β t in a weak β-reduction system. A redex of t is created by ρ if it is not the descendant of a (non frozen) redex of t. The reduction can create redexes in t at exactly three places:

1. At the root of the contractum, the body of the main λ-abstraction is connected to the context. This can create a new contact between an application and a λ-abstraction.

2. At the places where a substitution occurs, the argument is connected to the body of the main λ-abstraction, or to the context if the body is degenerated.

3. In the prefix of the main λ-abstraction, a previously frozen redex can be "unfrozen" by ρ, as r 1 in Example 7. In other words, a reduction forbidden by the weak restriction in t can be authorized in t .

Sharing-via-labelling systems

We define in this section a labelling for weak β-reduction systems which characterizes optimal sharing and yields a graph implementation. As in [START_REF] Lévy | Optimal reductions in the lambda-calculus[END_REF], the labels record the past history of a term. This is done in a distributed way since each label remembers only what is relevant to its position. The important point for optimality is that the labels of a redex r are characterized by the past reductions that contributed to the creation of r, which is ensured by the concluding lemmas 2 and 3. These two lemmas also play a key role in the proof of the preservation of the graph structure (so-called sharing property) in Section 2.3.

To embody this contribution relation into the labels, we build compound labels of the form [Ω, α] where a pre-existing label α is modified by the name Ω of a contributing redex. The labelled β-reduction then modifies the labels of the positions where the reduction can contribute to something, following the characterization of redex creation given at the end of the previous subsection. Names and contribution are required to satisfy three axioms which ensure that the name of a redex correctly reflects its contributors.

The labelled terms are formalized as usual CRS terms over a labelled signature. Since the labels should not interfere with the normal reduction behaviour, the labelled β-reduction is defined for any possible labelling of the source.

For any countable set L whose elements are called labels (and written α, β, γ...), a labelled signature Σ L is defined as the set {f α |f ∈ Σ, α ∈ L}. From now on, a L-labelled term denotes a CRS term over Σ L . In other words, the labels are associated to the symbols, and never directly to the variables or the bindings. Remark that the labels are arbitrary objects: in a concrete definition they can be simple letters as well as richly structured objects.

We write λ α x.t (resp. x α ) as a shorthand for λ α ([x]t) (resp. α (x)). Write τ (t) for the label of the root symbol of the labelled term t. Write α 1 ...α k k (t) as a shorthand for α 1 (... α k (t)), where the case k = 0 represents t.

Write |.| the (trivial) map from terms over Σ L to terms over Σ that removes the labels of all symbols. By requiring the condition |P(t)| = P(|t|), we get a straightforward extension to Σ L of any weak β-reduction system P over Σ. Since neither 's nor labels shall interfere with β-reduction, labelled βredexes allow any number of occurrences and can be decorated with any labels: for any L, a L-labelled β-redex is a L-labelled term of the form @ α ( β 1 ...β k k (λ γ x.t), a). Labelled β-reduction is defined later, since it requires an additional notion of sharing-via-labelling systems given below.

We consider sets of labels of the form L = V N , generated by the following grammar for any two countable sets V and N :

V N ::= V | [N , V N ] The label [Ω, α] denotes "the label α modified by Ω". Write [Ω 1 ...Ω n , α] as a shorthand for [Ω 1 , ...[Ω n , α]]. Any Ω i is called a modifier of [Ω 1 ...Ω n , α].
The virginal labels (the labels in V) denote positions that are free from any past history, they will be modified into labels of the form [Ω 1 ...Ω n , α] along the reductions. Let S be a tuple P, N , V, η, → where:

• P is a weak β-reduction system.

• N is a countable set whose elements are called (redex) names (notation Ω).

• V is a countable set whose elements are called virginal labels, with two distinguished elements and ⊥.

• η is a function from V N -labelled redexes to names.

• → is a transitive and irreflexive relation on N called contribution relation.

The terms considered in S are the V N -labelled terms. Call virginal term a term whose labels are all virginal and different.

Write ↑ Ω = {Ω | Ω → Ω} the set of all the contributors of the name Ω. Contribution is extended to labels: define

↑ α = ∅ if α is a virginal label, and ↑ [Ω, α] = {Ω} ∪ ↑ Ω ∪ ↑ α otherwise. Write Ω → α when Ω ∈ ↑ α.
S is a sharing-via-labelling system if the following axioms are satisfied:

• (Redex contributors) ↑ η(@ α ( β 1 ...β k k (λ γ x.t), a)) = ↑ α ∪ ( i ↑ β i ) ∪ ↑ γ • (Name scope) If λ γ x.
p is in the codomain of P, and a t , a u are any terms and t 1 , ..., t n , u 1 , ..., u n are terms whose free variables are not bound in λ γ x.p, then

η(@ α ( β 1 ...β k k (λ γ x.p[t 1 , ..., t n ]), a t )) = η(@ α ( β 1 ...β k k (λ γ x.p[u 1 , ..., u n ]), a u )) • (Name equality) If η(r) = η(r ) then τ (r) = τ (r ).
The axiom Redex contributors states that the name of a redex collects the contributors of the essential parts of the redex, that means its main application, its main λ-abstraction, and all that lays in between these two positions. The axiom Name scope states that the name of a redex does not depend of what is deeper than the smallest prefix of the main abstraction, while axiom Name equality states that the equality of the names of two redexes implies the equality of their respective root labels.

Example 8. Let V be any countable set.

1. The names in N seq are sequences of labels. Since the names also take part into the definition of the labels, a mutually recursive definition of names and labels is required:

N seq ::= L; ...; L L ::= V Nseq
Define the name of a redex as

η seq (@ α ( β 1 ...β k k (λ γ x.t), a)) = α; β 1 ; ...; β k ; γ
The contribution relation is defined by: Ω → seq α 1 ; ...; α n if and only if there is at least one i such that Ω → seq α i .

For P ∈ {P n , P ch }, the system P, N seq , V, η seq , → seq is a sharing-vialabelling system. The definitions of N seq , η seq , and → seq correspond to the system presented in [START_REF] Blanc | Sharing in the Weak Lambda-Calculus Revisited[END_REF].

2. The names in N ctx are L-labelled contexts, with once again a mutually recursive definition using L ::= V Nctx . Define

η ctx (@ α ( β 1 ...β k k (λ γ x.t), a)) = @ α ( β 1 ...β k k (λ γ x.p), [])
where P(λ γ x.t) = λ γ x.p.

Write Ω → ctx c if there is a label α in c such that Ω → ctx α.

For P ch , N ctx , V, η ctx , → ctx to be a sharing-via-labelling system, the axiom Redex contributors requires that the prefixes satisfy the following property: all the contributors of the labels of a prefix λ γ x.p contribute to γ. Fortunately, in this system this property is an invariant of labelled β-reduction (defined below).

The system P n , N ctx , V, η ctx , → ctx is not a sharing-via-labelling system since it breaks the axiom Name scope.

Labelled β-reduction is defined by a rule scheme which propagates the name of the reduced redex in the reduced term for recording of the contributions. For this, the constructor [., .] extends to a function on labelled terms: [Ω, t] is defined as the labelled term t in which all the labels are modified by the function α → [Ω, α].

Labelled β-reduction in a sharing-via-labelling system is defined by the rule scheme:

@ α ( β 1 ...β k k (λ γ x.p[t 1 , ..., t n ]), a) → β [Ω, ] ([Ω, p]) {x:= [Ω,⊥] (a)} [t 1 , ..., t n ]
where λ γ x.p = P(λ γ x.p[t 1 , ..., t n ]) and where Ω = η(@ α (

β 1 ...β k k (λ γ x.p[t 1 , ..., t n ]), a)).
The name Ω is added in three areas of the reduced term:

1. At the root of the contractum, with the new label [Ω, ].

At the places where a substitution occurs, with the new label [Ω, ⊥].

Remark in Example 9 how and ⊥ work as parentheses in the syntactic tree of the term.

3. In the prefix of the main abstraction of the redex, as an additional modifier to pre-existing labels.

Remark that these three places follow the three cases of redex creation given in Section 2.1 and that removing the labels in this rule yields exactly the unlabelled β-reduction of Section 2.1.

Example 9.

Let r = @ α (λ γ x.@ δ (@ ι (x µ , x ν ), λ κ y.y σ ), a) be a β-redex. We reduce r in two sharing-via-labelling systems of Example 8.

1. In P n , N seq , V, η seq , → seq the name of r is the sequence Ω = α; γ, and the prefix of the λ-abstraction is its whole body. Then all the labels are modified in the contractum:

@ α λ γ x @ δ @ ι x µ x ν λ κ y y σ a [Ω, ] @ [Ω,δ] @ [Ω,ι] [Ω,µ] [Ω,ν] [Ω,⊥] [Ω,⊥] λ [Ω,κ] y y [Ω,σ]
a a 2. In P ch , N ctx , V, η ctx , → ctx , the name of r is the labelled context Ω = @ α (λ γ x.@ δ (@ ι (x µ , x ν ), []), []). The only modified labels are those of the prefix of the λ-abstraction, marked with bold lines below.

@ α λ γ x @ δ @ ι x µ x ν λ κ y y σ a [Ω, ] @ [Ω,δ] @ [Ω,ι] [Ω,µ] [Ω,ν] [Ω,⊥] [Ω,⊥] λ κ y y σ a a
Example 10 tells why the root occurrence of is necessary for a correct recording of the history of the reduction into labels. The other occurrences of in the right hand side of the β-rule are useful to get some other properties of the labelling such as the reconstruction property defined in [START_REF]Term Rewriting Systems[END_REF]Chap. 8].

Example 10. Consider the term λ γ x.y δ in a sharing-via-labelling system based on the CHweak reduction system P ch . Since x does not appear in the body of the abstraction we have P ch (λ γ x.y δ ) = λ γ x.[]. Take Ω as the name of the reduced redex, then we have

@ α (λ γ x.y δ , u) → β [Ω, ] (y δ )
Remark that the only sign of a reduction step in [Ω, ] (y δ ) is the label [Ω, ] on the symbol.

This section ends with the two lemmas 2 and 3, which show how the labels reflect the contribution relation between redexes. In particular, the name of a redex r characterizes the past reductions that led to the creation of r.

Lemma 2 (Redex stability). Let r be a (non frozen) redex of a term t. If r d is a descendant of r after a reduction ρ : t → β t , then r d is still a (possibly frozen) redex and η(r d ) = η(r).

Proof. Case on the relative positions of r and ρ:

• If r is below ρ, then:
-Since r is not frozen its root can not be in the prefix of the main abstraction of ρ. -In all the other cases r d = r and hence η(r d ) = η(r).

• If ρ is below r, then:

-Since the redex of ρ is not frozen its root can not be in the prefix of the main abstraction of r. -In all the other cases η(r d ) = η(r) (axiom Name scope).

Lemma 3 (Direct contribution). If a redex of name Ω c is created by the reduction of a redex of name Ω, then Ω → Ω c . Proof. By case on the redex creation (given in Section 2.1), using the axiom Redex contributors.

Sharing

This section proves the main property of sharing-via-labelling systems: parallel labelled reduction simulates graph reduction (Theorem 1). As in [START_REF] Blanc | Sharing in the Weak Lambda-Calculus Revisited[END_REF], the labelled terms are linked to graphs with the sharing-via-labelling principle seen in the introduction: labels are interpreted as memory locations. The proof of the simulation is then done by ensuring that the two following invariants are preserved by parallel labelled reduction:

1. A term t has the sharing property, written S(t), when any two subterms of t with same label are syntactically equal. This is the main property we want to preserve.

2. A term t has the maximality property, written M(t), when for any (non frozen) redex of name Ω and any subterm of label α in t it is not true that Ω → α. This property is widely used in the subsequent proofs, it ensures in particular that all the occurrences of a given label are created at the same time (see Example 11). Lemmas 2 and 3 are the cornerstone of the preservation of the maximality property.

Parallel labelled reduction is defined for any term t satisfying the sharing property S(t): let α be the label of a (non frozen) redex of t. Since S(t) holds, all the redexes labelled by α are equal and have disjoint positions (however, some may be frozen). The parallel labelled reduction of α, written t α = ⇒ β t , is then defined as the simultaneous replacement of all the (non frozen) redexes with label α by their contractum. By lemmas 1 and 2, parallel labelled reduction is well defined as a sequence of single steps, for instance any iterated reduction of the non frozen redexes with label α.

Theorem 1 (Preservation of sharing). If M(t), S(t) and t α 0 = ⇒ β t , then M(t ), and S(t ).

Proof. By S(t) all the occurrences of the label α 0 denote the same redex. Write r 0 the redex, Ω 0 its name, and r 0 its contractum.

Verification of M(t ). Suppose there is a redex r with name Ω and a subterm u with label α in t such that Ω → α . Case on the origin of r :

• If the redex r is created by the reduction, then Ω 0 → Ω by Direct contribution lemma 3, and Ω 0 → α by transitivity. Since M(t) holds, α does not appear in t and is created by the reduction. Hence α is of the form [Ω 0 , α] where α is , ⊥ or a label of t. The labels and ⊥ are virginal. If α is a label of t then Ω → α is also false because by transitivity it would imply Ω 0 → α and M(t) would be broken. Then by definition either Ω → Ω 0 or Ω = Ω 0 . In particular, in any case Ω 0 → Ω 0 , which contradicts irreflexivity of →.

• If the redex r is a residual of a redex r of t with name Ω, then by Redex stability lemma 2 we have Ω = Ω . As above, since M(t) holds α is created by the reduction, and Ω → Ω 0 or Ω = Ω 0 . Case Ω = Ω 0 is impossible, because by the axiom Name equality all the non frozen redexes with name Ω 0 have the label α 0 and are reduced by the parallel reduction. Then Ω → Ω 0 , and by axiom Redex contributors there is a α in r 0 such that Ω → α, which breaks M(t).

Finally M(t ) holds.

Verification of S(t ). Let u and v be two subterms of t with same label α . By case on the origin of both labels α :

• If one is created and the other is a descendant of a label α in t. Since α is created by the parallel reduction Ω 0 we have Ω 0 → α , which contradicts M(t).

• If both are created:

-If α = [Ω 0 , ], then u = v = r 0 .
-

If α = [Ω 0 , ⊥], then u = v = [Ω 0 ,⊥] (a)
, where a is the argument of the β-redex.

-If α = [Ω 0 , α], then u and v are the descendants of two subterms u and v of t with same label α. By S(t) we have u = v. Moreover, u and v are affected by the same substitution. Hence u = v .

• If both are descendants of themselves: u and v have ancestors u and v in t with same label α = α . By S(t) we have u = v. Since α = α neither u nor v are affected by a substitution in the parallel reduction.

Hence either u = u and v = v or u

α 0 = ⇒ β u and v α 0 = ⇒ β v . In any case u = v .
Finally S(t ) also holds.

Example 11 shows why maximality M is necessary to the preservation of sharing S.

Example 11. Consider the system P ch , N seq , V, η seq , → seq defined in Example 8 and the labelled term t = @ α (x [γ;δ,ι] , @ γ (λ δ z.z ι , y κ )). The property S(t) holds since all the labels of t are different. Remark that t contains a redex @ γ (λ δ z.z ι , y κ ) of name γ; δ. Hence M(t) does not hold since t contains a label [γ; δ, ι]. Then t γ = ⇒ β @ α (x [γ;δ,ι] , [γ;δ,ι] (y κ )) = t where the two subterms of t with label [γ; δ, ι] are different: S(t ) is falsified.

Finally, labelled terms represent graphs and parallel labelled reduction represents graph reduction.

Full laziness

This section shows how the various known implementations of full laziness correspond to several (at least three) different sharing-via-labelling systems (Section 3.1). Thus, they correspond to different graph reductions featuring different amounts of sharing. However, we are going to prove in Section 3.2 that these implementations are reduction-wise equivalent.

Along this section, the signature Σ is restricted to {@, λ, }.

Encodings into sharing-via-labelling systems

The motto of sharing-via-labelling is "labels denote memory locations". What happens to the labels during reduction describes directly what happens to the nodes of the corresponding graph:

• A new label corresponds to a new node. There are two cases:

-A label of the form [Ω, ] or [Ω, ⊥] appears only on . It represents a new indirection node that contains a pointer leading to the term.

-Any other [Ω, α] denotes a new copy of a node labelled α.

• A label which does not change corresponds to a node unaffected by the reduction.

The key of the encoding of graph reduction systems or closure-based systems into sharing-via-labelling systems is to modify exactly the labels of what is needed to be copied. Since the rules of a sharing-via-labelling system modify exactly the labels of the prefix of the main λ-abstraction, this amounts to take as prefix of a λ-abstraction exactly what has to be duplicated of its body.

Remark 1. In this interpretation, an node represents an indirection node in the graph. Hence in a concrete implementation we cannot contract an arbitrary number of 's in unit time, contrarily to what our β-rule suggests. The techniques presented in [Jon87, Chap. 12] to avoid chains of indirections can be used to circle this issue.

To describe the encodings of the higher-order approaches to full laziness into sharing-via-labelling systems, we formally define two useful prefixes mentioned in Example 4.

• Call spine of a term λx.t the prefix λx.p where p is the prefix of t which contains exactly the positions that are above a free occurrence of x, including the free occurrences of x. Remark that in any weak β-reduction system P, any prefix P(λx.t) contains the spine of λx.t.

• Call skeleton of a term λx.t the prefix λx.p where p is the prefix of t containing exactly the positions that are not in a free expression of λx.t. As done in [START_REF] Shivers | Bottom-up β-reduction: Uplinks and λ-DAGs[END_REF] the skeleton can also be seen as an iterated spine: to get the skeleton of λx.t, start with the spine of λx.t and iteratively add to the obtained prefix the spines of all the λ-abstractions that are in the prefix built so far.

The two approaches by C.P. Wadsworth [START_REF] Wadsworth | Semantics and Pragmatics of the Lambda Calculus[END_REF] and O. Shivers and M. Wand [START_REF] Shivers | Bottom-up β-reduction: Uplinks and λ-DAGs[END_REF] reach fully lazy sharing by two graph implementations in which the duplicated part of an instantiated function is its skeleton. The former uses the definition based on the maximal free expressions while the latter follows the characterization by iterated spine. They are both represented by the weak β-reduction system P ch such that P ch (λx.t) is the skeleton of λx.t.

In [START_REF] Sestoft | Deriving a lazy abstract machine[END_REF], P. Sestoft revises Launchbury's lazy semantics [START_REF] Launchbury | A natural semantics for lazy evaluation[END_REF] and proposes a fully lazy variant using additional let-bindings: if λx.p is the skeleton of λx.t and λx.t = λx.p[t 1 , ..., t n ], then λx.t is replaced by let x 1 = t 1 , ..., x n = t n in λx.p[x 1 , ..., x n ] with x 1 , ..., x n fresh variables. After this extraction of the maximal free expressions t 1 , ..., t n of λx.t, a duplication of the λ-abstraction duplicates the subterm λx.p[x 1 , ..., x n ] but does not duplicate the let-parameters t 1 , ..., t n . This is again represented by the weak reduction system P ch .

The work by T. Blanc, J.-J. Lévy and L. Maranget [BLM07] already uses a system isomorphic to a sharing-via-labelling system. Their labelled β-reduction modifies only the labels of the spine of the main λ-abstraction. Thus it corresponds to a weak β-reduction system P blm where P blm (λx.t) is the spine of λx.t. Moreover their frozen redexes are the redexes containing a free occurrence of a variable bound above, which means that they coincide with those given by P ch .

In their call-by-need λ-calculus [AF97], Z. Ariola and M. Felleisen allow the substitution, and thus the duplication, of values. Their fully lazy extension consists in restricting these allowed duplications to a set of fully lazy values: values that do not contain any "free expression". The difference with the previous cases lies in their non-standard definition of free expressions: they use the usual criterion given in Section 1.2 but they exclude the variables and the λ-abstractions. Hence their fully lazy values correspond to the prefixes of the weak β-reduction system P af such that: • P af (λx.t) = P af (λx.t).

• If λx.p
• P af (@(t 1 , t 2 )) = [].

• If P af (t) = [] then P af ( (t)) = [] else P af ( (t)) = (P af (t)).
Finally, the higher-order approaches [Wad71, AF97, Ses97, SW04, BLM07] to full laziness correspond to three different weak β-reduction systems P ch , P blm and P af , which we are going to relate in the next section. Example 12 illustrates how the systems P blm and P af can yield the same parallel labelled reduction in spite of their differences.

Example 12. Let t = λx.λy.@(@(x, r 1 ), λz.r 2 ) be a term such that r 1 , r 2 are two redexes that do not contain any free occurrence of x. Hence a duplication of the spine P blm (t) of t (marked with bold lines in the picture) do not duplicate these redexes.

λx λy @ @ x r 1 λz r 2 y z
If r 1 contains a free occurrence of y and r 2 contains a free occurrence of z, then both redexes are at least partially contained in P af (t), and thus duplicated in this system. However, in this case r 1 and r 2 are and remain frozen in both systems, and their label will change before they are unfrozen. Hence the additional duplications are not harmful.

Equivalence of the parallel labelled reductions

In this section we define a family W of weak β-reduction systems that contains P ch , P blm and P af and we show that all the sharing-via-labelling systems based on the weak β-reduction systems of W are equivalent, in the sense that they can simulate one another using exactly the same number of shared reduction steps. For this we define a relation ∼ on labelled terms which is stable by reduction, and prove that any two terms in relation share the same non-frozen redexes. The relation ∼ relates two terms t 1 and t 2 of two different systems S 1 and S 2 whenever t 1 and t 2 can be reached from a common source by two equivalent reduction sequences in S 1 and S 2 (the whole being called a mirror reduction sequence).

The definition of W follows two ideas: the weak β-reduction systems in W shall enforce CH-weak reduction (for this the third point in particular prevents some applications to be included into a prefix), and all the prefixes are built from spines and skeletons (the first two points, which make the proofs tractable).

A weak β-reduction system P is in W if the following additional conditions are satisfied:

• For each abstraction t = λx.u, either P(t) is the spine of t, or P(t) = p[P (t 1 ), ..., P (t n )] where p is the skeleton of t and t = p[t 1 , ..., t n ].

• For any λx.t, P (λx.t) = [] or P (λx.t) = P(λx.t).

• P (@(t 1 , t 2 )) = [].

• If P (t) = [] then P ( (t)) = [] else P ( (t)) = (P (t)).

Remark 2. In any system of W, the frozen applications of any term are exactly the applications contained in the spine of some abstraction. Hence any system of W defines the same frozen redexes for any term. Moreover, all the systems of W are safe.

Let P 1 and P 2 be two systems of W. A mirror reduction sequence in the systems P 1 and P 2 is a pair ( 1 , 2 ) such that i = ρ 1 i ...ρ n i is a reduction sequence in P i and for any j ∈ {1...n} the redexes reduced by the single steps ρ j 1 and ρ j 2 have the same position q j in the respective source terms. The notion of mirror reduction sequence extends to parallel labelled reduction in two sharing-via-labelling systems based on two (possibly equal) weak β-reduction systems of W.

Let t 1 (resp. t 2 ) be a term in a sharing-via-labelling system S 1 (resp. S 2 ). Write t 1 ∼ t 2 when there is a virginal term t 0 in the intersection of S 1 and S 2 and a mirror reduction sequence ( 1 , 2 ) in the systems S 1 and S 2 such that i is a parallel labelled reduction sequence from t 0 to t i . Remark 3. If t 1 ∼ t 2 then the two terms have the same set of positions. In particular, they contain the same number of occurrences.

For any labelled term t, the labels in t induce an equivalence relation on the subterms of t. Say that two subterms u 1 and u 2 of t are labelequivalent if and only if τ (u 1 ) = τ (u 2 ).

Lemma 4 (Spine stability). Suppose S(t), M(t) and t = ⇒ β t . Let p be a spine in t , and p be the ancestor of p in t. Then p is a spine of t such that |p| = |p | and p and p define the same label-equivalence on their application subterms.

Proof. If p is disjoint from the prefix of the main abstraction of a redex, then its labels are unchanged. Suppose the prefix intersects p. Write p[t 1 , ..., t n ] and p [t 1 , ..., t n ] the subterms of t and t delimited by p and p . Let λx.u be the smallest superterm of p[t 1 , ..., t n ] free in t. Two possible cases:

• If P(λx.u) contains the skeleton of λx.u, then in particular P(λx.u) contains p and every label α in p is turned into [Ω, α]. In particular the equivalence classes do not change.

• If P(λx.u) is the spine of λx.u, then the label α of a subterm v of p[t 1 , ..., t n ] is modified (to [Ω, α]) if and only if v contains a free occurrence of x. Hence, suppose two applications in p have the same label α. By S(t) the two applications are equal: one contains a free occurrence of x if and only if the other does so. Then their descendants still have the same label (either α or [Ω, α]). Now suppose that two applications in p share the same label α but their ancestors have different labels α 1 and α 2 . For instance α 1 = α and [Ω, α 2 ] = α . Then Ω → α and α appears in t. Contradiction by M(t).

Theorem 2 (Sharing equivalence). If t 1 ∼ t 2 then the labellings of t 1 and t 2 induce the same label-equivalence on their non frozen applications.

Proof. We prove two invariants on the pair (t 1 , t 2 ):

1. The equivalence classes of non frozen applications are equal.

2. In each spine, the equivalence classes of applications are equal.

By definition of t 1 ∼ t 2 there is a parallel labelled mirror reduction sequence ( 1 , 2 ) leading from a virginal term t 0 to (t 1 , t 2 ). The proof of both invariants is by induction on the number of parallel steps in ( 1 , 2 ). Remark by Theorem 1 that any intermediate term t in the mirror reduction sequence satisfies M(t) and S(t).

• For an empty reduction, t 1 = t 2 .

• Suppose (t 1 , t 2 ) satisfies the two invariants, and t 1 = ⇒ β t 1 and t 2 = ⇒ β t 2 by two parallel labelled reductions affecting the same positions. The pair (t 1 , t 2 ) satisfies the invariants:

1. A descendant of a non frozen application of label α is a non frozen application of label α. On the other hand, a non frozen descendant of a frozen application α is an application of label [Ω, α]. Let q 1 , q 2 be the positions of two applications of t 1 with same label α . Suppose one if a descendant of label α and the other is a modified label. Then there is a α such that α = [Ω, α], and α appears in t 1 : contradiction of M(t 1 ). Then the ancestors are positions q 1 , q 2 of t 1 with same label. By induction hypothesis the positions q 1 , q 2 also have the same label in t 2 , and either both are non frozen, or both are in the main spine. In any case the descendants at positions q 1 , q 2 in t 2 have the same label α 2 . The other direction is symmetrical.

2. Let p 1 be a spine in t 1 , and p 2 be the corresponding spine in t 2 . By Lemma 4 p i define the same equivalence classes as its ancestor p i in t i . By induction hypothesis p 1 and p 2 have the same classes.

Theorem 2 proves in particular that ∼ is a bisimulation:

any diagram t t u β ∼ or t u u ∼ β can be closed as t t u u β ∼ β ∼
This means that in W, two sharing-via-labelling systems generate the same notion of parallel labelled reduction. In other words, their (possibly different) sharings have the same impact on the reduction. This applies in particular to P ch , P blm and P af , and thus it shows that all the notions of full laziness in [Wad71, AF97, Ses97, SW04, BLM07] define the same reduction spaces.

Fully lazy λ-lifting

The primary goal of the present section is to prove that the notion of full laziness defined by fully lazy λ-lifting in [START_REF] Hughes | Super combinators: A new implementation method for applicative languages[END_REF][START_REF] Jones | The Implementation of Functional Programming Languages[END_REF] is equivalent to the unified notion of the previous section. This study of λ-lifting also reveals a strong relationship between optimal sharing in weak λ-calculi [START_REF] Blanc | Sharing in the Weak Lambda-Calculus Revisited[END_REF] and the optimality theory of first-order rewriting [START_REF] Maranget | Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems[END_REF][START_REF]Term Rewriting Systems[END_REF].

In this section fully lazy λ-lifting is ultimately seen as a morphism between two systems: the source is the set of the λ-terms equipped with weak β-reduction, whereas the target is the set of first-order terms built with supercombinators equipped with their associated first-order reduction rules. However, the source and the target system are mixed in the intermediate steps. Fully lazy λ-lifting is then defined as an endomorphism of an object system combining the source and the target.

Our object system is a CRS over a labelling of the signature Σ defined in Section 2.1. The weak β-reduction is as defined in Section 2. The supercombinators forming the target subsystem are represented by the symbols in F = n F n and their reduction rules are defined in Section 4.1. Fully lazy λ-lifting itself is represented by a set of CRS rules which is proved to be confluent (Lemma 5), to be strongly normalizing (Lemma 6), to preserve one-step reduction (Theorem 3) and to preserve shared reduction (Theorem 4). Since we aim for this last result on shared reduction and since shared reduction is formalized in this paper by the labels, our λ-lifting is defined on labelled terms. Section 4.1 introduce an extension of sharing-via-labelling systems and defines fully lazy λ-lifting as a rewriting process. Section 4.2 then proves that fully lazy λ-lifting is a bisimulation between the source system and the target system, and Section 4.3 proves that parallel labelled fully lazy λ-lifting preserves optimal sharing.

Fully lazy λ-lifting systems

This section introduces the fully lazy λ-lifting systems as an extension of the sharing-via-labelling systems. Then, λ-lifting is defined as a CRS reduction in a fully-lazy λ-lifting system. This reduction is confluent and strongly normalizing.

The basic mechanism of λ-lifting is the replacement of a whole prefix by a supercombinator, the prefix and the supercombinator being related by an abstract invertible function called contractor. In order to preserve sharing, this replacement has to preserve all the information contained in the labels. Our solution consists in labelling the supercombinator with a structured label containing all the labels of the contracted prefix. Hence the basic operations of λ-lifting are reversible, and we define two inverse transformations (contraction and expansion) which allow to reversibly relate labelled prefixes and labelled supercombinators.

Fully lazy λ-lifting is related in this paper to the weak β-reduction system P ch of Example 5, whose definition is reminded below. We also recall that the system P ch is safe (Remark 2). The ch subscript is omitted along this section.

• P(λx.t) is the skeleton of λx.t.

• P (t) = [] for any term t.

The structured labels used for labelled λ-lifting are tree-shaped, similarly to terms (see Example 13). For any countable set V (whose elements are called atomic labels), the set V of tree labels over V is defined by the following grammar:

V

::= | | ⊥ | V | V( V, ..., V)
The label is an "empty" label which is used to denote the lack of label of the empty context [] (see Example 13). The labels in V are used as virginal labels along this section. A tree label is well-formed when no atomic label appears twice in it. For any Ω 1 , ..., Ω n , a label [Ω 1 ...Ω n , α] with α ∈ V is well-formed when α is well-formed.

The clash relation is defined on tree labels as: α β when α and β have an atomic label in common. The notion is used in Section 4.3 to express invariants on labels. For any V and any N , the clash extends to V N as follows:

α β if and only if α = [Ω 1 ...Ω n , α * ] and β = [Ω 1 ...Ω n , β * ] with α * , β * ∈ V and α * β * .
A contractor is an injective partial function ϕ mapping unlabelled nary skeletons to unlabelled n-ary function symbols. For any set of atomic labels V and any set of names N , a contractor ϕ is extended to V N -labelled skeletons and V N -labelled symbols by the following rules.

• If p is labelled with virginal labels, then ϕ(p) = f α such that f = ϕ(|p|) and α = p , where

[] = x α = α α (t) = α( t ) λ α x.t = α( t ) @ α (t 1 , t 2 ) = α( t 1 , t 2 ) f α (t 1 , ..., t n ) = α( t 1 , ..., t n ) • If p can be decomposed as p = [Ω, p ], then ϕ(p) = [Ω, ϕ(p )]. • Else, ϕ(p) is undefined.
The extension of ϕ to labelled skeletons is still injective, hence the labelled ϕ admits an inverse.

Example 13.

1. Consider the skeleton p = λ α x.@ β ([], λ γ y.@ δ (@ κ (y ν , []), x ι )). The collected label is p = α(β( , γ(δ(κ(ν, ), ι)))). It is interesting to compare the graphical representations of the prefix and the label: λx

@ [] λy @ x @ y [] α β γ δ ι κ ν 2. Suppose ϕ(λx.@([], x)) = g. Then • ϕ -1 (g α(β( ,γ)) ) = λ α x.@ β ([], x γ ) • ϕ -1 (g [Ω,α(β( ,γ))] ) = λ [Ω,α] x.@ [Ω,β] ([], x [Ω,γ] ) • ϕ -1 (g α(β(δ(ι),γ))
) is undefined because the label has not the same structure as ϕ -1 (g).

• ϕ(λ [Ω 1 ,α] x.@ [Ω 2 ,β] ([], x [Ω 2 ,γ]
)) is undefined because the labels have different modifiers Ω 1 and Ω 2 .

For any set of atomic labels V, for any set of names N and for any contractor ϕ, ϕ-contraction and ϕ-expansion are two CRS rule schemes on V N -labelled terms. For any skeleton λ α x.p and symbol f β such that ϕ(λ α x.p) = f β we have the two rules:

(ϕ-contraction) λ α x.p[Z 1 , ..., Z n ] → c f β (Z 1 , ..., Z n ) (ϕ-expansion) f β (Z 1 , ..., Z n ) → e λ α x.p[Z 1 , ..., Z n ]
Call an object redex a labelled term having one of the two following forms:

(source redex) @ α ( β 1 ...β k k (λ γ x.t), a) (target redex) @ α ( β 1 ...β k k (f γ (t 1 , ..., t n )), a)
Remark that the set of object redexes is stable by → c and → e . A fully lazy λ-lifting system is a tuple ϕ, N , V, η, → such that:

• P, N , V, η, → is a sharing-via-labelling system.

• ϕ is a contractor.

• P commutes with ϕ-contraction and ϕ-expansion.

• η is a function from object redexes to names that is stable by ϕcontraction and ϕ-expansion.

In a fully lazy λ-lifting system ϕ, N , V, η, → we consider L-labelled terms with L = V N .

Example 14 shows a straightforward extension of the function η seq of Example 8 which is not stable by contraction. Example 15 then gives stable variants of the functions η seq and η ctx .

Example 14. Consider the redex r = @ α (λ γ x.@ δ (x ι , y κ ), a), which can be ϕ-contracted to r = @ α (f γ(δ(ι, )) (y κ ), a) for some unary symbol f . Then η seq (r) = α; γ and η seq (r ) = α; γ(δ(ι, )): the name is not stable.

Example 15.

1. Define η seq (@ α ( β 1 ...β k k (λ γ x.t), a)) = α; β 1 ; ...; β k ; δ with γ = [Ω 1 ...Ω n , γ * ] and δ = [Ω 1 ...Ω n , δ * ] where γ * is virginal and δ * is the leftmost atomic label of γ * . This name function is stable since the leftmost atomic label is stable by contraction and expansion.

If

P(λx.t) = p, then define η ctx (@ α ( β 1 ...β k k (λ γ x.t), a)) = @ α ( β 1 ...β k k (f δ ([], ..., [])), [])
where f δ is the unique normal form of λ γ x.p by λ-lifting (see definition of λ-lifting and lemmas 5 and 6 below). This name function is stable by normalization.

We call source reduction the β-reduction, whose rule scheme can be simplified:

@ α ( β 1 ...β k k (λ γ x.p[Z 1 , ..., Z n ]), Z) → β [Ω, ] ([Ω, p]) {x:= [Ω,⊥] (Z)} [Z 1 , ..., Z n ]
where λ γ x.p is a skeleton and where Ω = η(@ α ( β 1 ...β k k (λ γ x.p[z 1 , ..., z n ]), z)).

We call target reduction the first-order reduction defined by the scheme:

@ α ( β 1 ...β k k (f γ (Z 1 , ..., Z n )), Z) → t [Ω, ] ([Ω, p]) {x:= [Ω,⊥] (Z)} [Z 1 , ..., Z n ]
where ϕ -1 (f γ ) = λ δ x.p and where Ω = η(@ α ( β 1 ...

β k k (f γ (z 1 , ..., z n )), z)).
Call object reduction the union of source reduction and target reduction:

→ o = → β ∪ → t .
Remark 4. Target reduction can be decomposed by ϕ-expanding the function symbol and then applying β-reduction.

Remark 5. Consider the system S = P ch , N ctx , V, η ctx , → ctx where N ctx and → ctx are defined in Example 8, η ctx is defined in Example 15, and V is any countable set. The target reduction of S is isomorphic to what is called Lévy-labelling in [START_REF]Term Rewriting Systems[END_REF]Chap. 8].

For a clean definition of λ-lifting and for simple proofs of its basic properties we use an extended notion of positions of a term. The so-called ϕpositions contain the usual syntactic positions but also the positions that are "hidden" in supercombinators: through the contractor ϕ each symbol represents a prefix, and the positions of these prefixes are taken into account in ϕ-positions.

The set Q(t) of ϕ-positions of t is defined by:

Q(x) = {ε} Q([]) = {ε} Q( (t)) = {ε} ∪ 1.Q(t) Q(λ α x.t) = {ε} ∪ 1.Q(t) Q(@ α (t 1 , t 2 )) = {ε} ∪ 1.Q(t 1 ) ∪ 2.Q(t 2 ) Q(f α (t 1 , ..., t n )) = {ε} ∪ 0.Q(ϕ -1 (f α )) ∪ ( i i.Q(t i ))
The following cases define λ-lifting as a CRS reduction:

• (Reify) If λ α x.p is a skeleton such that ϕ(λ α x.p) = f β , then λ α x.p[Z 1 , ..., Z n ] ε - → lft f β (Z 1 , ..., Z n ) • (Inside) If ϕ -1 (f α )[x 1 , ..., x n ] q - → lft ϕ -1 (g β )[x 1 , ...,
x n ] where x 1 , ..., x n are fresh variables then

f α (Z 1 , ..., Z n ) 0.q --→ lft g β (Z 1 , ..., Z n ) • (Context) If t q 1
-→ lft t and c is a unary context with a hole at position q 2 , then c[t]

q 2 .q 1 ---→ lft c[t ]
While Reify is the main rule of λ-lifting, Inside allows to close confluence diagrams (see Example 16) and consider λ-lifting as an orthogonal rewriting system (in the sense of [START_REF] Glauert | Expression reduction systems and extensions: An overview[END_REF], after the extension of the notion of descendants given below). An Inside reduction can be seen as a reduction Reify inside a symbol. An equivalent of Inside naturally appears in [START_REF] Ariola | The call-by-need lambda calculus[END_REF] or [START_REF] Sestoft | Deriving a lazy abstract machine[END_REF] as a reduction in the context of a let ... in ... construct. Please note that in the rule Context, c is an arbitrary context. This means that there is no particular weak restriction here.

Example 16.

Let t = λ α x.@ β (@(z 1 , z 2 ), λ γ y.@ δ (@ κ (y ν , z 3 ), x ι )) be a labelled term, where some labels are omitted. Write

ϕ -1 (f ) = λx.@([], λy.@(@(y, []), x)) µ = α(β( , γ(δ(κ(ν, ), ι)))) ϕ -1 (g) = λy.@(@(y, []), []) σ = γ(δ(κ(ν, ), )) ϕ -1 (f ) = λx.@([], g([], x)) µ = α(β( , σ( , ι)
)) The dotted lines denote the skeleton of the abstraction λ γ y, while the bold lines (solid or dotted) denote the skeleton of the abstraction λ α x. λ α x

@ β @ z 1 z 2 λ γ y @ δ x ι @ κ y ν z 3 1.2 λ α x @ β @ z 1 z 2 g σ x ι z 3 ε ε f µ @ z 1 z 2 z 3 0.1.2 Inside f µ @ z 1 z 2 z 3
Remark 6. The reduction Reify is a straightforward use of contraction → c , and the reduction Inside can be factorized using contraction → c and expansion → e : if t → lft t by Inside, then there are u and u such that t → e u → c u → c t .

The notion of descendant is extended to ϕ-positions:

• If t → β t and q = q 1 .0.q 2 is a position of t such that there is no 0 in q 1 , then the ϕ-descendants of q are the q 1 .0.q 2 such that q 1 is a descendant of q 1 .

• If t → c t at position q 1 and q 2 is a ϕ-position of the prefix of t| q 1 , then q 1 .q 2 has exactly one descendant in t , which is q 1 .0.q 2 .

• If t → e t at position q 1 and q 2 is a ϕ-position of the symbol at position q 1 in t, then q 1 .0.q 2 has exactly one descendant in t , which is q 1 .q 2

The notion of descendant extends to → lft and → t by decomposition of these reductions on → β , → c and → e (along Remark 6). Remark that in Example 16, the east (resp. south) reduction is a residual of the west (resp. north) reduction.

Lemma 5 (Diamond property). If t → lft u and t → lft v with u = v then there is w such that u → lft w and v → lft w.

Proof. Remark that the descendance relation after → c (resp. → e ) is a bijection between the ϕ-positions of the source and the target. Then the same is valid for → lft . Moreover, the descendant of a → lft -redex is still a → lft -redex (thanks to the rule Inside). From this we easily derive the orthogonality of → lft in the sense of [START_REF] Glauert | Expression reduction systems and extensions: An overview[END_REF], and deduce that → lft has the diamond property.

Lemma 6 (Termination). The system → lft is strongly normalizing.

Proof. We define a measure §(.) on terms denoting the number of → lftredexes. Formally:

§(x) = 0 §([]) = 0 §(λx.t) = 1 + §(t) §(@(t 1 , t 2 )) = §(t 1 ) + §(t 2 ) §( (t)) = §(t) §(f (t 1 , ..., t n )) = §(p) + Σ i §(t i ) with ϕ -1 (f ) = λx.p
An important part of the definition is that we ignore the λ at the root of ϕ -1 (f ).

If t → c t then §(t ) = §(t) -1, and if t → e t then §(t ) = §(t) + 1. By decomposition of → lft on → c and → e (remark 6) we deduce than if t → lft t then §(t ) = §(t) -1. Hence the measure strictly decreases and → lft is strongly normalizing.

Lemma 5 implies that → lft is confluent, and that all the → lft -sequences between two given terms have the same length [START_REF]Term Rewriting Systems[END_REF]. An immediate corollary of lemmas 5 and 6 is that any term has a unique → lft -normal form.

-Case Inside. This bisimulation is a strong property for λ-lifting: it associates a progressive transformation of reduction sequences to the progressive transformation of terms. Moreover, there is a bijection between the single steps of the image and the antecedent reduction sequences. In the next section, we show that this holds also for parallel labelled reduction.

t = f α (t 1 , ..., t n ) with λ β x.p = ϕ -1 (f α ). t → o t = f α (t 1 , t 2 , ..., t n ) with t 1 → o t 1 wlog. Then t → lft u = f γ u (t 1 , ..., t n ) → o f γ u (t 1 , t 2 , ..., t n ) = u with λ δ x.p u = ϕ -1 (f γ u )

Fully-lazy λ-lifting as a graph bisimulation

For r ∈ {β, t, o, c, e, lft}, write α = ⇒ r the simultaneous reduction of all the → rredexes of label α in a term satisfying the sharing property S. This last section shows that = ⇒ lft preserves sharing: the same subterms are shared in the source and in the target of this reduction. This allows to conclude that the full lazinesses of [START_REF] Wadsworth | Semantics and Pragmatics of the Lambda Calculus[END_REF] and [START_REF] Jones | The Implementation of Functional Programming Languages[END_REF] are bisimilar.

In this section we use again the invariants S and M introduced in Section 2.3. In our new setting we extend M to any object redex. We moreover use the following three invariants: 3. Say a term t has the independent labelling property, written I(t), when all the labels of t are well-formed and there is no pair of labels (α, β) of t such that α = β and α β. This property is useful to ensure that contraction and expansion do not break the sharing property.

4. Say a term t has the tuned skeletons property, written T(t), when every skeleton p in t is of the form [Ω 1 ...Ω n , p * ] where p * has only virginal labels. This property allows to apply a contractor ϕ to any prefix, and rules out the last case of Example 13.

5. Say a term t has the harmonious binding property, written H(t), when any two variables with the same label are either both free or both bound by abstractions bearing the same label. This property strengthens the sharing property: when both are present, two whole skeletons are shared whenever one of their nodes is shared.

Finally, say a term t has the SMITH property (written SMITH(t)) when the five properties are satisfied by t as well as by ϕ -1 (f α ) for any f α appearing in t (or recursively in the antecedent by ϕ of a symbol).

Lemma 9. For any r ∈ {β, t, o, c, e, lft} and any two terms t, t , if SMITH(t) and t α 0 = ⇒ r t then SMITH(t ).

Proof. By remarks 4 and 6 we need only consider the cases where r ∈ {β, c, e}.

Case

α 0 = ⇒ β .
The properties S(t ) and M(t ) are satisfied by Theorem 1. Verification of I(t ). Suppose there are two terms u and v of labels α and β in t such that α β . Case on the origins of α and β .

• If one is a descendant of itself and not the other, then by M(t ) we have a contradiction, since α and β have the same modifiers.

• If they are descendants of terms u and v in t with labels α and β , then contradiction by I(t).

• Else, they are descendants of terms u and v in t with labels α and β such that α = [Ω 0 , α] and β = [Ω 0 , β]. Hence α β, which contradicts I(t).

Verification of T(t ). Let p be a skeleton in t and p be its ancestor in t. Write p = [Ω 1 ...Ω n , p * ] with p * virginal. If p does not intersect the prefix of a reduced redex then p = p. On the other hand, if p intersects the prefix of a reduced redex, then it is contained in this prefix, and p = [Ω, p]. In both cases p has the expected form.

Verification of H(t ). Let x α and y α be two labelled variable occurrences of t . By case on the origin of both labels α :

• If one is created and the other is a descendant of a label α in t, then Ω 0 → α , which contradicts M(t).

• If both are descendants of labelled variables x α and y α of t, then H(t) applies:

-Either both are free, which is still true in t .

-Or both are bound, by abstractions with the same label β. Then by T(t ) the binders of x α and y α in t both have the label β.

• Else, both are descendants of labelled variables x α and y α of t such that α = [Ω 0 , α,], then H(t) applies:

-Either both are free, which is still true in t .

-Or both are bound, by abstractions with the same label β. Then by T(t ) the binders of x α and y α in t both have the label [Ω 0 , β].

Case

α 0 = ⇒ c .
Verification of H(t ). Let x α be a labelled variable in t . Its ancestor in t is x α (with same label). And if x is bound, then its binder has also the same label as its ancestor. Then H(t ) immediately follows from H(t).

Verification of T(t

). Straightforward since ϕ([Ω, p]) = [Ω, ϕ(p)].
Verification of I(t ). Let u and v be two terms in t with different labels α and β such that α β . By case on the origins of α and β .

• If both are descendants of themselves, then contradiction by I(t).

• If both are created by the reduction, then α = β , which is not the case.

• If α is created and β descends from β , then write α = [Ω 1 ...Ω n , p ]. Let α * be an atomic label that appears in α and β . In particular α * appears in a label α of p, and there is a label [Ω 1 ...Ω n , α] in t, which is such that [Ω 1 ...Ω n , α] β . Contradiction by I(t).

• The case where α descends from α and β is created is symmetrical.

Verification of M(t ). Suppose there is a redex r of name Ω and a subterm u of label α in t such that Ω → α . The redex r is the residual of a redex r of t with the same name Ω (by stability of η). Reason by case on the origin of α :

• If u is the descendant of a subterm u of t with label α then there is a contradiction with M(t).

• If α is created then α is of the form [Ω 1 ...Ω n , p ] and there is at least one α of the form [Ω 1 ...Ω n , α * ] in t with α * a virginal label appearing in p. Then ↑ α = ↑ α and there is a contradiction with M(t).

Verification of S(t ). Let u and v be two terms of t with the same label α . Reason by case on the origin of both occurrences of α .

• If one is created by the reduction and the other is a descendant of itself, then α = [Ω 1 ...Ω n , p ] and there is a label α in the redex such that α = [Ω 1 ...Ω n , α * ] and with α * virginal and α * appearing in p. In particular α * p and α α , which contradicts I(t).

• If both are created by the reduction, then u = v = r . Finally, write t ≈ t is t and t are = ⇒ lft -convertible.

We deduce that any ≈ This implies that the implementations of full laziness in [START_REF] Wadsworth | Semantics and Pragmatics of the Lambda Calculus[END_REF] and [START_REF] Jones | The Implementation of Functional Programming Languages[END_REF] define the same reduction space, which also correspond to optimal sharing along [START_REF] Maranget | Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems[END_REF][START_REF]Term Rewriting Systems[END_REF] for the first-order system defined by the target reduction → t , and to optimal sharing along [START_REF] Blanc | Sharing in the Weak Lambda-Calculus Revisited[END_REF] for the CH-weak reduction of the λ-calculus.

Conclusion

Sharing, and in particular fully lazy sharing, is described and implemented by different technical tools including graphs, closures, and program transformations. As a consequence, the many definitions of fully lazy sharing [Wad71, Jon87, Ses97, AF97, SW04, BLM07] are sometimes hardly comparable. Yet they all intend to implement the same basic ideas.

This paper unifies all these views of full laziness. To achieve this we define an axiomatic framework of sharing-via-labelling systems, in which the various approaches can be expressed. Then we prove that all the resulting systems are bisimilar, in the sense that they have isomorphic reduction spaces.

In particular, by linking [START_REF] Blanc | Sharing in the Weak Lambda-Calculus Revisited[END_REF] to other definitions of full laziness, we confirm the intuition of its authors that fully lazy sharing gives an optimal sharing for the weak λ-calculus of [C ¸H98].

Last but not least, we show that weak reduction in λ-calculus can be expressed in orthogonal first-order rewriting by means of fully lazy λ-lifting, with a one-to-one correspondence between their reduction steps. This remarkable last property makes our first-order formulation really different from the formulations that use de Bruijn indices or explicit substitutions [START_REF] Turner | A new implementation technique for applicative languages[END_REF][START_REF] Maranget | Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems[END_REF]. Moreover, our transformation preserves optimal sharing and expresses fully lazy sharing as optimal sharing for the target first-order system.

Related work

Related approaches to the efficient implementation of functional programming languages include in particular the study of optimal reduction and the attempts to implement it. The study of optimal reduction [Lé80, Mar91, GK96, vO96, BLM07] traditionally uses three equivalent characterizations called labelling, extraction, and zig-zag. This paper extends the labellingbased characterization of optimality to weak β-reduction systems.

The possibility of a straightforward implementation in graphs of the label-based characterization of optimality has for long been known to be a feature of first-order rewriting [START_REF] Maranget | Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems[END_REF] that did not hold in the λ-calculus. However, more recently this feature has been observed in a weak restriction of the λ-calculus [START_REF] Blanc | Sharing in the Weak Lambda-Calculus Revisited[END_REF]. The present paper confirms this observation by showing that it holds in any weak β-reduction system, and explains this first-order behaviour of weak reduction by expliciting a link between weak β-reduction systems and first-order rewriting.

Two kinds of implementations are known to perform less shared βreduction steps than some fully lazy implementations. In particular partial evaluation [START_REF] Holst | Partial evaluation is fuller laziness[END_REF] has been compared to [START_REF] Jones | The Implementation of Functional Programming Languages[END_REF], and optimality [START_REF] Lévy | Optimal reductions in the lambda-calculus[END_REF] is born as an idealization of [START_REF] Wadsworth | Semantics and Pragmatics of the Lambda Calculus[END_REF]. Hence this paper shows that partial evaluation [START_REF] Holst | Partial evaluation is fuller laziness[END_REF] as well as any implementation of optimality [AG98, PQ07] is able to perform less shared β-reduction steps than any implementation of full laziness.

On the other hand, a global comparison between all these approaches is still missing. In particular, the following facts keep the question open for now: the number of shared β-reduction steps in a fully lazy system is polynomially related to the actual cost of performing the reduction on a Turing machine (simple extension of [START_REF] Lago | On constructor rewrite systems and the lambda-calculus[END_REF]), but this does not hold with optimal sharing [START_REF] Lawall | Optimality and inefficiency: What isn't a cost model of the lambda calculus?[END_REF].

Future work

Fully lazy λ-lifting is shown to be a powerful tool to give a faithful first-order account of higher-order systems. This phenomenon prompts us to carry on investigations in at least two directions:

• Generalization of λ-lifting to any weak β-reduction system satisfying our axioms. Two interesting and challenging examples would be:

-The plain λ-lifting of [START_REF] Johnsson | Lambda lifting: Transforming programs to recursive equations[END_REF], in which the prefixes are not stable by reduction, as shown in Example 6.

-A new notion of λ-lifting based on P blm , which would turn the spines into supercombinators. Since the spines can bind variables in their holes, some function symbols would also bind some variables in their arguments (in the intermediate steps of the transformation).

• Generalization of sharing and λ-lifting to any higher-order system. This would include richer rewriting systems working on functions, such as proof assistants and compilers. As far as the author is aware, general higher-order rewriting knows no notion of weak reduction, sharing-vialabelling, or λ-lifting. However, the present work seems to be abstract enough to be generalized to higher-order rewriting frameworks such as combinatory reduction systems.

  The two 's in the right hand sides are used for the correct labelling of collapsing reductions (see Subsection 2.2). The use of the dummy symbol is inspired by the notion of expansion in term rewriting systems [Ter03, Chap. 8].

• 0 = ⇒ lft u , v α 0 =

 00 If τ (u) = α and τ (v) = α then τ (u) = τ (v) = α 0 . Suppose τ (u) = τ (v) = α. If α = α 0 , then τ (u ) = τ (u) = τ (v) = τ (v ). Else u = v, uα ⇒ lft v and u = v . In particular τ (u ) = τ (v ).

  is the skeleton of λx.t and λx.t = λx.p[t 1 , ..., t n ] then P

af (λx.t) = λx.p[P af (t 1 ), ..., P af (t n )].

  and λ β x.p[x 1 , ..., x n ] → lft λ δ x.p u [x 1 , ..., x n ] where x 1 , ..., x n are fresh variables. Thus t → lft u by Inside.• Reduction → o in the prefix of the → lft -redex: forbidden by weak reduction.

	The backward simulation lemma (second point) is similar.
	Lemma 8 yields as immediate corollary:
	Theorem 3 (Bisimulation). The relation lft is a bisimulation between
	the reduction → o and itself, which means that:
		lft		lft			lft
		t	u	t	u	t	u
	any diagram	o	or		o can be closed as	o	o
		t			u	t	lft	u

a reducible expression, or redex, designs a place where an evaluation step can take place

in brief, a system is orthogonal when no two rules are applicable to overlapping sets of positions of a term, see for instance[START_REF]Term Rewriting Systems[END_REF][START_REF] Bruggink | Residuals in higher-order rewriting[END_REF]

Acknowledgements

The author would like to thank Delia Kesner for her continuous support, Vincent van Oostrom for a mysterious but insightful remark that triggered this investigation, and the anonymous reviewers for numerous helpful comments and suggestions.

Fully-lazy λ-lifting as a bisimulation

This section proves that → lft does not only transform terms but also reduction sequences, and that the transformation operates forward as well as backward. Formally, the reflexive-transitive closure of the relation → lft (written lft ) is a bisimulation between → o and itself. Thanks to the CRS formalism which allows reasoning on the intermediate steps of the transformation, the proof can be reduced to a one-step simulation property (Lemma 8).

Proof. By induction on t → lft t , using stability of P by substitution and

Lemma 8 (One-step simulation).

Proof. Forward simulation (first point). By case on the relative positions of the two redexes. Write Ω the name of the → o redex. Most of the cases use the stability of η (which means here the stability of Ω), and the commutation of P with → lft .

• Reduction → lft on the main function of the → o -redex. Case on → lft .

-Case Reify. t = @ α ( β 1 ...β k k (λ γ x.p[t 1 , ..., t n ]), a), with λ γ x.p a skeleton, t 1 , ..., t n free expressions. Then t

), a) with λ γ x.p a skeleton and t 1 , ..., t n free expressions, then t

), a), with λ γ x.p a skeleton and t 1 , ..., t n free expressions, then t

.., t n ] = u , and moreover t → lft u .

• Reduction → lft in the argument of the → o -redex.

-Reduction → β . t = @ α ( β 1 ...β k k (λ γ x.p[t 1 , ..., t n ]), a), with λ γ x.p a skeleton and t 1 , ..., t n free expressions, then t

.., t n ] = u , and moreover t lft u .

• Reduction → o in a parameter of the → lft -redex.

-Case Reify.

Thus t → lft u by Reify.

• If both are descendants of terms u and v with same label α , then by S(t) we have u = v, u

Verification of H(t ). Let x α and y α be two labelled variables in t . By case on their origins:

• If both have an ancestor in t, then the ancestors are x α and y α (with the same labels), and the conclusion comes from H(t).

• If x α has an ancestor in t (equal to x α ) and the other is created, then α 0 = [Ω 1 ...Ω n , p ] and α = [Ω 1 ...Ω n , α * ] with α * virginal and α * appears in p , which contradicts I(t).

• If both are created, then there is a labelled symbol f α 0 such that x α and y α both appear in ϕ -1 (f α 0 ). Conclusion by H(ϕ -1 (f α 0 )).

Verification of T(t

Verification of I(t ). Let u and v be two terms in t with different labels α and β such that α β . By case on the origins of α and β .

• If both are descendants of themselves, then contradiction by I(t).

• If both are created by the reduction, then

with α * and β * two sublabels of p and α * β * . We have a contradiction since α = β and p is well-formed by SMITH(t).

• If α is created and β descends from β , then in particular α 0 =

[Ω 1 ...Ω n , p ] and α = [Ω 1 ...Ω n , α * ] where α * appears in p . Then α β implies α 0 β , which contradicts I(t).

• The case where α descends from α and β is created, is symmetrical.

The verifications of M(t ) and S(t ) are similar to those given in the case of

Theorem 4 (Preservation of optimal sharing). Let t be a term such that SMITH(t). Suppose t α 0 = ⇒ lft t . Let u (resp. v ) be a subterm of t , with ancestor u (resp. v) in t. Then τ (u ) = τ (v ) if and only if τ (u) = τ (v).

Proof. Suppose τ (u ) = τ (v ) = α . Case on the origin of α :

• If τ (u) = τ (v) = α , it's over.

• If τ (u) = α and τ (v) = α , then τ (v) = α 0 such that α 0 = [Ω 1 ...Ω n , α * 0 ] and α = [Ω 1 ...Ω n , α * ] with α * 0 appearing into α * , which implies α α 0 and contradicts I(t).


Eugen Barbu

Clement Chatelain

Sebastien Adam

Pierre Heroux

Eric Trupin

A simple one class classifier with rejection strategy : application to symbol classification

Keywords: pattern recognition, symbol classification, one class classifiers, outlier rejection strategy

At the preceding GREC, we have proposed to use a "bag of symbols" formalism (similar to the bag of words approach) for the indexing of a graphical document image database. In this paper, we extend the proposed approach through the introduction of a rejection stage in the system. This rejection is based on the use of an original One Class Classifier. Some preliminary results are proposed.

Introduction

At the preceding GREC [Barbu 2005] , we have proposed to use a "bag of symbols" formalism (similar to the bag of words approach) for the indexing of a graphical document image database. In this contribution, documents are represented and indexed using a set of symbols that are discovered in an unsupervised manner thanks to clustering algorithms and graph mining methods. The first enables to automatically label graph nodes representing connected components while the latter aims at finding frequent subgraphs in the graph describing the whole document. Numerous tests have been led since this proposition. An analysis of the obtained results has shown that the graph mining algorithm tends to integrate outliers in the proposed symbol classes. This problem strongly impacts on the global system performance. In this paper, we propose an outlier rejection strategy which has been developed to tackle this problem. It is based on a simple One-Class classifier and an original rejection strategy to filter outliers. In section 2, the general principles of one-class classifiers are given. Then, in section 3, our proposition is presented. In section 4, the application of the proposed approach to symbol classification is presented and evaluated.

One-class classifiers

Nowadays, new statistical learning methods such as Support Vector Machine (SVMs) or Artificial Neural Network (ANNs) provide strong classification performance for various pattern recognition applications. For example, in the field of handwriting recognition, recent benchmarks [START_REF] Liu | Performance evaluation of pattern classifiers for handwritten character recognition[END_REF] show that a precision accuracy of nearly 99% can be reached on the famous MNIST handwritten digits database, using SVM with RBF kernels. However, in real world applications, another important feature for pattern recognition systems is the rejection ability, i.e. the ability to reject the pattern which do not belong to any of the known classes. Such patterns are frequently denoted as outliers. In the case of a symbol recognition system, it consists in :

assigning the pattern to the right symbol class if a symbol appears rejecting the pattern if it is an outlier, i.e. it does not represent a known symbol.

The first objective can be performed by finding the best frontiers between the classes, whereas the second objective is reached by finding either a density estimation of the class, either its boundaries. One way to perform this second objective is the one-class classifiers. As said in [START_REF] Tax | Combining One-Class Classifiers[END_REF], the goal of one-class classification is to distinguish between a set of target objects and all other possible objects (per definition considered outliers objects). The advantage of this description is that it does not need outliers samples to train the model.

Proposed scheme

In this section we present a simple one-class classifier with an original and robust method to order the elements of a class with respect to the measure of how typical is an object within a class. Using this order, one can fix a rejection threshold in order to discard potential outliers from a class.

One way to obtain typical elements of a class of objects is to keep only the elements close to the center of the class. In order to measure this typicalness of objects, in a general dissimilarity space, a method is to compute the average distance of an element to all other objects of the class [START_REF] Bunke | Syntactic and structural pattern recognition : theory and applications[END_REF].

where N is the number of objects in a class, e i is an element of the class for which the index is computed, and d e , e '  a distance function between objects.

The values

T 1, T 2,. .. ,T N can be easily calculated and only a percent of these objects can be retained if a filtering is needed. In such a case, The first k elements in the ascending ordered set of typicality values are kept as being closer to class center.

T j 1 ≤T j 2 ≤, ... ,≤T j k ≤T j k1 ≤...≤T j N Another possibility to filter a class of objects, is to detect the potential outliers using the following described measure. Given the following notations :

• kNN d o the k-th nearest neighbor of an object o in the learning dataset using a distance function d .

• FN d o represents the farthest element of an object o in the learning using a distance function d . Then, the following equation can be used to measure if a pattern o i is an outlier or not : A value r i k bigger than 1 stands for an object o i out of the class, from the point of view of the k-th nearest neighbor of o i . The decisions of several neighbors of o i can be combined in a measure of membership :

R i K = ∑ k=1 K r i k /K
where K is the number of nearest neighbors used to estimate the membership. In Fig. 2 we can see that this second measure approximates better the class frontiers.

T i = ∑ j=1 N d e i , e j / N r i k = d o i , kNN d o i  d kNN d o i  , FN d  kNN d o i 

Application to symbol recognition

As said in the introduction, the proposed approach takes place in a graphical document retrieval system which uses a "bag of symbols" formalism to index documents. In this particular application, the aim is to filter outlier symbols which have been found using graph mining techniques. As explained in section 3, the single constraint in order to use the proposed approach is to define a distance measure between two individuals. Consequently, a matching distance between symbol images is needed. As presented in [Barbu 2005], each image can be made of a number of connected components. In the proposed approach each of the connected component is characterized by its surface and Zernike invariants. In order to measure the similarity of two symbol images, we compute the minimum cost matching between the set of connected components of the first image to the connected components of the second, with the possibility to delete connected components [START_REF] Kriegel | Similarity search in structured data[END_REF].

The problem is to find a function f that maps a connected component to other or to the delete operation

d c i , c j ' =L 1  area c i  , areac j '  L 2  zm c i  , zm c j '  with L 1 , L 2 euclidean norms.
Such assignment problems are well studied in the field of combinatorial optimization [START_REF] Papadimitriou | Combinatorial Optimization : Algorithms and Complexity[END_REF]]. The Hungarian Method is an algorithm used for weighted assignment with O n 3  time complexity, where n is the number of connected components in our case. Figure 3 illustrates the assignment process. On the left, we show the results of the assignment between a symbol and itself. In the middle, we show the results of the assignment between two occurrences of the same symbol.

On the right, we show the results of the assignment between two different symbols.

Figure 3. Assignment process

Table 1. Assignment results Table 1 shows another example of assignment results with 5 symbols. Using these results, the proposed approach can be applied to reject the outliers. We obtain :

T 1 =1.25T 3 =1.28T 2 =1.41T 4 =1.46T 5 =2.15  R 1 1 =0.403= R 3 1 =0.403 R 2 1 =0.406 R 4 1 =0.47 R 5 1 =0.89
and from that we can spot d5 as an outlier in the presented class of symbols.

Figure 1 .

 1 Figure 1. Illustration of the proposed approach principles

Figure 2 .

 2 Figure 2. a comparison between the membership functions obtained using T i and r k

Conclusion

In this paper, we have proposed a simple one class classifier. This one is applied in the context of symbol recognition for document retrieval. Preliminary results have shown promising results. Some tests are led currently on different databases.