Rodolphe Lepigre
email: rodolphe.lepigre@univ-smb.fr

A Classical Realizability Model for a Semantical Value Restriction

We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which are used for specifying program properties and for encoding dependent products. The main challenge arises from the lack of expressiveness of dependent products due to the value restriction. To circumvent this limitation we relax the syntactic restriction and only require equivalence to a value. The consistency of the system is obtained semantically by constructing a classical realizability model in three layers (values, stacks and terms).

Introduction

In this work we consider a new type system for a call-by-value language, with control operators, polymorphism and dependent products. It is intended to serve as a theoretical basis for a proof assistant focusing on program proving, in a language similar to OCaml or SML. The proof mechanism relies on dependent products and equality types t ≡ u, where t and u are (possibly untyped) terms of the language. Equality types are interpreted as ⊤ if the denoted equivalence holds and as ⊥ otherwise.

In our system, proofs are written using the same language as programs. For instance, a pattern-matching corresponds to a case analysis in a proof, and a recursive call to the use of an induction hypothesis. A proof is first and foremost a program, hence we may say that we follow the "program as proof" principle, rather than the usual "proof as program" principle. In particular, proofs can be composed as programs and with programs to form proof tactics.

Programming in our language is similar to programming in any dialect of ML. For example, we can define the type of unary natural numbers, and the corresponding addition function. We can then prove properties of addition such as add Z[] n ≡ n for all n in nat. This property can be expressed using a dependent product over nat and an equality type. The term 8< (to be pronounced "scissors") can be introduced whenever the goal is derivable from the context with equational reasoning. Our first proof is immediate since we have add Z[] n ≡ n by definition of add.

Let us now show that add n Z[] ≡ n for every n in nat. Although the statement of this property is similar to the previous one, its proof is slightly more complex and requires case analysis and induction. In the S[nn] case, the induction hypothesis (i.e. add nn Z[] ≡ nn) is obtained by a recursive call. It is then used to conclude the proof using equational reasoning. Note that in our system, programs that are considered as proofs need to go through a termination checker. Indeed, a looping program could be used to prove anything otherwise. The proofs addZeroN and addNZero are obviously terminating, and hence valid.

Several difficulties arise when combining call-by-value evaluation, side-effects, dependent products and equality over programs. Most notably, the expressiveness of dependent products is weakened by the value restriction: elimination of dependent product can only happen on arguments that are syntactic values. In other words, the typing rule Γ ⊢ t : Π a:A B Γ ⊢ u : A Γ ⊢ t u : B[a := u] cannot be proved safe if u is not a value. This means, for example, that we cannot derive a proof of add (add Z[] Z[]) Z[] ≡ add Z[] Z[] by applying addNZero (which has type Πn:nat (add n Z[] ≡ n)) to add Z[] Z[] since it is not a value. The restriction affects regular programs in a similar way. For instance, it is possible to define a list concatenation function append with the following type.

Πn:nat Πm:nat List(n) ⇒ List(m) ⇒ List(add n m) However, the append function cannot be used to implement a function concatenating three lists. Indeed, this would require being able to provide append with a non-value natural number argument of the form add n m.

Surprisingly, the equality types and the underlying observational equivalence relation provide a solution to the lack of expressiveness of dependent products. The value restriction can be relaxed to obtain the rule

Γ, u ≡ v ⊢ t : Π a:A B Γ, u ≡ v ⊢ u : A Γ, u ≡ v ⊢ t u : B[a := u]
which only requires u to be equivalent to some value v. The same idea can be applied to every rule requiring value restriction. The obtained system is conservative over the one with the syntactic restriction. Indeed, finding a value equivalent to a term that is already a value can always be done using the reflexivity of the equivalence relation.

Although the idea seems simple, proving the soundness of the new typing rules semantically is surprisingly subtle. A model is built using classical realizability techniques in which the interpretation of a type A is spread among two sets: a set of values A and a set of terms A ⊥⊥ . The former contains all values that should have type A. For example, nat should contain the values of the form S[S[...Z[]...]]. The set A ⊥⊥ is the completion of A with all the terms behaving like values of A (in the observational sense). To show that the relaxation of the value restriction is sound, we need the values of A ⊥⊥ to also be in A . In other words, the completion operation should not introduce new values. To obtain this property, we need to extend the language with a new, non-computable instruction internalizing equivalence. This new instruction is only used to build the model, and will not be available to the user (nor will it appear in an implementation).

About effects and value restriction

A soundness issue related to side-effects and call-by-value evaluation arose in the seventies with the advent of ML. The problem stems from a bad interaction between side-effects and Hindley-Milner polymorphism. It was first formulated in terms of references [30, section 2], and many alternative type systems were designed (e.g. [START_REF] Damas | Principal type-schemes for functional programs[END_REF][START_REF] Leroy | Polymorphism by name for references and continuations[END_REF][START_REF] Leroy | Polymorphic type inference and assignment[END_REF][START_REF] Tofte | Type inference for polymorphic references[END_REF]). However, they all introduced a complexity that contrasted with the elegance and simplicity of ML's type system (for a detailed account, see [31, section 2] and [5, section 2]).

A simple and elegant solution was finally found by Andrew Wright in the nineties. He suggested restricting generalization in let-bindings1 to cases where the bound term is a syntactic value [START_REF] Wright | Simple imperative polymorphism[END_REF][START_REF] Wright | A syntactic approach to type soundness[END_REF]. In slightly more expressive type systems, this restriction appears in the typing rule for the introduction of the universal quantifier. The usual rule

Γ ⊢ t : A X ∈ F V (Γ ) Γ ⊢ t : ∀X A
cannot be proved safe (in a call-by-value system with side-effects) if t is not a syntactic value. Similarly, the elimination rule for dependent product (shown previously) requires value restriction. It is possible to exhibit a counter-example breaking the type safety of our system if it is omitted [START_REF] Lepigre | A realizability model for a semantical value restriction[END_REF].

In this paper, we consider control structures, which have been shown to give a computational interpretation to classical logic by Timothy Griffin [START_REF] Griffin | A formulae-as-types notion of control[END_REF]. In 1991, Robert Harper and Mark Lillibridge found a complex program breaking the type safety of ML extended with Lisp's call/cc [START_REF] Harper | ML with callcc is unsound[END_REF]. As with references, value restriction solves the inconsistency and yields a sound type system. Instead of using control operators like call/cc, we adopt the syntax of Michel Parigot's λµ-calculus [START_REF] Parigot | λµ-calculus: An algorithmic interpretation of classical natural deduction[END_REF]. Our language hence contains a new binder µα t capturing the continuation in the µ-variable α. The continuation can then be restored in t using the syntax u * α2 . In the context of the λµ-calculus, the soundness issue arises when evaluating t (µα u) when µα u has a polymorphic type. Such a situation cannot happen with value restriction since µα u is not a value.

Main results

The main contribution of this paper is a new approach to value restriction. The syntactic restriction on terms is replaced by a semantical restriction expressed in terms of an observational equivalence relation denoted (≡). Although this approach seems simple, building a model to prove soundness semantically (theorem 6) is surprisingly subtle. Subject reduction is not required here, as our model construction implies type safety (theorem 7). Furthermore our type system is consistent as a logic (theorem 8).

In this paper, we restrict ourselves to a second order type system but it can easily be extended to higher-order. Types are built from two basic sorts of objects: propositions (the types themselves) and individuals (untyped terms of the language). Terms appear in a restriction operator A ↾ t ≡ u and a membership predicate t ∈ A. The former is used to define the equality types (by taking A = ⊤) and the latter is used to encode dependent product.

Π a:A B := ∀a(a ∈ A ⇒ B)
Overall, the higher-order version of our system is similar to a Curry-style HOL with ML programs as individuals. It does not allow the definition of a type which structure depends on a term (e.g. functions with a variable number of arguments). Our system can thus be placed between HOL (a.k.a. F ω ) and the pure calculus of constructions (a.k.a. CoC) in (a Curry-style and classical version of) Barendregt's λ-cube.

Throughout this paper we build a realizability model à la Krivine [START_REF] Krivine | Realizability in classical logic[END_REF] based on a call-by-value abstract machine. As a consequence, formulas are interpreted using three layers (values, stacks and terms) related via orthogonality (definition 9). The crucial property (theorem 4) for the soundness of semantical value restriction is that

φ ⊥⊥ ∩ Λ v = φ
for every set of values φ (closed under (≡)). Λ v denotes the set of all values and φ ⊥ (resp. φ ⊥⊥ ) the set of all stacks (resp. terms) that are compatible with every value in φ (resp. stacks in φ ⊥ ). To obtain a model satisfying this property, we need to extend our programming language with a term δ v,w which reduction depends on the observational equivalence of two values v and w.

Related work

To our knowledge, combining call-by-value evaluation, side-effects and dependent products has never been achieved before. At least not for a dependent product fully compatible with effects and call-by-value. For example, the Aura language [START_REF] Jia | AURA: a programming language for authorization and audit[END_REF] forbids dependency on terms that are not values in dependent applications.

Similarly, the F ⋆ language [START_REF] Swamy | Secure distributed programming with value-dependent types[END_REF] relies on (partial) let-normal forms to enforce values in argument position. Daniel Licata and Robert Harper have defined a notion of positively dependent types [START_REF] Licata | Positively dependent types[END_REF] which only allow dependency over strictly positive types. Finally, in language like ATS [START_REF] Xi | Applied Type System[END_REF] and DML [START_REF] Xi | Dependent types in practical programming[END_REF] dependent types are limited to a specific index language.

The system that seems the most similar to ours is NuPrl [START_REF] Constable | Implementing mathematics with the Nuprl proof development system[END_REF], although it is inconsistent with classical reasoning. NuPrl accommodates an observational equivalence (∼) (Howe's "squiggle" relation [START_REF] Howe | Equality in lazy computation systems[END_REF]) similar to our (≡) relation. It is partially reflected in the syntax of the system. Being based on a Kleene style realizability model, NuPrl can also be used to reason about untyped terms.

The central part of this paper consists in a classical realizability model construction in the style of Jean-Louis Krivine [START_REF] Krivine | Realizability in classical logic[END_REF]. We rely on a call-by-value presentation which yields a model in three layers (values, terms and stacks). Such a technique has already been used to account for classical ML-like polymorphism in call-by-value in the work of Guillaume Munch-Maccagnoni [START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF] 3 . It is here extended to include dependent products.

The most actively developed proof assistants following the Curry-Howard correspondence are Coq and Agda [START_REF]The Coq development team: The Coq proof assistant reference manual[END_REF][START_REF] Norell | Dependently Typed Programming in Agda[END_REF]. The former is based on Coquand and Huet's calculus of constructions and the latter on Martin-Löf's dependent type theory [START_REF] Coquand | The calculus of constructions[END_REF][START_REF] Martin-Löf | Constructive mathematics and computer programming[END_REF]. These two constructive theories provide dependent types, which allow the definition of very expressive specifications. Coq and Agda do not directly give a computational interpretation to classical logic. Classical reasoning can only be done through the definition of axioms such as the law of the excluded middle. Moreover, these two languages are logically consistent, and hence their type-checkers only allow terminating programs. As termination checking is a difficult (and undecidable) problem, many terminating programs are rejected. Although this is not a problem for formalizing mathematics, this makes programming tedious.

The TRELLYS project [START_REF] Casinghino | Combining proofs and programs in a dependently typed language[END_REF] aims at providing a language in which a consistent core can interact with type-safe dependently-typed programming with general recursion. Although the language defined in [START_REF] Casinghino | Combining proofs and programs in a dependently typed language[END_REF] is call-by-value and allows effect, it suffers from value restriction like Aura [START_REF] Jia | AURA: a programming language for authorization and audit[END_REF]. The value restriction does not appear explicitly but is encoded into a well-formedness judgement appearing as the premise of the typing rule for application. Apart from value restriction, the main difference between the language of the TRELLYS project and ours resides in the calculus itself. Their calculus is Church-style (or explicitly typed) while ours is Curry-style (or implicitly typed). In particular, their terms and types are defined simultaneously, while our type system is constructed on top of an untyped calculus.

Another similar system can be found in the work of Alexandre Miquel [START_REF] Miquel | Le Calcul des Constructions Implicites : Syntaxe et Sémantique[END_REF], where propositions can be classical and Curry-style. However the rest of the language remains Church style and does not embed a full ML-like language. The PVS system [START_REF] Owre | PVS: combining specification, proof checking, and model checking[END_REF] is similar to ours as it is based on classical higher-order logic. However this tool does not seem to be a programming language, but rather a specification language coupled with proof checking and model checking utilities. It is nonetheless worth mentioning that the undecidability of PVS's type system is handled by generating proof obligations. Our system will take a different approach and use a non-backtracking type-checking and type-inference algorithm.

Syntax, Reduction and Equivalence

The language is expressed in terms of a Krivine Abstract Machine [START_REF] Krivine | A call-by-name lambda-calculus machine[END_REF], which is a stack-based machine. It is formed using four syntactic entities: values, terms, stacks and processes. The distinction between terms and values is specific to the call-by-value presentation, they would be collapsed in call-by-name. We require three distinct countable sets of variables:

-V λ = {x, y, z...} for λ-variables, -V µ = {α, β, γ...} for µ-variables (also called stack variables) and -V ι = {a, b, c...} for term variables. Term variables will be bound in formulas, but never in terms.

We also require a countable set L = {l, l 1 , l 2 ...} of labels to name record fields and a countable set C = {C, C 1 , C 2 ...} of constructors.

Definition 1. Values, terms, stacks and processes are mutually inductively defined by the following grammars. The names of the corresponding sets are displayed on the right.

v, w ::

= x | λx t | C[v] | {l i = v i } i∈I (Λ v ) t, u ::= a | v | t u | µα t | p | v.l | case v [C i [x i ] → t i ] i∈I | δ v,w (Λ) π, ρ ::= α | v.π | [t]π (Π) p, q ::= t * π (Λ × Π)
Terms and values form a variation of the λµ-calculus [START_REF] Parigot | λµ-calculus: An algorithmic interpretation of classical natural deduction[END_REF] enriched with ML-like constructs (i.e. records and variants). For technical purposes that will become clear later on, we extend the language with a special kind of term δ v,w . It will only be used to build the model and is not intended to be accessed directly by the user. One may note that values and processes are terms. In particular, a process of the form t * α corresponds exactly to a named term [α]t in the most usual presentation of the λµ-calculus. A stack can be either a stack variable, a value pushed on top of a stack, or a stack frame containing a term on top of a stack. These two constructors are specific to the call-by-value presentation, only one would be required in call-by-name.

Remark 1. We enforce values in constructors, record fields, projection and case analysis. This makes the calculus simpler because only β-reduction will manipulate the stack. We can define syntactic sugars such as the following to hide the restriction from the programmer.

t.l := (λx x.l) t C[t] := (λx C[x]) t
Definition 2. Given a value, term, stack or process ψ we denote

F V λ (ψ) (resp. F V µ (ψ), T V (ψ)
) the set of free λ-variables (resp. free µ-variables, term variables) contained in ψ. We say that ψ is closed if it does not contain any free variable of any kind. The set of closed values and the set of closed terms are denoted Λ * v and Λ * respectively.

Remark 2. A stack, and hence a process, can never be closed as they always at least contain a stack variable.

Call-by-value reduction relation

Processes form the internal state of our abstract machine. They are to be thought of as a term put in some evaluation context represented using a stack. Intuitively, the stack π in the process t * π contains the arguments to be fed to t. Since we are in call-by-value the stack also handles the storing of functions while their arguments are being evaluated. This is why we need stack frames (i.e. stacks of the form [t]π). The operational semantics of our language is given by a relation (≻) over processes.

Definition 3. The relation (≻) ⊆ (Λ × Π) 2 is defined as the smallest relation satisfying the following reduction rules.

t u * π ≻ u * [t]π v * [t]π ≻ t * v.π λx t * v.π ≻ t[x := v] * π µα t * π ≻ t[α := π] * π p * π ≻ p {l i = v i } i∈I .l k * π ≻ v k * π k ∈ I case C k [v] [C i [x i ] → t i ] i∈I * π ≻ t k [x k := v] * π k ∈ I
We will denote (≻ + ) its transitive closure, (≻ * ) its reflexive-transitive closure and (≻ k ) its k-fold application.

The first three rules are those that handle β-reduction. When the abstract machine encounters an application, the function is stored in a stack-frame in order to evaluate its argument first. Once the argument has been completely computed, a value faces the stack-frame containing the function. At this point the function can be evaluated and the value is stored in the stack ready to be consumed by the function as soon as it evaluates to a λ-abstraction. A capture-avoiding substitution can then be performed to effectively apply the argument to the function.

The fourth and fifth rules rules handle the classical part of computation. When a µ-abstraction is reached, the current stack (i.e. the current evaluation context) is captured and substituted for the corresponding µ-variable. Conversely, when a process is reached, the current stack is thrown away and evaluation resumes with the process. The last two rules perform projection and case analysis in the expected way. Note that for now, states of the form δ v,w * π are unaffected by the reduction relation.

Remark 3.

For the abstract machine to be simpler, we use right-to-left call-byvalue evaluation, and not the more usual left-to-right call-by-value evaluation.

Lemma 1. The reduction relation (≻) is compatible with substitutions of variables of any kind. More formally, if p and q are processes such that p ≻ q then:

-for all x ∈ V λ and v ∈ Λ v , p[x := v] ≻ q[x := v], -for all α ∈ V µ and π ∈ Π, p[α := π] ≻ q[α := π], -for all a ∈ V ι and t ∈ Λ, p[a := t] ≻ q[a := t].
Consequently, if σ is a substitution for variables of any kind and if p ≻ q (resp. p ≻ * q, p ≻ + q, p ≻ k q) then pσ ≻ qσ (resp. pσ ≻ * qσ, pσ ≻ + qσ, pσ ≻ k qσ).

Proof. Immediate case analysis on the reduction rules.

We are now going to give the vocabulary that will be used to describe some specific classes of processes. In particular we need to identify processes that are to be considered as the evidence of a successful computation, and those that are to be recognised as expressing failure. Definition 4. A process p ∈ Λ × Π is said to be:

final if there is a value v ∈ Λ v and a stack variable α ∈ V µ such that p = v * α, -δ-like if there are values v, w ∈ Λ v and a stack π ∈ Π such that p = δ v,w * π, -blocked if there is no q ∈ Λ × Π such that p ≻ q, -stuck if it is not final nor δ-like, and if for every substitution σ, pσ is blocked, -non-terminating if there is no blocked process q ∈ Λ × Π such that p ≻ * q.

Lemma 2. Let p be a process and σ be a substitution for variables of any kind. If p is δ-like (resp. stuck, non-terminating) then pσ is also δ-like (resp. stuck, non-terminating).

Proof. Immediate by definition.

Lemma 3. A stuck state is of one of the following forms, where k /

∈ I. C[v].l * π (λx t).l * π C[v] * w.π {l i = v i } i∈I * v.π case λx t [C i [x i ] → t i ] i∈I * π case {li=vi}i∈I [C j [x j ] → t j ] j∈J * π case C k [v] [C i [x i ] → t i ] i∈I * π {l i = v i } i∈I .l k * π
Proof. Simple case analysis.

Lemma 4. A blocked process p ∈ Λ × Π is either stuck, final, δ-like, or of one of the following forms.

x.l * π x * v.π case x [C i [x i ] → t i ] i∈I * π a * π
Proof. Straight-forward case analysis using lemma 3.

Reduction of δ v,w and equivalence

The idea now is to define a notion of observational equivalence over terms using a relation (≡). We then extend the reduction relation with a rule reducing a state of the form δ v,w * π to v * π if v ≡ w. If v ≡ w then δ v,w is stuck. With this rule reduction and equivalence will become interdependent as equivalence will be defined using reduction.

Definition 5. Given a reduction relation R, we say that a process p ∈ Λ × Π converges, and write p ⇓ R , if there is a final state q ∈ Λ × Π such that pR * q (where R * is the reflexive-transitive closure of R). If p does not converge we say that it diverges and write p ⇑ R . We will use the notations p ⇓ i and p ⇑ i when working with indexed notation symbols like (։ i ).

Definition 6. For every natural number i we define a reduction relation (։ i ) and an equivalence relation (≡ i ) which negation will be denoted ( ≡ i ).

(։ i ) = (≻) ∪ {(δ v,w * π, v * π) | ∃j < i, v ≡ j w} (≡ i ) = {(t, u) | ∀j ≤ i, ∀π, ∀σ, tσ * π ⇓ j ⇔ uσ * π ⇓ j }
It is easy to see that (։ 0 ) = (≻). For every natural number i, the relation (≡ i ) is indeed an equivalence relation as it can be seen as an intersection of equivalence relations. Its negation can be expressed as follows.

( ≡ i ) = {(t, u), (u, t) | ∃j ≤ i, ∃π, ∃σ, tσ * π ⇓ j ∧ uσ * π ⇑ j } Definition 7.
We define a reduction relation (։) and an equivalence relation (≡) which negation will be denoted ( ≡).

(։) = i∈N (։ i ) (≡) = i∈N (≡ i )
These relations can be expressed directly (i.e. without the need of a union or an intersection) in the following way.

(≡) = {(t, u) | ∀i, ∀π, ∀σ, tσ * π ⇓ i ⇔ uσ * π ⇓ i } ( ≡) = {(t, u), (u, t) | ∃i, ∃π, ∃σ, tσ * π ⇓ i ∧ uσ * π ⇑ i } (։) = (≻) ∪ {(δ v,w * π, v * π) | v ≡ w} Remark 4. Obviously (։ i ) ⊆ (։ i+1
) and (≡ i+1 ) ⊆ (≡ i ). As a consequence the construction of (։ i ) i∈N and (≡ i ) i∈N converges. In fact (։) and (≡) form a fixpoint at ordinal ω. Surprisingly, this property is not explicitly required.

Theorem 1. Let t and u be terms. If t ≡ u then for every stack π ∈ Π and substitution σ we have tσ * π ⇓ ։ ⇔ uσ * π ⇓ ։ .

Proof. We suppose that t ≡ u and we take π 0 ∈ Π and a substitution σ 0 . By symmetry we can assume that tσ 0 * π 0 ⇓ ։ and show that uσ 0 * π 0 ⇓ ։ . By definition there is i 0 ∈ N such that tσ 0 * π 0 ⇓ i0 . Since t ≡ u we know that for every i ∈ N, π ∈ Π and substitution σ we have tσ * π ⇓ i ⇔ uσ * π ⇓ i . This is true in particular for i = i 0 , π = π 0 and σ = σ 0 . We hence obtain uσ 0 * π 0 ⇓ i0 which give us uσ 0 * π 0 ⇓ ։ .

Remark 5. The converse implication is not true in general: taking t = δ λx x,{} and u = λx x gives a counter-example. More generally p ⇓ ։ ⇔ q ⇓ ։ does not necessarily imply p ⇓ i ⇔ q ⇓ i for all i ∈ N.

Corollary 1. Let t and u be terms and π be a stack.

If t ≡ u and t * π ⇓ ։ then u * π ⇓ ։ .
Proof. Direct consequence of theorem 1 using π and an empty substitution.

Extensionality of the language

In order to be able to work with the equivalence relation (≡), we need to check that it is extensional. In other words, we need to be able to replace equals by equals at any place in terms without changing their observed behaviour. This property is summarized in the following two theorems.

Theorem 2. Let v and w be values, E be a term and x be a λ-variable.

If v ≡ w then E[x := v] ≡ E[x := w].
Proof. We are going to prove the contrapositive so we suppose E[x := v] ≡ E[x := w] and show v ≡ w. By definition there is i ∈ N, π ∈ Π and a substitution σ such that (E[x := v])σ * π ⇓ i and (E[x := w])σ * π ⇑ i (up to symmetry). Since we can rename x in such a way that it does not appear in dom(σ), we can suppose Eσ[x := vσ] * π ⇓ i and Eσ[x := wσ] * π ⇑ i . In order to show v ≡ w we need to find i 0 ∈ N, π 0 ∈ Π and a substitution σ 0 such that vσ 0 * π 0 ⇓ i0 and wσ 0 * π 0 ⇑ i0 (up to symmetry). We take i 0 = i, π 0 = [λx Eσ]π and σ 0 = σ. These values are suitable since by definition

vσ 0 * π 0 ։ i0 Eσ[x := vσ] * π ⇓ i0 and wσ 0 * π 0 ։ i0 Eσ[x := wσ] * π ⇑ i0 .
Lemma 5. Let s be a process, t be a term, a be a term variable and k be a natural number. If s[a := t] ⇓ k then there is a blocked state p such that s ≻ * p and either p = v * α for some value v and a stack variable α, -p = a * π for some stack π, -k > 0 and p = δ(v, w) * π for some values v and w and stack π, and in this case v[a := t] ≡ j w[a := t] for some j < k.

Proof. Let σ be the substitution [a := t]. If s is non-terminating, lemma 2 tells us that sσ is also non-terminating, which contradicts sσ ⇓ k . Consequently, there is a blocked process p such that s ≻ * p since (≻) ⊆ (։ k ). Using lemma 1 we get sσ ≻ * pσ from which we obtain pσ ⇓ k . The process p cannot be stuck, otherwise pσ would also be stuck by lemma 2, which would contradict pσ ⇓ k . Let us now suppose that p = δ v,w * π for some values v and w and some stack π. Since δ vσ,wσ * π ⇓ k there must be i < k such that vσ ≡ j wσ, otherwise this would contradict δ vσ,wσ * π ⇓ k . In this case we necessarily have k > 0, otherwise there would be no possible candidate for i. According to lemma 4 we need to rule out four more forms of therms: x.l * π, x * v.π, case x B * π and b * π in the case where b = a. If p was of one of these forms the substitution σ would not be able to unblock the reduction of p, which would contradict again pσ ⇓ k .

Lemma 6. Let t 1 , t 2 and E be terms and a be a term variable. For every k ∈ N,

if t 1 ≡ k t 2 then E[a := t 1 ] ≡ k E[a := t 2 ].
Proof. Let us take k ∈ N, suppose that t 1 ≡ k t 2 and show that E[a

:= t 1 ] ≡ k E[a := t 1 ]
. By symmetry we can assume that we have i ≤ k, π ∈ Π and a substitution σ such that (E[a :

= t 1 ])σ * π ⇓ i and show that (E[a := t 2 ])σ * π ⇓ i .
As we are free to rename a, we can suppose that it does not appear in dom(σ), T V (π), T V (t 1 ) or T V (t 2 ). In order to lighten the notations we define

E ′ = Eσ, σ 1 = [a := t 1 σ] and σ 2 = [a := t 2 σ].
We are hence assuming E ′ σ 1 * π ⇓ i and trying to show E ′ σ 2 * π ⇓ i .

We will now build a sequence (E i , π i , l i ) i∈I in such a way that

E ′ σ 1 * π ։ * k E i σ 1 * π i σ 1
in l i steps for every i ∈ I. Furthermore, we require that (l i ) i∈I is increasing and that it has a strictly increasing subsequence. Under this condition our sequence will necessarily be finite. If it was infinite the number of reduction steps that could be taken from the state E ′ σ 1 * π would not be bounded, which would contradict E ′ σ 1 * π ⇓ i . We now denote our finite sequence (E i , π i , l i ) i≤n with n ∈ N. In order to show that (l i ) i≤n has a strictly increasing subsequence, we will ensure that it does not have three equal consecutive values. More formally, we will require that if 0 < i < n and l i-1 = l i then l i+1 > l i .

To define (E 0 , π 0 , l 0 ) we consider the reduction of E ′ * π. Since we know that (E ′ * π)σ 1 = E ′ σ 1 * π ⇓ i we use lemma 5 to obtain a blocked state p such that E ′ * π ≻ j p. We can now take E 0 * π 0 = p and l 0 = j. By lemma 1 we have

(E ′ * π)σ 1 ≻ j E 0 σ 1 * π 0 σ 1 from which we can deduce that (E ′ * π)σ 1 ։ * k E 0 σ 1 * π 0 σ 1 in l 0 = j steps.
To define (E i+1 , π i+1 , l i+1 ) we consider the reduction of the process

E i σ 1 * π i . By construction we know that E ′ σ 1 * π ։ * k E i σ 1 * π i σ 1 = (E i σ 1 * π i )σ 1 in l i steps.
Using lemma 5 we know that E i * π i might be of three shapes.

-If E i * π i = v * α for some value v and stack variable α then the end of the sequence was reached with n = i.

-If E i = a then we consider the reduction of E i σ 1 * π i . Since (E i σ 1 * π i )σ 1 ⇓ k we
know from lemma 5 that there is a blocked process p such that E i σ 1 * π i ≻ j p.

Using lemma 1 we obtain that E i σ 1 * π i σ 1 ≻ j pσ 1 from which we can deduce that E i σ 1 * π i σ 1 ։ k pσ 1 in j steps. We then take E i+1 * π i+1 = p and l i+1 = l i + j.

Is it possible to have j = 0? This can only happen when E i σ 1 * π i is of one of the three forms of lemma 5. It cannot be of the form a * π as we assumed that a does not appear in t 1 or σ. If it is of the form v * α, then we reached the end of the sequence with i + 1 = n so there is no trouble. The process E i σ 1 * π i may be of the form δ(v, w) * π, but we will have l i+2 > l i+1 .

-If E i = δ(v, w) for some values v and w we have m < k such that vσ 1 ≡ m wσ 1 . Hence

E i σ 1 * π i = δ(vσ 1 , wσ 1 ) * π i ։ k vσ 1 * π i by definition. Moreover E i σ 1 * π i σ 1 ։ k vσ 1 * π i σ 1 by lemma 1. Since E ′ σ 1 * π ։ * k E i σ 1 * π i σ 1 in l i steps we obtain that E ′ σ 1 * π ։ * k vσ 1 * π i σ 1 in l i + 1 steps. This also gives us (vσ 1 * π i )σ 1 = vσ 1 * π i σ 1 ⇓ k .
We now consider the reduction of the process vσ 1 * π i . By lemma 5 there is a blocked process p such that vσ 1 * π i ≻ j p. Using lemma 1 we obtain vσ 1 * π i σ 1 ≻ j pσ 1 from which we deduce that vσ 1 * π i σ 1 ։ * k pσ 1 in j steps. We then take E i+1 * π i+1 = p and l i+1 = l i + j + 1. Note that in this case we have l i+1 > l i .

Intuitively (E i , π i , l i ) i≤n mimics the reduction of E ′ σ 1 * π while making explicit every substitution of a and every reduction of a δ-like state.

To end the proof we show that for every i ≤ n we have

E i σ 2 * π i σ 2 ⇓ k . For i = 0 this will give us E ′ σ 2 * π ⇓ k which is the expected result. Since E n * π n = v * α we have E n σ 2 * π n σ 2 = vσ 2 * α from which we trivially obtain E n σ 2 * π n σ 2 ⇓ k . We now suppose that E i+1 σ 2 * π i σ 2 ⇓ k for 0 ≤ i < n and show that E i σ 2 * π i σ 2 ⇓ k . By construction E i * π i can be of two shapes 4 :
-

If E i = a then t 1 σ * π i ։ * k E i+1 * π i+1 . Using lemma 1 we obtain t 1 σ * π i σ 2 ։ k E i+1 σ 2 * π i σ 2 from which we deduce t 1 σ * π i σ 2 ⇓ k by induction hypothesis. Since t 1 ≡ k t 2 we obtain t 2 σ * π i σ 2 = (E i * π i )σ 2 ⇓ k . -If E i = δ(v, w) then v * π i ։ k E i+1 * π i+1 and hence vσ 2 * π i σ 2 ։ k E i+1 σ 2 *
π i+1 σ 2 by lemma 1. Using the induction hypothesis we obtain vσ 2 * π i σ 2 ⇓ k . It remains to show that δ(vσ 2 , wσ 2 ) * π i σ 2 ։ * k vσ 2 * π i σ 2 . We need to find j < k such that vσ 2 ≡ j wσ 2 . By construction there is m < k such that vσ 1 ≡ m wσ 1 . We are going to show that vσ 2 ≡ m wσ 2 . By using the global induction hypothesis twice we obtain vσ 1 ≡ m vσ 2 and wσ 1 ≡ m vσ 2 . Now if vσ 2 ≡ m wσ 2 then vσ 1 ≡ m vσ 2 ≡ m wσ 2 ≡ m wσ 1 contradicts vσ 1 ≡ wσ 1 . Hence we must have vσ 2 ≡ m wσ 2 . Theorem 3. Let t 1 , t 2 and E be three terms and a be a term variable. If

t 1 ≡ t 2 then E[a := t 1 ] ≡ E[a := t 2 ].
Proof. We suppose that t 1 ≡ t 2 which means that t 1 ≡ i t 2 for every i ∈ N. We need to show that E[a := t 1 ] ≡ E[a := t 2 ] so we take i 0 ∈ N and show

E[a := t 1 ] ≡ i0 E[a := t 2 ]
. By hypothesis we have t 1 ≡ i0 t 2 and hence we can conclude using lemma 6.

Formulas and Semantics

The syntax presented in the previous section is part of a realizability machinery that will be built upon here. We aim at obtaining a semantical interpretation of the second-order type system that will be defined shortly. Our abstract machine slightly differs from the mainstream presentation of Krivine's classical realizability which is usually call-by-name. Although call-by-value presentations have rarely been published, such developments are well-known among classical realizability experts. The addition of the δ instruction and the related modifications are however due to the author.

Pole and orthogonality

As always in classical realizability, the model is parametrized by a pole, which serves as an exchange point between the world of programs and the world of execution contexts (i.e. stacks). Definition 8. A pole is a set of processes ⊥ ⊥ ⊆ Λ × Π which is saturated (i.e. closed under backward reduction). More formally, if we have q ∈ ⊥ ⊥ and p ։ q then p ∈ ⊥ ⊥.

Here, for the sake of simplicity and brevity, we are only going to use the pole

⊥ ⊥ = {p ∈ Λ × Π | p ⇓ ։ }
which is clearly saturated. Note that this particular pole is also closed under the reduction relation (։), even though this is not a general property. In particular ⊥ ⊥ contains all final processes.

The notion of orthogonality is central in Krivine's classical realizability. In this framework a type is interpreted (or realized) by programs computing corresponding values. This interpretation is spread in a three-layered construction, even though it is fully determined by the first layer (and the choice of the pole). The first layer consists of a set of values that we will call the raw semantics. It gathers all the syntactic values that should be considered as having the corresponding type. As an example, if we were to consider the type of natural numbers, its raw semantics would be the set {n | n ∈ N} where n is some encoding of n. The second layer, called falsity value is a set containing every stack that is a candidate for building a valid process using any value from the raw semantics. The notion of validity depends on the choice of the pole. Here for instance, a valid process is a normalizing one (i.e. one that reduces to a final state). The third layer, called truth value is a set of terms that is built by iterating the process once more. The formalism for the two levels of orthogonality is given in the following definition. Definition 9. For every set φ ⊆ Λ v we define a set φ ⊥ ⊆ Π and a set φ ⊥⊥ ⊆ Λ as follows.

φ ⊥ = {π ∈ Π | ∀v ∈ φ, v * π ∈ ⊥ ⊥} φ ⊥⊥ = {t ∈ Λ | ∀π ∈ φ ⊥ , t * π ∈ ⊥ ⊥}
We now give two general properties of orthogonality that are true in every classical realizability model. They will be useful when proving the soundness of our type system. The construction involving the terms of the form δ v,x and (≡) in the previous section is now going to gain meaning. The following theorem, which is our central result, does not hold in every classical realizability model. Obtaining a proof required us to internalize observational equivalence, which introduces a noncomputable reduction rule.

Theorem 4. If Φ ⊆ Λ v is a set of values closed under (≡), then Φ ⊥⊥ ∩ Λ v = Φ.
Proof. The direction Φ ⊆ Φ ⊥⊥ ∩ Λ v is straight-forward using lemma 7. We are going to show that Φ ⊥⊥ ∩ Λ v ⊆ Φ, which amounts to showing that for every value v ∈ Φ ⊥⊥ we have v ∈ Φ. We are going to show the contrapositive, so let us assume v ∈ Φ and show v ∈ Φ ⊥⊥ . We need to find a stack π 0 such that v * π 0 ∈ ⊥ ⊥ and for every value w ∈ Φ, w * π 0 ∈ ⊥ ⊥. We take π 0 = [λx δ x,v ] α and show that is is suitable. By definition of the reduction relation v * π 0 reduces to δ v,v * α which is not in ⊥ ⊥ (it is stuck as v ≡ v by reflexivity). Let us now take w ∈ Φ. Again by definition, w * π 0 reduces to δ w,v * α, but this time we have w ≡ v since Φ was supposed to be closed under (≡) and v ∈ Φ. Hence w * π 0 reduces to w * α ∈ ⊥ ⊥.

It is important to check that the pole we chose does not yield a degenerate model. In particular we check that no term is able to face every stacks. If it were the case, such a term could be use as a proof of ⊥.

Theorem 5. The pole ⊥ ⊥ is consistent, which means that for every closed term t there is a stack π such that t * π ∈ ⊥ ⊥.

Proof. Let t be a closed term and α be a stack constant. If we do not have t * α ⇓ ։ then we can directly take π = α. Otherwise we know that t * α ։ * v * α for some value v. Since t is closed α is the only available stack variable. We now show that π = [λx {}]{}.β is suitable. We denote σ the substitution [α := π]. Using a trivial extension of lemma 1 to the (։) relation we obtain

t * π = (t * α)σ ։ * (v * α)σ = vσ * π. We hence have t * π ։ * vσ * [λx {}]{}.β ։ 2 {} * {}.β ∈ ⊥ ⊥.

Formulas and their semantics

In this paper we limit ourselves to second-order logic, even though the system can easily be extended to higher-order. For every natural number n we require a countable set V n = {X n , Y n , Z n ...} of n-ary predicate variables.

Definition 10. The syntax of formulas is given by the following grammar.

A, B ::= X n (t 1 , ..., t n ) | A ⇒ B | ∀a A | ∃a A | ∀X n A | ∃X n A | {l i : A i } i∈I | [C i : A i ] i∈I | t ∈ A | A ↾ t ≡ u
Terms appear in several places in formulas, in particular, they form the individuals of the logic. They can be quantified over and are used as arguments for predicate variables. Besides the ML-like formers for sums and products (i.e. records and variants) we add a membership predicate and a restriction operation. The membership predicate t ∈ A is used to express the fact that the term t has type A. It provides a way to encode the dependent product type using universal quantification and the arrow type. In this sense, it is inspired and related to Krivine's relativization of quantifiers.

Π a:A B := ∀a(a ∈ A ⇒ B)
The restriction operator can be thought of as a kind of conjunction with no algorithmic content. The formula A ↾ t ≡ u is to be interpreted in the same way as A if the equivalence t ≡ u holds, and as ⊥ otherwise 5 . In particular, we will define the following types:

A ↾ t ≡ u := A ↾ t ≡ u ⇒ ⊥ t ≡ u := ⊤ ↾ t ≡ u t ≡ u := ⊤ ↾ t ≡ u
To handle free variables in formulas we will need to generalize the notion of substitution to allow the substitution of predicate variables. Definition 11. A substitution is a finite map σ ranging over λ-variables, µvariables, term and predicate variables such that:

-if x ∈ dom(σ) then σ(x) ∈ Λ v , -if α ∈ dom(σ) then σ(α) ∈ Π, -if a ∈ dom(σ) then σ(a) ∈ Λ, -if X n ∈ dom(σ) then σ(X n ) ∈ Λ n → P(Λ v /≡).
Remark 6. A predicate variable of arity n will be substituted by a n-ary predicate. Semantically, such predicate will correspond to some total (set-theoretic) function building a subset of Λ v /≡ from n terms. In the syntax, the binding of the arguments of a predicate variables will happen implicitly during its substitution.

Definition 12. Given a formula A we denote F V (A) the set of its free variables. Given a substitution σ such that F V (A) ⊆ dom(σ) we write A[σ] the closed formula built by applying σ to A.

In the semantics we will interpret closed formulas by sets of values closed under the equivalence relation (≡).

Definition 13. Given a formula A and a substitution σ such that A[σ] is closed, we define the raw semantics A σ ⊆ Λ v / ≡ of A under the substitution σ as follows.

X n (t 1 , ..., t n ) σ = σ(X n )(t 1 σ, ..., t n σ) A ⇒ B σ = {λx t | ∀v ∈ A σ , t[x := v] ∈ B ⊥⊥ σ } ∀a A σ = ∩ t∈Λ * A σ[a:=t] ∃a A σ = ∪ t∈Λ * A σ[a:=t] ∀X n A σ = ∩ P ∈Λ n →P(Λv /≡) A σ[Xn :=P ] ∃X n A σ = ∪ P ∈Λ n →P(Λv /≡) A σ[Xn :=P ] {l i : A i } i∈I σ = {{l i = v i } i∈I | ∀i ∈ I v i ∈ A i σ } [C i : A i ] i∈I σ = ∪ i∈I {C i [v] | v ∈ A i σ } t ∈ A σ = {v ∈ A σ | tσ ≡ v} A ↾ t ≡ u σ = A σ if tσ ≡ uσ ∅ otherwise
In the model, programs will realize closed formulas in two different ways according to their syntactic class. The interpretation of values will be given in terms of raw semantics, and the interpretation of terms in general will be given in terms of truth values. Definition 14. Let A be a formula and σ a substitution such that A[σ] is closed. We say that:

-v ∈ Λ v realizes A[σ] if v ∈ A σ , -t ∈ Λ realizes A[σ] if t ∈ A ⊥⊥ σ .

Contexts and typing rules

Before giving the typing rules of our system we need to define contexts and judgements. As explained in the introduction, several typing rules require a value restriction in our context. This is reflected in typing rule by the presence of two forms of judgements.

Definition 15. A context is an ordered list of hypotheses. In particular, it contains type declarations for λ-variables and µ-variables, and declaration of term variables and predicate variables. In our case, a context also contains term equivalences and inequivalences. A context is built using the following grammar.

Γ, ∆ ::= • | Γ, x : A | Γ, α : ¬A | Γ, a : T erm | Γ, X n : P red n | Γ, t ≡ u | Γ, t ≡ u
A context Γ is said to be valid if it is possible to derive Γ Valid using the rules of figure 1. In the following, every context will be considered valid implicitly. Definition 16. There are two forms of typing judgements:

Γ Valid x ∈ dom(Γ ) F V (A) ⊆ dom(Γ ) ∪ {x} Γ, x : A Valid Γ Valid α ∈ dom(Γ ) F V (A) ⊆ dom(Γ ) Γ, α : ¬A Valid Γ Valid a ∈ dom(Γ ) Γ, a : T erm Valid Γ Valid Xn ∈ dom(Γ ) Γ, Xn : P redn Valid Γ Valid F V (t) ∪ F V (u) ⊆ dom(Γ ) Γ, t ≡ u Valid Γ Valid F V (t) ∪ F V (u) ⊆ dom(Γ ) Γ, t ≡ u Valid • Valid
-Γ ⊢ val v : A meaning that the value v has type A in context Γ , -Γ ⊢ t : A meaning that the term t has type A in context Γ .
The typing rules of the system are given in figure 2. Although most of them are fairly usual, our type system differs in several ways. For instance the last four rules are related to the extensionality of the calculus. One can note the value restriction in several places: both universal quantification introduction rules and the introduction of the membership predicate. In fact, some value restriction is also hidden in the rules for the elimination of the existential quantifiers and the elimination rule for the restriction connective. These rules are presented in their left-hand side variation, and only values can appear on the left of the sequent. It is not surprising that elimination of an existential quantifier requires value restriction as it is the dual of the introduction rule of a universal quantifier.

An important and interesting difference with existing type systems is the presence of ↑ and ↓. These two rules allow one to go from one kind of sequent to the other when working on values. Going from Γ ⊢ val v : A to Γ ⊢ v : A is straight-forward. Going the other direction is the main motivation for our model. This allows us to lift the value restriction expressed in the syntax to a restriction expressed in terms of equivalence. For example, the two rules

ax Γ, x : A ⊢ val x : A Γ ⊢ val v : A ↑ Γ ⊢ v : A Γ ⊢ v : A ↓ Γ ⊢ val v : A Γ ⊢ t : A ⇒ B Γ ⊢ u : A ⇒e Γ ⊢ t u : B Γ, x : A ⊢ t : B ⇒i Γ ⊢ val λx t : A ⇒ B Γ, α : ¬A ⊢ t : A µ Γ ⊢ µα t : A Γ, α : ¬A ⊢ t : A * Γ, α : ¬A ⊢ t * α : B Γ ⊢ val v : A ∈i Γ ⊢ val v : v ∈ A Γ, x : A, x ≡ u ⊢ t : A ∈e Γ, x : u ∈ A ⊢ t : A
can be derived in the system (see figure 3). The value restriction can be removed similarly on every other rule. Thus, judgements on values can be completely ignored by the user of the system. Transition to value judgements will only happen internally.

Γ, t ≡ v ⊢ t : A ≡ t,l Γ, t ≡ v ⊢ v : A ↓ Γ, t ≡ v ⊢ val v : A a ∈ F V (Γ ) ∀i Γ, t ≡ v ⊢ val v : ∀a A ↑ Γ, t ≡ v ⊢ v : ∀a A ≡ t,l Γ, t ≡ v ⊢ t : ∀a A Γ, u ≡ v ⊢ t : Πa:AB Γ, u ≡ v ⊢ t : ∀a(a ∈ A ⇒ B) ∀e Γ, u ≡ v ⊢ t : u ∈ A ⇒ B[a := u] Γ, u ≡ v ⊢ u : A ≡ t,l Γ, u ≡ v ⊢ v : A ↓ Γ, u ≡ v ⊢ val v : A ∈i Γ, u ≡ v ⊢ val v : v ∈ A ↑ Γ, u ≡ v ⊢ v : v ∈ A ≡ t,l Γ, u ≡ v ⊢ u : v ∈ A ≡t,r Γ, u ≡ v ⊢ u : u ∈ A ⇒e Γ, u ≡ v ⊢ t u : B[a := u]

Adequacy

We are now going to prove the soundness of our type system by showing that it is compatible with our realizability model. This property is specified by the following theorem which is traditionally called the adequacy lemma. Definition 17. Let Γ be a (valid) context. We say that the substitution σ realizes Γ if:

for every x : A in Γ we have σ(x) ∈ A σ , -for every α : ¬A in Γ we have σ(α) ∈ A ⊥ σ , -for every a : T erm in Γ we have σ(a) ∈ Λ, -for every X n : P red n in Γ we have σ(X n ) ∈ Λ n → Λ v /≡, -for every t ≡ u in Γ we have tσ ≡ uσ and for every t ≡ u in Γ we have tσ ≡ uσ. Theorem 6. (Adequacy.) Let Γ be a (valid) context, A be a formula such that F V (A) ⊆ dom(Γ ) and σ be a substitution realizing Γ .

-

If Γ ⊢ val v : A then vσ ∈ A σ , -if Γ ⊢ t : A then tσ ∈ A ⊥⊥ σ .
Proof. We proceed by induction on the derivation of the judgement Γ ⊢ val v : A (resp. Γ ⊢ t : A) and we reason by case on the last rule used. (∈ e ) By hypothesis we know that σ realizes Γ, x : u ∈ A. To be able to conclude using the induction hypothesis, we need to show that σ realizes Γ, x : A, x ≡ u. Since we have σ(x) ∈ u ∈ A σ , we obtain that xσ ∈ A σ and xσ ≡ uσ by definition of u ∈ A σ .

(↾ i ) We need to show tσ ∈ A ↾ u 1 ≡ u 2 ⊥⊥ σ . By hypothesis u 1 σ ≡ u 2 σ, hence A ↾ u 1 ≡ u 2 σ = A σ .
Consequently, it is enough to show that tσ ∈ A ⊥⊥ σ , which is exactly the induction hypothesis. (↾ e ) By hypothesis we know that σ realizes Γ, x : A ↾ u 1 ≡ u 2 . To be able to use the induction hypothesis, we need to show that σ realizes Γ, x : A, u 1 ≡ u 2 . Since we have σ(x) ∈ A ↾ u 1 ≡ u 2 σ , we obtain that xσ ∈ A σ and that (∃ e ) By hypothesis we know that σ realizes Γ, x : ∃a A. In particular, we know that σ(x) ∈ ∃a A σ , which means that there is a term u ∈ Λ * such that σ(x) ∈ A σ (∃ i ) The proof for this rule is similar to the one for (∀ e ). We need to show that

u 1 σ ≡ u 2 σ by definition of A ↾ u 1 ≡ u 2 σ . (∀ i ) We need to show that vσ ∈ ∀a A σ = t∈Λ A σ
A[a := u] ⊥⊥ σ = A ⊥⊥ σ[a:=uσ] ⊆ ∃a A ⊥⊥ σ .
This follows from lemma 8 since A σ[a:=uσ] ⊆ ∃a A σ by definition. (∀ I ), (∀ E ), (∃ E ) and (∃ I ) are similar to similar to (∀ i ), (∀ e ), (∃ e ) and (∃ i ). (× i ) We need to show that {l i = v i σ} i∈I ∈ {l i : A i } i∈I σ . By definition we need to show that for all i ∈ I we have v i σ ∈ A i σ . This is immediate by induction hypothesis.

(× e ) We need to show that vσ.l i ∈ A i ⊥⊥ σ for some i ∈ I. By induction hypothesis we have vσ ∈ {l i : A i } i∈I σ and hence v has the form

{l i = v i } i∈I with v i σ ∈ A i σ . Let us now take π ∈ A i ⊥ σ and show that {l i = v i σ} i∈I .l i * π ∈ ⊥ ⊥. Since ⊥ ⊥ is saturated, it is enough to show v i σ * π ∈ ⊥ ⊥. This is true since v i σ ∈ A i σ and π ∈ A i ⊥ σ . (+ i ) We need to show C i [vσ] ∈ [C i : A i ] i∈I σ for some i ∈ I.

By induction hypothesis vσ ∈ A i σ and hence we can conclude by definition of [C

i : A i ] i∈I σ . (+ e ) We need to show case vσ [C i [x] → t i σ] i∈I ∈ B ⊥⊥ σ . By induction hypothesis vσ ∈ [C i of A i ] i∈I σ which means that there is i ∈ I and w ∈ A i σ such that vσ = C i [w]. We take π ∈ B ⊥ σ and show case Ci[w] [C i [x] → t i σ] i∈I * π ∈ ⊥ ⊥. Since ⊥ ⊥ is saturated, it is enough to show t i σ[x := w] * π ∈ ⊥ ⊥. It remains to show that t i σ[x := w] ∈ B ⊥⊥ σ .
To be able to conclude using the induction hypothesis we need to show that σ[x := w] realizes Γ, x : A i , C i [x] ≡ v. This is true since σ realizes Γ , w ∈ A i σ and C i [w] ≡ vσ by reflexivity. (≡ v,l ) We need to show t[x := w 1 ]σ = tσ[x := w 1 σ] ∈ A σ . By hypothesis we know that w 1 σ ≡ w 2 σ from which we can deduce tσ[x := w 1 σ] ≡ tσ[x := w 2 σ] by extensionality (theorem 2). Since A σ is closed under (≡) we can conclude using the induction hypothesis. (≡ t,l ), (≡ v,r ) and (≡ t,r ) are similar to (≡ v,l ), using extensionality (theorem 2 and theorem 3). Remark 7. For the sake of simplicity we fixed a pole ⊥ ⊥ at the beginning of the current section. However, many of the properties presented here (including the adequacy lemma) remain valid with similar poles. We will make use of this fact in the proof of the following theorem. Theorem 7. (Safety.) Let Γ be a context, A be a formula such that F V (A) ⊆ dom(Γ ) and σ be a substitution realizing Γ . If t is a term such that Γ ⊢ t : A and if A[σ] is pure (i.e. it does not contain any ⇒ ), then for every stack π ∈ A ⊥ σ there is a value v ∈ A σ and α ∈ V µ such that tσ * π ։ * v * α. Proof. We do a proof by realizability using the following pole.

⊥ ⊥ A = {p ∈ Λ × Π | p ։ * v * α ∧ v ∈ A σ }
It is well-defined as A is pure and hence A σ does not depend on the pole. Using the adequacy lemma (theorem 6) with ⊥ ⊥ A we obtain tσ ∈ A ⊥⊥ σ . Hence for every stack π ∈ A ⊥ σ we have tσ * π ∈ ⊥ ⊥ A . We can then conclude using the definition of the pole ⊥ ⊥ A .

Remark 8. It is easy to see that if A[σ] is closed and pure then v ∈ A σ implies that • ⊢ v : A. Theorem 8. (Consistency.) There is no t such that • ⊢ t : ⊥.

Proof. Let us suppose that • ⊢ t : ⊥. Using adequacy (theorem 6 ) we obtain that t ∈ ⊥ ⊥⊥ σ . Since ⊥ σ = ∅ we know that ⊥ ⊥ σ = Π by definition. Now using theorem 5 we obtain ⊥ ⊥⊥ σ = ∅. This is a contradiction.

Deciding Program Equivalence

The type system given in figure 2 does not provide any way of discharging an equivalence from the context. As a consequence the truth of an equivalence cannot be used. Furthermore, an equational contradiction in the context cannot be used to derive falsehood. To address these two problems, we will rely on a partial decision procedure for the equivalence of terms. Such a procedure can be easily implemented using an algorithm similar to Knuth-Bendix, provided that we are able to extract a set of equational axioms from the definition of (≡). In particular, we will use the following lemma to show that several reduction rules are contained in (≡). Lemma 9. Let t and u be terms. If for every stack π ∈ Π there is p ∈ Λ × Π such that t * π ≻ * p and u * π ≻ * p then t ≡ u.

Proof. Since (≻) ⊆ (։ i ) for every i ∈ N, we can deduce that t * π ։ * i p and u * π ։ * i p for every i ∈ N. Using lemma 1 we can deduce that for every substitution σ we have tσ * π ։ * i pσ and uσ * π ։ * i pσ for all i ∈ N. Consequently we obtain t ≡ u.

The equivalence relation contains call-by-value β-reduction, projection on records and case analysis on variants.

Theorem 9. For every x ∈ V λ , t ∈ Λ and v ∈ Λ v we have (λx t)v ≡ t[x := v].
Proof. Immediate using lemma 9.

Theorem 10. For all k such that 1 ≤ k ≤ n we have the following equivalences.

(λx t)v ≡ t[x := v] case C k [v] [C i [x i ] → t i ] 1≤i≤n ≡ t k [x k := v]
Proof. Immediate using lemma 9.

To observe contradictions, we also need to derive some inequivalences on values. For instance, we would like to deduce a contradiction if two values with a different head constructor are assumed to be equivalent.

i = v i } i∈I ≡ {l j = v j } j∈J .
Proof. Immediate using the stack π = [λx x.l k ]α.

Theorem 13. For every x ∈ V λ , v ∈ Λ v , t ∈ Λ, C ∈ C and for every record {l i = v i } i∈I we have the following inequivalences.

λx t ≡ C[v] λx t ≡ {l i = v i } i∈I C[v] ≡ {l i = v i } i∈I
Proof. The proof is mostly similar to the proofs of the previous two theorems. However, there is a subtlety with the second inequivalence. If for every value v the term t[x := v] diverges, then we do not have λx t ≡ {}. Indeed, there is no evaluation context (or stack) that is able to distinguish the empty record {} and a diverging function. To solve this problem, we can extend the language with a new kind of term unit v and extend the relation (≻) with the following rule.

unit {} * π ≻ {} * π

The process unit v * π is stuck for every value v = {}. The proof can the be completed using the stack π = [λx unit x ]α.

The previous five theorems together with the extensionality of (≡) and its properties as an equivalence relation can be used to implement a partial decision procedure for equivalence. We will incorporate this procedure into the typing rules by introducing a new form of judgment. Definition 18. An equational context E is a list of hypothetical equivalences and inequivalences. Equational contexts are built using the following grammar.

E := • | E, t ≡ u | E, t ≡ u
Given a context Γ , we denote E Γ its restriction to an equational context. Definition 19. Let E be an equational context. The judgement E ⊢ ⊥ is valid if and only if the partial decision procedure is able to derive a contradiction in E. We will write E ⊢ t ≡ u for E, t ≡ u ⊢ ⊥ and E ⊢ t ≡ u for E, t ≡ u ⊢ ⊥ To discharge equations from the context, the following two typing rules are added to the system.

Γ, u 1 ≡ u 2 ⊢ t : A E Γ ⊢ u 1 ≡ u 2 ≡ Γ ⊢ t : A Γ, u 1 ≡ u 2 ⊢ t : A E Γ ⊢ u 1 ≡ u 2 ≡ Γ ⊢ t : A
The soundness of these new rules follows easily since the decision procedure agrees with the semantical notion of equivalence. The axioms that were given at the beginning of this section are only used to partially reflect the semantical equivalence relation in the syntax. This is required if we are to implement the decision procedure.

Another way to use an equational context is to derive a contradiction directly. For instance, if we have a context Γ such that E Γ yields a contradiction, one should be able to finish the corresponding proof. This is particularly useful when working with variants and case analysis. For instance, some branches of the case analysis might not be reachable due to constraints on the matched term. For instance, we know that in the term

case C[v] [C[x] → x | D[x] → t]
the branch corresponding to the D constructor will never be reached. Consequently, we can replace t by any term and the computation will still behave correctly. For this purpose we introduce a special value 8< on which the abstract machine fails. It can be introduced with the following typing rule.

E Γ ⊢ ⊥ 8< Γ ⊢ val 8< : ⊥
The soundness of this rule is again immediate.

Further Work

The model presented in the previous sections is intended to be used as the basis for the design of a proof assistant based on a call-by-value ML language with control operators. A first prototype (with a different theoretical foundation) was implemented by Christophe Raffalli [START_REF] Raffalli | The PML programming language[END_REF]. Based on this experience, the design of a new version of the language with a clean theoretical basis can now be undertaken. The core of the system will consist of three independent components: a typechecker, a termination checker and a decision procedure for equivalence.

Working with a Curry style language has the disadvantage of making typechecking undecidable. While most proof systems avoid this problem by switching to Church style, it is possible to use heuristics making most Curry style programs that arise in practice directly typable. Christophe Raffalli implemented such a system [START_REF] Raffalli | A normaliser for pure and typed λ-calculus[END_REF] and from his experience it would seem that very little help from the user is required in general. In particular, if a term is typable then it is possible for the user to provide hints (e.g. the type of a variable) so that type-checking may succeed. This can be seen as a kind of completeness.

Proof assistants like Coq [START_REF]The Coq development team: The Coq proof assistant reference manual[END_REF] or Agda [START_REF] Norell | Dependently Typed Programming in Agda[END_REF] both have decidable type-checking algorithms. However, these systems provide mechanisms for handling implicit arguments or meta-variables which introduce some incompleteness. This does not make these systems any less usable in practice. We conjecture that going even further (i.e. full Curry style) provides a similar user experience.

To obtain a practical programming language we will need support for recursive programs. For this purpose we plan on adapting Pierre Hyvernat's termination checker [START_REF] Hyvernat | The size-change termination principle for constructor based languages[END_REF]. It is based on size change termination and has already been used in the first prototype implementation. We will also need to extend our type system with inductive (and coinductive) types [START_REF] Mendler | Recursive types and type constraints in second-order lambda calculus[END_REF][START_REF] Raffalli | L'Arithmétiques Fonctionnelle du Second Ordre avec Points Fixes[END_REF]. They can be introduced in the system using fixpoints µX A (and νX A).

  type nat = Z [] | S [ nat ] let rec add n m = match n with | Z [] → m | S [ nn ] → S [ add nn m ]

  let addZeroN n : nat : ( add Z [] n ≡ n ) = 8<

  let rec addNZero n : nat : ( add n Z [] ≡ n ) = match n with | Z [] → 8< | S [ nn ] → let r = addNZero nn in 8<

Lemma 7 .Lemma 8 .

 78 If φ ⊆ Λ v is a set of values, then φ ⊆ φ ⊥⊥ . Proof. Immediate following the definition of φ ⊥⊥ . Let φ ⊆ Λ v and ψ ⊆ Λ v be two sets of values. If φ ⊆ ψ then φ ⊥⊥ ⊆ ψ ⊥⊥ .Proof. Immediate by definition of orthogonality.

Fig. 1 .

 1 Fig. 1. Rules allowing the construction of a valid context.

Fig. 3 .

 3 Fig. 3. Derivation of the rules ∀i,≡ and Πe,≡.

  (ax) By hypothesis σ realizes Γ, x : A from which we directly obtain xσ ∈ A σ . (↑) and (↓) are direct consequences of lemma 7 and theorem 4 respectively. (⇒ e ) We need to prove that tσ uσ ∈ B ⊥⊥ σ , hence we take π ∈ B ⊥ σ and show tσ uσ * π ∈ ⊥ ⊥. Since ⊥ ⊥ is saturated, we can take a reduction step and show uσ * [tσ]π ∈ ⊥ ⊥. By induction hypothesis uσ ∈ A ⊥⊥ σ so we only have to show [tσ]π ∈ A ⊥ σ . To do so we take v ∈ A σ and show v * [tσ]π ∈ ⊥ ⊥. Here we can again take a reduction step and show tσ * v.π ∈ ⊥ ⊥. By induction hypothesis we havetσ ∈ A ⇒ B ⊥⊥ σ , hence it is enough to show v.π ∈ A ⇒ B ⊥ σ .We now take a value λx t x ∈ A ⇒ B σ and show that λx t x * v.π ∈ ⊥ ⊥. We then apply again a reduction step and showt x [x := v] * π ∈ ⊥ ⊥. Since π ∈ B ⊥ σ we only need to show t x [x := v] ∈ B ⊥⊥σ which is true by definition of A ⇒ B σ . (⇒ i ) We need to show λx tσ ∈ A ⇒ B σ so we take v ∈ A σ and show tσ[x := v] ∈ B ⊥⊥ σ . Since σ[x := v] realizes Γ, x : A we can conclude using the induction hypothesis. (µ) We need to show that µα tσ ∈ A ⊥⊥ σ hence we take π ∈ A ⊥ σ and show µα tσ * π ∈ ⊥ ⊥. Since ⊥ ⊥ is saturated, it is enough to show tσ[α := π] * π ∈ ⊥ ⊥. As σ[α := π] realizes Γ, α : ¬A we conclude by induction hypothesis. ( * ) We need to show tσ * ασ ∈ B ⊥⊥ σ , hence we take π ∈ B ⊥ σ and show that (tσ * ασ) * π ∈ ⊥ ⊥. Since ⊥ ⊥ is saturated, we can take a reduction step and show tσ * ασ ∈ ⊥ ⊥. By induction hypothesis tσ ∈ A ⊥⊥ σ hence it is enough to show ασ ∈ A ⊥ σ which is true by hypothesis. (∈ i ) We need to show vσ ∈ v ∈ A σ . We have vσ ∈ A σ by induction hypothesis, and vσ ≡ vσ by reflexivity of (≡).

  [a:=t] so we take t ∈ Λ and show vσ ∈ A σ[a:=t] . This is true by induction hypothesis since a ∈ F V (Γ ) and hence σ[a := t] realizes Γ . (∀ e ) We need to show tσ ∈ A[a := u] ⊥⊥ σ = A ⊥⊥ σ[a:=uσ] for some u ∈ Λ. By induction hypothesis we know tσ ∈ ∀a A ⊥⊥ σ , hence we only need to show that ∀a A ⊥⊥ σ ⊆ A ⊥⊥ σ[a:=uσ]. By definition we have ∀a A σ ⊆ A σ[a:=uσ] so we can conclude using lemma 8.

  [a:=u] . Since a / ∈ F V (Γ ), we obtain that the substitution σ[a := u] realizes the context Γ, x : A. Using the induction hypothesis, we finally get tσ = tσ[a := u] ∈ B ⊥⊥ σ[a:=u] = B ⊥⊥ σ since a / ∈ T V (t) and a / ∈ F V (B).

Theorem 11 .

 11 Let C, D ∈ C be constructors, and v, w ∈ Λ v be values. If C = D then C[v] ≡ D[w]. Proof. We take π = [λx case x [C[y] → y | D[y] → Ω]]α where Ω is an arbitrary diverging term. We then obtain C[v] * π ⇓ 0 and D[w] * π ⇑ 0 . Theorem 12. Let {l i = v i } i∈I and {l j = v j } j∈J be two records. If k is a index such that k ∈ I and k / ∈ J then we have {l

In ML the polymorphism mechanism is strongly linked with let-bindings. In OCaml syntax, they are expressions of the form let x = u in t.

This was originally denoted [α]u.

Our theorem

seems unrelated to lemma 9 in Munch-Maccagnoni's work[START_REF] Munch-Maccagnoni | Focalisation and classical realisability[END_REF].

Only En * πn can be of the form v * α.

We use the standard second-order encoding: ⊥ = ∀X0 X0 and ⊤ = ∃X0 X0.

Γ, t ≡ v ⊢ t : A a ∈ F V (Γ ) ∀ i,≡ Γ, t ≡ v ⊢ t : ∀a A Γ, u ≡ v ⊢ t : Π a:A B Γ, u ≡ v ⊢ u : A Π e,≡ Γ, u ≡ v ⊢ t u : B[a := u]

Γ, u1 ≡ u2 ⊢ t : A ↾i Γ, u1 ≡ u2 ⊢ t : A ↾ u1 ≡ u2 Γ, x : A, u1 ≡ u2 ⊢ t : B ↾e Γ, x : A ↾ u1 ≡ u2 ⊢ t : B Γ ⊢ val v : A a ∈ F V (Γ ) ∀i Γ ⊢ val v : ∀a A Γ ⊢ t : ∀a A ∀e Γ ⊢ t : A[a u] y : A ⊢ t : B a ∈ F V (Γ, B) ∪ T V (t) ∃e Γ, y : ∃a A ⊢ t : B Γ ⊢ t : A[a := u] ∃i Γ ⊢ t : ∃a A Γ ⊢ val v : A Xn ∈ F V (Γ ) ∀I Γ ⊢ val v : ∀Xn A Γ ⊢ t : ∀Xn A ∀E Γ ⊢ t : A[Xn := P ] Γ, x : A ⊢ t : B Xn ∈ F V (Γ, B) ∃E Γ, x : ∃Xn A ⊢ t : B Γ ⊢ t : A[Xn := P ] ∃I Γ ⊢ t : ∃Xn A [Γ ⊢ val vi : Ai] 1≤i≤n ×i Γ ⊢ val {li = vi} n i=1 : {li : Ai} 1≤i≤n Γ ⊢ val v : {li : Ai} 1≤i≤n ×e Γ ⊢ v.li : Ai Γ ⊢ val v : Ai +i

Acknowledgments

I would like to particularly thank my research advisor, Christophe Raffalli, for his guidance and input. I would also like to thank Alexandre Miquel for suggesting the encoding of dependent products. Thank you also to Pierre Hyvernat, Tom Hirschowitz, Robert Harper and the anonymous reviewers for their very helpful comments.


HAL is

Languages in contact: the case of Alsatian and French

-

  Features and cues are not as rigid as we might think. Some articulatory targets are clearly sufficient to ensure mutual understanding. -The question raised by these changes is that of the nature of phonological systems and their phonetic basis. -It seems feasible to suggest a more flexible reading of the phonetic system, based on variability and adaptation that arise within a group of different phonemes as part of language contact. Sock IPS et U.R 1339 (LiLPa) E.R Parole et Cognition Université de Strasbourg a b p/b

  (in ms) for initial G and K in Alsatian for 3 female speakers (M, J and C)


FR Jonathan Chappelon Lmpa
email: jonathan.chappelon@lmpa.univ-littoral.fr

REGULAR STEINHAUS GRAPHS OF ODD DEGREE

A Steinhaus matrix is a binary square matrix of size n which is symmetric, with diagonal of zeros, and whose upper-triangular coefficients satisfy a i,j = a i-1,j-1 +a i-1,j for all 2 i < j n. Steinhaus matrices are determined by their first row. A Steinhaus graph is a simple graph whose adjacency matrix is a Steinhaus matrix. We give a short new proof of a theorem, due to Dymacek, which states that even Steinhaus graphs, i.e. those with all vertex degrees even, have doubly-symmetric Steinhaus matrices. In 1979 Dymacek conjectured that the complete graph on two vertices K 2 is the only regular Steinhaus graph of odd degree. Using Dymacek's theorem, we prove that if (a i,j ) 1 i,j n is a Steinhaus matrix associated with a regular Steinhaus graph of odd degree then its sub-matrix (a i,j ) 2 i,j n-1 is a multi-symmetric matrix, that is a doubly-symmetric matrix where each row of its upper-triangular part is a symmetric sequence. We prove that the multi-symmetric Steinhaus matrices of size n whose Steinhaus graphs are regular modulo 4, i.e. where all vertex degrees are equal modulo 4, only depend on n 24 parameters for all even numbers n, and on n 30 parameters in the odd case. This result permits us to verify the Dymacek's conjecture up to 1500 vertices in the odd case.

Introduction

Let s = (a 1 , a 2 , . . . , a n-1 ) be a binary sequence of length n -1 1 with entries a j in F 2 = {0, 1}. The Steinhaus matrix associated with s is the square matrix M(s) = (a i,j ) of size n, defined as follows:

• a i,i = 0 for all 1 i n,

• a 1,j = a j-1 for all 2 j n,

• a i,j = a i-1,j-1 + a i-1,j for all 2 i < j n,

• a i,j = a j,i for all 1 i, j n.

By convention M(∅) = (0) is the Steinhaus matrix of size n = 1 associated with the empty sequence. For example, the following matrix M(s) in M 5 (F 2 ) is the Steinhaus matrix associated with the binary sequence s = (1, 1, 0, 0) of length 4.

M(s) =       0 1 1 0 0 1 0 0 1 0 1 0 0 1 1 0 1 1 0 0 0 0 1 0 0      
The set of all Steinhaus matrices of size n 2 will be denoted by SM n (F 2 ). It is clear that, for every positive integer n, the set SM n (F 2 ) has a cardinality of 2 n-1 .

The Steinhaus triangle associated with s is the upper-triangular part of the Steinhaus matrix M(s). It was introduced by Hugo Steinhaus in 1963 [START_REF] Steinhaus | One hundred problems in elementary mathematics[END_REF], who asked whether there exists a Steinhaus triangle containing as many 0's as 1's for each admissible size. Solutions of this problem appeared in [START_REF] Harborth | Solution of Steinhaus's problem with plus and minus signs[END_REF][START_REF] Eliahou | On a problem of Steinhaus concerning binary sequences[END_REF]. A generalization of this problem to all finite cyclic groups was posed in [START_REF] Molluzzo | Steinhaus graphs[END_REF] and was partially solved in [START_REF] Chappelon | On a problem of Molluzzo concerning Steinhaus triangles in finite cyclic groups[END_REF].

The Steinhaus graph associated with s is the simple graph G(s) on n vertices whose adjacency matrix is the Steinhaus matrix M(s). A vertex of a Steinhaus graph G(s) is usually labelled by its corresponding row number in M(s) and the ith vertex of G(s) will be denoted by V i . For instance, the following graph is the Steinhaus graph G(s) associated with the sequence s = (1, 1, 0, 0). 1 2 3 5 4

For every positive integer n, the zero-edge graph on n vertices is the Steinhaus graph associated with the sequence of zeros of length n -1.

Steinhaus graphs were introduced by Molluzzo in 1978 [START_REF] Molluzzo | Steinhaus graphs[END_REF]. A general problem on Steinhaus graphs is that of characterizing those satisfying a given graph property. The bipartite Steinhaus graphs were characterized in [START_REF] Chang | Characterizations of bipartite Steinhaus graphs[END_REF][START_REF] Dymacek | Bipartite Steinhaus graphs[END_REF][START_REF] Dymacek | Generating strings for bipartite Steinhaus graphs[END_REF] and the planar ones in [START_REF] Dymacek | Planar Steinhaus graphs[END_REF]. In [START_REF] Dymacek | Steinhaus graphs[END_REF], the following conjectures were made: Conjecture 1. The regular Steinhaus graphs of even degree are the zero-edge graph on n vertices, for all positive integers n, and the Steinhaus graph G(s) on n = 3m + 1 vertices generated by the periodic sequence s = (1, 1, 0, . . . , 1, 1, 0) of length 3m, for all positive integers m.

Conjecture 2. The complete graph on two vertices K 2 is the only regular Steinhaus graph of odd degree. These conjectures were verified up to n 25 in 1988 by exhaustive search [START_REF] Bailey | Regular Steinhaus graphs[END_REF]. More recently [START_REF] Augier | Parity-regular Steinhaus graphs[END_REF], Augier and Eliahou extended the verification up to n 117 vertices by considering the weaker notion of parity-regular Steinhaus graphs, i.e. Steinhaus graphs where all vertex degrees have the same parity. They searched regular graphs in the set of parityregular Steinhaus graphs. This has enabled them to perform the verification because it is known that Steinhaus matrices associated with parity-regular Steinhaus graphs on n vertices depend on approximately n/3 parameters [START_REF] Bailey | Regular Steinhaus graphs[END_REF][START_REF] Augier | Parity-regular Steinhaus graphs[END_REF]. This result is based on a theorem, due to Dymacek, which states that Steinhaus matrices associated with parity-regular Steinhaus graphs of even type are doubly-symmetric matrices, i.e. where all the entries are symmetric with respect to the diagonal and the anti-diagonal of the matrices. A short new proof of this theorem is given in Section 2. Using Dymacek's theorem, Bailey and Dymacek showed [START_REF] Bailey | Regular Steinhaus graphs[END_REF] that binary sequences associated with regular Steinhaus graphs of odd degree are of the form (x 1 , x 2 , . . . , x k , x k , . . . , x 2 , x 1 , 1). In Section 3, we refine this result and, more precisely, we prove that if (a i,j ) 1 i,j n is a Steinhaus matrix associated with a regular Steinhaus graph of odd degree, then its sub-matrix (a i,j ) 2 i,j n-1 is a multi-symmetric Steinhaus matrix, i.e. a doubly-symmetric matrix where each row of the upper-triangular part is a symmetric sequence. A parametrization and a counting of multi-symmetric Steinhaus matrices of size n are also given in Section 3 for all n 1. In Section 4, we show that, for a Steinhaus graph whose Steinhaus matrix is multi-symmetric, the knowledge of the vertex degrees modulo 4 leads to a system of binary equations on the entries of its Steinhaus matrix. In Section 5, we study the special case of multi-symmetric Steinhaus matrices whose Steinhaus graphs are regular modulo 4, i.e. where all vertex degrees are equal modulo 4. We show that a such matrix of size n only depends on n 24 parameters for all n even, and on n 30 parameters in the odd case. Using these parametrizations, we obtain, by computer search, that for all positive integers n 1500, the zero-edge graph on n vertices is the only Steinhaus graph on n vertices with a multi-symmetric matrix and which is regular modulo 4. This permits us to extend the verification of Conjecture 2 up to 1500 vertices.

A new proof of Dymacek's theorem

Recall that a square matrix M = (a i,j ) of size n 1 is said to be doubly-symmetric if the entries of M are symmetric with respect to the diagonal and to the anti-diagonal of M, that is a i,j = a j,i = a n-j+1,n-i+1 , for all 1 i, j n.

In [START_REF] Dymacek | Steinhaus graphs[END_REF], Dymacek characterized the parity-regular Steinhaus graphs. These results are based on the following theorem on parity-regular Steinhaus graphs of even type, where all vertex degrees are even.

Theorem 2.1 (Dymacek's theorem). The Steinhaus matrix of a parity-regular Steinhaus graph of even type is doubly-symmetric.

In this section we give a new easier proof of Dymacek's theorem. The main idea of our proof is that the anti-diagonal entries of a Steinhaus matrix are determined by the vertex degrees of its associated Steinhaus graph.

Theorem 2.2. Let G be a Steinhaus graph on n 2 vertices and M = (a i,j ) its associated Steinhaus matrix. Then every anti-diagonal entry of M can be expressed by means of the vertex degrees of G. If we denote by deg(V i ) the degree of the vertex V i in G, then for all 1 i n 2 , we have

a i,n-i+1 ≡ i-1 k=0 i -1 k deg (V i+k+1 ) ≡ i-1 k=0 i -1 k deg (V n-i-k ) (mod 2).
The proof is based on the following lemma which shows that each entry of the uppertriangular part of a Steinhaus matrix M = (a i,j ) can be expressed by means of the entries of the first row {a 1,2 , . . . , a 1,n }, the last column {a 1,n , . . . , a n-1,n } or the over-diagonal {a 1,2 , . . . , a n-1,n } of M. Lemma 2.3. Let M = (a i,j ) be a Steinhaus matrix of size n 2. Then, for all 1 i < j n, we have

a i,j = i-1 k=0 i -1 k a 1,j-k = n-j k=0 n -j k a i+k,n = j-i-1 k=0 j -i -1 k a i+k,i+k+1 .
Proof. Easily follows from the relation: a i,j = a i-1,j-1 + a i-1,j for all 2 i < j n.

Proof of Theorem 2.2. We begin by expressing each vertex degree of the Steinhaus graph G by means of the entries of the first row, the last column and the over-diagonal of M. Here we view the entries a i,j as 0,1 integers. For all 2 i n -1, we obtain

deg(V i ) = n j=1 a i,j = i-1 j=1 a j,i + n j=i+1 a i,j ≡ i-1 j=1 (a j,i+1 + a j+1,i+1 ) + n j=i+1 (a i-1,j-1 + a i-1,j ) ≡ i-1 j=1 a j,i+1 + i j=2 a j,i+1 + n-1 j=i a i-1,j + n j=i+1 a i-1,j ≡ a 1,i+1 + a i,i+1 + a i-1,i + a i-1,n (mod 2). By Lemma 2.3, it follows that i-1 k=0 i -1 k deg (V i+k+1 ) ≡ i-1 k=0 i -1 k (a 1,i+k+2 + a i+k+1,i+k+2 + a i+k,i+k+1 + a i+k,n ) ≡ i-1 k=0 i -1 k a 1,2i-k+1 + i-1 k=0 i -1 k a i+k+1,i+k+2 + i-1 k=0 i -1 k a i+k,i+k+1 + i-1 k=0 i -1 k a i+k,n ≡ a i,2i+1 + a i+1,2i+1 + a i,2i + a i,n-i+1 ≡ a i,n-i+1 (mod 2), for all 1 i n 2 .
The second congruence can be treated by the same way. Remark. We deduce from Theorem 2.2 a necessary condition on the vertex degrees of a given labelled graph to be a Steinhaus graph. Indeed, vertex degrees of a Steinhaus graph on n vertices must satisfy the following binary equations:

i-1 k=0 i -1 k deg (V i+k+1 ) ≡ i-1 k=0 i -1 k deg (V n-i-k ) (mod 2), for all 1 i n 2 .
More generally, an open problem, corresponding to Question 3 in [START_REF] Dymacek | A survey of Steinhaus graphs[END_REF], is to determine if an arbitrary graph, not necessary labelled, is isomorphic to a Steinhaus graph. Now, we characterize doubly-symmetric Steinhaus matrices.

Proposition 2.4. Let M = (a i,j ) be a Steinhaus matrix of size n 3. Then the following assertions are equivalent:

(i) the matrix M is doubly-symmetric, (ii) the over-diagonal of M is a symmetric sequence, (iii) the entries a i,n-i+1 of the anti-diagonal of M vanish for all 1 i n-1 2 .
Proof.

(i) =⇒ (ii) : Trivial.

(ii) =⇒ (iii) : Suppose that the over-diagonal of M is a symmetric sequence, that is

a i,i+1 = a n-i,n-i+1 ,
for all 1 i n -1. If n is odd, then we have

a i,n-i+1 = n-2i k=0 n -2i k a i+k,i+k+1 = n-2i+1 2 k=0 n -2i k (a i+k,i+k+1 + a n-i-k,n-i-k+1 ) = 0, for all 1 i n-1 2
. Otherwise, if n is even, then we obtain

a i,n-i+1 = n 2 -i-1 k=0 n -2i k (a i+k,i+k+1 + a n-i-k,n-i-k+1 ) + 2 n -2i -1 n 2 -i a n 2 , n 2 +1 = 0, for all 1 i n-1 2
.

(iii) =⇒ (i) : By induction on n. Consider the sub-matrix N = (a i,j ) 2 i,j n-1 that is a Steinhaus matrix of size n -2. By induction hypothesis, the matrix N is doubly-symmetric.

Then it remains to prove that a 1,j = a n-j+1,n for all 2 j n. First, since a 1,n = 0, it follows that a 1,n-1 = a 1,n + a 2,n = a 2,n and for all 2 j n -2, we have

a 1,j = n-1 k=j+1 a 2,k + a 1,n-1 = n-j k=2 a k,n-1 + a 2,n = a n-j+1,n .
We are now ready to prove Dymacek's theorem.

Proof of Theorem 2.1. Let G be a parity-regular Steinhaus graph of even type on n vertices and M = (a i,j ) its Steinhaus matrix. If n = 1, then M = (0) which is trivially doublysymmetric. Otherwise, for n 2, Theorem 2.2 implies that

a i,n-i+1 ≡ i-1 k=0 i -1 k deg (V i+k+1 ) ≡ 0 (mod 2),
for all 1 i n 2 . Finally, the matrix M is doubly-symmetric by Proposition 2.4.

Multi-symmetric Steinhaus matrices

In this section, we will study in detail the structure of Steinhaus matrices associated with regular Steinhaus graphs of odd degree.

Let G be a Steinhaus graph on n 1 vertices. Then, for every integer 1 i n, we denote by G \ {V i } the graph obtained from G by deleting its ith vertex V i and its incident edges in G. Since the adjacency matrix of the graph G\{V 1 } (resp. G\{V n }) is the Steinhaus matrix obtained by removing the first row (resp. the last column) in the adjacency matrix of G, it follows that the graph

G \ {V 1 } (resp. G \ {V n }) is a Steinhaus graph on n -1 vertices.
Bailey and Dymacek studied the regular Steinhaus graphs of odd degree in [START_REF] Bailey | Regular Steinhaus graphs[END_REF], where the following theorem is stated, using Dymacek's theorem.

Theorem 3.1 ([2]

). Let G be a regular Steinhaus graph of odd degree d on 2n 4 vertices. Then d = n, the Steinhaus graph G \ {V 1 , V 2n } is regular of even degree n -1, and a 1,j = a 1,2n-j+1 for all 2 j 2n -1.

Remark. In every simple graph, there are an even number of vertices of odd degree. Therefore parity-regular Steinhaus graphs of odd type and thus regular Steinhaus graphs of odd degree have an even number of vertices.

In their theorem, the authors studied the form of the sequence associated with G. We are more interested in the Steinhaus matrix of G \ {V 1 , V 2n } in the sequel.

Recall that a square matrix of size n 1 is said to be multi-symmetric if M is doublysymmetric and each row of the upper-triangular part of M is a symmetric sequence, that is a i,j = a i,n-j+i+1 , for all 1 i < j n.

First, it is easy to see that each column of the upper-triangular part of a multi-symmetric matrix is also a symmetric sequence. Proposition 3.2. Let M = (a i,j ) be a multi-symmetric matrix of size n. Then, each column of the upper-triangular part of M is a symmetric sequence, that is a i,j = a j-i,j for all 1 i < j n.

Proof. Easily follows from the relation: a i,j = a i,n-j+i+1 = a j-i,n-i+1 = a j-i,j for all 1 i < j n.

As for doubly-symmetric Steinhaus matrices, multi-symmetric Steinhaus matrices can be characterized as follows.

Proposition 3.3. Let M = (a i,j ) be a Steinhaus matrix of size n 3. Then the following assertions are equivalent: (i) the matrix M is multi-symmetric, (ii) the first row, the last column and the over-diagonal of M are symmetric sequences, (iii) the entries a i,n-i+1 , a n-2i+1,n-i+1 and a i,2i vanish for all 1 i n-1 2

.

Proof. Similar to the proof of Proposition 2.4 and by using Lemma 2.3 and Proposition 3.2.

We now refine Theorem 3.1. Proof. Let M = (a i,j ) be the Steinhaus matrix associated with G. Theorem 3.1 implies that the Steinhaus graph G \ {V 1 , V 2n } is regular of even degree n -1 and that we have

a 1,j = a 1,2n-j+1 ,
for all 2 j 2n -1. Therefore, for all 3 j 2n -1, we have a 2,j +a 2,2n-j+2 = (a 1,j-1 +a 1,j )+(a 1,2n-j+1 +a 1,2n-j+2 ) = (a 1,j-1 +a 1,2n-j+2 )+(a 1,j +a 1,2n-j+1 ) = 0.

Then the first row of the matrix B = (a i,j ) 2 i,j 2n-1 , the Steinhaus matrix of the graph In the sequel of this section we will study in detail the multi-symmetric Steinhaus matrices. First, in order to determine a parametrization of these matrices, we introduce the following operator

G \ {V 1 , V 2n },
T : SM n (F 2 ) -→ SM n-3 (F 2 ),
which assigns to each matrix M = (a i,j ) in SM n (F 2 ) the Steinhaus matrix T (M) = (b i,j ) in SM n-3 (F 2 ) defined by b i,j = a i-1,j-2 , for all 1 i < j n -3. As depicted in the following matrix, the upper-triangular part of M is an extension of the upper-triangular part of T (M).

                        0 a 1,2 a 1,3 a 1,4 a 1,5 a 1,6 • • • • • • a 1,n-4 a 1,n-3 a 1,n-2 a 1,n-1 a 1,n 0 a 2,3 b 1,2 b 1,3 b 1,4 • • • • • • • • • b 1,n-5 b 1,n-4 b 1,n-3 a 2,n 0 a 3,4 b 2,3 b 2,4 b 2,n-4 b 2,n-3 a 3,n 0 a 4,
0 a n-5,n-4 b n-6,n-5 b n-6,n-4 b n-6,n-3 a n-5,n 0 a n-4,n-3 b n-5,n-4 b n-5,n-3 a n-4,n 0 a n-3,n-2 b n-4,n-3 a n-3,n 0 a n-2,n-1 a n-2,n 0 a n-1,n 0                         Proposition 3.5. Let M = (a i,j
) be a Steinhaus matrix of size n 4. Then the extension M of T (M) only depends on the parameters a 1,2 , a 1,j 0 and a 1,n , with j 0 in {3, . . . , n -1}.

Proof. Let 3 j 0 n -1. Each entry a 1,j , for 3 j n -1, can be expressed by means of a 1,j 0 and the entries of T (M) = (b i,j ). Indeed, we have

a 1,j = a 1,j 0 + j 0 -2 k=j-1 b 1,k , for all 3 j < j 0 , a 1,j = a 1,j 0 + j-2 k=j 0 -1 b 1,k , for all j 0 < j n -1.
Then the entries a 1,2 , a 1,j 0 and a 1,n determine the extension M of T (M).

Therefore, for every Steinhaus matrix N of size n -3, there exist 8 distinct Steinhaus matrices M of size n such that T (M) = N. We can also use this operator to determine parametrizations of multi-symmetric Steinhaus matrices. Proposition 3.6. Let M = (a i,j ) be a multi-symmetric Steinhaus matrix of size n. Let j i be an element of the set {2i + 1, . . . , n -i} for all 1 i n-1 3

. Then the matrix M depends on the following parameters:

• a 1,j 1 and a 2i,j 2i 1 i n 6 -1 , for n even, • a 2i+1,j 2i+1 0 i n-3 6 -1 , for n odd.
Proof. Let M = (a i,j ) be a multi-symmetric matrix of size n. We consider the sub-matrices T (M), T 2 (M) = T (T (M)), T 3 (M), T 4 (M), . . .. By successive application of Proposition 3.5 on the extension T i-1 (M) of T i (M) and since the entries a i,n-i+1 , a n-2i+1,n-i+1 and a i,2i vanish for all 1 i

MS(n) = 2 ⌈ n 6 ⌉ , for n even, 2 ⌈ n-3
6 ⌉ , for n odd.

Vertex degrees of Steinhaus graphs associated with multi-symmetric Steinhaus matrices

In this section, we analyse the vertex degrees of a Steinhaus graph associated with a multisymmetric Steinhaus matrix of size n. We begin with the case of doubly-symmetric Steinhaus matrices.

Proposition 4.1. Let n be a positive integer and G be a Steinhaus graph on n vertices whose Steinhaus matrix is doubly-symmetric. Then, for all 1 i n, we have

deg(V i ) = deg(V n-i+1 ).
Proof. If we denote by M = (a i,j ) the Steinhaus matrix associated with the graph G, then, for all 1 i n, we have

deg(V i ) = n j=1 a i,j = n j=1 a n-j+1,n-i+1 = n j=1 a j,n-i+1 = deg(V n-i+1 ).
We shall now see that, for a Steinhaus graph associated with a multi-symmetric Steinhaus matrix, the knowledge of the vertex degrees modulo 4 imposes strong conditions on the entries of its Steinhaus matrix. In order to prove this result, we distinguish different cases depending on the parity of n. Proposition 4.2. Let n be an even number and G be a Steinhaus graph on n vertices whose Steinhaus matrix M = (a i,j ) is multi-symmetric. Then, we have

deg(V 1 ) = deg(V n ) ≡ a 1, n 2 +1 (mod 2), deg(V 2 ) = deg(V n-1 ) ≡ 2a 1, n 2 +1 (mod 4), deg(V 3 ) = deg(V n-2 ) ≡ 2a 2, n 2 +1 (mod 4), deg(V 2i ) = deg(V n-2i+1 ) ≡ 2a 2,2i+1 + 2a i,2i+1 (mod 4), for all 2 i n 2 -2.
Proof. First, Proposition 3.3 implies that the entries a i,2i and a 2i+1, n 2 +i+1 vanish for all 1 i n 2 -1. This leads to

deg(V 1 ) = n j=2 a 1,j = n 2 j=2 (a 1,j + a 1,n-j+2 ) + a 1, n 2 +1 ≡ a 1, n 2 +1 (mod 2), deg(V 2 ) = a 1,2 + n 2 +1 j=3 (a 2,j + a 2,n-j+3 ) = 2 n 2 +1 j=3 a 2,j ≡ 2a 1,2 + 2a 1, n 2 +1 ≡ 2a 1, n 2 +1
(mod 4),

deg(V 3 ) = (a 1,3 + a 2,3 ) + n 2 +1 j=4 (a 3,j + a 3,n-j+4 ) + a 3, n 2 +2 = 2a 2,3 + 2 n 2 +1 j=4 a 3,j ≡ 2a 2, n 2 +1
(mod 4), and, for all 2 i n 2 -2, we have

deg(V 2i ) = 2i-1 j=i+1 (a j,2i + a 2i-j,2i ) + a i,2i + n 2 +i j=2i+1 (a 2i,j + a 2i,n-j+2i+1 ) = 2 2i-1 j=i+1 a j,2i + 2 n 2 +i j=2i+1 a 2i,j ≡ 2 2i-1 j=i+1 a j,2i+1 + 2 2i j=i+2 a j,2i+1 + 2 n 2 +i-1 j=2i a 2i-1,j + 2 n 2 +i j=2i+1 a 2i-1,j ≡ 2a i+1,2i+1 + 2a 2i,2i+1 + 2a 2i-1,2i + 2a 2i-1, n 2 +i ≡ 2a i+1,2i+1 + 2a 2i-1,2i+1 ≡ 2a 2,2i+1 + 2a i,2i+1 (mod 4).
Finally, we complete the proof by Proposition 4.1.

Remark. Let n be an even number. In every Steinhaus graph on n vertices whose Steinhaus matrix is multi-symmetric the fourth vertex V 4 has a degree divisible by 4.

Proposition 4.3. Let n be an odd number and G be a Steinhaus graph on n vertices whose Steinhaus matrix M = (a i,j ) is multi-symmetric. Then, we have

deg(V 1 ) = deg(V n ) ≡ 0 (mod 2), deg(V 2 ) = deg(V n-1 ) ≡ 2a 1, n+1 2
(mod 4), deg(V 2i ) ≡ 2a i+1,2i+1 + 2a 2i-1,2i+1 + 2a 2i-1, n-1 2 +i (mod 4), for all 2 i n-3 2 , deg(V 2i+1 ) ≡ 2a 2,2i+2 (mod 4), for all 1 i n-3 2 .
Proof. Proposition 3.3 implies that the entries a i,2i and a 2i,(n+1)/2+i vanish for all 1 i n-3 2 . Since each row and each column of the upper triangular part of M is symmetric, we can use the relation m k=1 a i,j+k ≡ a i-1,j + a i-1,j+m (mod 2), for all 2 i < j nm + 1 as in the proof of Proposition 4.2, and the results follow.

Remark. Let n be an odd number. In every Steinhaus graph on n vertices whose Steinhaus matrix is multi-symmetric the third vertex V 3 has a degree divisible by 4.

Multi-symmetric Steinhaus matrices of Steinhaus graphs with regularity modulo 4

In this section, we consider the multi-symmetric Steinhaus matrices associated with Steinhaus graphs which are regular modulo 4, i.e. where all vertex degrees are equal modulo 4. First, we determine an upper bound of the number of these matrices. Two cases are distinguished, according to the parity of n. Proof. Let n be an odd number and M = (a i,j ) a multi-symmetric Steinhaus matrix of size n. By Proposition 3.6, the matrix M depends on the parameters a 2i+1, n+1

2 +i for 0 i n-3 6

-1. If the Steinhaus graph associated with M is regular modulo 4, then Proposition 4.3 implies that a 2,2j = 0 for all 2 j n-1 2 and thus

a 2i,2j = i-1 k=0 a 2,2j-2k = 0,
for all 1 i < j n-1 2 . If n ≡ 1 (mod 4), then n+1

2 is odd and

a 4i+1, n+1 2 +2i = a 4i, n-1 2 +2i + a 4i, n+1 2 +2i = 0, for all 0 i ⌈ n-3 6 ⌉-1 2
. Therefore the matrix M can be parametrized by

a 4i+3, n+3 2 +2i 0 i m -1 , with m = n-3 6 - 1 2
.

Suppose that we know the p parameters in

P = a 4i+3, n+3 2 +2i
mp i m -1 .

Then, by Proposition 3.6 again, the multi-symmetric matrix T 4(m-p)-1 (M) can be parametrized by P . Therefore the entries

a i,2i+1 4(m -p) i n -1 2 -2(m -p)
in T 4(m-p)-1 (M) depend on the parameters in P . Moreover, if the Steinhaus graph associated with M is regular modulo 4, then Proposition 4.3 implies that

a 2,2i+1 = a 2i-1,2i+1 ≡ a i+1,2i+1 + a 2i-1, n-1 2 +i ≡ a i+1,2i+1 + a ( n+1 2 -i)+1,2( n+1 2 -i)+1 (mod 2), for all 1 i n-1 2 . If the inequality n + 1 2 -4(m -p) 4(m -p)
holds, then the entries a 2,2i+1 depend on the parameters in P for all 4(mp) i n+1 2 -4(mp). Since we have a 2,2i = 0 for all 4(mp) i n+3 2 -4(mp), it follows that the entries

a i,j 2 i n + 5 -16(m -p) 8(m -p) + i -1 j n + 3 -8(m -p)
depend on the parameters in P . Suppose now that p is solution of the following inequality

n + 5 -16(m -p) 4(m -p) -1.
Therefore the extension M of T (4(m-p)-1) (M) depends on the entries a i,n+3-8(m-p) for 2 i 4(mp) -1 and a 1, n+1 2 which vanishes by Proposition 4.3. Thus, all the entries of the matrix M depend on the p parameters in P . Finally, a solution of this inequality can be obtained when

p = n 30 n-3 6 -1 2 - n + 6 20 .
If n ≡ 3 (mod 4), then n+1 2 is even and

a 4i+3, n+3 2 +2i = a 4i+2, n+1 2 +2i + a 4i+2, n+3 2 +2i = 0, for all 0 i ⌈ n-3 6 ⌉-1 2 -1.
Therefore the matrix M can be parametrized by

a 4i+1, n+1 2 +2i 0 i m with m = n-3 6 -1 2 .
As above, in the case n ≡ 1 (mod 4), we can prove that all the entries of the matrix M depend on the p parameters in

a 4i+1, n+1 2 +2i m -p + 1 i m if p is solution of the following inequality n -16(m -p) -4 4(m -p) + 1.
A solution is obtained when

p = n 30 n-3 6 -1 2 - n -5 20 .
Theorem 5.2. For all even numbers n, there are at most 2 ⌈ n 24 ⌉ multi-symmetric Steinhaus matrices of size n whose associated Steinhaus graphs are regular modulo 4.

Sketch of proof. Similar to the proof of Theorem 5.1. Let M = (a i,j ) be a multi-symmetric Steinhaus matrix of even size n. First, by Proposition 3.6, for all positive integers p < m -1 with m = n 6 , the multi-symmetric Steinhaus matrix T 2(m-p-1) (M) can be parametrized by the p entries in

P = {a 2i,4i+1 | m -p i m -1} .
Moreover, if the Steinhaus graph associated with M is regular modulo 4, then Proposition 4.2 implies that a 1, n 2 +1 = 0 and a 2,2i+1 = a i,2i+1 for all 2 i n 2 -1. It follows that the entries a 2i,n-2(m-p)+1 also depends on the parameters in P for all 1 i n 2 -3(mp) + 2. Finally, we can see that, if p is solution of the following inequality

n 2 -3(m -p) + 2 m -p -1,
then, as in the proof of Proposition 3.6, the extension M of T 2(m-p-1) (M) depends on the entries a 2i,n-2(m-p)+1 for 1 i mp -1 and thus all the entries of the matrix M can be expressed by means of the p parameters in P . We conclude the proof by observing that the inequality is obtained when

p = n 24 n 6 - n + 6 8 .
Using these explicit parametrizations of the multi-symmetric Steinhaus matrices whose Steinhaus graphs are regular modulo 4, we obtain the following result by computer search:

Computational Result. For all positive integers n 1500, the zero-edge graph on n vertices is the only Steinhaus graph on n vertices with a multi-symmetric Steinhaus matrix and which is regular modulo 4. This result can be easily proved for all odd numbers in the special case of regular Steinhaus graphs on n vertices whose Steinhaus matrices are multi-symmetric. This leads to deg(V i ) = 0 for all 1 i n and thus G is the zero-edge graph on n vertices.

Finally, the above computational result permits us to extend the verification of Conjecture 2 up to n 1500 vertices. Indeed, as proved in the remark following Theorem 3.4, for a Steinhaus graph G on 2n vertices, if G \ {V 1 , V 2n } is the zero-edge graph on 2n -2 vertices, then G is the star graph on 2n vertices which is not a regular graph. Therefore, by Theorem 3.4, we obtain Theorem 5.4. There is no regular Steinhaus graph of odd degree on 2 < n 1500 vertices.

Theorem 3 . 4 .

 34 Let G be a regular Steinhaus graph of odd degree n on 2n 4 vertices. Then G \ {V 1 , V 2n } is a regular Steinhaus graph of even degree n -1 whose associated Steinhaus matrix is multi-symmetric.

n-1 2 by

 2 Proposition 3.3, the parametrizations of the multisymmetric matrix M follow. For all positive integers n, the number of multi-symmetric Steinhaus matrices of size n immediately follows. Theorem 3.7. Let n be a positive integer. If we denote by MS(n) the number of multisymmetric Steinhaus matrices of size n, then we have

Theorem 5 . 1 .

 51 For all odd numbers n, there are at most 2 ⌈ n 30 ⌉ multi-symmetric Steinhaus matrices of size n whose associated Steinhaus graphs are regular modulo 4.

Theorem 5 . 3 . 2 j=2(a 3 ,= 2a 2, 3 + n-3 2 j=2(a 2 ,

 5323322 For all odd numbers n, there is no regular Steinhaus graph on n vertices whose Steinhaus matrix is multi-symmetric, except the zero-edge graph on n vertices.Proof. Let n be an odd number. Let G be a regular Steinhaus graph on n vertices and M = (a i,j ) its Steinhaus matrix. Then Proposition 4.3 implies that deg(V i ) ≡ 0 (mod 4), for all 1 i n and a 2,2i+2 = 0, for all 1 i n-3 2 . If we denote by ⊕ the addition in F 2 and + the addition in the integers, then we obtaindeg(V 3 ) = a 1,3 + a 2,3 + n j=4 a 3,j = (a 1,2 ⊕ a 2,3 + a 2,3 ) + n-3 2j+1 + a 3,2j+2 ) + 2a 3,n 2j ⊕ a 2,2j+1 + a 2,2j+1 ⊕ a 2,2j+2 ) + 2(a 2,n-1 ⊕ a 2,n ) j ) = 2 × deg(V 2 ).

  is a symmetric sequence. Moreover, by Dymacek's theorem, the matrix B is doubly-symmetric. Finally, by Proposition 3.3, the matrix B is multi-symmetric.Remark. By Theorem 3.4, it is easy to show that Conjecture 1 implies Conjecture 2. Indeed, if Conjecture 1 is true, then the zero-edge graph on n vertices is the only regular Steinhaus graph of even degree whose Steinhaus matrix is multi-symmetric. It follows, byTheorem 3.4,

that if G(s) is a regular Steinhaus graph of odd degree on n + 2 vertices then s = (0, . . . , 0, 1) or s = (1, . . . , 1). Therefore the Steinhaus graph G(s) is the star graph on n + 2 vertices which is not a regular Steinhaus graph.

Acknowledgments

The author would like to thank Shalom Eliahou for introducing him to the subject and for his help in preparing this paper.