Peng Fu

Aaron Stump

Jeff Vaughan

A Framework for Internalizing Relations into Type Theory

This paper introduces the concept of internalization structure, which can be used to incorporate certain relations into F Π , a variant of system F, while maintaining termination of the new system. We will call this process of incorporation internalization, F Π the base system and the new system after the incorporation the internalized system. We first specify the syntax, and then the semantics of F Π via the Tait-Girard reducibility method. We then define internalization structure. We show that we can obtain a terminating internalized system from an internalization structure. Finally, as motivating examples, we demonstrate how our framework can be applied to internalize subtyping, full-beta term equality and term-type inhabitation relations.

Introduction

Type systems, including the Calculus of Inductive Constructions [START_REF] Coquand | Inductively defined types[END_REF] and F <: [START_REF] Pierce | Types and programming languages[END_REF], incorporate auxiliary judgments in their typing relations. For example, the subtype judgment is a premise of F <: 's subsumption rule:

Γ � t : T T <: T � Γ � t : T � sub
Likewise, the type-equivalence judgment appears in CIC's conversion rule:

Γ � t : T T ≡ T � Γ � t : T � conv
Conventionally, adding a rule like sub or conv to a lambda calculus requires ad-hoc reasoning about the auxiliary judgment system and its relation to the underlying type theory. This paper proposes a new framework for defining language extensions in the style of sub or conv, and shows how to systematically verify that such extensions yield terminationing systems under call-by-name reduction.

We call deduction systems producing auxiliary judgments metasystems, and refer to typing rules that modify types based such metasystem judgments automatic conversion rules. We will also consider cut-down type systems without automatic conversion rules; these are called base systems.

For instance the subtyping (<:) and type-equivalence (≡) derivation systems are metasystems, and rules sub and conv are automatic conversion rules. System F is F <: 's base system. Automatic conversion rules may be viewed as a bridge between a base system and a metasystem; metasystem derivations serve as evidence that type conversion or subsumption should be allowed.

Type structure may be used to reflect metasystem judgments. Indeed this has been done in several languages: equality sets in Martin-Löf type theory enable reasoning about equality relations [START_REF] Nordström | Programming in Martin-Löf 's Type Theory: An Introduction[END_REF], Sjöberg and Stump's T vec uses types to reflect call-by-value term equality in the presence of divergence [START_REF] Sjöberg | Equality, Quasi-Implicit Products, and Large Eliminations[END_REF], and the AuraConf language uses proofs of type e isa t to indicate expression e may be cast to type t [START_REF] Vaughan | Aura: Programming with Authorization and Audit[END_REF]. As we will see, the language extension framework proposed in this paper is implemented using a generalization of these ideas.

The Curry-Howard isomorphism enable us to view the base system as a kind of constructive logic. Once we internalized metasystem judgments as types, we can reason about these judgments using the logic provided by the base system. Moreover, using features of the internalized system we can derive new, admissible judgments that may not derivable in either the base system or the metasystem alone. Later we will see how the internalized system makes this possible.

This paper introduces a new framework, internalization, that enables the systemic definition and investigation of λ-calculi with automatic conversion rules. We use a dependent variant of polymorphic lambda calculus F Π as a base system (Section 2). We then show how to create generalizations of F Π -internalized systems-given a compact internalization structure (Section 3). A sound internalization structure yields a terminating internalized system (Section 4). This framework is powerful enough to augment F Π with interesting features, including subtyping, conversion based on full-beta term joinability, and a reflected typing relation (Section 5). Finally this paper compares internalization with several related ideas from type theory (Section 6).

An internalization structure is a triple �D, E, I�. Reflective relational sentences D define the syntax of metasystem propositions and identify valid metasystem judgments. Elimination relation E defines automatic conversion rules based on judgments from D. Finally, interpretation I defines semantics for reflective relational sentences as relations over sets of terms. All internalization structures require that D and E are sound. As a central result of our work, we show that any sound internalized system constructed from an internalization structure is guaranteed to be terminating.

The contributions of this work are as follows. We define internalization, a framework that enables the systematic study of automatic conversion rules and metasystems relative to a base system. We instantiate this framework with respect to system F Π , and prove that every internalization structure yields a new, terminating lambda calculus. Finally we demonstrate the utility of this methodology with examples.

2 Base system F Π Internalization builds off of base system F Π , a variant of system F. F Π 's syntax and operational semantics are given in Figure 1. We use call-by-name operational semantics. Key differences between F and F Π are as follows:

1. F Π is parametrized by a finite set B of constant types and it contains a constant term axiom.

2.

Values is extended by including constant terms. 3. F Π uses dependent product Π instead of arrow → as the function type constructor.

A word about the use of call-by-name reduction is warranted. The main result of this paper is normalization for systems derived by internalization from the base system F Π . Strong normalization does not hold for all such systems, as we show by example in Section 5. 1. So (weak) normalization is all that we can obtain. An interesting result of our investigation into internalization is that normalization with respect to call-by-name reduction imposes fewer requirements on internalization structures than with call-by-value reduction. Specifically, the λ-abstraction case of the proof of Theorem 1 goes through more directly using call-by-name reduction; with call-by-value reduction, dependent typing imposes additional requirements on the internalization structure.

For F Π , we use dependent product instead of arrow anticipating the use of internalization structures whose types mention terms. F Π contains constant axiom but does not give it a type; later, internalized systems will use axiom to inhabit special types. Moreover, defining axiom now allows us to fix a single universe of reducibility candidates and to use F Π type interpretations directly when interpreting these special internalized-system types.

Syntax of F Π

Figure 2 gives the type assignment rules for F Π . The definition of typing context is standard. We define the judgment Γ � OK for well-formedness of context Γ as follows:

• � OK Γ � OK Γ, X � OK Γ � OK FVar(T ) ⊆ dom(Γ ) Γ, x : T � OK
FVar(T ) means the set of free type variables and free term variables in type T . dom(Γ ) means the domain of the context, i.e., e ∈ dom(Γ ) iff e is either a type variable such that Γ ≡ Γ 1 , e, Γ 2 , or a term variable such that Γ ≡ Γ 1 , e : T, Γ 2 .

Interpretation of Types in F Π

Reducibility is a well-known technique for proving the normalization of type systems such as F. In this paper, we use it to interpret F Π 's types. Reducibility will both provide intuition for F Π 's semantics and yield a normalization result. To begin, we define reducibility candidates following Girard's Proofs and Types [START_REF] Girard | Proofs and types[END_REF].

Types T ::= B | X | Πx : T.T | ∀X.T Terms t, u ::= axiom | x | (t t) | λx.t Contexts C ::= [] | C t Values v ::= λx.t | axiom C [(λx.t) t � ] � C [[t � /x]t]
x : T ) ∈ Γ Γ � OK Γ � x : T Var Γ, x : T1 � t : T2 Γ � λx.t : Πx : T1.T2 Π-intro Γ � t1 : Πx : T1.T2 Γ � t2 : T1 Γ � t1 t2 : [t2/x]T2 Π-elim Γ, X � t : T Γ � t : ∀X.T ∀-intro Γ � t : ∀X.T F V ar(T � ) ⊆ dom(Γ ) Γ � t : [T � /X]T ∀-elim Fig. 2.
(φ) ⊆ �. If dom(φ) = {X 1 , X 2 , ...X n }, then we usually write φ as [R 1 /X 1 , ...R n /X n ].
Figure 3 defines the interpretation [[T ]] φ of a type T as a set of terms. Note that constant types B and their interpretations R B are left unspecified; these may be filled in later. For any [[T ]] φ , let F V (T ) be the set of free type variable in T .we assume F V (T ) ⊆ dom (φ).

t ∈ [[B]] φ iff t ∈ RB, where RB ∈ � t ∈ [[X]] φ iff t ∈ φ(X) t ∈ [[Πx : T1.T2]] φ iff t ∈ V and (∀u ∈ [[T1]] φ ⇒ (t u) ∈ [[[u/x]T2]] φ ) t ∈ [[∀X.T ]] φ iff ∀R ∈ �, t ∈ [[T ]] φ[R/X]

Type Soundness

The theorem below shows that any typable closed term is normalizing, and can be shown in a standard way using Tait-Girard reducibility (cf. [START_REF] Girard | Proofs and types[END_REF]). Several properties of the interpretation of types are required, which can all be proved by induction on the structure of types in F Π . The proofs of the lemmas and theorems below are relegated to the appendix.

Lemma 1. [[T ]

] φ ∈ �, in the other words, the interpretation of a type is indeed a reducibility candidate.

Lemma 2. Let Sub be the set of all capture avoiding term-level substitutions with a domain of term variables and a range of terms that are in

V. ∀σ ∈ Sub, [[σT ]] φ = [[T ]] φ .
Since F Π essentially is system F, it does not contain terms in the types, we have σT ≡ T in F Π , thus this lemma is true.

Lemma 3 (Substitution lemma). [[[T � /X]T ]] φ = [[T ]] φ[[[T � ]] φ /X] .
Definition 3. We define the set [Γ ] of well-typed substitutions (σ, δ) w.r.t. Γ as follows:

(∅, ∅) ∈ [.] (σ, δ) ∈ [Γ ] R ∈ � (σ, δ ∪ {(X, R)}) ∈ [Γ, X] (σ, δ) ∈ [Γ ] t ∈ [[σT ]] δ (σ ∪ {(x, t)}, δ) ∈ [Γ, x : T ] Theorem 1 (Type Soundness). If Γ � t : T , then ∀(σ, δ) ∈ [Γ ], (σ t) ∈ [[σT ]] δ .

Internalized Structure

Internalization is based on internalization structure. The internalization structure contains the information of how to construct reflective relational sentences and how these reflective relational sentences interact with the base system. It also gives the meaning of the reflective relational sentences through the interpretation of types in the base system. Once we define an internalization structure, we can then begin the process of internalization by first internalizing the reflective relational sentences as types, then add two new typing rules to deal with these reflective relational sentences.

Internalization structure consists of three parts, they are reflective relational sentences, elimination relation and interpretation. Besides these three parts, an internalization structure has two soundness properties, which we will identify later. In this section, we will first describe these three parts of the internalization structure and the two soundness properties of internalization structure. Then we will illustrate how to construct a new system, which is called internalized system, from an internalization structure. The internalized system is shown to be terminating.

Reflective Relational Sentence-D

We define the kind of judgments or relations that could be integrated into the base system. Essentially these are the relations on the terms and types from the base system. A relational sentence on the basic system is a syntactic object of form R (n×m) (t 1 , ..., t n , T 1 , ..., T m ), where t, T are defined in F Π and R (n×m) ∈ Σ.

Note that in this paper we do not deal with nesting relational sentences. Definition 6. Let A be the set of all relational sentences. A set of reflective relational sentences D is a subset of all relational sentences, i.e. D ⊆ A.

Reflective relational sentences are used to formalize a metasystem's derivable judgments. When we define specifically how to recognize the reflective relational sentences from relational sentences, we obtain a kind of metasystem. This metasystem need not be recursive; it can be defined axiomatically.

Elimination Relation-E

An elimination relation is a syntactic constraint used to specify how the metasystem influences the base system. We will appeal to an elimination relation when we add the elimination rule to the base system for the reflective relational sentences. Since the elimination relation is used after internalizing reflective relational sentences as types, we need to extend the definition of types and the context accordingly. Definition 7. We define extended types and extended contexts as follows:

RTypes A ::= R (n×m) 1 (t 1 , ..., t n , T 1 , ..., T m ) | ... | R (n×m) l (t 1 , ..., t n , T 1 , ..., T m ) ETypes S ::= B | X | Πx : S.S | ∀X.S | A EContext Δ ::= • | Δ, x : S | Δ, X
We can see that the extended types and the extended context defined above are really extended in the sense of adding the relational sentences as new types. Definition 8. We specify an elimination relation E by:

E ⊆ EContext × Terms × Terms × A × ETypes × ETypes.
For example, when we consider the specific internalization structure for subtyping below, we will define an elimination relation where (Δ, t, t � , T < T � , T, T � ) ∈ E holds iff in extended context Δ, t has the type T , t � has the type T < T � , and we can change the type of t to T � .

Interpretation-I

We defined the interpretation of types of F Π before. Since interpretation of types is a set of terms and the reflective relational sentences are relations about between terms and types in F Π , it is natural to understand the meaning of these reflective relational sentences as set-theoretic relations between interpretation of types. Take subtyping as an example; we interpret subtype judgment <: as the mathematical subset relation ⊆ on interpretation of types [START_REF] Rehof | Strong normalization for non-structural subtyping via saturated sets[END_REF].

Interpretation-I is defined to capture this intuition. Later we will relate interpretation-I to reflective relational sentences and elimination relation through two soundness properties.

Definition 9. Let � be the set of all reducibility candidates as defined in F Π . We define an interpretation of R (n×m) -I R (n×m) to be I R (n×m) ⊆ Terms n × � m .

Soundness Properties

Now that we have defined all parts of an internalization structure, we can formulate two soundness properties for an internalization structure. Since one of the soundness properties is related to the extended types, we first define the interpretation for extended types. Then we identify the soundness properties.

Definition 10. Let φ be an environment function w.r.t. type S, which is defined in the same way as definition 2 except we extend it to type S. Let A be the set of closed terms that normalize at axiom. The interpretation of types [ [S]] φ is defined inductively as follows:

-t ∈ [[B]] φ iff t ∈ R B . -t ∈ [[X]] φ iff t ∈ φ(X). -t ∈ [[Πx : S 1 .S 2 ]] φ iff t ∈ V and (∀u ∈ [[S 1 ]] φ ⇒ (t u) ∈ [[[u/x]S 2 ]] φ ). -t ∈ [[∀X.S]] φ iff ∀R ∈ �, t ∈ [[S]] φ[R/X] . -t ∈ [[R (n×m) (t 1 , ..., t n , T 1 , ..., T m )]] φ iff t ∈ A and (t 1 , ..., t n , [[T 1 ]] φ , ..., [[T m ]] φ ) ∈ I R (n×m) .
Define (σ, δ) ∈ [Δ] in the same way as (σ, δ) ∈ [Γ ], except with extended contexts and extended types.

Definition 11. We say a tuple �D, E, I� is an internalization structure iff it satisfies the following soundness properties:

-Soundness of reflective relational sentences If R (n×m) (t 1 , ..., t n , T 1 , ..., T m ) ∈ D, then ∀φ, ∀σ ∈ Sub, (σt 1 , ..., σt n , [[σT 1 ]] φ , ..., [[σT m ]] φ ) ∈ I R (n×m)
) ∈ D. Then σ(t) ∈ [[σS � ]] δ .
Soundness of reflective relational sentences means that the reflective relational sentences are a conservative approximation of interpretation-I. Soundness of the elimination relation will imply that the elimination rule for internalized systems respects the Girard-Tait type interpretation and is semantically compatible with substitutions that arise duing CBN evaluation. We will see that in next section. We can extend the lemmas from Section 2.3 above to our extended interpretation of types:

Lemma 4. ∀φ, [[S]] φ ∈ �. Lemma 5 (Substitution lemma). If [S � /X]S ∈ ETypes, then [[[S � /X]S]] φ = [[S]] φ[[[S � ]] φ /X] .

Internalized System

So far, we defined the internalization structure-�D, E, I�. Now using an internalization structure, we can construct a new system-we call it the internalized system-from the internalization structure and F Π . The term syntax and operational semantics of internalized system are the same as F Π , while the syntax of types and contexts are the RTypes, ETypes, EContexts in definition 7. The well-formed extended context Δ � OK is defined just as before except using EContexts. Figure 4 shows the new type assignment rules for the internalized system. We can see that the new type assignment system contains two new rules:A-intro and A-elim. The A-intro rule is used to introduce reflective relational sentences as types in the internalized system, while the A-elim rule is for using the reflective relational sentences to change the type of a term accordingly. The theorem below guarantees that the internalized system generated from F Π and internalization structure is terminating, which is the central result of internalization.

A ∈ D FVar(A) ⊆ dom(Δ) Δ � OK Δ � axiom : A A-intro Δ(x) = S Δ � OK Δ � x : S Var Δ � t : T Δ � t � : A E(Δ, t, t � , A, T, T � ) Δ � t : T � A-elim Δ, x : S1 � t : S2 Δ � λx.t : Πx : S1.S2 Π intro Δ � t1 : Πx : S1.S2 Δ � t2 : S1 Δ � t1 t2 : [t2/x]S2 Π elim Δ, X � t : S Δ � t : ∀X.S ∀ intro Δ � t : ∀X.S [S � /X]S ∈ ETypes F V ar(S � ) ⊆ dom(Δ) Δ � t : [S � /X]S ∀ elim
Theorem 2 (Type Soundness). If �D, E, I� is an internalization structure and Δ � t : S, then ∀(σ, δ)

∈ [Δ], (σ t) ∈ [[σS]] δ .
The proof of this theorem is in appendix.

Corollary 1. If • � t : S, then t ∈ V.
Because typing contexts may introduce spurious assumptions, some open contexts may assign a type to a diverging term. Section 5.1 shows gives an example. This is an expected outcome of reasoning from invalid premises. Indeed Corollary 1 may be strengthened to allow contexts where all variables are classified by inhabited types.

Examples

In previous section, we capsule our development of internalized system as constructing a sound internalization structure. Now let us see how we can apply our formalization of internalization to internalize subtyping, full-beta term equality and term-type inhabitation relations as types. First, we specify an instance of F Π . Essentially, we instantiate constant types as B ::

= � | ⊥. Additionally, we define [[⊥]] φ := ∅, [[�]] φ := V.
Recall that internalization works as follows. We first define the set of reflective relational sentences that contains all the derivable judgments from subtyping, full-beta term equality and term-type inhabitation. Then we define the elimination relation and interpretation. We show our definition interpretation structure is sound. Finally we present the internalized system as the result of internalization. We will follow this recipe in the sequel.

Subtyping

We need to instantiate the three parts of internalization structure-�D, E, I�. First, we specify Σ := {< 0+2 }. Then we know all the reflective relational sentences should be in the form T 1 < T 2 . We identify reflective relational sentences D as follows:

T < � ∈ D ⊥ < T ∈ D X < X ∈ D T 1 < T 2 ∈ D ∀X.T 1 < ∀X.T 2 ∈ D T � 1 < T 1 ∈ D T 2 < T � 2 ∈ D Πx : T 1 .T 2 < Πx : T � 1 .T � 2 ∈ D
We can see that the way we identify D is similar to the way we write subtyping rules. Now we define E as follows:

(Δ, t, t � , T < T � , T, T � ) ∈ E
The meaning of this elimination relation is that if t has type T in context Δ and t � has type T < T � , then t can also has the type T � .

We define interpretation I < :

I < := {(R 1 , R 2 ) |R 1 ⊆ R 2 }
We can see that I < capture all the subset relations on reducibility candidates. The following two lemmas make sure we obtain a sound internalization structure from �D, E, I < � we defined above.

Lemma 6 (Soundness of the Reflective Relational Sentence).

If (T < T � ) ∈ D, then ∀σ ∈ Sub, ∀φ, ([[σT ]] φ , [[σT � ]] φ ) ∈ I < . Proof. Since [[σT ]] φ = [[T ]] φ by lemma 2. We just need to show: If (T < T � ) ∈ D, then ∀φ, ([[T ]] φ , [[T � ]] φ ) ∈ I < .
We will prove this by induction on the structure of T .

Case: T = � or T = ⊥ By inversion, it holds. Case: T = X By inversion, we know T � = X or �, again, it is the case.

Case: T = Πx : T 1 .T 2 By inversion, T � = � or T � = Πx : T � 1 .T � 2 . Let us consider T � = Πx : T � 1 .T � 2 . In this case, by inversion, T � 1 < T 1 ∈ D, T 2 < T � 2 ∈ D. By IH, we have [[T � 1 ]] φ ⊆ [[T 1 ]] φ . Again, by IH, we have [[T 2 ]] φ ⊆ [[T � 2 ]] φ . For any u ∈ [[T � 1 ]] φ ⊆ [[T 1 ]] φ , if t ∈ [[Πx : T 1 .T 2 ]] φ , we have tu ∈ [[[u/x]T 2 ]] φ = [[T 2 ]] φ ⊆ [[T � 2 ]] φ . So t ∈ [[Πx : T � 1 .T � 2 ]] φ . Case: T = ∀X.T By inversion, T � = � or ∀X.T � . So let's consider T � = ∀X.T � . By inversion, we know T < T � ∈ D. We know for t ∈ [[∀X.T ]] φ , ∀R ∈ �, t ∈ [[T ]] φ[R/X] . By IH, [[T ]] φ[R/X] ⊆ [[T � ]] φ[R/X] . So t ∈ [[∀X.T � ]] φ .
Lemma 7 (Soundness of the Elimination Relation).

If (Δ, t, t � , T 1 < T 2 , T 1 , T 2 ) ∈ E, (σ, δ) ∈ [Δ] and σ(t) ∈ [[σT 1 ]] δ = [[T 1 ]] δ and T 1 < T 2 ∈ D, then σ(t) ∈ [[σT 2 ]] δ = [[T 2 ]] δ .
It is the case by soundness of the reflective relational sentences.

For this internalization structure-�D, E, I < �, the A-intro and A-elim rules are equivalent to:

T 1 < T 2 ∈ D FVar(T 1 < T 2 ) ⊆ dom(Δ) Δ � OK Δ � axiom : T 1 < T 2 A-intro Δ � t : T 1 Δ � t � : T 1 < T 2 Δ � t : T 2 A-elim
The subtyping setting also provides a clear illustration that it is possible to have diverging term under open terms and full-beta reduction in internalized system. Here it is possible to derive y : (� < (� → �)) � (λx.xx)(λx.xx) : � using the underivable fact � < (� → �) and derivable (� → �) < � to establish an isomorphism between types � and � → �. Sticking to closed terms means we need not worry about this derivation directly. And call-by-name evaluation ensures that

• � λy.(λx.xx)(λx.xx) : (� < (� → �)) → �
does not reduce. In contrast, full reduction would loop.

Full-beta Term Equality, Term-Type Inhabitation

We can go even further to explore the internalization structure. We add two more relation symbols to signature so that Σ = {↓ (2+0) , < (0+2) , � (1+1) }. For simplicity, we usually do not specify the arity. Thus the relational sentences have form: t 1 ↓ t 2 , T 1 < T 2 , and t � T for base-system t and T . Now we are ready to specify more reflective relational sentences. We define � reflective relational sentences by the following condition:

t � T ∈ D iff ∀φ, t ∈ [[T ]] φ
Notice that this definition is not algorithmic, which is fine since our framework does not require decidability for the set D for reflective relational sentences.

The � symbol allows us to give "morally correct" types to terms which cannot otherwise be checked. In practice, such terms are created when extracting computational content from mechanically checked proofs. As a concrete example, the Coq proof assistant uses an expressive language to define functional programs and exports that code to OCaml for efficient compilation. Resulting OCaml programs do not go wrong, but must use Obj.magic:α → β to pass ML's weaker type system. Likewise, AuraConf [START_REF] Vaughan | Aura: Programming with Authorization and Audit[END_REF] uses a type constructor resembling � to inform the type checker about the concealed types of opaque ciphertexts. Note that weaker variants of � may be possible when, as in the case of extracted proofs, there is a conservative procedure for checking semantic type inclusion, t � alt T ∈ D iff Oracle(t, T ). (We do not consider such variants further.)

We define t 1 ↓ t 2 ∈ D by the following rules:

t ↓ t ∈ D (λx.t)t � ↓ [t � /x]t ∈ D t 1 ↓ t 2 ∈ D t 1 t ↓ t 2 t ∈ D t 1 ↓ t 2 ∈ D λx.t 1 ↓ λx.t 2 ∈ D t 1 ↓ t 2 ∈ D t t 1 ↓ t t 2 ∈ D t 1 ↓ t 2 ∈ D t 2 ↓ t 3 ∈ D t 1 ↓ t 3 ∈ D t 1 ↓ t 2 ∈ D t 2 ↓ t 1 ∈ D
The rules above are the same as how we define the conversion in lambda calculus. In this case, the syntax of extended types (as defined by the internalization framework) is:

EType S ::= � | ⊥ | X | Πx : S.S | ∀X.S | t 1 ↓ t 2 | T 1 < T 2 | t � T
The additional elimination relations are:

(Δ, t, t � , t 1 ↓ t 2 , [t 1 /x](t 3 ↓ t 4 ), [t 2 /x](t 3 ↓ t 4 )) ∈ E. (Δ, t, t � , t � T � , T, T � ) ∈ E
The additional interpretations I ↓ , I � are:

-I ↓ ⊆ Terms × Terms defined by

I ↓ := {(t 1 , t 2 ) | t 1 ↓ t 2 ∈ D}. -I � ⊆ Terms × � defined by I � := {(t, R) | t ∈ R}.
We have now defined the three parts of the internalization structure. We need to show that this structure is sound. For that purpose, we have following lemmas.

Lemma 8 (Soundness of the Reflective Relational Sentence).

-

If (t 1 ↓ t 2 ) ∈ D, then ∀σ ∈ Sub, (σt 1 , σt 2 ) ∈ I ↓ . -If (t � T ) ∈ D, then ∀σ ∈ Sub, ∀φ, (σt, [[σT ]] φ ) ∈ I � .
Proof. If (t 1 ↓ t 2 ) ∈ D, we have ∀σ ∈ Sub, (σt 1 , σt 2 ) ∈ D. This is because we define the t ↓ t � relation same as the conversion in lambda calculus and this is one of its properties. (see [START_REF] Barendregt | The Lambda Calculus: Its Syntax and Semantics. Sole Distributors for the U.S.A. And Canada[END_REF]) Thus ( σt -

If (Δ, t, t � , t 1 ↓ t 2 , [t 1 /x](t 3 ↓ t 4 ), [t 2 /x](t 3 ↓ t 4 )) ∈ E, (σ, δ) ∈ [Δ] and σ(t) ∈ [[σ[t 1 /x](t 3 ↓ t 4 )]] δ and t 1 ↓ t 2 ∈ D, then σ(t) ∈ [[σ[t 2 /x](t 3 ↓ t 4 )]] δ . -If (Δ, t, t � , t � T � , T, T � ) ∈ E, (σ, δ) ∈ [Δ] and σ(t) ∈ [[σT ]] δ and t � T � ∈ D, then σ(t) ∈ [[σT � ]] δ . Proof. We have σ(t) ∈ [[σ[t 1 /x](t 3 ↓ t 4 )]] δ , thus σ(t) ∈ A and (σ[t 1 /x]t 3 ) ↓ (σ[t 1 /x]t 4 ) ∈ D. Since t 1 ↓ t 2 ∈ D, then we have (σ[t 2 /x]t 3 ) ↓ (σ[t 2 /x]t 4 ) ∈ D.
This is also followed by the property of t ↓ t � (see [START_REF] Barendregt | The Lambda Calculus: Its Syntax and Semantics. Sole Distributors for the U.S.A. And Canada[END_REF]). So σ

(t) ∈ [[σ[t 2 /x](t 3 ↓ t 4 )]] δ .
By soundness of reflective relational sentences,

t � T � ∈ D implies ∀φ, σt = t ∈ [[T � ]] φ .
So it is the case.

So the structure �D, E, I < , I ↓ , I � � we have defined is a sound internalization structure. Let us see some instances of A-elim rule and A-intro rule for the internalized system based on this internalization structure:

t 1 ↓ t 2 ∈ D FVar(t 1 ↓ t 2 ) ⊆ dom(Δ) Δ � OK Δ � axiom : t 1 ↓ t 2 A-intro Δ � t : [t 1 /x](t 3 ↓ t 4 ) Δ � t � : t 1 ↓ t 2 Δ � t : [t 2 /x](t 3 ↓ t 4 ) A-elim t � T � ∈ D FVar(t � T � ) ⊆ dom(Δ) Δ � OK Δ � axiom : t � T � A-intro Δ � t : T Δ � t � : t � T � Δ � t : T � A-elim
We can see that our elimination rule for ↓ realizes a more general form of transitivity. For example, if we have a term with a type [t 2 /y](t 1 ↓ y) and t 2 ↓ t 3 ∈ D, then we can assign this term a new type [t 3 /y](t 1 ↓ y) by the elimination rule.

Related Work

Reflection allows users of logical frameworks such as Coq or NuPRL to use object-level definitions and computations as proxies or replacements for metalevel processes such as tactic application. NuPRL includes a built-in reflection rule, showing (roughly) that H � G follows from � ∃p.p proves rep(H � G).

A key difficulty in making this precise is reflecting uses of the reflection rule itself [START_REF] Robert | Using reflection to explain and enhance type theory[END_REF]. Solutions to this problem are given by [START_REF] Allen | The semantics of reflected proof[END_REF] and [START_REF] Barzilay | Implementing Reflection in Nuprl[END_REF]. Like the internalization discussed in the present paper, reflection involves a subtle interaction between the object-and meta-level. However, while reflection uses the object language to replace meta-level reasoning, internalization uses systematic meta-level operations to extend and enhance the object language. Scharp seems to address similar issues of internalization, from the perspective of natural language with Tarski semantics [START_REF] Scharp | Truth and internalizability[END_REF].

Many type theories make direct use of auxiliary judgments. For example, Pure Type Systems includes a conversion rule based on a convertibility judgment that is is not internalized as a type [3]. In CIC (and similar systems), one can define an equality type inductively. In a sense this internalizes the convertibility judgment [START_REF] Pfenning | Inductively Defined Types in the Calculus of Constructions[END_REF], but such an equality type cannot be used to change the type of a given term; rather, an explicit cast is required. In contrast, the current paper's internalized equality can be used to change the type of a term without an explicit cast. Cast terms raise a number of well-known problems, addressed using axioms like Streicher's axiom K [START_REF] Streicher | Investigations into Intensional Type Theory[END_REF]. Systems like the Implicit Calculus of Constructions have sought to alleviate similar problems by leaving term annotations implicit, although not for equality casts [START_REF] Miquel | The Implicit Calculus of Constructions[END_REF]. More recently, Sjöberg and Stump have proposed a system where all such equality casts are implicit, eliminating the practical need for methods like axiom K [START_REF] Sjöberg | Equality, Quasi-Implicit Products, and Large Eliminations[END_REF]. Indeed, providing a framework to support systems like their T vec system is one motivation for the present work. The problem of equality in type theory is, of course, one of the most longstanding and central ones, and has been addressed in too many works to summarize further (but see also [START_REF] Altenkirch | Observational Equality, Now![END_REF] for a recent approach combining intensional and extensional features).

Also related is language extension using meta-programming techniques. Felleisen builds a formal model describing the power of and limitations of macros for extending programming languages with new features [START_REF] Felleisen | On the expressive power of programming languages[END_REF]. As with internalization, macros can define "local" language extensions. In Felleisen's setting locality is induced by a requirement that macro expansion be a homomorphism on base-language syntax. In contrast to this syntactic approach, our internalization framework specifies semantic constraints which, if satisfied, enable preservation of deep semantic properties of the system being extended.

Conclusion and Future Work

We have formalized the notion of internalization structure and demonstrated that the internalized system is terminating. We also have shown how our formalization can be applied to full-beta term equality, subtyping and term-type inhabitation relation. Our approach makes it easier to establish normalization for type theories with these features, since the framework provides the analysis for all but the internalization-specific parts of the language. In future work, we hope to change our base system to the Calculus of Construction and see if we can obtain a similar internalization structure from it. Also, we plan to prove other standard meta-theoretic results, such as type preservation (i.e. subject reduction). Another direction would be trying to find out more relations that can be incorporated into base system through internalization.

Fig. 1 .

 1 Fig. 1. Syntax and Operational Semantics of F Π

(

Fig. 3 .

 3 Fig. 3. Interpretation of Types in F Π

Definition 4 .

 4 Let signature Σ ⊆ Symbols × N × N, where Symbols means a set of relation symbols, and N is the set of natural numbers. R n×m ∈ Σ means R ∈ Symbols and the arity of R is n + m. Definition 5.

Fig. 4 .

 4 Fig. 4. Type Assignment System of Internalized System

  1 , σt 2 ) ∈ I ↓ by definition of I ↓ . If (t � T ) ∈ D, by definition, we have ∀φ, t ∈ [[T ]] φ . Since t is closed, ∀σ ∈ Sub, σt ≡ t. And we have [[σT ]] φ = [[T ]] φ . So ∀φ, ∀σ ∈ Sub, σt ∈ [[σT ]] φ . Thus ∀σ ∈ Sub, ∀φ, (σt, [[σT ]] φ ) ∈ I � .Lemma 9 (Soundness of the Elimination Relation).

  Type Assignment System of F Π If t ∈ R,then t ∈ V, where V is the set of closed terms that that reduces to a value in Values. CR 2 If t ∈ R and t � t � , then t � ∈ R. CR 3 If t is a closed term, t � t � and t � ∈ R, then t ∈ R.

	Definition 1. A reducibility candidate R is a set of terms that satisfies the
	following conditions:
	CR 1 Definition 2. Let � be the set of all reducibility candidates. Let TVar be the
	set of all type variables.

Let φ be a finite function with dom(φ) ⊆ TVar and range

  . -Soundness of the elimination relation Suppose (Δ, t, t � , R (n×m) (t 1 , ..., t n , T 1 , ..., T m ), S, S � ) ∈ E, and (σ, δ) ∈ [Δ]. Also, suppose σ(t) ∈ [[σS]] δ and R (n×m) (t 1 , ..., t n , T 1 , ..., T m

A Proofs

With our reduction strategy, (t u) � (t � u). By IH(CR 1), u is closed, thus we know (t u) is closed . By IH(CR 3)

We know that � is non-empty (for example, V ∈ �, this follow by lemma 10). Take an arbitrary reducibility candidate R. Case: T = X, B

So it is the case.

The other direction is similar.

A.3 Proof of Theorem 1

Proof. By induction on the typing derivation of Γ � t : T Case:

Case:

We need to prove that σ(t

] δ , which is true.

Case:

We need to show that for all (σ, δ)

So it is the case.

Case:

We need to show for any (σ, δ)

So it is the case.

A.4 Proof of Lemma 4

Proof. By induction on the structure of S.

Case: S = X, B CR 1-CR 3 Obvious from the definition.

and arbitrary

So it is the case.

The other direction is similar.

which is true because lemma 3.

A.6 Proof of Theorem 2

proof By induction on the typing derivation of Δ � t : S Case:

Case:

We need to prove that σ(t

So it is the case.

Notice that if we use LTR-CBV as underlying operational semantics, to show λx.

Thus it is more complicated in this situation.

Case:

Δ, X � t : S Δ � t : ∀X.S

We need to show for any (σ, δ) ∈

We need to show for any (σ, δ)


Erik Hollnagel

Shawn Pruchnicki

Rogier Woltjer

Shawn Etcher

with the functional resonance accident model

published or not. The documents may come

Introduction

The goal of any accident investigation is to determine why a certain combination of conditions, events, and actions led to the specific outcome. There are normally few problems determining what happened, since in most industrial domains the consequences are manifest. (The situation may not be the same for "accidents" in other fields of endeavour, for instance financial markets.) But the explanation of why something happened may be less obvious. In order to construct an explanation it is necessary to have a methodical approach, which in turn requires an articulated accident model or accident theory, i.e., a formal or semi-formal description of how accidents occur, often in terms of cause-effect relations. Since the systematic concern for industrial accidents began about 100 years ago, practitioners and researchers have developed several different accident models and methods to help them in accident investigation. Such models and methods are usually adequate for the typical problems of their time; indeed, there would be little reason to develop models and methods that were more complex or powerful than needed. Yet because socio-technical systems continue to develop and thereby become more complex and more tightly coupled, all models and methods will eventually become outdated and underpowered. Models have over time gone from simple linear models, such as the domino model [START_REF] Heinrich | Industrial accident prevention: a scientific approach[END_REF], via complex linear or epidemiological models, such as the Swiss cheese model [START_REF] Reason | Human error[END_REF], to systemic models (e.g., [START_REF] Leveson | A new accident model for engineering safer systems[END_REF]. Despite their differences, they all adhere to the principle that accidents are caused and that the causes can be understood as failures or malfunctions of technology, humans or organizations -either alone or together. It has only recently become accepted that accidents can be the outcome of unexpected combinations of normal performance variability, i.e., arise from normal actions. This view recognizes that normal actions never can be completely prescribed or regulated because working conditions always are underspecified. Short and longer term adjustments are therefore needed to match specific situations or conditions. This variability is not just normal and useful, but indeed necessary for work to be done. On the individual level the adjustments have been described as sacrificing decisions or efficiency-thoroughness trade-offs [START_REF] Hollnagel | Barriers and accident prevention[END_REF]. On the collective or organisational level, the adjustments have been described using terms as drift or migration [START_REF] Cook | Going solid": a model of system dynamics and consequences for patient safety[END_REF]. Since the variability normally is useful it mostly goes unnoticed, regardless of the level at which it takes place. It is only when the variability gives rise to unexpected outcomes that it is noticed and deemed to be bad and a cause of failures. Although many different accident models exist, the accident investigation community has yet to adopt one that is able to explain how the fundamental interrelationships among system functions may lead to adverse outcomes. This is nevertheless important if we are ever to change from a reactive to a proactive safety management. The Functional Resonance Accident Model (FRAM) and the associated method provide a way to examine individual system functions and determine their interrelationship. This paper reports the application of the FRAM to analyse a highly publicized aviation accident, the crash of Comair flight 5191 in Lexington, KY on August 27th, 2006. The goal of this application was to see what relationships the use of FRAM would discover as compared to how the investigation was performed in the traditional sense.

Comair flight 5191

At 0606 hours the morning of August 27th, 2006, Comair flight 5191 a Canadair 50 seat Regional Jet (CRJ) crashed after an attempted takeoff from the Lexington Blue Grass Airport in Lexington, KY. The flight was a 14 CFR Part 121 passenger revenue flight from Lexington (KLEX) to Atlanta, Georgia (KATL). The aircraft taxied out uneventfully and then inadvertently proceeded to depart from the shorter general aviation runway (runway 26) as opposed to the longer air carrier runway (runway 22). The aircraft became momentarily airborne after it struck an earthen berm, then collided with trees, and crashed. There was a significant post-crash fire consuming most of the aircraft, and 49 of the 50 passengers and crew perished. Figure 1 shows an aerial view of the Lexington Blue Grass Airport with an overlay of the aircraft's actual taxi route, the intended taxi route and the former taxi route prior to airport construction. The NTSB investigation of the accident concluded that:

... the probable cause of this accident was the flight crewmembers' failure to use available cues and aids to identify the airplane's location on the airport surface during taxi and their failure to crosscheck and verify that the airplane was on the correct runway before takeoff. Contributing to the accident were the flight crew's nonpertinent conversation during taxi, which resulted in a loss of positional awareness, and the Federal Aviation Administration's (FAA) failure to require that all runway crossings be authorized only by specific air traffic control (ATC) clearances. The accident was explained as being caused mainly by the failures of the humans at the sharp end, with some blame also going to the Federal Aviation Administration (FAA). The remainder of this paper will illustrate how a FRAM analysis can produce a more nuanced -and therefore hopefully also a more adequate -explanation.

Overview of the Functional Resonance Accident Model (FRAM)

The Functional Resonance Accident Model and the associated method provide a way to describe how multiple functions and conditions can combine to produce an adverse outcome [START_REF] Hollnagel | Barriers and accident prevention[END_REF]. FRAM is based on the following principles:

• The principle of equivalence of successes and failures. FRAM adheres to the resilience engineering view that failures represent the flip side of the adaptations necessary to cope with the real world complexity rather than a failure of normal system functions. Success depends on the ability of organisations, groups and individuals to anticipate risks and critical situations, to recognise them in time, and to take appropriate action; failure is due to the temporary or permanent absence of that ability.

• The principle of approximate adjustments. Since the conditions of work never completely match what has been specified or prescribed, individuals and organisations must always adjust their performance so that it can succeed under the existing conditions, specifically the actual resources and requirements. Because resources (time, manpower, information, etc.) always are finite, such adjustments are invariably approximate rather than exact.

• The principle of emergence. The variability of normal performance is rarely large enough to be the cause of an accident in itself or even to constitute a malfunction. But the variability from multiple functions may combine in unexpected ways, leading to consequences that are disproportionally large, hence produce a non-linear effect. Both failures and normal performance are emergent rather than resultant phenomena, because neither can be attributed to or explained only by referring to the (mal)functions of specific components or parts. • The principle of functional resonance. The variability of a number of functions may every now and then resonate, i.e., reinforce each other and thereby cause the variability of one function to exceed normal limits. The consequences may spread through tight couplings rather than via identifiable and enumerable cause-effect links, e.g., as described by the Small World Phenomenon. This can be described as a resonance of the normal variability of functions, hence as functional resonance. The resonance analogy emphasises that this is a dynamic phenomenon, hence not attributable to a simple combination of causal links.

FRAM Functions and Aspects

In the context of an accident investigation using FRAM, the explanation is produced by proceeding through the following steps.

1. Identify essential system functions, using normal or accident-free performance as a baseline. This step characterises each function separately but does not try to arrange or order them in any way. The starting point may be existing task analyses, procedures, expert knowledge, etc. The characterisation uses the following six aspects:

• Input (I): that which the function processes or transforms or that which starts the function,

• Output (O): that which is the result of the function, either an entity or a state change,

• Preconditions (P): conditions that must be exist before a function can be executed,

• Resources (R): that which the function needs or consumes to produce the output,

• Time (T): temporal constraints affecting the function (with regard to starting time, finishing time, or duration), and • Control (C): how the function is monitored or controlled. Each function may be described by a simple table, which then can be used for the further analysis. It is also possible to show the functions graphically using a hexagon to represent each function (FRAM modules, Figure 2). Characterise the observed variability of system functions, considering both actual and potential variability. The purpose of FRAM is to provide an explanation of the accident in terms of combinations of performance variabilities. The second step is therefore for each function to describe the actual variability during the accident. This may point to other functions that must be characterised as part of the explanation. For instance, if the input to a function came too late, or was of the wrong kind, then the source of that input -i.e., another function -must be described and characterised. This may in turn require yet other functions to be described, until the total scenario has been accounted for.

3. Identify and describe the functional resonance from the observed dependencies / couplings among functions and the observed performance variability. The output of the first and the second steps is a list of functions each characterised by two or more of the six aspects. (Notice that a function may require several instances of an aspect to be described.) The dependencies among functions can be found by matching or linking their aspects. For example, the output of one function may be the input to another function, constitute a resource, fulfil a pre-condition, or enforce a control or time constraint. The result is an overall description of how the functions were linked or coupled in the accident scenario, and therefore of how functional variability propagated through the system. In general, the links specify where the variability of one function may have an impact, or how it may propagate. Many such occurrences and propagations of variability may create a resonance effect: although the variability of each function may be below the normal detection threshold, they may in combination become a 'signal', hence constitute a risk. This step may be supported by a visualisation of how the functions are linked. The visualisation can be valuable in tracing functional dependencies, but the analysis should nevertheless be based on the description of the functions rather than on the graphical representation. 4. Identify barriers for variability (damping factors) and specify required performance monitoring. Barriers are means to prevent an unwanted event from taking place, or to protect against the consequences of an unwanted event [START_REF] Hollnagel | Barriers and accident prevention[END_REF]). Barriers can be described in terms of barrier systems (the organizational and/or physical structure of the barrier) and barrier functions (the manner by which the barrier achieves its purpose). The four fundamental barrier systems are: (1) physical barrier systems that block the movement or transportation of mass, energy, or information; (2) functional barrier systems that set up pre-conditions that must be met before an action (by human and/ or machine) can be undertaken; (3) symbolic barrier systems that are indications of constraints on action that are physically present; and (4) incorporeal barrier systems that are indications of constraints on action that are not physically present. Besides recommendations for barriers, a FRAM analysis can provide the basis for recommendations on how to monitor performance in order to detect excessive variability. Performance indicators may be developed both for functions and for the couplings between them.

FRAM analysis

The first step of the FRAM accident analysis is to describe the functions that make up the normal departure routine. For a typical civilian flight some of these may include:

• Review of weather and airport data, • Taxi briefing, • Takeoff briefing, • Clearance(s) from ATC,

• Perform a taxi checklist, • Taxi to runway, • Perform a before takeoff checklist,

• Turn onto the runway,

• Takeoff.

The functions should include all those needed to begin the analysis. It is, however, not necessary to begin with a complete list. The analysis may identify further functions to be included, and since the functions are not ordered, e.g., in a sequence or a hierarchy, functions can easily be added or removed at a later time. To illustrate the principle, consider the function Review of weather and airport data.

All US air carrier flights are operated under regulations which require that a certified dispatcher and the captain assume joint responsibility for all pre-flight planning and preparation. Typically, a certified dispatcher will prepare and include all relevant flight information in the form of a flight release document for the crew to review. Additional information usually includes any applicable Notice to Airmen (NOTAMs) which describe changes at the departure and arrival airports or any navigational sources to be used during the flight that have not yet been included in charts or other sources of information. The investigation found no evidence that captain did not review this material. The FRAM analysis normally continues by describing the other functions in the same way. Here we will, however, proceed to look at whether there was any variability in the way that the Review of weather and airport data was carried out in the accident.

One NOTAM describing a portion of a taxiway closed due to construction (taxiway Alpha North of runway 26) was missing from the flight release. This section of taxiway was an important consideration because it changed the taxi route that the pilots were accustomed to.

An additional source of NOTAM information regarding taxiway closures was the pre-recorded Automatic Terminal Information Service (ATIS). This recorded message by air traffic control contains current weather, runways in use and any relevant NOTAMs for the airport. Pilots listen to this broadcast on a specific radio frequency. The NOTAM regarding the taxiway closure was not included in the ATIS broadcast on the morning of the accident as required. The investigation was unable to determine why the controller omitted this information from that specific recording. Even this initial description of Review of weather and airport data makes clear that it depends on at least three other functions, and that at least two of these have a common source of information, cf. Figure 3. The analysis may be continued by looking at the other aspects of the function node, e.g., preconditions or resources, to get a better understanding of how the performance of this function depends on the work situation.

The accident investigation must obviously try to describe all relevant functions on a level of detail that makes it possible to explain the performance variability. For the purpose of illustration, it is reasonable to focus on one function, Taxi to runway, to understand the factors and conditions that resulted in the aircraft being on runway 26 instead of runway 22.

At 06:02 the first officer calls Lexington ground to request taxi clearance to the runway; seconds later ground control clears the flight to "… taxi to runway two two altimeter three zero zero zero and the winds two zero zero at eight." As part of this clearance, the controller is required to give the pertinent information from the new ATIS or require the flight crew to listen to the ATIS broadcast. The controller, however, did not realise that one NOTAM was missing, nor that it had been omitted from the ATIS. After the taxi checklist was completed the captain stated "finish it up your leisure." This set a relaxed tone for the first officer to go through the before-takeoff checklist as he desired. Since this was the first flight of the day, there are several other items on the checklist, which therefore takes a little longer and requires the first officer to work "heads down" much of the time. Right after this there is about 40 seconds of social conversation, which the NTSB referred to as "nonpertinent conversation." This conversation took place where taxiway Alpha made several turns. The above strongly suggests that Taxi to runway should not be described as one function but as several. But even a description on an aggregate level shows that Taxi to runway is rather tightly coupled to several other functions. Figure 4 provides an illustration of that.

Going into a little more detail, Figure 5 is an excerpt from the surface chart the crew had available. It is significant to note that taxiway designation "A4" on the chart was marked on the airport surface with a sign that read "A6". This alone would make it difficult for the crew to detect any discrepancy between where they thought were and where they actually were. The before-takeoff checklist consists of 13 items only one of which is a challenge and response. The rest are action items for the first officer which must be verbally read when complete. This serves as a method to verify that all items were in fact accomplished. One item is the pre-takeoff announcement, where the first officer talked to the passengers over the intercom system. This took about 10 seconds to complete and occurred at the hold-short line for runway 26. Once this item had been completed, the first officer continued to finish the before takeoff checklist. During the entire taxi to this point, the first officer was extremely busy with his required duties. When they arrived at the hold-short sign for runway 26, he apparently assumed that the captain had delivered them to the correct runway. The first officer was unable to see the red runway 26 sign to the left of the aircraft from his position in the cockpit's right seat. The height of the flight deck above the runway sign made it impossible for the first officer to see it once they were stopped at the hold short line impossible. At 06:05, the crew called ready for takeoff. These aspects of ATC information and clearances can be seen as variability in the preconditions of the Taxi to runway function, incomplete charts as variability in resources, and the "nonpertinent conversation" as variability affecting controls of this function. The variability in visibility of taxiway markings, signs, and lighting affects the resources used in Turn onto runway. Another important source of variability was that only a single controller was performing all ATC tasks at Lexington at the time, affecting the time available for ATC functions. Lastly, obviously the preconditions of takeoff availability of sufficient length of unobstructed runway were not met, resulting in the output of achieving V1, rotation and climb out being unsuccessful. By making a similar analysis of other functions, a view gradually emerges of why the accident happened. Due to the size of the final analysis, it cannot be presented here, but Figure 6 illustrates the complexity of the situation and the level of detail that is needed to understand why the accident happened.

Summary and Conclusions

Although it is impossible to go through the complete analysis in this paper, the two functions described above illustrate how the FRAM method step-by-step builds up an explanation of the accident. Previous experience with FRAM has shown that it is often convenient to provide a graphical rendering of the analysis, such as shown in Figure 6. A simple software tool is available for this visual representation directly from the descriptions of the functions. It is, however, important to keep in mind that the substance of the analysis resides in the description and characterisation of the functions, and not in the resulting images. The summary makes clear that the conclusions of the NTSB fall somewhat short of the mark by pointing to the failures of the flightcrew as the primary cause of the accident. As Figures 3,4, and 6 demonstrate, the explanation cannot be reduced to a sequence of failures or mistakes, but must consider the situation and the conditions at the time as a whole, the lack of information, etc. The explanation is important for Step 4 of the investigation where appropriate countermeasures are developed, specifically how performance variability can be observed and dampened when needed. If the explanation is that the flightcrew did not follow procedures, then the obvious recommendation is to strengthen procedure compliance. In the case of this accident, the NTSB recommendations consist mainly of constraining performance to ensure procedure compliance and of improving information presentation in the cockpit as well as outside. The alternative, to manage performance and to control the sources of performance variability, is not considered. As a method, FRAM has a clear theoretical grounding and is easy to learn and use. Since FRAM does not produce a simple sequential description, the administration of the analysis and of the findings can be time consuming. This can quite easily be alleviated by software tools; a prototype of these is already in use, and further developments are underway.

Figure 1 :

 1 Figure 1: Comair flight 5191: Actual, intended, and former taxi paths.

Figure 2 :

 2 Figure 2: A FRAM module describing an activity or function in terms of six aspects.

Figure 3 :

 3 Figure 3: FRAM diagram for Review of weather and airport data function.

Figure 5 :

 5 Figure 5: Lexington Jeppesen Chart. (Not for navigational use)

Figure 4 :

 4 Figure 4: Taxi to runway

Figure 6 :

 6 Figure 6: Important functions and couplings in the Lexington accident.


Marco Pellegrini
email: pellegrini@mail.dm.unipi.it

Chiara Marcolla
email: chiara.marcolla@unitn.it3maxsalacodes@gmail.com

Massimiliano Sala

On the weights of affine-variety codes and some Hermitian codes

Keywords: Affine-variety codes, linear code, distance, minimum-weight word, Hermitian code

For any affine-variety code we show how to construct an ideal whose solutions correspond to codewords with any assigned weight. We use our ideal and a geometric characterization to determine the number of small-weight codewords for some families of Hermitian codes over any Fq. In particular, we determine the number of minimum-weight codewords for all Hermitian codes with d ≤ q. For such codes we also count some other small-weight codewords.

Preliminary results

Let F q be a finite field. Let k ≥ 1. For any ideal I in a polynomial ring F q [X], where X = {x 1 , . . . , x k }, we denote by V(I) ⊂ (F q ) k its variety. For any Z ⊂ (F q ) k we denote by I(Z) ⊂ F q [X] the vanishing ideal of Z.

Let g 1 , . . . , g s ∈ F q [X], we denote by I = g 1 , . . . , g s the ideal generated by the g i 's. Let {x q 1 -x 1 , . . . , x q k -x k } ⊂ I. Then I is zero-dimensional and radical. Let V(I) = {P 1 , P 2 , . . . , P n }. We have an isomorphism of F q vector spaces (an evaluation map): φ : R = F q [x 1 , . . . , x k ]/I -→ (F q ) n f -→ (f (P 1 ), . . . , f (P n )).

Let L ⊆ R be an F q vector subspace of R with dimension r.

Definition 1. The affine-variety code C(I, L) is the image φ(L) and the affine-variety code C ⊥ (I, L) is its dual code.

Our definition is slightly different with respect to that in [START_REF] Fitzgerald | Decoding affine variety codes using Gröbner bases[END_REF]. Let L be linearly generated by b 1 , . . . , b r then the matrix

H =    b 1 (P 1 ) b 1 (P 2 ) . . . b 1 (P n ) . . . . . . • • • . . . b r (P 1 ) b r (P 2 ) . . . b r (P n )   
is a generator matrix for C(I, L) and a parity-check matrix for C ⊥ (I, L). Let z ∈ (F q ) n , z = (z 1 , . . . , zn ). Then z ∈ C(I, L) ⊥ ⇐⇒ H zT = 0 ⇐⇒ n i=1 zi b j (P i ) = 0 j = 1, . . . , r

Proposition 1. Let 1 ≤ w ≤ n. Let J w be the ideal in F q [x 1,1 , . . . x 1,k , . . . , x w,1 , . . . x w,k , z 1 , . . . , z w ] generated by

w i=1 z i b j (P i ) j = 1, . . . , r (3)
g h (x i,1 , . . . x i,k ) i = 1, . . . , w and h = 1, . . . , s

z q-1 i -1 i = 1, . . . , w (4)
1≤l≤k

((x j,l -x i,l ) q-1 -1) 1 ≤ j < i ≤ w. (6)
Then any solution of J w corresponds to a codeword of C ⊥ (I, L) with weight w. Moreover,

A w (C ⊥ (I, L)) = |V(J w )| w! .
Proof. Let σ be a permutation, σ ∈ S n . It induces a permutation σ acting over {x 1,1 , . . . , x 1,k , . . . , x w,1 , . . . x w,k , z 1 , . . . , z w } as σ(x i,l ) = x σ(i),l and σ(z i ) = z σ(i) . It is easy to show that J w is invariant w.r.t. any σ, since each of ( 3), ( 4), ( 5) and ( 6) is so.

Let Q = (x 1,1 , . . . x 1,k , . . . , x w,1 , . . . x w,k , z 1 , . . . , z w ) ∈ V(J w ).
We can associate a codeword to Q in the following way. For each i = 1, . . . , w, P ri = (x i,1 , . . . x i,k ) is in V(I), by [START_REF] Lax | Generic interpolation polynomial for list decoding[END_REF]. We can assume r 1 < r 2 < . . . < r w , via a permutation σ if necessary. Note that (6) ensures that for each (i, j), with i = j, we have P ri = P rj , since there is a l such that x i,l = x j,l . Since z q-1 i = 1 [START_REF] Marcolla | Parole di peso piccolo dei codici hermitiani[END_REF],

z i ∈ F q \{0}. Let c ∈ (F q ) n be c = (0, . . . , 0, z 1 ↑ Pr 1 , 0, . . . , 0, z i ↑ Pr i , 0, . . . , 0, z w ↑ Pr w , 0, . . . , 0).
We have that c ∈ C ⊥ (I, L), since (3) is equal to [START_REF] Geil | Evaluation codes from an affine-variety codes perspective[END_REF]. Reversing the previous argument, we can associate to any codeword, a solution of J w . By invariance of J w , we actually have w! distinct solutions for any codeword. So, to get the number of codewords of weight w, we divide |V(J w )| by w!.

For more recent results on affine-variety codes see [START_REF] Geil | Evaluation codes from an affine-variety codes perspective[END_REF][START_REF] Marcolla | Improved decoding of affine-variety codes[END_REF][START_REF] Lax | Generic interpolation polynomial for list decoding[END_REF].

Hermitian Codes

Hermitian codes are interesting affine-variety codes. They can be defined as follows. Let q be a power of a prime, the Hermitian curve H is the curve defined over F q 2 by the affine equation

x q+1 = y + y q (7)
This curve has genus g = q(q-1)

2

and has n = q 3 rational affine points, denoted by P 1 , . . . , P n . For any x ∈ F q 2 , the equation ( 7) has exactly q distinct solutions in F q 2 . The curve has also one point at infinity P ∞ , so it has q 3 + 1 rational points over F q 2 . Lemma 1. Let L be any vertical line {x = t}, with t ∈ F q 2 . Then L intersects H in q affine points.

Proof. For any t ∈ F q 2 , the equation y q +y = t q+1 has exactly q distinct solutions, since t q+1 ∈ F q and the trace is linear.

Lemma 2. In the affine plane (F q 2 ) 2 , the total number of non-vertical line is q 4 . Of these, (q 4 -q 3 ) intersect the Hermitian curve in (q + 1) points and q 3 are tangent to H, i.e. they intersect H in one point.

Proof. Let L any non-vertical line, L = {y = ax + b}. We have q 2 choice for both a and b, so the total number is q 4 . Then

H ∩ L = {(x, ax + b) | a q x q + b q + ax + b = x q+1 }.
Let c = a q+1 + b q + b. We have two distinct cases:

c = 0. Then a q x q + b q + ax + b = x q+1 becomes a q x q -a q+1 + ax = x q+1 , which gives x = a q , that is, L is tangent. -c = 0. Then a q x q + b q + ax + b = x q+1 becomes x q+1 -a q x q + a q+1 -ax = c, which gives (x -a q ) q+1 = c. Since c = (α q+1 ) r for 1 ≤ r ≤ q -1, we have x = a q + α r+i(q-1) for any 0 ≤ i ≤ q.

The number of pairs (a, b) satisfying c = 0 is q 3 and so the others are (q 4 -q 3 ).

Let I = y q + y -x q+1 , x q 2 -x, y q 2 -y ⊂ F q 2 [x, y] and let R = F q 2 [x, y]/I. We take L ⊆ R generated by

B m,q = {x r y s + I | qr + (q + 1)s ≤ m, 0 ≤ s ≤ q -1, 0 ≤ r ≤ q 2 -1},
where m is an integer 0 ≤ m ≤ q 3 + q 2 -q -2. For simplicity, we also write x r y s for x r y s + I. We consider the evaluation map (1) φ : R → (F q 2 ) n . We have the following affine-variety codes C(I, L) = Span F q 2 φ(B m,q ) and we denote by C(m, q) = (C(I, L)) ⊥ its dual. Then the affine-variety code C(m, q) is called the Hermitian code with parity-check matrix

H H =    f 1 (P 1 ) . . . f 1 (P n ) . . . . . . . . . f i (P 1 ) . . . f i (P n )    where f j ∈ B m,q (8)
The Hermitian codes can be divided in four phases ( [START_REF] Høholdt | Algebraic geometry of codes[END_REF]), any having specific explicit formulae linking their dimension and their distance, as in Table 1.

In the remainder of this paper we focus on the first phase. This case can be characterised by the condition d ≤ q.

0 ≤ m ≤ q 2 -2 m = aq + b 0 ≤ b ≤ a ≤ q -1 b ≤ q -2 a + 1 a > b a + 2 a = b ⇐⇒ d ≤ q q 3 -a(a+1) 2 -(b + 1) 2 q 2 -1 ≤ m ≤ 2q 2 -2q -2 m = 2q 2 -q -aq -b -1 1 ≤ a ≤ q -1 0 ≤ b ≤ q -1 (q -a)q -b a < b (q -a)q a ≥ b q 3 -m + q(q-1) 2 - 1
3 2q 2 -2q -1 ≤ m ≤ q 3 -1 m -q 2 + q + 1 q 3 -m + q(q-1) 2 -1 4
q 3 ≤ m < q 3 + q 2 -q -1 m = q 3 + aq + b 0 ≤ a ≤ q -1, 0 ≤ b ≤ q -2 q 3 + aq + b -2g a < b q 3 + aq + a + 1 -2g b ≤ a k ≥ g -aq -b 2.

Corner Codes and Edge Codes

The first-phase Hermitian codes can be either edge codes or corner codes.

Definition 2. Let 2 ≤ d ≤ q and let 1 ≤ j ≤ d -1. Let L d 0 = {1, x, . . . , x d-2 }, L d 1 = {y, xy, . . . , x d-3 y}, . . . , L d d-2 = {y d-2 }. Let l d 1 = x d-1 , . . . , l d j = x d-j y j-1 .
-

If B m,q = L d 0 ⊔ • • • ⊔ L d d-2
, then we say that C(m, q) is a corner code and we denote it by

H 0 d . -If B m,q = L d 0 ⊔ • • • ⊔ L d d-2 ⊔ {l d 1 , .
. . , l d j }, then we say that C(m, q) is an edge code and we denote it by H j d .

From classical results in Table 1 we have

Theorem 1. Let 2 ≤ d ≤ q, 1 ≤ j ≤ d -1. Then d(H 0 d ) = d(H j d ) = d, dim F q 2 (H 0 d ) = n - d(d -1) 2 , dim F q 2 (H j d ) = n - d(d -1) 2 -j
In other words, all φ(x r y s ) are linearly independent (i.e. H has maximal rank) and for any distance d there are exactly d Hermitian codes (one corner code and d -1 edge codes). We can represent the above codes as in the following picture, where we consider the five smallest non-trivial codes (for any q ≥ 3).

H 0 2 is a [n, n -1, 2] code. B m,q = L 2 0 = {1}, so the parity-check matrix of H 0 2 is (1, . . . , 1). H 1 2 is a [n, n -2, 2] code. B m,q = L 2 0 ⊔ l 2 1 = {1, x} H 0 3 is a [n, n -3, 3] code. B m,q = L 3 0 ⊔ L 3 1 = {1, x, y} H 1 3 is a [n, n -4, 3] code. B m,q = L 3 0 ⊔ L 3 1 ⊔ l 3 1 = {1, x, y, x 2 } H 2 3 is a [n, n -5, 3] code. Bm,q = L 3 0 ⊔ L 3 1 ⊔ {l 3 1 , l 3 2 } = {1, x, y, x 2 , xy}
3 Our results on the number of words

Ideal J w of Proposition 1 for C(m, q) is J w = w i=1 z i x r i y s i x r y s ∈Bm,q , x q+1 i -y q i -y i i=1,...,w , z q 2 -1 i -1 i=1,...,w , x q 2 i -x i i=1,...,w , y q 2 i -y i i=1,...,w , 1≤i<j≤w ((x i -x j ) q 2 -1 -1)((y i -y j ) q 2 -1 -1 . (9)
Let w ≥ v ≥ 1. Let Q = (x 1 , . . . , x w , y 1 , . . . , y w , z 1 , . . . , z w ) ∈ V(J w ). We say that Q is in v-block position if we can partition {1, . . . , n} in v blocks I 1 , . . . , I v such that

x i = x j ⇐⇒ ∃ 1 ≤ h ≤ v such that i, j ∈ I h .
(a) u = 1 v > d w ≥ d + 1 (b) v = 1, that is, x1 = • • • = xw If d = 2 and w = 2, then (a) holds for H 1 2 . Proof. We denote for all 1 ≤ h ≤ v X h = xi if i ∈ I h , Z h = i∈I h zi , Y h,δ = i∈I h ȳδ i zi with 1 ≤ δ ≤ u -1 (a) u = 1. We have to prove, by contradiction, that v > d. Let v ≤ d. Since Q ∈ V(J w ), then L w 0 (Q) = l w 1 (Q) = 0, that is 0 = w i=1 xr i zi = i∈I h X r h zi = v h=1 X r h Z h 0 ≤ r ≤ d -1. ( 10
)
We can consider only the first v equations of (10), because v ≤ d, so

v h=1 X r h Z h = 0 0 ≤ r ≤ v -1 ⇐⇒      1 . . . 1 X 1 . . . X v . . . . . . . . . X v-1 1 . . . X v-1 v         Z 1 . . . Z v    = 0 (11)
The above matrix is a Vandermonde matrix, so it has maximal rank v. Therefore, the solution of ( 11) is (Z 1 , . . . , Z v ) = (0, . . . , 0). Since u = 1, then

Z 1 = z 1 = 0, which contradicts z i ∈ F q 2 \ {0}. So if v > d then w ≥ d + 1.
(b) u ≥ 2. We suppose by contradiction that v ≥ 2. We consider Proposition 1. A subset of equations of condition (3) is the following system, where 0

≤ r ≤ v          w i=1 xr i zi = 0 w i=1 xr i ȳi zi = 0 . . . w i=1 xr i ȳu-1 i zi = 0 ⇐⇒          v h=1 X r h Z h = 0 v h=1 X r h Y h,1 = 0 . . . v h=1 X r h Y h,u-1 = 0 (12)
In fact system (12) is a subset of (3) if and only if deg(

x v i ȳu-1 i ) ≤ d -1 for any i = 1, . . . , w. That is, v + (u -1) ≤ d -1 ⇐⇒ v + u ≤ d.
To verify it, since v ≥ 2, it is sufficient to apply Lemma 3 and we obtain u + v ≤ ⌊ w 2 ⌋ + 2 ≤ ⌊ 2d-3 2 ⌋ + 2 = d. By system (12) we obtain u Vandermonde matrices (all having rank v). Therefore the solutions of these matrices are zero-solutions. So, in the particular case h = 1, we have

Z 1 = Y 1,1 = . . . = Y 1,u-1 = 0, that is          u i=0 zi = 0 u i=0 ȳi zi = 0 . . . u i=0 ȳu-1 i zi = 0 ⇐⇒      1 . . . 1 ȳ1 . . . ȳu . . . . . . . . . ȳu-1 1 . . . ȳu-1 u         z1 . . . zu    = 0
Since the ȳi 's are all distinct (because the xi 's are all equal), we obtain a Vandermonde matrix, and so z1 =

• • • = zu = 0, but it is impossible because zi ∈ F q 2 \ {0}. Therefore v = 1.
The case H 1 2 is trivial.

Corollary 1. Let us consider the edge code

H j d with 1 ≤ j ≤ d -1. If Q = (x 1 , . . . , x d , y 1 , . . . , y d , z 1 , . . . , z d ) ∈ V(J d ), then x1 = • • • = xd .
In other words, the points that correspond to a minimum-weight word lie in the intersection of the Hermitian curve H and one vertical line. Whereas if d ≥ 4 and Q = (x 1 , . . . , x d+1 , y 1 , . . . , y d+1 , z 1 , . . . , z d+1 ) ∈ V(J d+1 ), then one of the following cases holds Theorem 2. The number of minimum weight words of an edge code H j d is

A d = q 2 (q 2 -1) q d .
Proof. By Proposition 1 we know that J d represents all words of minimum weight. The first set of ideal basis (9) has exactly d(d-1)

2

+ j equations, where 1 ≤ j ≤ d -1. So, if j = 1, this set implies the following system:

8 > > > > > > > > > < > > > > > > > > > : z1 + • • • + zd = 0 x1 z1 + • • • + xd zd = 0 ȳ1 z1 + • • • + ȳd zd = 0 x2 1 z1 + • • • + x2 d zd = 0 . . . ȳd-2 1 z1 + • • • + ȳd-2 d zd = 0 xd-1 1 z1 + • • • + xd-1 d zd = 0 (13)
Whereas, if j > 1 then we have to add the first j -1 of following equations:

8 > < > : xd-2 1 ȳ1 z1 + • • • + xd-2 d ȳd zd = 0 . . . x1 ȳd-2 1 z1 + • • • + xd ȳd-2 d zd = 0
But x1 = . . . = xd , since we are in the hypotheses of Corollary 1. So the system becomes

8 > > > < > > > : z1 + • • • + zd = 0 ȳ1 z1 + • • • + ȳd zd = 0 . . . ȳd-2 1 z1 + • • • + ȳd-2 d zd = 0 (14)
We have q 2 choice for the xi 's and, by Lemma 1, we have

" q d « d! different ȳi 's,
since for any choice of the xi 's there are exactly q possible value for the ȳi 's, but we need just d of them and any permutation of these will be again a solution. Now we have to calculate the solutions for the zi 's. We write the system (14) as a matrix, which is a Vandermonde matrix with rank d -1. This means that the solution space has linear dimension 1 because 1 = d -(d -1) = number of variables -rank of matrix. So the solutions are (a 1 α, a 2 α, . . . , a d-1 α) with α ∈ F * q 2 , where a j are fixed since they depend on ȳi . So the number of the z's is

|F * q 2 | = q 2 -1, then A d = 1 d! q 2 (q 2 -1) q d d ! .
We consider a corner code. We have the following geometric characterisation.

Proposition 2. Let us consider the corner code H 0 d , then the points (x1, ȳ1), . . . , (x d , ȳd ) corresponding to minimum-weight words lie on the same line.

Proof. The minimum-weight words of a corner code have to verify the first condition set of J w , which has d(d-1) 2 equations. That is

8 > > > > > > > < > > > > > > > : z1 + • • • + zd = 0 x1 z1 + • • • + xd zd = 0 ȳ1 z1 + • • • + ȳd zd = 0 x2 1 z1 + • • • + x2 d zd = 0 . . . ȳd-2 1 z1 + • • • + ȳd-2 d zd = 0 (15)
This system is the same as ( 13), but with a missing equation. This means that (15) have all solutions of system (13) plus other solutions. If we consider a subset of (15):

8 > > > > > < > > > > > : z1 + • • • + zd = 0 x1 z1 + • • • + xd zd = 0 x2 1 z1 + • • • + x2 d zd = 0 . . . xd-2 1 z1 + • • • + xd-2 d zd = 0 (16)
we note that the zi 's are all non-zero if all xi 's are distinct (or all are equal). Therefore, we have only two possibilities for the xi 's: either are all different or they coincide. The same consideration is true for the ȳi 's, in fact when we consider (15) and we exchange x with y, we obtain again (15). So we have an alternative:

-The xi 's are all equal or the ȳi 's are all equal, so our proposition is true.

-The xi 's and the ȳi 's are all distinct. We prove that they line in the intersection of a non-horizontal line. Let y = βx + λ be a non-vertical line passing for two points in a minimum weight configuration. We can do an affine transformation of this type:

x = x ′ y = y ′ + ax ′ a ∈ F q 2
such that some of the y ′ 's are equal and not all y's are coincident. Substituting the above transformation in (15) and applying some operations between the equations, we obtain a system that is equivalent to (15). But this new system have all y ′ 's equal (or all distinct), so the y ′ 's have to be all equal.

Hence we can conclude that the points lie on the same line.

We finally prove the following theorem:

Theorem 3. The number of words having weight d of a corner code H 0 d is

A d = q 2 (q 2 -1) q d -1 q 3 -d + 1 d .
Proof. Again, the points corresponding to minimum-weight words of a corner code have to verify (15). By above proposition, we know that these points lie in the intersections of any line and the Hermitian curve H.

Let Q = (x 1 , . . . , x d , y 1 , . . . , y d , z 1 , . . . , z d ) ∈ V(J d ) such that x 1 = . . . = x d ,
that is, the points (x i , ȳi ) lie on a vertical line. We know that the number of such Q's is q 2 (q 2 -1) q d d !. Now we have to calculate the number of solutions Q ∈ V(J d ) such that (x i , ȳi ) lie on a non-vertical line.

By Lemma 2 we know that the number of the ȳi 's and xi 's is (q 4 -q

3 ) q + 1 d d !,
since for any choice of the ȳi 's there are exactly q + 1 possible values for the xi 's, but we need just d of this (and the system is invariant). As regards the number of the zi 's, we have to calculate the number of solutions of system (15). We apply an affine transformation to the system (15) to obtain a horizontal line, that is, to have all the ȳi 's different and all the xi 's are equal, so we obtain a system equivalent to system (14). Therefore we have a Vandermonde matrix, hence the number of the zi 's is q 2 -1. So

A d = 1 d! " q 2 (q 2 -1) " q d « d ! + (q 4 -q 3 )(q 2 -1) " q + 1 d « d ! « = q 2 (q 2 -1) " q d -1 « q 3 -d+1 d .

Words having weight d + 1

In this section we state more theorems for edge and corner codes taken from [START_REF] Marcolla | Parole di peso piccolo dei codici hermitiani[END_REF].

We study the case when the x i 's coincide or when the y i 's coincide.

Theorem 4. The number of words of weight d + 1 with y 1 = . . . = y d+1 of a corner code H 0 d is:

A d+1 = (q 2 -q)(q 4 -(d + 1)q 2 + d) q + 1 d + 1 .

Whereas of an edge code H j d with 1 ≤ j ≤ d -1 is:

A d+1 = (q 2 -1)(q 2 -q) q + 1 d + 1 .

Theorem 5. The number of words of weight d + 1 with x 1 = . . . = x d+1 of a corner code H 0 d and of an edge code H j d is:

A d+1 = q 2 (q 4 -(d + 1)q 2 + d) q d + 1

.

The proofs are similar to those of the statements as in Section 3 and so are omitted. In other cases, we have to consider intersection of the curve with higher degree curves and the formulae get more complicated. We list without proof a few of these special cases: Theorem 6. Let us consider the corner code H 0 3 . Let us consider 4-weight codewords with x i = x j for any i, j = 1, . . . , 4. Then y1 = y2 = y3 = y4 A4 = 0 y1 = y2 = y3 = y4 A4 = 1 8 q 2 (q 2 -1) 2 (q -2)(q 3 + 2q 2 -2q + 1) y1 = y2 = y3, y4 and y3 = y4 A4 > 1 4 q 2 (q 2 -1) 2 (2q 6 -7q 5 -6q 4 + 19q 3 -9q 2 -4q + 4) A4 < 1 4 q 2 (q 2 -1) 2 (2q 6 -3q 5 -11q 4 + 9q 3 + 25q 2 -14q + 4)

Theorem 7. Let us consider the edge codes H 1 3 and H 2 3 . Let us consider 4-weight codewords with x i = x j for any i, j = 1, . . . , 4. Then there are no such words if y 1 = y 2 = y 3 = y 4 or y 1 = y 2 = y 3 = y 4 . In particular, if y 1 = y 2 = y 3 , y 4 and y 3 = y 4 , H 2 3 has no such words and H 1 3 has at most 1 4 q 2 (q 2 -1) 2 (2q 5 -3q 4 -10q 3 + 10q 2 + 15q -4) such words. Remark 1. We are identifying general conditions for algebraic-geometry codes satisfying Proposition 2, jointly with C. Fontanari.

WLemma 3 .

 3 .l.o.g. we can assume |I 1 | ≤ • • • ≤ |I v | and I 1 = {1, . . . , u}. It is simple to prove the following numerical lemma. We always have u+ v ≤ w + 1. If u ≥ 2 and v ≥ 2, then v ≤ ⌊ w 2 ⌋ and u + v ≤ ⌊ w 2 ⌋ + 2.We need the following technical lemma[START_REF] Pellegrini | On the weight distribution of some Goppa AG codes[END_REF]. Lemma 4. Let us consider the edge code H j d with 1 ≤ j ≤ d -1 and 3 ≤ d ≤ w ≤ 2d -3. Let Q = (x 1 , . . . , x d , y 1 , . . . , y d , z 1 , . . . , z d ) be a solution of J w in v-block position, with v ≤ w, then exactly one of the following cases holds

  (a) xi = xj con i = j per 1 ≤ i, j ≤ d + 1 (b) x1 = • • • = xd+1 . Proof. We are in the hypotheses of Lemma 4. So if w = d then u = 1. So v = 1. Whereas, if w = d + 1 then there are two possibilities. In case (a) of Lemma 4, all the xi 's are different, since v = d + 1, or, case (b), x1 = • • • = xd+1 . Now we can prove the following theorem.

Table 1 .

 1 The four phases of Hermitian codes

	Phase	m	Distance d	Dimension k
	1

Acknowledgements

The first two authors would like to thank their supervisor: the third author. The authors would like to thank: C. Fontanari, T. Mora and C. Traverso.