Gabriel Scherer

Multi-focusing on extensional rewriting with sums

Keywords: 1998 ACM Subject Classification F.4.1 Lambda calculus and related systems Maximal multi-focusing, extensional sums, rewriting, natural deduction Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p

We propose a logical justification for the rewriting-based equivalence procedure for simply-typed lambda-terms with sums of Lindley [Lin07]. It relies on maximally multi-focused proofs, a notion of canonical derivations introduced for linear logic. Lindley's rewriting closely corresponds to preemptive rewriting [CMS08], a technical device used in the meta-theory of maximal multi-focus.

Introduction

Deciding observational equality of pure typed lambda-terms in presence of sum types is a difficult problem. After several solutions based on complex syntactic [Gha95] or semantic [ADHS01, BCF04] techniques, Sam Lindley presented a surprisingly simple rewriting solution [Lin07]. While the underlying intuition (extrude contexts to move pattern-matchings as high as possible in the term) makes sense, the algorithm is still mysterious in many aspects: even though they were synthesized from the previous highly-principled approach, the rewriting rules may feel strangely ad-hoc.

In this paper, we will propose a logical justification of this algorithm. It is based on recent developments in proof search, maximally multi-focused proofs [CMS08]. The notion of preemptive rewriting was introduced in the meta-theory of multi-focusing as a purely technical device; we claim that it is in fact strongly related to Lindley's rewriting, and formally establish the correspondence.

The reference work on multi-focused systems [CMS08] has been carried in a sequent calculus for linear logic. We will first establish the meta-theory of maximal multi-focusing for intuitionistic logic (Section 2). We start from a sequent calculus presentation, which is closest to the original system. Our first contribution is to propose an equivalent multifocusing system in natural deduction 2.2. We then define preemptive rewriting in this natural deduction 2.4 and establish canonicity of maximally multi-focused proofs 2.6.

In Section 3, we transpose the preemptive rewrite rules into a relation on proof terms. We can then formally study the correspondence between rewriting a multi-focused proof into a canonical maximally multi-focused one, and Lindley's γ-reduction on lambda-terms. We demonstrate that they compute the same normal forms, modulo a form of redundancy elimination that is missing in the multi-focused system.

We finally introduce redundancy-elimination rewriting and equivalence for the proof terms of the multi-focused natural deduction (Section 4). The resulting notion of canonical proofs, simplified maximal proofs, precisely corresponds to normal forms of Lindley's rewriting relation. The natural notion of local equivalence between simplified maximal proofs therefore captures extensional equality.

Intuitionistic multi-focusing

The space of proofs in sequent calculus or natural deduction exhibits a lot of redundancy: many proofs that are syntactically distinct really encode the same semantics. In particular, it is often possible to permute two inference rules in a way that preserves the validity of proofs, but also the reduction semantics of the corresponding proof terms. If a permutation transforms a proof with rule A applied above rule B into a proof with rule B applied above rule A, we say that it is an A/B permutation (A is above the slash, as in the source proof).

Focusing is a general discipline that can be imposed upon proof system, based on the separation of inference rules into two classes. Invertible rules (called as such because their inverse is admissible) always preserve provability, and can thus be applied as early as possible. Non-invertible rules may result in dead ends if they are applied too early (consider proving A+B A+B by first introducing the sum on the right-hand side)). In focusing calculi, derivations are structured in "sequences" or "phases", that either only apply invertible rules or only non-invertible rules. Focusing imposes that phases be as long as possible. During invertible phases, one must apply any valid invertible rule. During non-invertible phases, one focuses on a set of formulas, and applies non-invertible operations on those formulas as long as possible -if the phase is started too early, this may result in a dead end.

Invertibility determines a notion of polarity of logical connectives: we call positive those whose right-hand-side rule is non-invertible (they are "only interesting in positive position"), and negative those whose left-hand-side rule is non-invertible. In single-succedent intuitionistic logic, (→) is negative, (+) is positive, and the product (×) may actually be assigned either polarity.

In single-sided calculi, non-invertible rules are those that introduce positive connectives, and are called "positive". For continuity of vocabulary, we will also call non-invertible rules positive, and invertible rules negative. In particular, a permutation that moves a non-invertible rule below an invertible rule is a "pos/neg permutation".

Multi-focused sequent calculus

Multi-focusing ([MS07,CMS08]) is an extension of focusing calculi where, instead of focusing on a single formula of the sequent (either on the left or on the right), we allow to simultaneously focus on several formulas at once. The multiple foci do not interact during the focusing phase, and this allows to express the fact that several focusing sequences are in fact independent and can be performed in parallel, condensing several distinct focused proofs into a single multi-focused derivation.

We start with a multi-focused variant of the intuitionistic sequent calculus, presented in Fig. 1. We denote focus using brackets: the rules with no brackets are invertible. This notation will change in natural deduction calculi.

In particular, we write A n or ∆ p for formula or contexts that must be all negative or positive, and X, Y or Z for atoms. We write B pa and Γ na when either a positive (resp. negative) or an atom is allowed. For readability reasons, we only add polarity annotations when necessary; if we consider only derivations whose end conclusion is unfocused, then the invariant holds that the unfocused left-hand-side context is always all-negative, while the unfocused right-hand-side formula is always positive.

Our intuitionistic calculi are, as is most frequent, single-succedent. The notation A | B on the right does not denote a real disjunction but a single formula, one of the two variables being empty. The focusing rule seq-focus with conclusion Γ, ∆ A | B can be instantiated in two ways, one when A is empty, and the premise is Γ, [∆] [B] (the succedent is part of the multi-focus), and one when B is empty, and the premise is Γ, [∆] A (the succedent is not part of the multi-focus). Note that ∆ is a set and may be empty, in which case the focus only happens on the right.

As a minor presentation difference to the reference work on multi-focusing [CMS08], our contexts are unordered multi-sets, and all the formulas under focus are released at once -by seq-release, which releases positives (resp. negatives) or atoms.

seq-atom X atomic Γ n , X X seq-inv-sum-l Γ, A C Γ, B C Γ, A + B C seq-inv-prod-r Γ A Γ B Γ A × B seq-inv-arr-r Γ, A B Γ A → B seq-focus Γ na , [∆ n ] A pa | [B pa ] Γ na , ∆ n A pa | B pa seq-release Γ, ∆ pa A | B na Γ, [∆ pa ] A | [B na ] seq-foc-arr-l Γ [A] Γ, [∆, B] C | [D] Γ, [∆, A → B] C | [D] seq-foc-prod-l Γ, [∆, A i ] B | [C] Γ, [∆, A 1 × A 2 ] B | [C] seq-foc-sum-l Γ, [∆] [A i ] Γ, [∆] [A 1 + A 2 ] Figure 1 Multifocused sequent calculus for intuitionistic logic
This multi-focused calculus proves exactly the same formulas as the singly-focused sequent calculus. The latter is trivially included in the former, and conversely one can turn a multifocus into an arbitrarily ordered sequence of single foci. As a corollary, relying on non-trivial proofs from the literature (e.g., [Sim11]), it is equivalent in provability to the (non-focused) sequent calculus for intuitionistic logic.

Multi-focused natural deduction

While the multi-focusing sequent calculus closely corresponds to existing focused presentations, its natural deduction presentation in Fig. 2 is new. We took inspiration from the presentation of focused linear logic in natural deduction of [BNS10], in particular the ⇑ and ⇓ notations coming from intercalation calculi.

nat-atom X atomic Γ na , X X nat-inv-sum-l Γ, A C Γ, B C Γ, A + B C nat-inv-prod-r Γ A Γ B Γ A × B nat-inv-arr-r Γ, A B Γ A → B nat-focus Γ na ⇓ Γ A pa ⇑ ? A Γ na , Γ A Γ na A pa nat-end-elim Γ; A na ⇓ A na nat-end-intro A na ⇑ A na nat-elim-arr Γ; A ⇓ B → C B ⇑ B Γ B Γ; A ⇓ C nat-elim-prod Γ; A ⇓ B 1 × B 2 Γ; A ⇓ B i nat-intro-sum A i ⇑ B A 1 + A 2 ⇑ B nat-start-no-intro A ⇑ ? A = = = = = = = = nat-start-intro A p ⇑ B na A p ⇑ ? B na = = = = = = = = = = = nat-start-elim (A i n ) i∈I ⊆ Γ (Γ; A i n ⇓ A i pa ) i∈I Γ ⇓ (A i pa ) i∈I = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =

Figure 2 Multifocused natural deduction for intuitionistic logic

There are three main judgments. Γ A is the unfocused judgment with the invertible rules. Γ; A ⇓ B is the "elimination-focused" judgment, and A ⇑ B is the "introductionfocused" judgment (focused on A). Γ; A ⇓ B means that the assertion B can be produced from the hypothesis A by non-invertible elimination rules; the context Γ is used in any non-focused subgoal. A ⇑ B means that proving the goal A can be reduced, by applying non-invertible introduction rules, to proving the goal B. Those two judgments do not come separately, they are introduced by the focusing rule nat-focus.

In Fig. 2, we used auxiliary rules (nat-start-intro, nat-start-no-intro, nat-start-elim) to present the focusing compactly (this is important when rewriting proofs); those rules can only happen immediately above nat-focus, and can thus be considered definitional syntactic sugar -we used a double bar to reflect this. If we inlined these auxiliary rules, the focusing rule would read (equivalently):

(A i n ) i∈I ⊆ Γ na (Γ na ; A i n ⇓ A i pa ) i∈I (B p ⇑ B na | B = B ) Γ na , (A i pa ) i∈I B Γ na B pa
This rule can only be used when all invertible rules have been performed: the context must be negative or atomic, and the goal positive or atomic. It selects set of foci on the left, the family of strictly negative assumptions (A i n ) i∈I (we consistently use the superscript notation for family indices), and optionally a focus on the right; if the goal is focused it must be strictly positive. All foci must be as long as possible: elimination foci go from a variable down to a positive or atomic A i pa , and the introduction focus goes up until it encounters a negative or atomic B na .

In comparison to the sequent calculus, the positive or atomic formulas (A i pa ) i∈I appearing at the start of the elimination-focus correspond to the formulas released at the end of a multi-focus in a sequent proof; natural deduction, when compared to the sequent calculus, has elimination rules "upside down". Also characteristic of natural deduction is the horizontal parallelism between eliminations and introductions; for example, the following two partial derivations correspond to the same natural deduction:

A pa × B, A pa C na A pa × B, [A pa ] [C na ] A pa × B, [A pa ] [C na + D] A pa × B, [A pa × B] [C na + D] A pa × B C na + D A pa × B, A pa C na A pa × B, [A pa ] [C na ] A pa × B, [A pa × B] [C na ] A pa × B, [A pa × B] [C na + D] A pa × B C na + D A pa × B; A pa × B ⇓ A pa × B A pa × B; A pa × B ⇓ A pa C na ⇑ C na C na + D ⇑ C na A pa × B, A pa C na A pa × B C na + D
On the other hand, we kept the less important invertible rules in sequent style: the sum elimination is a left introduction. Invertible rules being morally "automatically" applied, the sequent-style left introduction, which is directed by the type of its conclusion, is more natural in this context. Ironically, this brings us rather close to the sequent calculus of Krishnaswami [Kri09] which, for presentation purposes, preserved a function-elimination rule in natural deduction style.

Lemma 1. The multi-focused natural deduction system proves exactly the same non-focused judgments as the multi-focused sequent calculus.

Proof. See Appendix C.1.

A preemptive variant of multi-focused natural deduction

preempt-focus Multi-focusing was introduced to express the idea of parallelism between non-invertible rules on several independent foci. A proof has more parallelism than another if two sequential foci of the latter are merged (through rule permutations) in a single multi-focus in the former. A natural question is whether there exists "maximally parallel proofs". To answer it (affirmatively), the original article on multi-focusing ([CMS08]) introduced a rewriting relation that permutes non-invertible phases down in proof derivations, until they cannot go any further without losing provability -neighboring phases can then be merged into a maximally focused proof.

Γ npa ⇓ ∆ pa B p ⇑ ? B na Γ npa , ∆ pa A npa | B na Γ npa A npa | B p preempt-elim Γ npa ⇓ ∆ pa Γ npa , ∆ pa ; A ⇓ A Γ npa ; A ⇓ A
In the process of moving down, a non-invertible phase will traverse invertible phases below. The intermediary states of this reduction sequence may break the invariant that invertible rules must be applied as early as possible; we say that the non-invertible phase preempts (a part of) the invertible phase. As this intermediary state is not a valid proof in off-the-shelf multi-focusing systems, the original article introduced a relaxed variant called a preemptive system, in which the phase-sinking transformation, called preemptive rewriting, can be defined following [CMS08].

We present in Fig. 3 a preemptive variant of multi-focused natural deduction, except for the invertible and focused-introduction rules that are strictly unchanged from the previous multi-focusing rules in Fig. 2. There are two important differences: Preemption of invertible phases. To allow the start of a focusing phase when some invertible rules could still be applied, we lifted the polarity constraints for starting focusing. In the rule preempt-focus, the goal Γ npa A npa may be of any polarity. We use a tautological Γ npa annotation to emphasize this change. Preemption of non-invertible phases. This is expressed by the rule preempt-elim, where an ongoing focus on A is preempted by a complete focus on ∆ pa . Note that stored contexts are not available during the current elimination phase (they are unused in nat-end-elim); they are only available to non-focused phases that appear as subgoals (in the arrow elimination rule). This preserves the central idea that the simultaneous foci of a single focusing rule are independent.

Preemptive rewriting

We can then define in Fig. 4 the rewriting relation on the preemptive calculus, that lets any non-invertible phase move as far as possible down the derivation tree. Maximally multi-focused proofs, which can be characterized on permutation-equivalence classes of multi-focused proofs, correspond to normal forms of this rewriting relation.

A focused phase cannot move below an inference rule if some of the foci depend on this inference rule. Instead of expressing the non-dependency requirement by implicit absence of the foci, we have explicitly canceled out the foci that must be absent to improve readability.

Γ,Z A ⇓ ∆ X X X X B ⇑ B Γ, A, ∆ B Γ, A B Γ A → B → Γ ⇓ ∆ Γ, ∆, A B Γ, ∆ A → B Γ A → B Γ ⇓ ∆ X X X A ⇑ A Γ, ∆ A Γ A Γ B Γ A × B → Γ ⇓ ∆ Γ, ∆ A Γ B Γ, ∆ A × B Γ A × B Γ,Z A ⇓ ∆ C ⇑ ? D Γ, A, ∆ D Γ, A C Γ,Z B ⇓ ∆ C ⇑ ? D Γ, B, ∆ D Γ, B C Γ, ∆ B Γ A ↔ Γ ⇓ ∆, ∆ A ⇑ ? C Γ, ∆, ∆ C Γ A Figure 4
Preemptive rewriting for multifocused natural deduction for intuitionistic logic

In the first rule for example, Γ, @ A ⇓ ∆ means that the A hypothesis must be weakened (not used) in the derivation of Γ ⇓ ∆, orelse it cannot move below the introduction of A.

In this situation, it may be the case that other parts of the multi-focus do not depend on the rule below, and those should not be blocked. To allow rewriting to continue, the last rewrite of our system is bidirectional. It allows to separate the foci of a multi-focus, in particular separate the foci that depend on the rule below from those that do not -and can thus permute again. This corresponds to the first rule of the original preemptive rewriting system [CMS08], which splits a multi-focus in two. We only need to apply this rule when the result can make one more unidirectional rewrite step -this strategy ensures termination.

In the left-to-right direction, this rule relies on the possibility of merging together two elimination-focused derivations, or two optional introduction-focused derivations, with the implicit requirement that at least one of them is empty.

Reinversion

After the preemptive rewriting rules have been applied, the result is not, in general, a valid derivation in the non-preemptive system. Consider for example the following rewriting process:

       ν3 π3 ν2 π2 ν1 π1        → *        ν3 ν2 π3; ν2 π2 ν1 π1        → *    ν2 ν3 π2 π3 ν1 π1    → *      ν2 ν3 π2; ν3 ν1 π3; ν1 π1      → *    ν2 ν3 π2; ν3 ν1 π1 π3   
We are here representing derivations from a high-level point of view, by naming complete sequences of rules of the same polarity. Sequences of positive (non-invertible) are named π n , and sequences of negative (invertible) rules ν m . We use horizontal position to denote parallelism, or dependencies between phases: each dipole (π k , ν k ) is vertically aligned as the invertibles of ν k have been produced by the foci of π k , but we furthermore assume that the second dipole depends on formulas released by the first, while the third dipole is independent.

The third dipole is independent from the others, and its foci in π 3 move downward in the derivation as expected in the preemptive system. After the first step, its negative phase has preempted the invertible phase ν 2 , and it is thus written π 3 ; ν 2 to emphasize that any rule of this sequence will have all the invertible formulas of ν 2 in non-focused positions (positives in the hypotheses, and negatives in the succedent). It can then be merged with the foci of π 2 , in which case it does not see the invertibles of ν 2 anymore. When it moves further down, the invertible formulas in its topmost sequent, those consumed by ν 3 , are present/preempted by all the non-invertible rules of π 2 . It is eventually merged with π 1 .

The normal form of this rewrite sequence could be considered a maximally multi-focused proof, in the sense that the foci happen as soon as possible in the derivation -which was not the case in the initial proof, where π 3 was delayed. However, while the initial proof is a valid proof in the non-preemptive system, the last derivation is not: the invertible formulas produced by π 3 are not consumed as early as possible, but only at the very end of the derivation, and the foci of π 2 therefore happen while there are still invertible rules to be applied.

We introduce a reinversion relation between proofs, written D E, that turns the proof D with possible preemption into a proof E valid in the non-preemptive system, by doing the inversions where they are required, without changing the structure of the negative phases -the foci are exactly the same. In our example, we have:

   ν2 ν3 π2; ν3 ν1 π1 π3       ν2 π2 ν1 ν3 π1 π3   
Definition 2 (Rewriting relation). If D and E are proofs of the non-preemptive system, we write D ⇒ E if there exists a E such that D → * E E.

Reinversion was not discussed directly in the original multi-focusing work [CMS08], but it plays an important role and can be described and understood in several fairly different ways. For lack of space, we only discuss those points of view in Appendix A , and will only formally define reinversion as a relation on the (more concise) proof terms in Section 3.1, Definition 4.

Maximal multi-focusing and canonicity

Now that we have defined the focusing-lowering rewrite (⇒) between non-preemptive proof, we can define the notion of maximal multi-focusing and its meta-theory. It is defined by looking at the width of multi-focus phases in equivalence classes of rule permutations; but it can also be characterized as the normal forms of the (⇒) relation.

For lack of space, we have reserved this development (which is a mere adaptation of the previous work [CMS08]) to Appendix B. The central result is summarized below.

Definition. We say that two proofs D and E are locally equivalent, or iso-polar, written D ≈ loc E, if one can be rewritten into the other using only local positive/positive and negative/negative permutations, preserving their initial sequents.

Definition. We say that two proofs D and E are globally equivalent, or iso-initial, written D glob E, when one can be rewritten into the other using local permutations of any polarity (so when seen as proofs in a non-focused system), preserving their initial sequents.

Corollary (28). Two multi-focused proofs are globally equivalent if and only if they are rewritten by (⇒) in locally equivalent maximal proofs.

3

On the side of proof terms

Preemption and reinversion as term rewriting

Now that we have a notion of maximally multi-focused proofs in natural deduction, we can cross the second bridge between multi-focusing and Lindley's work by moving to a term system. We define in Figure 5 a term syntax for multi-focused derivations in natural deduction.

As the distinction between the preemptive and the non-preemptive systems are mostly about invariants of the focusing rule, the same term calculus is applicable to both. The only syntactic difference is that preemptive terms allow a multi-focusing f [n] to preempt an ambient elimination focus n .

Structural constraints on the multi-focusing system (preemptive or not) guarantee that strong typing invariants are verified. In particular, in a focused term (let x = n in p ? t), the n are typed by the formulas in ∆ at the end of a Γ ⇓ ∆ elimination phase: by our release discipline they have a positive or atomic type, so the let-introduced x are always bound to Proof. Immediate by inspection on both rewriting relations.

t ::= terms | x, y, z variable | λ(x) t lambda | (t, t) pair | δ(x, x.t, x.t) case | f [t] focusing X atomic Γ na , x : X x : X Γ, x : A t : C Γ, x : B u : C Γ, x : A + B δ(x, x.t, x.u) : C Γ t : A Γ u : B Γ (t, u) : A × B Γ, x : A t : B Γ λ(x) t : A → B f [ ] ::= let x = n in p ? multi-focusing p ? ::= optional introduction focus | ∅ no introduction | p introduction focus Γ na ⇓ let x = n : Γ A pa ⇑ ? p ? : A Γ na , Γ t : A Γ na let x = n in p ? t : A pa A ⇑ ? ∅ : A = = = = = = = = = = = A p ⇑ p : B na A p ⇑ ? p : B na = = = = = = = = = = = = = = (x i : A i n ) i∈I ⊆ Γ (Γ; x i : A i n ⇓ n i : A i pa ) i∈I Γ ⇓ let (x i ) i∈I = (n i ) i∈I : (A i pa ) i∈I = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = n ::= negatives | x, y, z variable | π i n pair projection | n p(t) function application | let x = n in n focusing (only in the preemptive calculus) Γ; x : A na ⇓ x : A na Γ; A ⇓ n : B → C B ⇑ p : B Γ t : B Γ; A ⇓ n p(t) : C Γ; A ⇓ n : B 1 × B 2 Γ; A ⇓ π i n : B i i ∈ {1, 2} Γ npa ⇓ let (x i ) i∈I = (n i ) i∈I : ∆ pa Γ npa , ∆ pa ; A ⇓ n : A Γ npa ; A ⇓ let (x i ) i∈I = (n i ) i∈I in n : A p ::= positives | identity | σ i p sum injection A na ⇑ : A na A i ⇑ p : B A 1 + A 2 ⇑ σ i pB i ∈ {1, 2}
The reinversion relation also has a corresponding term-rewriting interpretation. To

λ(y) let x = n in t y / ∈n → let x = n in λ(y) t ((let x = n in t 1 ), t 2 ) → let x = n in (t 1 , t 2 ) (t 1 , (let x = n in t 2 )) → let x = n in (t 1 , t 2 ) δ(y, y 1 . (let x = n in p ? t 1 ), y 2 . (let x = n in p ? t 2 )) y1,y2 / ∈n → let x = n in p ? δ(y, y 1 .t 1 , y 2 .t 2 ) π i (let x = n in n ) → let x = n in π i n (let x = n in n ) t → let x = n in n t n p(let x = n in t) → let x = n in n p(t) let y = (let x = n in n ) in p ? t → let x = n in let y = n in p ? t let x = n in p ? (let ȳ = n in q ? t)
x / ∈ n ↔ let x, ȳ = n, n in (p ? .q ? )t p ? .∅ = p ? ∅.q ? = q ?

.q = q (σ i p).q = σ i (p.q)

Figure 6 Preemptive rewriting on proof terms perform each invertible rule as early as it should be, it suffices to let any invertible rule skip over a non-invertible phase it does not depend on. Depending on the order of the invertible rules after this phase, the invertible rule we want to move may be after a series of invertible rules that cannot be moved.

We "skip" over invertible contexts, we reduce invertible rules happening inside contexts of the form

C ni [C i [ ]]
, where C i [t] is a notation for invertible contexts (defined using invertible frames F i [t]), and C ni [t] for non-invertible contexts. Defining the latter requires describing negative/elimination contexts C neg [t], with holes where a term may appear in a series of elimination-focused terms.

F i [ ] ::= λ(x) | δ(x, x 1 . , x 2 .t) | δ(x, x 1 .t, x 2 . ) | (t, ) | ( , t) C neg [ ] ::= n p( ) | C neg [ ] p(t) | π i C neg [ ] | C ni [C neg [ ]] C i [ ] ::= | F i [C i [ ]] C ni [ ] ::= let x = n in p ? | let x, y = n, C neg [ ] in p ? t Figure 7
Invertible frames and contexts, non-invertible contexts and elimination contexts.

Definition 4. Reinversion can be precisely defined as the transitive congruence closure of the rewrite rules listed in Figure 8. For example, it would make no sense to extrude a λ in argument position in a destructor, or move a sum-elimination δ(x) across the frame that defined the variable x. This blocking relation is defined in Figure 9 -(A | B) in a rule means that the rule holds with either A or B in place of (A | B). It may at first seem surprising that reinversion rules have instances that are the opposite of some of the preemptive rewriting rules -those about pos/neg permutations. But that is precisely one of the purposes of reinversion: after preemptive rewriting rules have been fully applied, we undo those that have gone "too far", in the sense that they let a non-invertible phase preempt a portion of an invertible phase below, but were blocked by dependencies without reaching the next non-invertible phase. This blocked phase does not increase the parallelism of multi-focusing in the proof, but stops the derivation from being valid in the original multi-focusing system, so reinversion undoes its preemption.

C ni [C i [λ(x) t]] Cni[Ci[ ]] ≺λ λ(x) C ni [C i [t]] C ni [C i [(t 1 , t 2 )]] Cni[Ci[ ]] ≺(,) (C ni [C i [t 1 ]], C ni [C i [t 2 ]]) C ni [C i [δ(x, x 1 .t 1 , x 2 .t 2 )]] Cni[Ci[ ]] ≺δ(x) δ(x, x 1 .C ni [C i [t 1 ]], x 2 .C ni [C i [t 2 ]])
c ::= (, ) | λ | δ(x) y ∈ x let x = n in p ? ≺ δ(y) p = ∅ let x = n in p ≺ (, ) | λ C neg [ ] ≺ c let x, y = n, C neg [ ] in p ? t ≺ c (( , t) | (t, ) | λ(x) ) ≺ ((, ) | λ) λ(x) ≺ δ(x) (δ(x, y. , z.t) | δ(x, z.t, y. )) ≺ δ(y) n p( ) ≺ (, ) | λ C neg [ ] ≺ c C neg [ ] p(t) | π i C neg [ ] | C ni [C neg [ ]] ≺ c C ni [ ] ≺ c | C neg [ ] ≺ c C ni [C neg [ ]] ≺ c F i [ ] ≺ c | C i [ ] ≺ c F i [C i [ ]] ≺ c C ni [ ] ≺ c | C i [ ] ≺ c C ni [C i [ ]] ≺ c
Remark, in relation to this situation, that preemptive rewriting cannot be easily defined on equivalence classes of neg/neg permutations (or other presentations of focusing that crush the invertible phase in one not-so-interesting step, such as higher-order focusing), as the order of the invertible rules in a single phase may determine where a non-invertible phase stops its preemption and is blocked in the middle of the invertible phase. Reinversion restores this independence on invertible ordering. This explains why the meta-theory of maximal multi-focusing was conducted in the non-preemptive system, using the relation between proofs that always applies reinversion after preemptive rewriting.

The other interesting case is a non-invertible phase π 0 having traversed a family of non-invertible phases (π i ) i∈I , before merging into some non-invertible phase π 1 . Reinversion will move its negative phase ν 0 , reverting the preemption of the (π i ) on the invertible formulas introduced by π 0 . But the important preemptions that happened, namely the traversal by π 0 of each of the invertible phases (ν i ) i∈I , are not reverted: each ν i is blocked by the π i below and thus cannot be reverted below π 0 . As π 0 traversed both the ν i and the π i , it does not have the corresponding invertible formulas in its context anymore, and is well-positioned even in a non-preemptive proof.

Lemma 5. If t is the proof term of the preemptive derivation D : Γ A, and u is such that t u, then u is a valid (preemptive) proof term for Γ A. Lemma 6. If u is a valid proof term in the preemptive system, and a normal form of the relation ( ), then u is also a valid proof term for the non-preemptive system.

Proof. See Appendix C.4

Theorem 7. If t is a proof term for D and u for E, then D ⇒ E if and only there is a u such that t → * u u, and u is a normal form for ( ).

Multi-focused terms as lambda-terms

There is a natural embedding t of a multi-focused term t into the standard lambdacalculus, generated by the following transformation, where t[x := ū] represents simultaneous substitution:

let x = n in p ? t := p ? ( t [x := ¯ n ]) ∅ (t) := t (t) := t σ i p (t) := σ i p (t)
The substitutions break the invariant that the scrutinee of a sum-elimination construct is always a variable. However, as only negative terms are substituted, sum-elimination scrutinee are always neutrals -embedding of negative terms. In particular, this embedding does not create any β-redex. Proof terms coming from non-preemptive multi-focusing are also always in η-long form, and this is preserved by the embedding; with the restriction present in Lindley's work that only neutral terms (eliminations) are expanded -this avoids issues of commuting conversions. We mean here the weak η-long form, determined by the weak equation (m :

A + B) = weak-η δ(m, x 1 .σ 1 x 1 , x 2 .σ 2 x 2 ).
Lemma 8. If Γ t : A in the preemptive multi-focused system, then Γ t : A in simply-typed lambda-calculus, and t is in β-normal form. If t is valid in the non-preemptive system, then the pure neutral subterms of t are also in weak η-long form.

Proof. See Appendix C.3.

Lindley's rewriting relation

The strong η-equivalence for sums makes lambda-term equivalence a difficult notion. For any term m : A+B and well-typed

context C[ ], it dictates that C[m] ≈ δ(m, x 1 .C[x 1 ], x 2 .C[x 2 ]).
In his article [Lin07], Sam Lindley breaks it down in four simpler equations, including in particular the "weak", non-local η-rule (where F represents a frame, that is a context of term-size exactly 1):

m ≈ δ(m, x 1 .σ 1 x 1 , x 2 .σ 2 x 2 ) (+.η) F [δ(p, x 1 .t 1 , x 2 .t 2 )] ≈ δ(p, x 1 .F [t 1 ], x 2 .F [t 2 ]) (move-case) δ p, x 1 .δ(p, y 1 .t 1 , y 2 .t 2 ), x 2 .δ(p, z 1 .u 1 , z 2 .u 2 ) ≈ δ(p, x 1 .t 1 [y 1 := x 1 ], x 2 .u 2 [z 2 := x 2 ]) (repeated-guard) δ(p, x 1 .t, x 2 .t) x1,x2 / ∈t ≈ t (redundant-guard)
Lindley further refines the move-case equivalence into a less-local hoist-case rule. Writing D for a frame that is either δ(p, x 1 . , x 2 .t) or δ(p, x 1 .t, x 2 . ), D * for an arbitrary (possibly empty) sequence of them, and H any frame that is not of this from, hoist-case is defined as:

H[D * [δ(t, x 1 .t 1 , x 2 .t 2 )]] → δ(t, x 1 .H[D * [t 1 ]], x 2 .H[D * [t 2 ]])
Lindley's equivalence algorithm (Theorem 36, p. 13) proceeds in three steps: rewriting terms in βηγ E -normal forms (using the weak (+.η) on sums), then rewriting them in γ-normal form, and finally using a decidable redundancy-eliminating equivalence relation called ∼. The rewriting relation γ is defined as the closure of repeated-guard, redundant-guard (when read left-to-right) and hoist-case; γ E is a weak restriction of it defined below. The equivalence ∼ is the equivalence closure of the equivalence repeated-guard, redundant-guard, and move-case restricted to D-frames -clauses of a sum elimination.

We discuss redundancy elimination, that is aspects related to repeated-guard and redundant guard, in Section 4, and focus here on explanation of the other rewriting processes (βηγ E and hoist-case) in logical terms. We show that multi-focused terms in (⇒)-normal form embed into βηγ E γ-normal forms. As we ignore redundancy elimination, this is modulo ∼.

The β and η rewriting rules are standard -for sums, this is the weak, local η-relation, and not the strong η-equivalence. As explained in the previous subsection, embeddings of proof terms valid in the non-preemptive system -as are (⇒)-normal forms -are in βη-normal form. The rewriting γ E is defined as the extrusion of a sum-elimination out of an elimination context:

t | π i | δ( , x 1 .t, x 2 .t).
Lemma 9. Terms for valid preemptive multi-focusing derivations are in γ E -normal form.

Proof. This comes from the static structure of valid focused proofs: contexts t and π i may only contain negative terms, which exclude sum eliminations, and variables of sum-elimination scrutinees may only be bound to negative terms, so their embedding cannot be a sum elimination either. This rigid structure of focused proofs is well-known, just as βη-normality or commuting conversions are not the interesting points of Lindley's work. The crux of the correspondence is between the transformation to maximal proofs, computed by (⇒), and his γ-rewriting relation. There is an interesting dichotomy:

Preemptive rewriting, which merges non-invertible phases, is where most of the work happens from a logical point of view. Yet this transformation, on the embeddings of the multi-focused proof terms, corresponds to the identity! Reinversion, which is obvious logically as it only concerns invertible rules which commute easily, corresponds to γ-rewriting on the embeddings.

Of course, preemptive rewriting is in fact crucial for γ-rewriting. It is the one that determines upto where negative terms can move in the derivation, and in particular the scrutinees of sum eliminations. Reinversion would not work without the first preemptive rewriting step, and applying reinversion on a proof term that is not in preemptive-normal form may not give a γ-normal embedding. Note that the proof of the last theorem in this section makes essential use of the confluence of γ-rewriting, one of Lindley's key results.

Lemma 10. If t → u, then t = α u .

Proof. Immediate by inspection of the term-level preemptive-rewriting rules.

Lemma 11. If t u, then t → * γ u .

Proof. See Appendix C.5.

Lemma 12. If u is in (⇒)-normal form, then for some u ≈ loc u, u is in γ-normal form modulo ∼.

Theorem 13 (γ-normal forms are embeddings of maximally-focused proofs). If t → * γ n and n is γ-normal, then there are u ≈ loc u such that t ⇒ u and u ∼ n. In particular, u is maximally multi-focused.

Proof. See Appendix C.5

Redundancy elimination

In the previous section, we have glossed over the fact that Lindley's γ-reduction also simplifies redundant and duplicated sum-eliminations. Those simplifications are not implied by multifocusing -they are not justified by proof theory alone. Our understanding is that they correspond to purity assumptions that are stronger than the natural equational theory of focused proofs. On the other hand, starting from maximally multi-focused forms is essential to being able to define those extra simplifications. We do so in this section, to obtain a system that is completely equivalent to Lindley's.

We simply have to add the following simplifications on proof terms:

redundant-focus let x, y, z = n, n , n in p ? t → s let x, y = n, n in p ? t[z := y] redundant-guard δ(x, x 1 .t, x 2 .t) x1,x2 / ∈t ≈ loc t repeated-case-1 δ(x, x 1 .δ(x, y 1 .u 1 , y 2 .u 2 ), x 2 .t 2 ) ≈ loc δ(x, x 1 .u 1 [y 1 := x 1 ], x 2 .t 2 ) repeated-case-2 δ(x, x 1 .t 1 , x 2 .δ(x, y 1 .u 1 , y 2 .u 2 )) ≈ loc δ(x, x 1 .y 1 , x 2 .u 2 [y 2 := x 2 ])
While those rules are not implied by focusing, they are reasonable in a focused setting, as they respect the phase separation. As the redundancy-elimination rules test for equality of subterms, they have an unpleasant non-atomic aspect (repeated cases only test variables), but this seems unavoidable to handle sum equivalence (Lindley [Lin07], or Balat, Di Cosmo and Fiore [BCF04], have a similar test in their normal form judgments), and have also been used previously in the multi-focusing literature, for other purposes; in Alexis Saurin's PhD thesis [Sau08], an equality test is used to give a convenient ⊗/& permutation rule (p. 231).

One should however remark that they break the property of preserving the initial sequents of proofs (when seen as a multiset), property which was carefully preserved by our previous notions of equivalence. Yet we only apply these simplifications after reduction to maximally multi-focused proofs, they do not interfere with previous canonicity results for maximal multi-focusing. Definition 14. We define the relation t ⇒ s u between proof terms of the (preemptive) multi-focusing calculus as follows, where t 1 is a preemptive normal form, t 2 is a redundant-foci normal form, and u 0 is a ( )-normal form:

t → * t 1 → * s t 2 * u 0 ≈ loc u
Definition 15. We call the u in the target of the (⇒ s ) relation simplified maximal forms.

Having embedded redundancy-elimination in the definition of maximal forms, we can now get strong correspondence results between (⇒ s )-normal and γ-normal forms.

Theorem 16 (Simplified maximal forms are γ-normal). Given a multi-focused term t, there exists some u such that t ⇒ s u, t → * γ u , and u is in γ-normal form. This u is unique modulo local equivalence.

Proof. See Appendix C.6.

Corollary 17. Two multi-focused proof terms are extensionally equivalent if their maximally multi-focused normal forms are locally equivalent (modulo redundancy elimination).

Related and Future work

Maximally multi-focused proofs were previously used to bridge the gap between sequent calculus, as a rather versatile way of defining proof systems, and specialized proof structures designed to minimize redundancy for a fixed logic. The original paper on multi-focusing [CMS08] demonstrated an isomorphism between maximal proofs and proof nets for a subset of linear logic. In recent work [CHM12], maximally multi-focused proof of a sequent calculus for first-order logic have been shown isomorphic to expansion proofs, a compact description of first-order classical proofs.

There are some recognized design choices in the land of equivalence-checking presentation that can now be linked to design choices of focused system. For example, Altenkirch et al. [ADHS01] proposed to make the syntax more canonical with respect to redundancyelimination by using a n-ary sum elimination construct, while Lindley prefers to quotient over local reorderings of unary sum-eliminations. This sounds similar to the choice between higher-order focusing ( [Zei09]), where all invertible rules are applied at once, or quotienting of concrete proofs by neg/neg permutations as used here.

When we started this work, we planned to also study the proof-term presentation of preemptive rewriting, in a term language for sequent calculus. We have been collaborating with Guillaume Munch-Maccagnoni to study the normal forms of an intuitionistic restriction of System L, with sums. In this untyped calculus, syntactic phases appear that closely resemble a focusing discipline, and equivalence relations can be defined in a more uniform way, thanks to the symmetric status of the (non)-invertible rules that "change the type of the result" (terms, values) and those that only manipulate the environments (co-terms, stacks).

Conclusion

We propose a multi-focused calculus for intuitionistic logic in natural deduction, and establish the canonicity of maximally multi-focused proofs by transposing the preemptive rewriting technique [CMS08] in our intuitionistic, natural deduction setting. By studying the computational effect of preemptive rewriting on proof terms, we demonstrate the close correspondence with the rewriting on lambda-terms with sums proposed by Lindley [Lin07] to compute extensional equivalence. Adding a notion of redundancy elimination to our multi-focused system makes preemptive rewriting precisely equivalent to Lindley's γ-rules. In particular, the resulting canonical forms, simplified maximal proofs, capture extensional equality.

A The many faces of reinversion Reinversion as a rewriting relation

We can define reinversion by permuting some invertible phases downward in the derivation. We know this is always possible as neg/neg and neg/pos permutations, those where an invertible rule is originally at the top, always preserve provability. Invertibility properties are clearly explained in Alexis Saurin's thesis. We will show (Corollary 28) that global equivalence, that is equivalence modulo arbitrary rule permutations, can be decided by complete preemptive rewriting followed by reinversion. This is a sequentialization of permutations (after quotienting on "local" pos/pos and neg/neg permutations): instead of an arbitrary sequence of permutations, we can just perform a series of pos/neg permutations (preemptive rewriting), followed by a series of neg/pos permutations (reinversion).

While rewriting is the simplest way to define reinversion, we will refrain from defining it explicitly now as it is quite verbose, and less interesting than the preemptive rewriting rules. The rewrite steps will be written in full in Section 3.1 on proof terms for multi-focusing, where they can be more concisely expressed.

Reinversion as partial evaluation

Instead of moving some invertible phases downwards in the derivation, we could traverse it from the root to the leaves. Each time we encounter a positive phase π; ν that preempts some invertible formulas, we could change it to first perform the necessary invertible phase, then π. We can do that without looking at ν, the actual positive phase that was preempted, and is above in the derivation, as invertibility guarantees that any application order will be equivalent -this is thus fairly different from seeing reinversion as a rewriting relation, although it is equivalent modulo permutation of invertible rules.

In each leaf of the invertible phase, we can then add the negative phase π and continue traversing the original derivation. When we encounter the original phase ν, we should simplify it, according to the branch we are in. For example, if one of the invertible rules was an elimination of A + B, this elimination has been reenacted below π; we are either in the A or the B branch and can remove the sum-elimination accordingly.

It is very easy to define this transformation formally by relying on a cut-elimination result. Consider the following derivation, preempting the non-invertible phase π over the invertible hypothesis A + B:

S π; (A + B) Γ n , A + B C
Assuming the admissibility of a cut rule, we can transform it into:

cut . . . A A+B S π; (A+B) Γ n , A+B C Γ n , A C cut . . . B A+B S π; (A+B) Γ n , A+B C Γ n , B C Γ n , A+B C
More generally, for any proof S against a positive context Σ p , we can first perform an identity-expansion of Σ p and, at each leaf, cut against S. The cut-elimination process then removes any invertible rules against Σ in S. If a negative is the succedent, we can similarly η-expand then cut.

Reinversion corresponds to performing that transformation, on all invertible formulas of the sequents before any multi-focusing rule of the input derivation.

Reinversion as completeness of focusing

In Alexis Saurin's PhD thesis [Sau08], the reinversion operation is somewhat hidden in the proof that two multi-focusing phases can merged by moving non-invertible phases downward (Theorem 10.16, p. 234): it simply mentions that reconstructing a valid multifocused proof is exactly the same technique as the one used to establish the completeness of (single)-focusing in the first place.

In the present work, we are interested in the computational meaning of reinversion, to be able to see where it fits in Lindley's algorithm. We therefore present it as an explicit computation, instead of the implicit application of a proof.

B Maximal multi-focusing and canonicity

Definition 18. We say that two proofs D and E are locally equivalent, or iso-polar, written D ≈ loc E, if one can be rewritten into the other using only local positive/positive and negative/negative permutations, preserving their initial sequents.

Definition 19. We say that two proofs D and E are globally equivalent, or iso-initial, written D glob E, when one can be rewritten into the other using local permutations of any polarity (so when seen as proofs in a non-focused system), preserving their initial sequents.

Definition 20. We define roots(D), where D is a derivation in the non-preemptive multifocusing calculus, as the set of formulas over focus in its lowest multi-focusing rule, or ∅ if it has none. Proof. The proof is essentially identical to the original one [CMS08]. In each of the preemptive rewrite rules, a focusing rule is brought closer to the root of the derivation, and the rest of the structure is preserved.

For any subderivation D of D, there is a corresponding subderivation E of E with D ⇒ E -even if no rewrite happened in this subderivation, we take E = D . By monotonicity we have roots(D ) ⊆ roots(E ). By soundness we have D glob E and, by maximality, roots(D ) ⊇ roots(E ). So we have roots(D ) = roots(E ): the multi-focusing rules in D and E are equivalent modulo local permutations. As the rest of the rules also are, we have D ≈ loc E.

To our knowledge, the following lemma was not part of previous characterizations of maximal proofs.

Lemma 24 (Normal forms are maximal). If D is such that D ≈ loc E whenever D ⇒ E, then D is maximal.

Proof. By contraposition, let us assume that D is not maximal and rewrite it into some E such that D ≈ loc E.

If D is not maximal, there is a subderivation D of it and a counter-example E such that D glob E but roots(E ) roots(D ). We call interesting the foci that are in roots(E ) but not in roots(D ) -there is at least one. Given that those two subproofs are globally equivalent, they can still be found somewhere in D , just not in the first multi-focusing rule; they are in another, separated by a non-empty sequence of invertible rules -as those are proofs in the non-preemptive system.

We claim that these interesting foci could be moved down in D -along with their complete sequences of non-invertible rules. A focus can only be moved down if it does not depend on the rules below, or if they can themselves be moved down. But we know that they do not depend on any other focus of D , as they are present in the very first multi-focusing rule of E and global rule permutations do preserve dependencies. We can therefore move them to the root of D .

This gives a new sub-proof, D , that is globally equivalent to E and D , but not locally equivalent to D : we permuted non-invertible rules below invertible rules. We conclude by defining E as D[D /D ], or D where its subproof D is replaced by D . We have D ⇒ D , hence D ⇒ E, but D ≈ loc E.

These two lemmas provide a computable characterization of maximal proofs: they are the normal forms of the preemptive rewriting relation.

Theorem 25 (Characterization of maximality). Maximal proofs are exactly the normal form, upto local equivalence, of the rewriting relation.

We can also prove that they are unique modulo global equivalence.

Lemma 26 (Completeness of preemptive rewriting (right decomposition)). If D glob E and E is maximal, then D ⇒ E.

Proof. As in the original paper [CMS08]. We proceed by case analysis on rule permutations that send a focus down. For each, we can verify that it is a valid preemptive rewriting.

C Additional proofs

C.1 Equivalence of sequent-calculus and natural-deduction multifocused calculi

Proof of Lemma 1. Our proof is similar in spirit to the usual proofs of equivalence between sequent calculus and natural deduction: reversing a sequence of left-focusing rules in sequent calculus upside-down gives a sequence of elimination-focused rules in natural deductionand conversely.

For an example, consider the following proof:

(X × Y ) × Z, X X (X × Y ) × Z, [X] X (X × Y ) × Z, [X × Y ] X (X × Y ) × Z, [(X × Y ) × Z] X (X × Y ) × Z X
It gets reversed into the corresponding natural deduction derivation:

(X × Y ) × Z ⇓ (X × Y ) × Z (X × Y ) × Z ⇓ (X × Y ) (X × Y ) × Z ⇓ X (X × Y ) × Z, X X (X × Y ) × Z X
We show how to map each fragment of a derivation starting with a focusing rule and ending with release rules -in fact exactly one release rule -from one system to another. This is sufficient, as we can then rewrite whole derivations by structural induction from the leaves to the root.

Let us now consider the general case of a focused sequence S surrounded by a multifocusing and a release rule

π Γ na , ∆ pa B pa | C na Γ na , [∆ pa ] B pa | [C na ] S Γ na , [∆ n ] B pa | [C p ] Γ na , ∆ n B pa | C p
The contexts ∆ n and ∆ pa are multisets of the same cardinality (as can be checked by a direct induction on the non-invertible left-introduction rules); let I be a family of indices over those multisets, such that ∆ n is some family (A i n ) i∈I and ∆ pa is (A i pa ) i∈I . We rewrite it into the following derivation fragment in multi-focused natural deduction:

∀i ∈ I, Γ na ; A i n ⇓ A i n elim(S, A i n ) Γ na ; A i n ⇓ A i pa B na ⇑ B na intro(S, B na ) B p ⇑ ? B na π Γ na , ∆ pa A p | B na Γ na , ∆ n A p | B p
Where intro(S, B) and elim(S, A i∈I ) are sequences of focusing rules defined by induction on S:

S Γ, [∆ ] [Bi] Γ, [∆ ] [B1 + B2] → intro(S, B ) Bi ⇑ B B1 + B2 ⇑ B , i ∈ I → elim(S, A i ) S Γ, [∆ , C k ] A | [B] Γ, [∆ , (C1 × C2) i ] A | [B] k∈{1,2} → intro(S, B ) ,          i → ∆; A i ⇓ C1 × C2 ∆; A i ⇓ C k elim(S, A i ) j = i → elim(S, A j ) S Γ, [∆ , D] A | [B] π Γ C na Γ [C na ] Sarg Γ [C] Γ, [∆ , (C → D) i ] A | [B] → intro(S, B ),                    i → Γ; A i ⇓ C → D C ⇑ C intro(Sarg, C na ) C ⇑ C na π Γ C na Γ; A i ⇓ D elim(S, A i ) j = i → elim(S, A j ) ∅ → (∅ , ∅)
Note that applying an inference rule on top of elim(S, A i ) is well-defined because elimination-focused rules always have exactly one elimination-focused premise, which we will call its top judgment.

Remark that the mapping we have defined is bijective on the top and bottom judgments of the focused derivation fragments -it preserves provability back and forth -but not on the derivation themselves. Indeed, several distinct focusing fragments of the sequent calculus may map to the same natural deduction fragment, if they only differ in the ordering of left-and right-introduction rules. We recover the well-known fact that natural deduction (and lambda-calculus as its term language) has less bureaucracy than sequent calculus. The sequent calculus allows for insignificant ordering that must be eliminated by quotienting over pos/pos permutations, or fixing a forced order; whereas the syntax of natural deduction exhibits a spatial parallelism between the introduction and elimination rules of a focusing sequence that structurally removes (some of the) redundancy.

C.2 Soundness of reinversion

Proof of Lemma 5. We will list here the derivation-level transformations that correspond to reinversion rewriting. We express them as a judgment Γ A F , where F is a invertible multi-hole context (λ(x) , ( , ) or δ(x, x 1 . , x 2 . )) that is allowed to permute below a derivation for Γ A. The derivations for this judgment correspond to the (context, constructor) pairs that are absent from the blocking relation ≺.

Γ A → B λ Γ A × B (, ) Γ, x : A + B C δ(x) Γ, x : A + B C δ(x) Γ, x : A + B D Γ, x : A + B C × D δ(x) Γ, x : A + B C Γ, x : A + B D δ(x) Γ, x : A + B C × D δ(x) Γ, x : A + B, Z x :C D δ(x) Γ, x : A + B C → D δ(x) Γ, A c Γ, B c Γ, A + B c c ∈ {(, ), λ} Γ, x : A + B, Z x :C E δ(x) Γ, x : A + B, D E Γ, x : A + B E δ(x) Γ, x : A + B, C E Γ, x : A + B, Z x :D E δ(x) Γ, x : A + B E δ(x) Γ ⇓ ∆ X X X X A ⇑ A Γ, ∆ A c
η-long normal form: each subterm with a non-atomic type starts with the constructor for its head type constructor (η-expansion is already done), or is inside a destructor context for this constructor, and η-expansion would create a β-redex, or is case split δ(x, . . . ), that is not a pure neutral term. Note that in the case of sums, this only captures the weak η-expansion, not the general one, because this restriction only imposes adding "destructors" (δ(x)) immediately above non-constructor uses, instead of above an arbitrary context.

We will reason by case analysis on the several possible type constructors.

Arrows β-short

The only possible occurrence of applications is in neutrals of the form n p(t), where n cannot be a λ-abstraction.

η-long

Terms of type A → B can be produced by the judgment Γ t : A → B, or the judgment Γ A ⇓ n : B → C.

A term of the form Γ t : A → B may either start with a right-introduction (t = λxt for some t ), in which case it is already η-expanded, or a sum elimination (t = δ(x, . . . )), in which case its embedding is not a pure neutral term as we assumed. Note that the restriction of the axiom rule to atomic types is crucial here -otherwise Γ, x : A → B x : A → B could be a non-η-long proof.

In the second case Γ A ⇓ n : B → C, we know that this subterm must itself be included in an inference of the form

Γ; A ⇓ n : B → C B ⇑ p : B Γ t : B Γ; A ⇓ n p(t) : C
Indeed, B → C is a negative type so it cannot be at the bottom of the focused elimination phase: the rule nat-start-elim only accepts judgments of restricted polarity Γ; A n ⇓ A pa . This means that n : B → C appears in applied position, and η-expanding it would create a β-redex.

Remark that in the preemptive calculus, the rule below may also be a focusing let x = n in n, but this gets substituted away by the embedding into λ-calculus let x = n in n .

Products β-short

The only possible occurence of projections is in neutrals of the form π i n, where n cannot be a product.

η-long

Terms of type A × B can be produced by the judgment Γ

t : A × B, or the judgment Γ A ⇓ n : B 1 × B 2 .
A term of the form Γ t : A × B may either start with a right-introduction (t = (t , u ) for some t , u ), in which case it is already η-expanded, or a sum elimination (t = δ(x, . . . )), in which case its embedding is not a pure neutral term as we assumed. Note that the restriction of the axiom rule to atomic types is crucial here -otherwise Γ, x : A × B x : A × B coud be a non-η-long proof.

In the second case Γ A ⇓ n : B 1 × B 2 , we know that this subterm must itself be included in an inference of the form

Γ; A ⇓ n : B 1 × B 2 Γ; A ⇓ π i n : B i
Indeed, B × C is a negative type so it cannot be at the bottom of the focused elimination phase: the rule nat-start-elim only accepts judgments of restricted polarity Γ; A n ⇓ A pa . This means that n : B × C appears in projected position, and η-expanding it would create a β-redex.

Sums β-short

The destructor for sums only appears applied to variables: δ(x, x.t, x.u). We could have a β-redex if one of the substitutions provoked by embedding a focused term into the λ-calculus substituted a term of head σ i t for x. But this cannot happen, as only elimination neutral terms of the form Γ; A ⇓ n : A are substituted, and those cannot start with a term injection.

η-long

Conversely, whenever we have a subderivation Γ; A ⇓ n : B 1 + B 2 , it is a the end of an elimination phase (no elimination rules have positive premises) and thus appear directly as a let-bound term let x = n in t.

This binder x is of positive type and it is thus necessarily eliminated in the following invertible phase. This is because in our system, all focused derivations have at least one invertible premise, and they necessarily destruct all sums in context. Note that this is not true in the preemptive system where invertible phases may stop earlier -this is where our non-preemptive assumption comes into action. The variable x thus appears (and only once) in a subterm of the form δ (x, x.t, x.u).

This means that such n only appear in the embedded (substituted) forms t in the form of case-splits δ ( n , x. t , x. u ). It is not η-expansible without creating a β-redex.

C.4 Preempted proofs that are normal for reinversion are also valid non-preempted proof

Proof of Lemma 6. By contraposition, we show that if u does use preemption, that is if a multi-focusing happens while an invertible rule is applicable, then ( ) can rewrite u into a different proof.

A preemptive focusing is of the form

Γ na , Σ p ⇓ ∆ p A ⇑ ? B Γ na , Σ p , ∆ p B Γ na , Σ p A
where either Σ is non-empty, or A is negative (and A = B). Supposing Σ is non-empty, there is a non-atomic positive formula in the context of our derivation. It cannot be used by the axiom rule, which requires the variable type to be atomic, nor in the variable rule of the elimination-focused judgment which only uses negative formulas. If it is used, it is in an invertible sum-elimination judgment higher in the derivation. This judgment either happens in the invertible phase directly above the current focusing, or later, after some other focusing higher in the derivation. In any case, the positive formula is in the context of this last focusing, and can be reinverted to be sum-eliminated just below it, which produces a distinct reinverted proof.

(If the positive hypothesis is never used, we could claim that weakening the derivation to remove it gets us closer to a valid preemptive proof. Alternatively, we have a negativity restriction on the context of the axiom rule, which enforces that it must be eliminated somewhere in any complete proof. We prefer to avoid discussing this axiom rules and potential atomic polarity assignment, as those concerns are orthogonal to the present work; we insist that this "negative axiom context" technique is not crucial to the present proof.)

Similarly, if the succedent of the focusing rule is a non-atomic negative formula, then it is either introduced in the following invertible phase, or one just after some focusing rule of the same succedent -in any case, it must be introduced before the axiom rules which requires an atomic succedent. We can move that inversion rule below the closest focusing, which produces a distinct reinverted proof.

C.5 Lindley's rewriting relation

Proof of Lemma 11. Our reinversion contexts C ni [C i [ ]] were naturally motivated by the translation from one logical system to another -from preemptive to non-preemptive proofs; yet they closely correspond to Lindley's notion of hoisting contexts H[D * ]. However, while we permute all the syntactic construction corresponding to invertible rules, in particular lambdas and pairs, the hoist-case rule only moves sum-eliminations. We can however show that our other permutations are invisible on the embedded term:

C ni [C i [λ(x) t]] λ(x) C ni [C i [t]] =⇒ C ni [C i [λ(x) t]] = λ(x) C ni [C i [t]] C ni [C i [(t 1 , t 2 )]] (C ni [C i [t 1 ]], C ni [C i [t 2 ]]) =⇒ C ni [C i [(t 1 , t 2 )]] = (C ni [C i [t 1 ]], C ni [C i [t 2 ]])
This crucially relies on the blocking relation: we can immediately verify that for any

C ni [C i [ ]] such that C ni [C i [λ(x) t]] = λ(x) C ni [C i [t]] , we have C ni [C i [ ]]
≺ λ, and therefore the ( )-reduction hypothesis cannot hold -and similarly for pairs.

In the last case where we hoist sum-eliminations, we still have to be careful because of the non-locality of the embedding t : negative terms at the very root of the focused proofs may find themselves substituted very far inside the lambda-term. The interesting case is the following rewrite, where E[ ] is an arbitrary term context with x / ∈ E: The sum-elimination has been extruded out of the whole context E, which may be arbitrarily large and use arbitrary term constructors. This is allowed by → γ . Furthermore, if E is not linear (the hole occurs several times in E), what is a single sum-elimination extrusion in the multi-focused term may in fact translate into several sumeliminations (on the same scrutinee) in its embedding. Just applying hoist-case as many times does not produce the desired reduced term, we also have to use repeated-guard.

let x = δ(y,

Figure 3

 3 Figure 3 Preemptive rules for intuitionistic multifocused natural deduction

Figure 5

 5 Figure 5 Preemptive term calculus

Figure 8

 8 Figure 8 Reinversion rewrite rules

Figure 9

 9 Figure 9 Reinversion blocking relation

Definition 21 .

 21 A derivation D is maximally multi-focused, or maximal, if, for any subderivation D of D, for any proof E glob D we have roots(E ) ⊆ roots(D ). Lemma 22 (Soundness and monotonicity of preemptive rewriting). If D ⇒ E then D glob E and roots(D) ⊇ roots(E).

Proof.

  Immediate, by inspection of each rewrite rule. Lemma 23 (Maximal proofs are normal forms (left decomposition)). If D is maximal and D ⇒ E, then D ≈ loc E.

  Theorem 27(Canonicity). If two maximally multi-focused proofs are globally equivalent, they are in fact locally equivalent. As in the original paper [CMS08]: if D glob E are both maximal, then D ⇒ E by completeness (Lemma 26), but the maximal proof D is a normal form (Lemma 23) so D ≈ loc E. Two multi-focused proofs are globally equivalent if and only if they are rewritten by (⇒) in locally equivalent maximal proofs.

	Proof. Corollary 28.

  y 1 .t 1 , y 2 .t 2 ) in E[x] δ(y, y 1 .let x = t 1 in E[x], y 2 .let x = t 2 in E[x])While this rewrite is very local in nature, the corresponding embedding is not:E [δ(y, y 1 . t 1 , y 2 . t 2 )] → * γ δ(y, y 1 . E[t 1 ] , y 2 . E[t 2 ] )

Γ, A + B C → Γ ⇓ ∆ C ⇑ ? D Γ, A, ∆ D Γ, B, ∆ D Γ, A + B, ∆ D Γ, A + B C, D Γ ⇓ Γ Γ, Γ ; A ⇓ B1 × B2 Γ; A ⇓ B1 × B2 Γ, Γ ; A ⇓ Bi → Γ ⇓ Γ Γ, Γ ; A ⇓ B1 × B2 Γ, Γ ; A ⇓ Bi Γ; A ⇓ Bi Γ ⇓ Γ Γ, Γ ; A ⇓ B → C Γ; A ⇓ B → C B ⇑ B Γ B Γ; A ⇓ C → Γ ⇓ Γ Γ, Γ ; A ⇓ B → C B ⇑ B Γ B Γ, Γ ⇓ B → C Γ; A ⇓ C Γ; A ⇓ B → C B ⇑ B na Γ ⇓ Γ Γ, Γ B na Γ B na Γ; A ⇓ C → Γ ⇓ Γ Γ; A ⇓ B → C B ⇑ B na Γ, Γ B na Γ, Γ ; A ⇓ C Γ; A ⇓ C Γ ⇓ Γ An ∈ Γ Γ ⇓ ∆ Γ, ∆; An ⇓ A Γ; An ⇓ A Γ ⇓ Γ , A = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = B ⇑ ? B Γ, Γ , A B Γ B → Γ ⇓ ∆ Γ ⇓ Γ An ∈ Γ Γ, ∆; An ⇓ A Γ, ∆ ⇓ Γ , A = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = B ⇑ ? B Γ, Γ , A B Γ, ∆ B Γ B Γ ⇓ ∆ A ⇑ ? B Γ ⇓ ∆ B ⇑ ? C Γ, ∆, ∆ C

Proof. See Appendix C.2.

Proof. See Appendix C.5

Γ A c c ∈ {(, ), λ} Γ, x : A + B ⇓ ȳ : ∆ X X X x ∈ ȳ C ⇑ ? D Γ, x : A + B, ∆ D δ(x) Γ, x : A + B C δ(x) Γ ⇓ ∆ c A ⇑ ? B Γ, ∆ B Γ A c Γ; Γ ⇓ ∆, C 1 × C 2 δ(x) Γ; Γ ⇓ ∆, C i δ(x) Γ, Γ C Γ; Γ ⇓ ∆, C → D δ(x) Γ; Γ ⇓ ∆, D δ(x) ΓΓ C δ(x) Γ; Γ ⇓ ∆, C → D Γ; Γ ⇓ ∆, D δ(x) Γ; Γ ⇓ ∆ δ(x) Γ; Γ , ∆ ⇓ ∆ Γ; Γ ⇓ ∆ δ(x) Γ; Γ ⇓ ∆ Γ; Γ , ȳ : ∆ ⇓ ∆ δ(x) X X X x ∈ ȳ Γ; Γ ⇓ ∆ δ(x)

Acknowledgements

The author thanks his advisor, Didier Rémy for the freedom of making an overly long detour through the proof search literature; Alexis Saurin for his advice, and Pierre-Évariste Dagand, Sam Lindley, and anonymous reviewers for their helpful comments.

This shows preservation of preemptive well-typing as one then simply has to check that each inference rule Γ A F Γ A F verifies that if applying the rule corresponding to the constructor F is a correct way to start a proof of Γ A , then it is also a correct way to start a proof of Γ A.

C.3 beta-short eta-long normal forms of embeddings

Lemma 8. The (unsurprising) typing rules that connect the term syntax with the preemptive calculus for multi-focused natural deduction are given explicit in Figure 5.

Assuming Γ t : A in the preemptive multi-focused system, we prove that t has no constructor inside a matching destructor: it is in β-normal form.

Assuming that it in fact belongs to the non-preemptive system (or to the non-preemptive restriction of the preemptive system), we will prove that its pure neutral subterms are also in Proof of Lemma 12. Even if we have u → γ m for some m, it is impossible that a case elimination of u could be hoisted over the constructor of a non-invertible rule: that would amount to permuting an invertible rule below a non-invertible phase, which would allow to make a step of ( )-reduction from u -assuming that the preemptive rewrites have been fully applied, which is the case here.

Any step of reduction from u then corresponds to permuting a sum-elimination over a lambda or a pair constructor inside an invertible phase. We can apply those permutations fully, and get a u ≈ loc u such that u is in γ-normal form.

Theorem 13. Simply using ( ) on t is not enough, as a sum-elimination may then be blocked by where the focus on its scrutinee happens in t, while → γ would still be able to move the elimination and its scrutinee below in the proof. We have to first rewrite t into t , a normal form for preemptive rewriting, and then apply reinversion completely on t to get u. We have t = t from Lemma 10, and t → * γ u from Lemma 11. Applying Lemma 12 gives us a u ≈ loc u such that u is a γ-normal form modulo ∼. The term n is also γ-normal, and both can be reached from t . Lindley proved confluence of γ-rewriting modulo ∼ (Proposition 28, p. 11), and we therefore have u ∼ n as desired.

C.6 Simplified maximal forms are γ-normal

Theorem 16. We have already shown that (⇒)-normal forms are γ-normal form modulo redundancy elimination and hoisting of δ over λ. A (⇒ s )-normal form is a (⇒)-normal form where repeated-guard and redundant-guard have been eliminated. Furthermore, in the ≈ loc -equivalence class of proofs u such that t ⇒ s u, we can pick the one in which invertible phases always have all sum-eliminations before any lambda or pair constructor. By construction, u is then a γ-normal form.

Note that it is not completely obvious, a priori, that (⇒ s )-normal forms always embed into γ-normal form, and this crucially relies on the redundant-focus rule. Indeed, consider for example the term let y 1 , y 2 = f x, f x in δ(z, z 1 .y 1 , z 2 .y 2 ). While it is in redundantguard-normal form, its embedding δ(z, z 1 .f x, z 2 .f x) is not. The source of the problem is that redundancy rules rely on term equality, and we may have t = u but t = u .

We can prove however that maximal proofs that are redundant-focus-normal forms are normal for the repeated-guard or redundant-guard only if their embedding is as well. It suffices to prove that if t, u have no redundant cases, then t = u implies t = u. Consider for example terms of the form C[π 1 x], C[π 2 y], where C is a common context -the following proof generalizes to all other cases. If C[π 1 x] = C[π 2 y] , there is a substitution σ such that x[σ] = y[σ], which means that either x = y or they have been substituted terms of equal embedding: σ is of the form [x := n 1 , y := n 2 , . . . ] with n 1 = n 2 . Inductively (the chain of nested substitutions is finite), we can assume that n 1 = n 2 . As our terms are maximally preempted, the definitions let x = n 1 in and let y = n 2 in therefore happen in the same non-invertible phase (n 1 and n 2 being equal, they have the same dependencies), and can be merged by the redundant-focus rule.


Sahar Kallel
email: sahar.kallel@lirmm.fr

Chouki Tibermacine
email: chouki.tibermacine@lirmm.fr

Bastien Tramoni
email: bastien.tramoni@lirmm.fr

Christophe Dony
email: dony@lirmm.fr

Ahmed Hadj Kacem
email: ahmed.hadjkacem@fsegs.rnu.tn

Ahmed Hadj

Kacem Redcad

Automatic Translation of OCL Meta-Level Constraints into Java Meta-programs

Keywords: Software Architecture, Architecture Constraint, Object Constraint Language, Java Reflect

In order to make explicit and tangible their design choices, software developers integrate, in their applications' models, constraints that their models and their implemetations should satisfy. Various environments enable constraint checking during the modeling stage, but in most cases they do not generate code that would enable the checking of these constraints during the implementation stage. It turns out that this is possible in a number of cases. Environments that provide this functionality only offer it for functional constraints (related to the states of objects in applications) and not for architectural ones (related to the structure of applications). Considering this limitation, we describe in this paper a system that generates metaprograms starting from architecture constraints, written in OCL at the metamodel level, and associated to a specific UML model of an application. These metaprograms enable the checking of these constraints at runtime.

Introduction

Software architecture description is one of the main building blocks of an application's design [START_REF] Bass | BCEL: The byte code engineering library[END_REF]. It gives us an overview of the application organization that helps us to reason about certain properties, such as quality attributes. In this context, architecture description languages have been created to specify and verify such application architectures without worrying, at first, about the implementation of their functionality. The verification can be especially based on constraints that those languages associate to architecture descriptions. These constraints can be classified into two categories: functional and architectural.

Functional constraints check the state of the architecture's objects. For example, if we consider a UML model (an architecture description) containing a class Employee (a component in that architecture) which has an integer attribute age, a functional constraint presenting an invariant in this class could impose that the values of this attribute (slot of an object of that class) must be included in the interval for all instances of this class. On the other side, architecture constraints analyze the structure of the application, and not objects states. For example, they define invariants (boolean conditions) imposed by the choice of a particular architectural style or pattern, like the layered architecture style [START_REF] Shaw | Software Architecture: Perspectives on an Emerging Discipline[END_REF]. All these constraints can be specified at design stage through a constraint language like the "Object Constraint Language" (OCL) [START_REF]OMG: Object constraint language, version 2[END_REF], the OMG standard.

In the literature and practice of software engineering there exists a large number of architecture patterns [START_REF] Zdun | A catalog of architectural primitives for modeling architectural patterns[END_REF][START_REF] Gamma | Design patterns: Elements of Reusable Object-Oriented Software[END_REF][START_REF] Erl | SOA design patterns[END_REF] whose architecture constraints have been formalized. But unfortunately, currently architecture constraints can be checked only at design time on design artifacts; they are ignored in the implementation stage. Therefore, a part of the knowledge and the expertise in the implementation of a software project "evaporates". To guarantee that architecture pattern source code will not undergo changes during evolution in the implementation artifacts or at runtime, we need to find a way to check the associated architecture constraints at the implementation stage knowing that with OCL language (for example), we can not check the architecture constraints at this stage. We can opt to rewrite them entirely with languages used by the developers at that development stage. And this task of rewriting all these constraints is tedious, time consuming and error prone. Constraints on the two stages of development (design and implementation) are syntactically different but they are semantically equivalent (conditions on architecture descriptions that are present in the two stages). So why not generate the ones from the others, like code can be generated from UML models? Moreover, most of existing tools for model-to-text (code) generation do not consider the generation of code for constraints associated to models. For those which exist [START_REF]Eclipse ocl[END_REF][START_REF]Octopus: Ocl tool for precise uml specifications[END_REF][START_REF] Demuth | The dresden ocl toolkit and its role in information systems development[END_REF], they only translate functional constraints, and not architectural ones.

Considering these limitations, we propose a multi-steps process for translating OCL architecture constraints into Java code. The obtained Java code uses the introspection mechanism provided by the programming language (Java Reflect) to analyze the structure of the application. This choice is motivated by our willingness to use a standard mechanism without resorting to external libraries. Reflection (introspection) enables language users to analyze architectures and to examine the structure of their classes at runtime. In our work, the generated code is considered as a "metaprogram" since it uses the introspection mechanism of the programming language for implementing an architecture constraint.

The remaining of this paper is organized as follows. In the following section, we illustrate the input and the output of the proposed process to better understand the context of our work. These will serve as running examples throughout the paper. In Section 3, we present our general approach indicating the steps for generating constraints into Java metaprograms. Sections 4, 5 and 6 describe these steps in detail. Before concluding and presenting some perspectives, we discuss the related work in Section 7. To introduce the context of our work, we present an example of an architecture constraint enabling the checking of the "MVC (Model-View-Controller) pattern" [START_REF] Reenskaug | Thing-model-view editor an example from a planning system[END_REF]. We assume that we have three stereotypes, allowing us to annotate the classes in an application which represent the view (View), the model (Model) and the controller (Controller). This constraint states that the classes stereotyped Model must not declare dependencies with the classes stereotyped View. This makes it possible, among other things, to have several views for the same model, and thus to uncouple these classes that play different roles in the pattern. In addition, the classes stereotyped Model must not have dependencies with the classes stereotyped Controller. This makes it possible to have several possible controllers for the model.

Illustrative Example

Using OCL and the UML metamodel (Fig. 1), we obtain the following constraint: The first line in the Listing 1 declares the context of the constraint. It indicates that the constraint applies to each class of the application ; the meta-class Class is then the starting point for all navigations in the rest of the constraint. Lines 2 to 3 serve to collect the set of classes representing the model (having the stereotype Model) by using the navigation package.profileApplication.appliedProfile. owned-Stereotype. UML metamodel allows us to get an applied stereotype only starting from the package that contains the modeling element (a class, in our case) and not from the element itself. The problem is resolved in some tools like RSA-IBM where the UML metamodel has been extended with an operation named getAppliedStereotypes(), which is inherited by the Class metaclass. In Line 5 we obtain the set of classes which have a direct dependency with the context of the constraint. The remaining of the Listing allows to iterate over the set of class instances and test if it contains classes stereotyped with View or Controller.

c
Our goal is to obtain automatically a metaprogram generated from an OCL/UML architecture constraint. The result would be expressed in Java as follows: The method invariant(...) in Listing 2 accepts as a parameter an object of type Class, representing each of the classes of the application (the classes which compose the application business domain. This excludes classes of the libraries used by the application). Unfortunately, we cannot start navigation from the Package object representing the application package, because in java.reflect, this object does not enable to obtain references to the classes which are declared inside it. The Package object relates to a simple object containing information about the package(e.g. its name). We assume that the dependencies between classes in UML is translated as the declaration of at least one field in the first class having as a type the second class. In addition, we assume that the equivalent of stereotypes in UML are annotations in Java. The method invariant (..) uses the Java reflect library by invoking, for example, getDeclaredFields() in Line 3 to collect fields, and isAnnotationPresent(..) in Lines 6 and 7 to check if a given type has been marked with a particular annotation.

General Approach

We propose a three-step process for generating executable Java code from architecture constraints. We note the presence of two metamodels the first one is the UML metamodel and the second is the Java metamodel that are presented in the following sections. Fig. 2 depicts the process of metaprogram generation. If the OCL constraint needs a refinement, the first step consists in rewriting the OCL constraint in order to make it more accurate and concrete. For example, if the constraint has a navigation to Dependency metaclass (in UML metamodel) then we need to refine this constraint by specifying the different levels of dependencies. Else, the step of transforming OCL constraints from UML metamodel to Java metamodel is established in order to go forward in the process, to the Java code generation. These steps are detailed in the following sections. We did not perform a direct translation from OCL/UML to Java because this translation includes at the same time several transformations: shifting to a new metamodel, changing the syntax of constraints, etc. In fact, our approach requires first a mapping from abstractions of design level to abstractions of implementation level (mapping abstractions from UML metamodel to the Java metamodel) and subsequently a translation of the syntax.

In the literature, there are many languages enabling the specification of architecture constraints (see [START_REF] Tibermacine | Software Architecture 2, chap. Software Architecture: Architecture Constraints[END_REF] for a survey). The choice of OCL and UML is motivated by the fact that UML is the de facto standard modeling language, and that OCL is its original constraint language. Even if a recent study [START_REF] Petre | Uml in practice[END_REF] pointed that UML is not widely used by developers, we all agree that it is a general-purpose modeling language known by a lot of developers. We have intuitively chosen to make constraints programmable in the implementation level in Java because it is a main-stream language in object-oriented programming, which provides introspection capabilities.

Constraint Refinement

The refinement mechanism is used whenever some abstractions in the UML metamodel do not have an equivalence in the JAVA language. For example, in the specification of the OCL constraint expressed on the UML metamodel, we have collected all types (Classes) which have dependencies with a specific type by using supplierDependency.client. This expression has not a direct equivalence Listing 3 Refined MVC pattern constraint Our constraint in Listing 3 (after refinement) is composed of three sub-constraints (Lines 5-8, Lines 10-13 and Lines 15-18). Each sub-constraint matches one level of the dependencies. In Line 5, the dependency is primarily verified on all attributes defined in classes. Note that oclAsType(Class) operation is used in this constraint to allow navigation between Type and Class through the specialization relation. In Lines 10 and 15, the dependency is related to the types of operation parameters and their returned values.

The refinement of a constraint means a translation of this constraint from an abstract level to a concrete one. In contrast to the translation detailed in the following section, in this step, the translation is an endogenous transformation, since the constraints which are the source and the target of the transformation both navigate in the same (UML) metamodel.

Constraint transformation

Before generating code, we transform in this step the OCL constraint specified on the UML metamodel into an OCL constraint specified on the Java metamodel. This simplifies the translation into Java code, since the mapping of abstractions from UML to Java is performed in this step. In order to perform constraint transformation we used a Java metamodel. Unfortunately, none of the metamodels found in the literature and practice satisfied our needs. We relied on Java Reflect library to create a new simplified Java metamodel. In fact, we can define our metamodel relying on Java specification but we deliberately chose Java Reflect because it gives us access to the meta-level of the language and also because it reflects exactly what we can do in the generated Java code. In this metamodel, we limited ourselves to the elements necessary for architecture constraint specification. Fig 3 depicts the Java metamodel that we have defined 1 .

The goal of constraint transformation is to replace in an architecture constraint the UML metamodel vocabulary by Java metamodel vocabulary. It had to establish a mapping between UML terms and Java terms that are classified in three categories: metaclasses, roles and navigations.

Table 1 presents for each UML metaclass, role and navigation its equivalent in Java.

We opted for the specification of these mappings in xml, and we have written an ad-hoc program for implementing the transformation instead of using an existing model transformation language like Acceleo [3], Kermeta [START_REF] Kermeta | [END_REF] or ATL [START_REF] Jouault | Transforming models with atl[END_REF]. In fact, architecture constraints are not models. We might have generated models from constraints. But this process is complex to implement. It requires to transform the text of the constraint in models, to use a transformation language for transforming these models and then generate again the text of the new constraint from the new model. We opted for a simple solution that consists in exploiting an OCL compiler. It allows to generate an abstract syntax tree (AST) from the text of the constraint. This AST allows us to apply easily different transformations.

We apply the table presented before (Table 1) on the generated AST in order to obtain a constraint expressed in Java metamodel. For applying mappings, we start by navigations, then the roles and finally the metaclasses. The following Listing 4 presents our constraint example after applying the transformation method: Listing 4 MVC pattern constraint in OCL/Java

As indicated in Listing 4, we replace, among others, package.profileApplication. appliedProfile.ownedStereotype by annotation, ownedOperation by method, by respecting the mappings defined before.

The use of declarative mappings gives us the opportunity when the metamodels evolve to modify easily the changed elements. In addition, it allows us to offer a generic method which does not depend on particular metamodels.

Constraints generation into Java metaprograms

Code generation consists in translating the constraint expressed in Java metamodel into a Java metaprogram. To generate this code, we relied on the following steps. First, we generate the abstract syntax tree (AST) from the constraint expressed in Java metamodel. Then, when traverse this tree in a Depth-First Pre-Order way in order to generate progressively the java code by relying on rules presented below. It is worth mentioning that the first rule is applied only once in a constraint generation code. The other rules are applied along the analysis of the type of the AST nodes. In fact, if it is a role or navigation then we must apply Rule 2. If is is a quantifier, the rule 3 is then applied and so on.

1. We must consider first that a constraint is represented by a Java method that returns a boolean, which takes as parameter an object of type the metaclass on which the constraint applies (its context). This method is located in a Java class and invokes if necessary other methods that are implemented during the code generation. 2. Each role and navigation in the Java metamodel will be transformed to its accessor method defined in Java. For example, if we navigate to Field, we apply getDeclaredFields() 2 , and if we would like to access to a method return type we call getReturnType(). 3. Concerning the OCL quantifiers and the operations, we defined for each one a Java template. Examples are presented in Table 2. select(...) method presented in the last row of the table can be applied on different OCL collection types, like Set or Sequence. During the code generation , each OCL type will be replaced by its Java equivalent. 2 OCL Quantifiers and operations generation in Java 4. In each quantifier or operation, we traverse recursively the evaluated expression as a sub-constraint and we generate again the corresponding code: if we meet a role or navigation in Java metamodel, we re-apply rule 2. If the quantifier is nested, we re-apply rule 3, and so on. 5. In the case of a nested quantifier (two quantifiers for example are defined one inside the other), the second quantifier frequently needs to use the variables of the first one to define its expression. So, in this case, we store the variables of the first one (parameters of method that correspond to the first quantifier) in order to pass them among the parameters of the method corresponding to the second one. 6. Concerning the logic operators (and, not..), we defined also methods equivalent for each one. These methods are implemented in a class called LogicalOperator.

If the constraint contains a logic operator, This class will be declared as a super class of the generated class that contains the invariant method. 7. The arithmetic operations (>, <, =, ...) and the types (Integer, Real, String, ...) are the same in the generated metaprogram.

In order to better explain the code generation process, Table 3 presents an example of a metaprogram which is generated from our MVC constraint presented in 2. For simplicity reasons, we consider for the dependency between two classes that the first class has at least one method return type having as type the second class.

We have presented in Table 3, for each part of constraint, its equivalent Java code by respecting the rules that was explained previously. The generated code uses the introspection of Java in order to examine the application structure at runtime (getAnnotations(), getMethods()). This code should be called before and after each method and affectation implemented in the application.

It is worth noting that this code is syntactically different from the optimal code presented at the beginning of the paper (see Listing 2) but they are semantically equivalent. It is evident that the automatic translation does not allow to obtain a code having an optimal complexity. However, it is a valuable tool for developers who will rather focus on implementing the business logic of their application.

Related Work

In this section we present works related to OCL constraint transformation and OCL code generation. Hassam et al. [START_REF] Hassam | Adapting ocl constraints after a refactoring of their model using an mde process[END_REF] proposed a method for transforming OCL constraints during UML model refactoring using model transformations. Their approach uses first an annotation method for marking the initial UML model, in order to obtain an annotated target model. Then, a mapping table is created from these two annotations in order to transform OCL constraints of the initial model into OCL constraints of the target one. Their solution of constraint transformations is difficult to establish and it needs some knowledge about model transformation languages and tools. In our work, constraint transformation is simple. It is performed in an adhoc way without using additional modeling and transformation languages. In [START_REF] Ferdjoukh | A csp approach for metamodel instantiation[END_REF], the authors propose an approach to generate (instantiate) models from metamodels taking into account OCL constraints, using CSP (Constraint Satisfaction Problem). They defined some mathematical rules to transform models and constraints associated to them. Cabot et al. [START_REF] Cabot | Umltocsp: a tool for the formal verification of uml/ocl models using constraint programming[END_REF] worked also on UML/OCL transformation into CSP in order to check quality properties of models. These approaches are similar to our transformation process because they use an OCL compiler (DresdenOCL [START_REF] Demuth | The dresden ocl toolkit and its role in information systems development[END_REF]) to transform constraints. But in our approach, we consider source code generation from these constraints, in order to make them executable with application's code.

In contrast to CSP, this does not require an external tool for the interpretation of constraints.

In the practice of model-driven engineering, there exist several tools like Eclipse OCL [START_REF]Eclipse ocl[END_REF], Octopus [START_REF]Octopus: Ocl tool for precise uml specifications[END_REF], and DresdenOCL [START_REF] Demuth | The dresden ocl toolkit and its role in information systems development[END_REF][START_REF] Hussmann | Modular architecture for a toolset supporting ocl[END_REF]17] which aim to translate OCL constraints in Java source code. They however transform constraints which are functional and not architectural. These tools translate this kind of constraints into objectoriented programs which do not use the introspection mechanism. The generated code by Dresden OCL is difficult to understand. Indeed, it is true that Dresden OCL is the first tool implemented in this domain, but it extensively uses a vocabulary proposed only by its APIs. This code is normally intended to developers who master, and will continue to use, Dresden OCL, contrary to our work, where code is intended to be used by any Java developer. Besides, with these tools, we need to create beforehand the classes of the model before generating constraints. Other works like Briand et al. in [START_REF] Briand | Using aspect-oriented programming to instrument ocl contracts in java[END_REF] and Hamie et al. in [START_REF] Hamie | Pattern-based mapping of ocl specifications to jml contracts[END_REF] proposed a tool to transform functional (and not architectural) constraints respectively into Java using aspect-oriented programming and JML contracts.

Conclusion

It has been demonstrated that architecture constraints bring a valuable help for preserving architecture styles, patterns or general design principles in a given application after having evolved its architecture description [START_REF] Tibermacine | On-demand quality-oriented assistance in component-based software evolution[END_REF]. These architecture constraints are checked at design time. But what if the architecture evolves in the implementation artifacts (the application's programs)? Or, what if the architecture evolves at runtime (through dynamic adaptation, for example)? To be able to check these constraints in that development stage and at runtime, architecture constraints should be translated into an appropriate format: meta-programs.

We have presented in this paper a process for generating Java code starting from OCL architecture constraint specifications expressed in the UML metamodel. This Java code uses the introspection mechanism provided by the programming language. Our process is composed of three steps. The first optional one consists in refining the constraints. The second step allows to transform them into OCL constraints expressed in Java metamodel. The last step generates Java source code relying on specific code generation rules. The reflection (instrospection) mechanism used in our approach is a standard mechanism in Java. Otherwise, we can use static analysis libraries like JDT [START_REF]JDT: Java development tools[END_REF] or ByteCode libraries like BCEL [5] but our goal was to use what is standard in Java and not resort to external libraries. In addition, with reflection, architecture constraints can be checked at runtime (by invoking the invariant method in all the methods of the application where the architecture is changed: new objects are created, references to objects are assigned to fields, etc.).

In our proposal, OCL coverage is not complete. We have implemented a prototype called MOJaRT: Meta-OCL to JAva Reflect Translator. It is available for download here: https://github.com/saharkallel/mojart.git/. which does not take into consideration some OCL constructions, like some collection operations (union, for example). But this does not have any impact on the work proposed in this paper.

As a future work, we plan to generalize the proposed approach, by specifying architecture constraints in a language-independent way: using predicates on graphs and operations on them and then making automatic transformations towards a particular object-oriented programming language.

Fig. 1

 1 Fig. 1 An excerpt of UML metamodel

10 } 11 r e t u r n t r u e ; 12 }

 101112 p u b l i c b o o l e a n i n v a r i a n t ( C l a s s <?> a C l a s s ) { i f ( a C l a s s . i s A n n o t a t i o n P r e s e n t ( Model . c l a s s ) ) { F i e l d [ ] f i e l d s = a C l a s s . g e t D e c l a r e d F i e l d s ( ) ; f o r ( F i e l d a F i e l d : f i e l d s ) { C l a s s <?> f i e l d T y p e = a F i e l d . g e t T y p e ( ) ; i f ( f i e l d T y p e . i s A n n o t a t i o n P r e s e n t ( View . c l a s s ) | | f i e l d T y p e . i s A n n o t a t i o n P r e s e n t ( C o n t r o l l e r . c l a s s ) ) r e t u r n f a l s e ; } Listing 2 MVC pattern constraint in Java

Fig. 2

 2 Fig. 2 Approach Description

Fig.

  Fig. 3 Java metamodel

  :OclExpression): Boolean java private boolean forAll(Collection c) { for(Iterator i = c.iterator(); c.hasNext();) { if(!exInJava) return false; } return true; } exists ocl exists(ex:OclExpression):Boolean java private boolean exists(Collection c) { for (Iterator i = c.iterator(); c.hasNext();) { ElementType e = (ElementType) i.next(); if(exInJava) return true; } return false; } select ocl select(ex:OclExpression):Sequence java List result = new ...(); private list select(Collection c) { for (Iterator i = c.iterator(); c.hasNext();){ ElementType e = (ElementType) i.next(); if (exInJava) { result.add(e); } } return result; } Table

3

  Java metamodel

		UML	Java
	Metaclass	Class	Class
	Role	ownedAttribute	field
		ownedOperation	method
		superClass	superClass
		nestedType	declaringClass
		interfaceRealization	interface
		package	package
	Navigation	package.profileApplication
		.appliedProfile.ownedStereotype	annotation
	Metaclass	Property	Field
	Role	type	type
		declaringTypeattribute	declaringClass
	Metaclass	Operation	Method
	Role	returnValuetype	returnType
		declaringTypeoperation	declaringClass
		ownedParameter	parameterType
		raisedException	exceptionType
	Metaclass	Stereotype	Annotation
	Metaclass	Package	Package

Table 1

 1

Mapping UML-Java (Metaclass, Role, Navigation)

. a p p l i e d P r o f i l e . o w n e d S t e r e o t y p e ->e x i s t s ( s : S t e r e o t y p e |

We assume in this paper that the reader is familiar with UML and Java languages. This is the reason why the two metamodels are not detailed. They are depicted only for accompanying OCL constraints in order to see how navigations in the metamodels are established.

We use getDeclaredField() instead of getFields() to retrieve all attributes (private and public). For those we inherit, we must specify them in the OCL constraint using the role superClass.

Kallel, Tibermacine, Tramoni, Dony and HadjKacem