D A Feller

J B Wells

Sébastien Carlier

F Kamareddine

What Does This Notation Mean Anyway? BNF-Style Notation as it is Actually Used

Following the introduction of BNF notation by Backus for the Algol 60 report and subsequent notational variants, a metalanguage involving formal "grammars" has developed for discussing structured objects in Computer Science and Mathematical Logic. We refer to this offspring of BNF as Math-BNF or MBNF, to the original BNF and its notational variants just as BNF, and to aspects common to both as BNF-style. What all BNF-style notations share is the use of production rules roughly of this form:

•

Normally, such a rule says "every instance of • i for i ∈ {1, . . . , n} is also an instance of •". MBNF is distinct from BNF in the entities and operations it allows. Instead of strings, MBNF builds arrangements of symbols that we call math-text. Sometimes "syntax" is defined by interleaving MBNF production rules and other mathematical definitions that can contain chunks of math-text.

There is no clear definition of MBNF. Readers do not have a document which tells them how MBNF is to be read and must learn MBNF through a process of cultural initiation. To the extent that MBNF is defined, it is largely through examples scattered throughout the literature.

This paper gives MBNF examples illustrating some of the differences between MBNF and BNF. We propose a definition of syntactic math text (SMT) which handles many (but far from all) uses of math-text and MBNF in the wild. We aim to balance the goal of being accessible and not requiring too much prerequisite knowledge with the conflicting goal of providing a rich mathematical structure that already supports many uses and has possibilities to be extended to support more challenging cases.

Background and Motivation

Understanding MBNF is important to interpreting papers in theoretical computer science. Out of the 30 papers in the ESOP 2012 proceedings [START_REF]Programming Languages and Systems[END_REF], 19 used MBNF, while not one used BNF. 1 This section highlights some of the ways in which the notation we call MBNF differs from BNF. This should demonstrate that a definition could be helpful.

Where BNF uses Strings, MBNF Uses Math-Text In addition to arranging symbols from left to right on the page, math-text allows subscripting, superscripting, and placing text above or below other text. It also allows for marking whole segments of text, for example with an overbar (a vinculum). Readers can find more detailed information on how math-text can be laid out in The TeXbook [START_REF] Knuth | The TeXbook[END_REF], or the Presentation MathML [START_REF] Patrick D F Ion | Mathematical Markup Language (MathML) Version 2.0. W3C Recommendation, W3C[END_REF] and OpenDocument [START_REF]Information technology -Open Document Format for Office Applications (OpenDocument) v1.2 -Part 1: OpenDocument Schema. Standard[END_REF] standards. Here is a nonsense piece of Math-text to illustrate how it may be laid out:

c ↓ a ′ = p v ′′ x ⊙ a 2+1 -f n x + y • f j + ∞ i=0 s i∈1...n -a,b,c ---→ bâ
Instead of non-terminal symbols, MBNF uses metavariables2 , which appear in math-text and obey the conventions of mathematical variables. Metavariables are not distinguished from other symbols by annotating them as BNF does, but by font, spacing, or merely tradition.

Parentheses for disambiguation are not needed in MBNF grammars and when an MBNF grammar specifies such parentheses they can often be omitted without any need to explain. When possible, MBNF takes advantage of the tree-like structure implicit in the layout of symbols on the page when features like superscripting and overbarring are used.

MBNF Is Aimed at Human Readers MBNF is meant to be interpreted by humans, not computers/parser generators. It is common to define a MBNF grammar in an article for humans and a separate EBNF grammar for use with a parser generator to build a corresponding implementation. Entities defined with MBNF are not intended or expected to be serialized or parsed and MBNF grammars are typically missing features needed to disambiguate complex terms. Papers often put complicated uses of the mathematical metalanguage in the middle of MBNF notation.

MBNF Allows Powerful Operators Like Context Hole Filling (a.k.a. Tree Splicing) Chang and Felleisen [2, p 134] present an MBNF grammar defining the λ-term contexts with one hole where the spine 3 is a balanced segment 4 ending in a hole. For explanatory purposes we alter their grammar slightly by writing e@e instead of e e and adding parentheses. Concrete syntax and BNF-style notation are green. Metavariables are blue. Additional operators are red. One can think of the context hole filling operation in this grammar ([ ] in (A[(λx.A)]@e)) as performing tree splicing operations within the syntax. Consider these trees which illustrate steps in building syntax trees for A:

@ [ ] [ ] λx 1 [ ] x 2 @ λx 1 [ ] x 2
These trees show the result of the second rule where each A is [ ] and e is a variable. The tree on the left is the tree corresponding to A[λx.A]@e before the hole filling operation is performed, where the first A is assigned [ ]. The tree on the right represents an unparsing of what we would normally consider the syntax tree for ((λx 1 .[ ])@x 2 ). We write x 1 and x 2 for disambiguated instances of x. A metavariable assigned a value won't appear in the final tree. If it's not a terminal node, [ ] tells us to fill in the leaf in the frame on the left with the the tree in the frame on the right. Once performed, [ ] disappears.

Unlike BNF, the "language" of the metavariable/non-terminal A (the set of strings derived from A using roughly the rules of BNF plus hole filling) is not context-free and so MBNF certainly isn't. [4, pg 20] mix BNF-style notation freely with mathematical notation in such a way that the resulting grammar relies upon both sets produced from the result of MBNF calculations and MBNF production rules which use metavariables defined using mathematical notation: u ∈ UVar = a set of identifiers ccall ∈ CCall ::= (q e * ) γ k ∈ CVar = a set of identifiers e, f ∈ UExp = UVar + ULam lam ∈ Lam = ULam + CLam q ∈ CExp = CVar + CLam ulam ∈ ULam ::= (λe(u * k)call)

MBNF Mixes Math Stuff With BNF-Style Notation Germane and Might

ℓ ∈ ULab = a set of labels clam ∈ CLam ::= (λ γ (u * )call)

γ ∈ CLab = a set of labels call ∈ Call = UCall + CCall ucall ∈ UCall ::= ( f e * q) ℓ The results of math computations are interleaved with MBNF production rules, not just applied after the results of the production rules have been obtained. This grammar uses • 1 ∈ • 2 to mean "• 2 is the language of • 1 " (this is the case in both the MBNF production rules (::=) and the math itself (=)).

MBNF Has at

Least the Power of Indexed Grammars Inoe and Taha [7, pg 361] use this MBNF:

E ℓ,m ∈ ECtx ℓ,m n ::= • • • | E ℓ+1,m | • • •
This suggests that MBNF deals with the family of indexed grammars [6, p 389-390], which is yet another reason it's not context-free. The ℓ + 1 is a calculation that is not intended to be part of the syntax. The production rule above defines an infinite set of metavariables ranging over different sets.

MBNF Allows Arbitrary Side Conditions on Production Rules An example of a production rule with a side condition can be found in Chang and Felleisen [2, p 134]:

E = [ ] | Ee | A[E] | Â[A[λx. Ǎ[E[x]]]E] where Â[ Ǎ] ∈ A
It is possible to make side conditions that prevent MBNF rules from having a solution. A definition for MBNF can help in finding restrictions on side conditions that ensure MBNF rules actually define something.

MBNF "Syntax" Can Contain Very Large Infinite Sets

e ::= • • • | t set , {e * κ }
We are told {e * κ } denotes "sets comprised of no more than κ terms from the language of e". The author does not state what κ is, but elsewhere in the paper it is an inaccessible cardinal. It seems as though κ is also intended to be an inaccessible cardinal here. This section of an MBNF for e is taken from a larger MBNF that contains a term which ranges over all the encodings of all the hereditarily accessible sets. BNF, by contrast, only deals with strings of finite length.

MBNF Allows Infinitary Operators Fdo, Díaz and Núñez [12, p 539] write an MBNF with the following operator:

P ::= • • • | i∈I P i | • • •
The authors state this is infinitary (i.e. we should regard I to be infinite). The authors tell us the MBNF this is taken from is defined by regarding (M)BNF expressions as fixed point equations and a least fixed point can be found by bounding the size of the possible set of indices by some infinite cardinal. We may think of infinitary operators as allowing us to define trees of infinite breadth (i.e. trees whose internal nodes may have infinitely many direct children), where BNF only deals with finite strings.

MBNF Allows Co-Inductive Definitions Eberhart, Hirschowitz and Seiller [3, p 94] intend the following MBNF to define infinite terms co-inductively:

P, Q ::= Σ i∈n G i | (P|Q) G ::= a b .P | a(b).P | νa.P | τ.P | ♥.P
We may think of co-inductive definitions as allowing us to define trees of infinite depth (i.e. trees in which paths may pass through infinitely many nodes), where BNF only deals with finite strings.

A Method to Allow Reading Some Uses of Mathematical "Syntax"

This section defines syntactic math text (SMT) which will allow reading some uses of math text as being "syntax" and standing for essentially themselves, e.g., 1 + 3 can continue to stand for 4 while λx.x can in some sense stand for itself. SMT plus a definition of the ::= notation allows us to interpret the more common uses of MBNF as they are written. It also provides some support for more complicated uses with a little extra machinery. We do not aim to cover every use of MBNF in the literature, but we hope to provide a good foundation which can be built upon.

As well as dealing with some of MBNF, SMT provides a more general notion of objects appearing within syntax that behave like equivalences over chunks of math-text representing syntax. This enables us to interpret working modulo equivalences on math-text representing syntax.

Kamareddine et al. [START_REF] Kamareddine | Computerising Mathematical Text[END_REF] make the point that converting mathematical text to a form where it can be checked by a proof assistant is a process that involves both human input and intermediary translations. Our proposal focuses on the translation, performed by the reader, of math-text used to define syntax, as it appears in a document, to a more formal structure, which is not encoded in the language of a theorem prover or proof assistant.

Our proposal relies as much as possible on the mathematical meta-level. For example, we use ellipses and related methods for abbreviating sequences from the mathematical meta-level. Incomplete definitions (relying on some choice of metavariable) cause the resulting grammar to be defined as the output of a function depending on this choice. Any otherwise pointless statement of the form x ∈ S declares x and any decorated x (e.g., x 1 , x 2 , . . ., x ′ , x ′′ , etc.) as a variable ranging over S .

Our proposal is intended to be descriptive rather than prescriptive. We aim to handle both historical documents and new works. For published uses of MBNF that our proposal fails to handle, this is a problem to be solved in future work. We do not aim at displacing the input languages of proof assistants or syntactic variants of BNF which already have solid definitions.

Objects, Arrangements, and Symbols

We now define the main notion of syntactic objects and the auxiliary notion of arrangements. In essence, syntactic objects are arrangements of symbols, numbers, and pointers to subobjects, where the arrangement can include left-to-right sequencing, superscripting, subscripting and overlining. We use pointers to subobjects inside objects rather than the subobjects themselves, because the sets within the model for objects would be too large otherwise and because we wanted to allow for objects to be nested within themselves, provided some syntax is added as part of this nesting. To support α-conversion and operators that are associative, commutative, idempotent, etc., the objects are defined so that in effect they work modulo an equivalence relation on arrangements that is defined separately.

Let s range over the set Symbol containing syntactic symbols to be used in arrangements. We require that Symbol is disjoint from all other sets defined here. We also require that some symbols are not in Symbol, namely the square brackets ("[" and "]") and the special square symbol (which represents a hole in which an object can be placed). The symbols can include letters, parentheses and other parenthesis-like symbols (e.g., and and [ and ]), punctuation, and other symbols. Letters (Roman or Greek) used as syntactic symbols will be typeset using an upright sans-serif font to distinguish them from metavariables which are written in a slanted serif font (generally italics). For example, a, C, λ, and Γ could be syntactic symbols while a, C, λ, and Γ would be metavariables. We avoid using any particular letter both ways, except for symbols used in names, where for example x i could be a syntactic name at the same time as x could be a metavariable ranging over names (see section 2.5).

The set Object of syntactic objects and the set Arrangement of syntactic arrangements are defined simultaneously. Let O range over Object and let A range over Arrangement. We represent each object by a member of the set Pointer. Let P O be the pointer that indicates O. Let ≈ ⊂ Arrangement × Arrangement be an equivalence relation that is reflexive on Arrangement. We require that if A 1 ≈ A 2 and A 1 A 2 , then neither A 1 nor A 2 may have used the special object in their construction.

The sets Object and Arrangement are the smallest sets satisfying the following conditions.

1. The empty arrangement ǫ is in Arrangement.

2. The core items of arrangements are symbols, pointers to objects, numbers, and overlined arrangements. For any symbol s, pointer P O , number n ∈ N, and nonempty arrangement A ǫ, all of the following are in Arrangement: s, P O , n, and A. Furthermore, these are all core arrangements, which are ranged over by the metavariable Â.

3. Left-to-right sequencing allows appending additional core arrangements to a non-empt arrangement. For any arrangement A ǫ and core arrangement Â, it holds that A Â is in Arrangement.

4. Superscripting, subscripting etc. are supported. For non-empty arrangements A, A 1 and A 2 , all of the following are in Arrangement:

A A 1 , A A 2 , A A 1 A 2 , A 1 A... 5.
If S contains does not contain any arrangements consisting of a bare pointer to an object, S is non-empty, and |S| ≤ ℵ 0 , then S ∈ Object.

If S ⊂ Arrangement is not an equivalence class of ≈ or any members of S are ill-formed, then S is ill-formed. An arrangement is ill-formed iff any of its subcomponents is ill-formed. (Symbols and natural numbers are well formed.) (Thus, it is allowed to build an object from ill-formed arrangements, and the resulting object is ill-formed.)

6. There is a special symbol in Object indicating a hole in which an object is to be placed.

There are various reasons why we have built equivalence classes into arrangements rather than making them identical to math-text. We want to eventually support math stuff in syntax, with math stuff containing objects not arrangements. We want to allow object-to-object operations in production rules. When we define equivalences inductively over arrangements we want some of that structure to be represented by our model.

We write [A] ≈ for the object that contains all the arrangements equivalent to A by the equivalence relation ≈. Only objects of the form [A] ≈ are well formed.

Syntax Shorthand: Arrangement Coercions

From example 2.13, the reader will observe that it's cumbersome to write P O in so many places when all we're interested in is the identity for objects. We introduce the following convention: Convention 2.1 (Coercing Objects to Pointers). We allow O to be written instead of

P O in an arrange- ment. Example 2.2. The expression [λO 1 .O 2 ] ≈ , stands for [λP O 1 .P O 2 ] ≈ .
We define meta-level parentheses to be those parentheses which surround a single object and which may optionally be omitted from some arrangements with a similar form. 5It is still cumbersome to write [ • ] ≈ in so many places. One of the ways we deal with this is to arrange for this to happen automatically at places where a piece of meta-level syntax requires an arrangement to be regarded as an object.

Convention 2.3 (Coercing Arrangements to Objects). We require that when an arrangement A is written, but the surrounding context only makes sense if the value of the expression is an object, then the arrangement A is implicitly coerced to the object [A] ≈ , as though the latter had been written instead. As a special case of this, we require that an arrangement that containing meta-level parentheses is to be read as though the parentheses were instead a use of [ • ] ≈ .

Convention 2.4 (Coercing Arrangements to Pointers). We require that when an arrangement A is written, but the surrounding context only makes sense if the value of the expression is a pointer, then the arrangement A is implicitly coerced to the pointer to the object given by convention 2.3.

Due to the combination of convention 2.3, convention 2.4 and the tight restrictions on where round parentheses can occur in proper arrangements, most uses of round parentheses will not be symbols that are part of syntactic arrangements but instead will be part of the meta-level mathematical reasoning. Example 2.5. The expression

(O 1 O 2 ) O 3 , which contains meta-level parentheses, stands for [O 1 O 2 ] ≈ O 3 . If we write O = (O 1 O 2 ) O 3 , then this stands for writing O = [[O 1 O 2 ] ≈ O 3 ] ≈ ,
because the equation's lefthand side must be an object due to the declaration that the metavariable O ranges over Object.

We have left ≈ mostly unspecified so far. The sets Object and Arrangement do not depend on ≈, but their subsets of well formed objects and arrangements do depend on ≈. The definition of ≈ may be adjusted by the authors of a paper at any point, and the set of well formed objects in scope will therefore change at the times these adjustments are made. The effect of convention 2.3 will similarly change; the same expression can denote different objects at different places if there is an intervening change to ≈.

Contexts and Hole Filling

A context is an object O ∈ Object with at least one use of the special hole object . The number of hole symbols in an object or arrangement is its arity. We now define context-hole filling for arbitrary objects and arrangements (although it will in general only do something useful for well formed objects and arrangements with the correct arity). Let the operations

O[O 1 , . . . , O n ], P O [O 1 , . . . , O n ] and A[O 1 , . . . , O n ]
which fill the holes reachable from O, P O and A with the objects in the sequence O = [O 1 , . . . , O n ] be defined as follows:

1. P O O = P O ′ and O O = O ′ iff fill(O, O) = (O ′ , []). Similarly, A O = A ′ iff fill(A, O) = (A ′ , []).
The results of fill(O, O) and fill(A, O) are undefined except where explicitly defined below. (The result is undefined unless all of the replacements are used, so the number of replacements must match the arity.)

2. fill( , [O] • O) = (O, O).
(Each hole uses up one of the replacements.)

3. fill({A}, O) = ([A ′ ] ≈ , O ′ ) if fill(A, O) = (A ′ , O ′ ).
(Context-hole filling in a well formed context can only descend inside an arrangement that is alone in its equivalence class. This is part of the motivation for our requirement that ≈ must not relate distinct arrangements containing holes.)

4. fill(O, O) = (O, O) if O is not a context. (
fill(A, O 1 ) = (A ′ , O 2 ) fill(A 1 , O 2 ) = (A ′ 1 , O 3 ) fill(A 2 , O 3 ) = (A ′ 2 , O 4 ) fill( Â, O 2 ) = ( Â′ , O 3 )
then all of these must follow:

fill(A Â, O 1 ) = (A ′ Â′ , O 3 ) fill(A A 1 A 2 , O 1 ) = (A ′ A ′ 1 A ′ 2 , O 4 ) fill(A A 1 , O 1 ) = (A ′A ′ 1 , O 3 ) fill(A A 1 , O 1 ) = (A ′ A ′ 1 , O 3 ) fill(A, O 1 ) = (A ′ , O 2 ) fill(A, O 1 ) = (A ′ , O 2 ) 7. fill(P O , O 1 • O 2 ) = fill(P O 3 , O 2 ) if fill(O, O 1 • O 2 ) = fill(O 3 , O 2 ). (Context-
( )[O, O] = O O [O] = O ( → O 1 )[O 2 → O 2 ] = (O 2 → O 2 ) → O 1 ( ≔ , )[O 1 , O 2 , O 3 ] = (O 1 ≔ O 2 , O 3 )
We now will define (S 1 , S 2 )-Context to be the the contexts which act as functions from S 1 to S 2 , i.e., the set of every context O c of arity 1 such that for all

O ∈ S 1 it holds that O c [O] ∈ S 2 . Let S-Context = (S, S)-Context. Given a relation R such that (domain(R)∪range(R)) ⊆ S ⊆ Object, let [R] S denote the S-compatible closure of R, defined as follows: if O c ∈ S-Context and O 1 -R - → O 2 , 6 then O c [O 1 ] -[R] S ---→ O c [O 2 ]. Let [R] denote [R] S for
( ) ↓ • ! + = ∈
Every well formed non-hole object O can be decomposed into a primitive constructor and the subobjects to be placed in the primitive constructor's holes. A primitive constructor decomposition of O is a pair (c, O) such that O = c O. An object will have one primitive constructor decomposition for each of its arrangements. Furthermore, the subobjects in a decomposition can be recursively decomposed similarly. A recursive decomposition of an object into primitive constructors is very similar to the concept of an abstract syntax tree of a string in a language defined by a grammar. If any of the equivalence classes in an object are non-singletons, then the object will not have a unique recursive decomposition.

Example 2.8. Some examples of recursive decomposition of an object into primitive constructors can already be seen in example 2.6. Here are some additional examples:

(!O) = [! [O]] (O 1 + O 2 ) + O 3 = ( + ) [( + )[O 1 , O 2 ], O 3 ]
2.4 Syntax Shorthand: Primitive Constuctor Decomposition Convention 2.3 allows avoiding the need to write [ • ] ≈ by implicitly invoking [ • ] ≈ at obvious arrangement boundaries and also at most uses of ( • ) in arrangements. For example, convention 2.3 allows us to know that the expression (O 1 @ O 2 ) @ O 3 stands for the object whose primitive constructor decomposition is given by

O ′ = c @ [c @ [O 1 , O 2 ], O 3 ]
where c @ = @ . But the shorthand notation provided by convention 2.3 is not enough. Additionally, we want to allow inferring uses of [ • ] ≈ in other places in the middle of what appear to be arrangements. As a concrete example, we want to allow inferring that the expression O 1 @ O 2 @ O 3 stands for the same object as the expression (O 1 @ O 2 ) @ O 3 , namely the object O ′ mentioned in the previous paragraph. We want that the expression O 1 @ O 2 @ O 3 must not stand for the object whose primitive constructor decomposition is

c ′′ [O 1 , O 2 , O 3 ] where c ′′ = ( @ @ ).
To provide the additional shorthand notation that is needed, we establish mechanisms for (1) declaring primitive constructors and (2) parsing arrangements. We build the parsing mechanism by adapting the notions of operator precedence and declared associativity from parsing of languages to our setting; this will allow splitting what appears to be a single primitive constructor into multiple primitive constructors.

As an auxiliary device, we define splicing of arrangements. Remember that every arrangement is, in effect, a sequence of core arrangements (symbols, objects, numbers, or overlined arrangements), possibly superscripted or subscripted. An arrangement A ′ can be spliced into another arrangement A ′′ by inserting the main core arrangement sequence of A ′ into one of the core arrangement sequences of A ′′ in place of an occurrence of . (If we wanted to avoid the interpretation of convention 2.9, we could do so by avoiding the implicit coercion of convention 2.3 and writing instead O = [ !O ′ ] ≈ , which would use the primitive constructor ! instead of the two smaller primitive constructors and ! .) Suppose we write the expression O 1 @ O 2 . This declares the primitive constructor c @ = @ . If we then state that c @ is left-associative, then writing O = O 1 @ O 2 @ O 3 produces the same result as writing O = (O 1 @ O 2 ) @ O 3 . If we did not give the associativity of c @ , then writing O = O 1 @ O 2 @ O 3 would be an error, because there are multiple distinct ways the arrangement @ @ can be built by splicing the arrangement @ into itself.

Names, Binding, α-Conversion, and Substitution

The relation ≈ provides a mechanism for working with syntax considered modulo equivalences on arrangements. One of the most important equivalences is the notion of α-conversion which renames bound names. 7Some of the members of Object can be declared to be names. The names may be furthermore subdivided into groups. Formally, the concepts of names and groups of names are given by an equivalence relation ∼ ⊂ Object × Object which relates names in the same group. An object O is a name iff O ∼ O. Declaring a subset S ⊂ O to be a name group is the same as declaring that S is a ∼-equivalence class. The definition of ∼ will be extended incrementally with declarations of groups. Any objects that have not been declared to be related by ∼ are not related by ∼. To keep things simple we require that no name contains another name (of the same group or of a different group) as a subobject.

Specific primitive constructors can be declared to bind a name placed in one of the constructor's holes across some of the constructor's holes. We define the free names of an object O, written FN(O): The free names of an arrangement A are defined by FN(A) = FN({A}). A name that is not free is bound.

1. If O is a name, then FN(O) = {O}.
Example 2.11. Consider c λ = λ . of arity 2. Suppose we declare that c λ binds any name placed in its first hole in both of its holes. Suppose we declare that { x i i ∈ N } is a name group. (We will in fact make both of these declarations later, so this example is not just hypothetical.) Suppose that we have not declared any bindings for the constructor c @ = @ . Then FN((λx 1 .(x 1 @ x 2 )) @ x 3 ) = {x 2 , x 3 }.

Consider c let = (let = in ) of arity 3. Suppose we declare that c let binds any name placed in its 1st hole in its 1st and 3rd hole. Then FN(let

x 1 = x 3 in (x 1 @ x 2 )) = {x 2 , x 3 }.
We now define the auxiliary notion of name swapping. Given

} ∩ FN(O) = {O x , O y } ∩ FN(A) = ∅, then O ≡ α swap(O x , O y , O) and A ≡ α swap(O x , O y , A).
Definition 2.12 (α-Conversion as a Syntactic Equivalence). If a paper says that it is "working modulo α" or "identifying α-equivalent terms" that means ≡ α restricted to arrangements is a subset of ≈, i.e., if

A 1 ≡ α A 2 then A 1 ≈ A 2 .
Definition 2.12 implies that ≈ will change whenever adjustments are made to the declared bindings of primitive constructors or to the definition of ∼.

We now define the substitution operation, written as

O[O x ≔ O ′ ]
. This expression will be defined to stand for the result of replacing all free occurrences of O x in O by O ′ . This operation must be defined carefully. The result of O[O x ≔ O ′ ] must not allow names that are free in O ′ to be captured by bindings in O. Also, the operation must respect ≈ so that if both O and O ′ are well formed, then

O[O x ≔ O ′ ] is also well formed. Given a name O x , define O[O x ≔ O ′ ] formally as follows. 1. If O = O x , then O[O x ≔ O ′ ] = O ′ . 2. Otherwise, O[O x ≔ O ′ ] is defined as follows.
First, we must define substitution for primitive constructor decompositions (p.c.d.'s). Given 9Example 2.13. Below, on the left are some example syntactic objects [2, p 134], [START_REF] Rahli | Bar induction: The good, the bad, and the ugly[END_REF], [22, p 386]. These objects may not be well formed, because the singleton sets may not be equivalence classes of ≈. The objects to the right of them are adjusted to be well formed (assuming the subobjects O 1 , to O 4 are well formed):

O = c[O 1 , . . . , O n ], let S be the subset of {O 1 , . . . , O n } of names bound by this occurrence of c. If S ∩ FN(O ′ ) ∅, then let (c, [O 1 , . . . , O n ])[O x ≔ O ′ ] be undefined. 8 Otherwise, let (c, [O 1 , . . . , O n ])[O x ≔ O ′ ] = c[O 1 [O x ≔ O ′ ], . . . , O n [O x ≔ O ′ ]]. If there exists an O ′′ such that O ′′ = (c, O)[O x ≔ O ′ ] for every p.c.d. (c, O) of O such that (c, O)[O x ≔ O ′ ] is defined, then O[O x ≔ O ′ ] = O ′′ . Otherwise O[O x ≔ O ′ ] is undefined.
{λP O 1 .P O 2 } [λP O 1 .P O 2 ] ≈ {ΠP O 1 : P O 2 .P O 3 } [ΠP O 1 : P O 2 .P O 3 ] ≈ { P O 1 ↓ {P O 2 P O 3 } • P O 4 } [ P O 1 ↓ [P O 2 P O 3 ] ≈ • P O 4 ] ≈

Production Rules for Defining Syntactic Sets

We have already defined syntactic objects, but the set Object is too big. Carefully defined subsets of Object may be defined via syntax production rules, which we write in the form

ν 1 , . . . , ν n ∈ S A 1 | • • • | A m
where ν 1 , . . . , ν n are metavariables, S is the name of the subset of Object being defined, and A 1 , . . . , A m are alternatives. Each alternative is either the special notation "• • • " or an expression e, together with an optional side condition c (written "e if c", where c is a formula containing only expressions), which evaluates to a member of Object when values are supplied for metavariables occurring in e, provided both c holds of that choice of metavariables. One can omit the "∈ S", allowing the reader to fill in S whose name is distinct from the names of all other declared sets. One can omit the side condition in which case we can read it as if true. One can provide a global side condition if c ′ which we read as appending ∧c ′ to all A. Such a syntax production rule has the following effects:

1. It declares S to be a set of syntactic objects, in particular the smallest one that satisfies all other constraints placed on it not just by this rule but also by the rest of the document.

2. It declares the metavariables ν 1 , . . . , ν n to range over the set S. 5. For each alternative A in the rule which is not "• • • ", a constraint on the membership of S is added. The constraint is that for each legal choice10 of values for the metavariables occurring in A, if O is the result of evaluating the expression e in A using those metavariable assignments, then O ∈ S.

Metavariables occurring in an alternative A that are not yet declared to range over any set are presumed to range over a countable set of objects disjoint from all the other sets of objects in the paper. This assumption is dropped if a value for a metavariable gets declared later in the paper and values for A are recalculated accordingly.

6. If the first alternative is not the special alternative "• • • ", then any constraints on the membership of S established by earlier rules are forgotten.

7. The rule triggers a recalculation of all of the sets declared by all syntax production rules. Such a recalculation is also triggered whenever the definition of ≈ is altered. Or when a definition of what metavariables range over is altered. This recalculation evaluates all of the constraint expressions for all syntactic sets using the current bindings for all metavariables, set names, the equivalence relation ≈, etc., and rebinds the set names to the recalculated values in the subsequent text. 11Multiple rules can be given for the same set S. If a later rule for S begins with the special alternative "• • • ", then its alternatives are combined with the alternatives already in force for S. Usually the alternatives of the later rule replace the previous alternatives if this is not the case. However, if the author uses a single alternative in each of their production rules, then they normally expect these to be combined as though they had used • • • . The special alternative "• • • " used as the final alternative of a rule has no mathematical consequence and is used only as a signal to the reader warning that there will be later rules for the same set.

When a syntax alternative is intended to allow building terms from multiple subterms of the same set, it is necessary to use distinct metavariables for each possible subterm to allow the subterms to differ. It is always possible to find distinct metavariables for the same set by using subscripts. Example 2.14. We can define the usual simple types like this:

a, b ∈ Ty-Variable a i T ∈ Simple-Type a | T 1 → T 2
Given this definition, a possible example type is T 0 = a → (b → a). In this example T 0 , we leave unspecified which exact type variables are used. We could make T 0 concrete by specifying a = a 0 and b = a 1 yielding T 0 = a 0 → (a 1 → a 0 ). If we had written the second alternative in the production rule for Simple-Type as T → T , then the type T 0 would not be allowed and we could only write types like a → a and (a → a) → (a → a) where both arguments of each → are equal. Example 2.15. We can define the lambda calculus like this:

e ∈ exp ::= v | λv.e | e e
Each v ranges over a countable set of objects disjoint from the objects produced by the other production rules. The production rule e ∈ exp ::= v can be read as giving us the constraint var ⊆ exp. The constraint { [λP v .P e ] ≈ ptr(v) = P v ∧ ptr(e) = P e } ⊆ exp is given by e ∈ exp ::= λx.e. The constraint { [P e 1 P e 2 ] ≈ ptr(e 1 ) = P e 1 ∧ ptr(e 2 ) = P e 2 } ⊆ exp is given by e ∈ exp ::= e e. We pick the least exp ⊆ Object and var ⊆ Object satisfying these constraints with an ordering given by the subset relation.

In addition to declaring e as ranging over exp this definition also declares e 1 , e 2 ,..., e ′ , e ′′ etc. to range over exp and similarly for v ∈ var. The subset of Object picked out by these constraints depends on the choice of equivalence relation ≈, in the lambda calculus this is most likely α equivalence, although it may also be the identity relation on Arrangement

In order to be confident that this set can be picked out (e.g. for exp) we begin with exp 0 = ∅ and let exp 1 contain all the things exp must contain if exp is at least exp 0 and so on for each +1 case. For a limit point ε we let exp ε be ε i=0 exp i . We take the least fixed point of the function f ∈ P(Object) → P(Object) such that f (exp i ) = exp i+1 over some appropriately large set of exp i ordered but the subset relation (this is smaller than P(Object)).

We define the reduction relation as the e-compatible closure of the smallest β (in the ordering given by ⊆) satisfying the constraint (λv.e 1 )e

l ∈ label ::= y i R ∈ Type-Records ::= ǫ | l : T, R where l lab(R) ê ∈ texp ::= • • • | {r} | ê.l t ∈ Record-Type ::= T | {R} r ∈ Term-Records ::= ǫ | l = ê, r
where l lab(r)

Where we define lab s.t. lab(ǫ) = ∅, lab(l : T, R) = {l} ∪ lab(R) and lab(l = ê, r) = {l} ∪ lab(r). Both r and R are equivalent up to reordering (i.e. l : T, R ≈ R, l : T and l = ê, r ≈ r, l = ê). Here, ≈ is the smallest equivalence relation fulfilling these constraints. It is defined incrementally over each R and each r as a new one is added. We add a rewriting rule:

{l = v, r}.l -RCD ---→ v For each * ∈ { x ∈ Object × Object x = β } ∪ { x ∈ Object × Object x = η } ∪ {RCD} we add additional constraints: (ê 1 - * - → ê2 ) (ê 1 .l - * - → ê2 .l) (ê 1 - * - → ê2 ) ({r, l = ê1 } - * - → {r, l = ê2 })
(The horizontal line is read as the logical operator ⇒).

Model for Syntactic Math Text

In this section we show that there is a model for SMT. In order to do so, we choose sets to represent Symbol, Pos, Pointer, , ǫ and B. Our invariant constraints are those that will hold of sets thought to approximate Object and Arrangement in the proof these are well defined. Our constraints on the final selection will only hold of the set we pick out from these approximations. Definition 3.1 (Symbol, Pos, Pointer, { , ǫ, B}). We can create a countable set, D, representing symbols, accenting and positioning from the ordinals 12 following ω which are themselves smaller than 2ω. We pick a finite set of elements, Pos, from D to represent the positions subscript, superscript, pre-subscript, pre superscript, text above, text below etc (at least as many as positions as detailed in the OpenDocument [START_REF]Information technology -Open Document Format for Office Applications (OpenDocument) v1.2 -Part 1: OpenDocument Schema. Standard[END_REF] standard). We pick out an element of D which we call B. We pick out a element D to represent the context-hole , and one to represent the empty arrangement ǫ. We let the remainder of the elements in D represent Symbol (at least as many symbols as in unicode).

Definition 3.2 (Invariant Constraints).

ptr ∈ Object → Pointer and ptr is a bijection between Object and Pointer. B Object ∧ B Arrangement.

∈ Object ∧ Arrangement ∧ ǫ ∈ Arrangement Pos ⊥ Object ∧ Pos ⊥ Arrangement. Symbol ⊂ Core. N ⊂ Core. Core ⊂ Arrangement. Definition 3.3 (Constraints on Final Selection). Pointer ⊂ Core. If A ∈ Arrangement, A ǫ and x ∈ Symbol then (B, x, A) ∈ Core. Arrangement × Core ⊂ Arrangement. If A ∈ Arrangement and x ∈ Pos → Arrangement \ {ǫ} and x ∅ then (A, x) ∈ Arrangement.
If S ⊂ Arrangement and |S| ≤ ℵ 0 , then S ∈ Object. 13Theorem 3.4. Object and Arrangement are well defined. Proof Sketch. We define a sequence of sets thought to contain closer approximations of Object and Arrangement until some member contains a model for Object and Arrangement themselves. The smallest set in our sequence contains all tuples of:

1. The set containing (approximating Object).

2. An injective function p ∈ { } → Pointer (approximating ptr).

3. Symbol ∪ N ∪ {ǫ} (approximating Arrangement).

Symbol ∪ N (approximating Core).

Each subsequent set in our sequence contains those tuples of sets which would be added by applying our constraints as though Object were its approximation, Pointer were its approximation and Arrangement were its approximation. Where our sequence reaches a limit point each set in each tuple is calculated as though Arrangement was the union of arrangements up to that point (apart from the set approximating Arrangement which also gets the pointers to the approximation of Object at that limit).

These sets remain sufficiently small to pick mappings for Object. Further, there is a fixed point for the function mapping each member of this sequence to the member above it. From this fixed point we can select a model for Object and Arrangement.

(Full proof in Appendix B)

4 How Can This Definition be Used?

Non-MBNF "Grammars" As well as covering some uses of MBNF to define syntax, SMT also provides us with a notion of what it means to use the structures of math-text together with syntactic equivalences, even in documents where MBNF does not feature, or where MBNF is mixed with other notation for picking out objects. Coverage of this sort may require users to select appropriate sets of objects that resolve ambiguities.

A Flexible Notion of Equivalence Not only is the notion of equivalence presented in SMT sufficient to deal with α-equivalence over finite terms, regardless of how binding may be represented in the syntax, it also deals with things like equality up to reordering of finitely many chunks of syntax and equality of finitely many compositions with zero, both of which appear in the π-calculus [START_REF] Carbone | Structured Communication-Centred Programming for Web Services[END_REF]. It deals with many of the equivalences an author might define using "=," provided they do not quantify over an uncountable set when using it. Furthermore it provides tools to consider equalities over sub-objects, not just the syntactic objects themselves, which can be vital when talking about the structure of a grammar.

Combining Objects in Math-Text SMT deals with most combinations of characters likely to appear in math text used to represent "syntax" in a fairly general manner (it does not deal with matrices/grids, numbers other than the naturals, or an use of sets that cannot be thought of in terms of equivalences up to reordering and repetition on finite lists of elements, but none of these is likely to appear in "syntax").

Automatic Bracketing Since SMT preserves the tree-like structure of syntax, it can be readily used for grammars where authors treat bracketing as optional. We also give authors the option of making this structure more explicit by primitive decomposition. Bracketing structures may often also be derived by noticing where objects appear in production rules.

Functionality Inherited From BNF Our definition extends the basic functions covered by BNF to MBNF and the richer syntactic structures that are represented by math-text. Substitution of non-terminals becomes assigning values to metavariables and choice of production rules remains supported.

Hole Filling

The following chunk of the MBNF we took from Chang and Felleisen [2, p 134] defining A can be handled by our definition using convention 2.3:

e = x i | λx i .e | e e A = [ ] | A[λx i .A] e
5 Related work

OTT [START_REF] Sewell | Ott: Effective Tool Support for the Working Semanticist[END_REF] provides a formal language for writing specifications like those written in MBNF. The process of moving from an OTT specification to an MBNF can be performed automatically. However, the focus of this article is moving the other way -interpreting MBNF without requiring it to be specified in a theorem-prover friendly format. Furthermore, we wish to provide a general mathematical intuition suitable for translation to multiple theorem provers, whereas OTT focuses on translating to COQ 8.3, HOL 4 and Isabelle directly, but offers less support for those seeking a general mathematical intuition.

In addition, OTT only supports context hole filling for contexts with a single hole and currently does not support rules being used coinductively. We already handle more cases of context hole filling and we aim to deal with coinduction, though SMT as it stands doesn't.

Guy Steele [START_REF] Guy | It's Time for a New Old Language[END_REF] covers many of the notational variants of BNF, including some MBNFs. However, Steele's focus is primarily on surface differences. He does not discuss how the underlying mathematical structure of MBNF differs wildly from BNF.

Grewe et al. [START_REF] Grewe | Exploration of language specifications by compilation to first-order logic[END_REF] discuss the exploration of language specifications with first-order theorem provers. However, they still require the reader to be able to intuitively translate language specifications to a sufficiently formal language first. This is the part of language specification checking this paper aims to help with.

Reynolds [START_REF] Reynolds | Theories of Programming Languages, 1st edition[END_REF] has the best attempt at a definition of MBNF, which he calls "abstract syntax", 14which we could find after looking through the books in our collection. However, he only deals contextfree grammars and in many places he proceeds by example.

Future Work

While we do not deal with trees of infinite breadth or depth here, we hypothesise that the method outlined in this document could be used on trees with countably infinite breadth and depth. The main difference in doing so would be that Object and Arrangement would likely have to be of cardinality ℵ 2 , rather than ℵ 1 , but apart from that it seems likely a similar proof would work.

While we provide some powerful tools for writing syntax patterns more explicitly and dealing with numbers in the syntax, we do not provide procedures for generating countably many production rules. Guy Steele [START_REF] Guy | It's Time for a New Old Language[END_REF] has done work in this area, but doesn't address differences between MBNF and BNF. etc), (2) adding a single, double, or triple prime to ν, producing respectively in ν ′ , ν ′′ , and ν ′′′ , or (3) a combination of (1) and [START_REF] Chang | The Call-by-need Lambda Calculus, Revisited[END_REF].

In contrast, we use superscripts (e.g., ν 1 , ν 2 ) and accents (e.g., ν, ν) to distinguish metavariables that are in some way related to the corresponding undecorated metavariable, but not necessarily ranging over the same class. For example, if we have declared ν to range over the set S, we might have ν 0 ranging over S 0 , ν 1 ranging over S 1 , and S 1 ⊂ S 0 ⊂ S.

A.2 Sets

The mathematical foundation we use is set theory with choice. ZFC is suitable, so are other variants. If P(X) is a proposition of first-order logic that mentions X, then (1) P(Y) differs from P(X) only by mentioning Y instead of X, and (2) the notation { X P(X) } stands for { X ∈ S P(X) } for some set S which is left to the reader to infer from the context of discussion. Given some expression f (X 1 , . . . , X n ) mentioning variables X 1 , . . . , X n , we use the notation

{ f (X 1 , . . . , X n ) P(X 1 , . . . , X n ) } for { Y ∃X 1 , . . . , X n . Y = f (X 1 , . . . , X n ) ∧ P(X 1 , . . . , X n ) }.
Given two sets X and Y we use the notation X ⊥ Y to mean 'X and Y are disjoint.'

A.3 Pairs

We rely on a operator ( • , • ) for building ordered pairs and corresponding projection operators fst and snd, such that if Z = (X, Y), then fst(Z) = X and snd(Z) = Y. We require that it is impossible for a pair to also be a set of pairs and that the natural numbers do not overlap with pairs. 15 Given two sets S and T , the product set S × T is the set of pairs { (X, Y) X ∈ S and Y ∈ T }. Let tuple notation be defined so that (X 1 , X 2 , X 3 , . . . , X n ) = ((X 1 , X 2 , X 3 , . . . , X n-1 ), X n ).

A.4 Relations

Let R range over sets of pairs. The statement (X, Y) ∈ R can be written with three kinds of alternate notation: R(X, Y), and X R Y, and X -R -→ Y. A relation R is reflexive w.r.t. S iff R ⊇ { (X, X) X ∈ S }. As is common practice, if we mention that a relation is reflexive without saying what set S this is with respect to, this means we are leaving it to the reader to infer from the context of discussion which set S to use.

Let R * be the reflexive and transitive closure of R and let R = be the reflexive, symmetric, and transitive closure of R; in both cases we use the above-mentioned convention that the reader must infer the set S w.r.t. which to take the reflexive closure.

Let X -R -։ Y mean X -R * -→ Y, and let X և R -։ Y mean X -R = --→ Y. A relation is an equivalence iff it is symmetric and transitive. Given an equivalence relation R, let [X] R = { Y (X, Y) ∈ R } be the equivalence class of X w.r.t. R and let [X] R be an equivalence class of R. A relation R is terminating iff there is no infinite sequence X 1 , X 2 , . . . such that X 1 -R - → X 2 -R - → • • • . If X -R
-։ Y, and there exists no Z such that Y -R -→ Z, then we call Y an R-normal form of X. If R is terminating, then it can be used for induction: If it can be shown that R is terminating and ∀X ∈ S. (∀Y ∈ S. X -R -→ Y ⇒ P(Y)) ⇒ P(X), then it follows that ∀X ∈ S. P(X). 15 We therefore can not use Kuratowski's encoding of pairs where (X, Y) = {{X}, {X, Y}}, because (for example) {(X, X)} = {{{X}}} = ({X}, {X}). Similarly, we can not use the "short" encoding where (X, Y) = {X, {X, Y}} together with von Neumann's encoding of natural numbers (actually of all ordinal numbers) where 0 = ∅ and i + 1 = i ∪ {i} because (0, 0) = {0, {0, 0}} = {∅, {∅, ∅}} = {∅, {∅}} = {∅} ∪ {{∅}} = 1 ∪ {1} = 2. We can use Wiener's encoding of pairs where (X, Y) = {{{X}, ∅}, {{Y}}}, because in this encoding a pair can not be a set of pairs, a set of sets of pairs, or a von Neumann ordinal number. We can also work in a set theory with a primitive pairing operator.

A relation is a partial order on S iff it is transitive and antisymmetric. A partial order is strict iff it is irreflexive. A non-strict partial order, ≤, is a total order on S iff for all X, Y ∈ S either X ≤ Y or Y ≤ X. A strict partial order, <, is a strict total order on S iff for all X, Y ∈ S s.t. X Y either X < Y or Y < X.

A.5 Functions

A function is a relation f such that for all X, Y, and Z

, if {(X, Y), (X, Z)} ⊆ f then Y = Z. Let S → T = { f f ⊆ S × T and f is a function }. Let f be from S to T iff f ∈ S → T . A function f is injective iff f -1 is a function. If (X, Y) ∈ f for some Y, then f (X) denotes Y, otherwise f (X) is undefined. A function f is total on S iff f (X) is defined for all X ∈ S. Given a function f , let f [X → Y] = ( f \ { Z ∈ f fst(Z) = X }) ∪ {(X, Y)}.
A fixed point of a function f is some x for which f (X) = X. If the set of fixed points of f has a greatest lower bound which is itself a fixed point, then we call this the least fixed point of f and if it has a least upper bound which is itself a fixed point, then we call this the greatest fixed point of f .

A function is f order preserving w.r.t a partial ordering leq if f (X) ≤ f (Y) iff X Y.

A.6 Sequences

Given a set S which is not a relation (if S contains only pairs then instead the notation refers to the definition of R * from section A.4, the reflexive and transitive closure of R), let S * , the set of finite sequences of elements in S, be the set of all finite functions f such that range( f ) ⊆ S, and domain( f ) ⊆ N, and m < n ∈ domain( f ) implies m ∈ domain( f ).

Convention A.1 (Metavariables over Sequences). If ν is declared to range over S, then ν is automatically declared to range over S * .

The notation [ν 0 , . . . , ν n ] stands for the least-defined function ν such that ν(i) = ν i for all i ∈ {0, . . . , n}. For example, the singleton sequence [ν] containing ν as its only element is {(0, ν)}, and we have [ν 0 , ν 1 , ν 2 ] = {(0, ν 0 ), (1, ν 1 ), (2, ν 2 )}. The component of a sequence ν at index i is simply ν(i). Note that the first component of a sequence is at index 0, and that the empty sequence [] is merely the empty set. The length of a sequence ν is the smallest n ∈ N which is larger than all elements of domain( ν). The concatenation of sequences ν 1 and ν

2 is ν 1 • ν 2 = ν 1 ∪ { (| ν 1 | + i, ν) (i, ν) ∈ ν 2 }.
Note that (S * , •, []) forms a monoid, i.e., the following equalities hold:

[] • ν = ν ν • [] = ν ( ν 1 • ν 2 ) • ν 3 = ν 1 • ( ν 2 • ν 3 )

B Proof of Key Results

Section 2 is sufficient for any reader who wants an outline of our definition in order to interpret those pieces of MBNF it defines. This appendix will be of interest either to those readers who are looking to extend our definition to define more uses of MBNF, or to those readers who want to reassure themselves that the sort of entities described in section 2.1 can always be thought to exist. While it is our intention that our definition should be easy to work with, a deeper working knowledge of set theory is assumed for this appendix than the rest of this document and everything apart from section 3 may be read without this section.

For this appendix we use Wiener's [START_REF] Wiener | A Simplification of the Logic of Relations[END_REF] encoding of pairs and von Neumann's encoding of ordinals, the natural numbers [START_REF] John Von Neumann | Zur Einführung der transfiniten Zahlen[END_REF] and cardinal assignment [START_REF] Moschovakis | Notes on Set Theory[END_REF]. We also make use of the axiom of choice. follows easily. As Obj ε ⊆ Obj i , for each i ≤ ε there exists some ptr which assigns pointers for Obj ε and which may also be used to assign pointers for Obj i . Definition B.4 (fun). Let Z = { OPAc i i < κ } for some κ < ω 2 . We define a function fun ∈ Z → Z such that fun(OPAC i ) = OPAC i+1 Lemma B.5. fun has a least fixed point.

Proof. The Knaster-Tarski theorem [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF] tells us that any any order-preserving function on a complete lattice has a least fixed point. For OPAC a , OPAC b ∈ Z we define ≤ such that OPAC a ≤ OPAC b iff (either, for all (Obj b , p, q, r) ∈ OPAC b , there exists (Obj a , b, c, d) ∈ OPAC a s. Z is a complete lattice ordered by ≤ and fun is an order preserving function on Z. 17Theorem B.6. Object and Arrangement are well defined.

Proof. For some tuple a in OPAC i there exists some tuple b in OPAC i such that:

1. The first member of b contains all the objects our rules say must exist if Arrangement is at least the third member of a, 2. The third member of b contains all the arrangements that our rules say must exist if Arrangement is at least the third member of a, Object is at least the first member of a and ptr is at least the second member of a.

If OPAC i is the least fixed point of fun then OPAC i+1 = OPAC i . We now take the least fixed point, lfp(fun), of fun ∈ Z→Z and select some tuple (Obj, ptr, Arr, Core) ∈ lfp(fun). The first member of the tuple gives us a model for Object and the third member, Arrangement. or s Ǎ1 ⊂ s Ǎ2 or sE 1 ⊂ sE 2 . We observe that each set out of (se, sv, sa, sA, s Â, s Ǎ, sE) either gets new elements added to it or remains the same every time a recalculation is triggered and is bounded above by Object. We can therefore take the least fixed point on f satisfying all of these constraints.

C Examples of our Definition in Action

If the side condition on E were to re-trigger the calculation on A, Â or Ǎ we would have to be able to check that the new side condition produced by this recalculation could not effect any E previously added. This grammar relies on an assignation of values to x, otherwise all of its sets are either ∅ or . For a given equivalence (e.g. ≡ α or ≡ A ) this grammar may define a different collection of (se, sv, sa, sA, s Â, s Ǎ, sE).

We add the reduction rule for this Grammar which is the least R satisfying:

Â[A 1 [λx. Ǎ[E[x]]]A 2 [v]] -R - → ( Â[A 1 [A 2 [( Ǎ[E[x]])[x ≔ v]]]])
where Â[ Ǎ] ∈ A

e

  ::= x | (λx.e) | (e@e) A ::= [ ] | (A[(λx.A)]@e)

  This is the only way context-hole filling can skip over embedded objects which are non-singleton equivalence classes of arrangements.)5. fill(s, O) = (s, O) and fill(n, O) = (n, O).6. Context-hole filling essentially traverses the arrangement tree in a left-to-right order filling in holes in the order it encounters them. Thus, for any arrangements A, A 1 , and A 2 , core arrangement Â, and object sequences O 1 , O 2 , O 3 , and O 4 , if it holds that

2 .

 2 Otherwise, if FN(O) is defined, it is as follows. First, we must define the free names of primitive constructor decompositions (p.c.d.'s) of O. Suppose O = c[O 1 , . . . , O n ] gives one such p.c.d. Let S i be the names bound by c in O i for 1 ≤ i ≤ n. Then FN(c, [O 1 , . . . , O n ]) = i∈{1,...,n} FN(O i ) \ S i . If there exists a set S such that S = FN(c, O) for every p.c.d. (c, O) of O, then FN(O) = S.

3 .

 3 A global side condition if c ′ appends ∧c ′ to each A 1 , . . . A n . 4. If each A 1 , . . . A n contains only undecorated instances of ν, then for any A containing multiple instances of ν and no side conditions containing ν that apply to A, we can rewrite it with each ν given a different decoration. I.e., m ∈ M ::= x | m m becomes m, m 1 , m 2 ∈ M ::= x | m 1 m 2 .

  t. Obj a ⊂ Obj b , or, for all (Obj b , p, Arr b , r) ∈ OPAC b , there exists (Obj a , b, Arr a , d) ∈ OPAC a s.t. (Obj a = Obj b and Arr a ⊂ Arr b )).

C. 1

 1 Call by NeedThe following example is derived from Chang and Felleisen[2, p 134]:e ∈ se ::= x | λx.e | e e  ∈ s  ::= | A[ Â] e v ∈ sv ::= λx.e Ǎ ∈ s Ǎ ::= | A[λx. Ǎ] e a ∈ sa ::= A[v] E ∈ sE ::= | E e | A[E] | Â[A[λx. Ǎ[E[x]]]E] A ∈ sA ::= | A[λx.A] ewhereÂ[ Ǎ] ∈ AEach constraint is added sequentially and the least set of objects satisfying them is recalculated. Where the value of a set a metavariable can range over is recalculated and it is referenced in another rule, the set that rule applies to is recalculated with a new value. For example, initially a ∈ sa = ∅, but when A ::= is read it triggers a recalculation of A[v] so sa = sv. Then when A ::= A[λx.A] e is read, first it triggers a recalculation of A so sA = { } ∪ { [P λA P e ] ≈ ptr(e) = P e ∧ ptr([λx. ] ≈ ) = P λA } then it triggers a recalculation of a so sa = v ∪ { [P λA[v] P e ] ≈ ptr(e) = P e ∧ ptr([λx.P v ] ≈ ) = P λA[v] ∧ ptr(v) = P v } then

  some set S which the reader can infer from the context of discussion. Let c range over primitive constructors, non-hole objects whose only immediate subobjects are .

	Example 2.7. Here are some examples of primitive constructors [2, p 134], [22, p386], [7, pg 360], [16]:

  Convention 2.9 (Declaring and Parsing Primitive Constructors). 1. Unless prevented by part 2 of this convention, at the first use of a proper arrangement A, if there is a primitive constructor c = {A ′ } and objects O 1 , . . . , O n such that {A} = c[O 1 , . . . , O n ], then this use of A declares the primitive constructor c and the arrangement A ′ . Note that A ′ differs from A exactly in having in place of every non-object appearing in A. 2. At each place where we coerce an arrangement A into an object O using convention 2.3, the arrangement A is inspected to see if it can be built by splicing together already-declared arrangements. If A can be built entirely by splicing together already-declared arrangements, and then filling the holes in the splicing result with objects, and there is no explicit indication forbidding the use of this convention, then A is to be interpreted as though it had been written with uses of [ • ] ≈ around each splice point. If there is more than one way A can be built by splicing alreadydeclared arrangements, then it must be specified somewhere which one to choose. (This choice will typically involve notions of operator precedence and declarations of associativity.) Example 2.10. Suppose we have written the expressions O 1 and !O 2 . This declares the primitive constructors O 1 and !O 2 . If we then write O = !O ′ , then by convention 2.9 this produces the same result as writing O = (!O ′ ) . This happens because the arrangement !O ′ can be built by splicing ! into O 1 and then filling the hole with O ′ .

  two names O x and O y such that O x ∼ O y , let swap(O x , O y , O) be the object O ′ that results from replacing every occurrence of O x in O by O y , and vice versa. Let swap(O x , O y , A) be defined similarly. We now define α-conversion. Let ≡ α be the smallest equivalence relation satisfying the following condition. For all O x , O y , O, and A, if O x ∼ O y and {O x , O y

  2 -β -→ (e 1 [v ≔ e 2 ]). The notation O 1 [O 2 ≔ O 3 ] is defined in section 2.5. We do the same for λv.e 1 v -η -→ e. Note that because we have bracketed the term after substitution we are able to reapply equivalences that may have otherwise been lost in the process. Example 2.16. Given the definition of simple types in Example 2.14 we can define the simply typed lambda calculus as follows: ê ∈ texp ::= v | ê ê | λv : T. ê Example 2.17. We can extend example 2.14 with records in a similar way to Pierce [15, pg 129]. We can define lambda calculus with records like this:

  a won't trigger recalculations, but we have a recalculation on A waiting. Let f (se, sv, sa, sA, s Â, s Ǎ, sE) take (se, sv, sa, sA, s Â, s Ǎ, sE) when a recalculation is triggered to their values after a recalculation is performed. Let < be an relation on (se, sv, sa, sA, s Â, s Ǎ, sE) such that (se 1 , sv 1 , sa 1 , sA 1 , s Â1 , s Ǎ1 , sE 1 ) < (se 2 , sv 2 , sa 2 , sA 2 , s Â2 , s Ǎ2 , sE 2 ) iff se 1 ⊂ se 2 or sv 1 ⊂ sv 2 or sa 1 ⊂ sa 2 or sA 1 ⊂ sA 2 or s Â1 ⊂ s Â2

We chose ESOP

because its book was the most recent conference proceedings that we had as a paper book. Because the first book we picked contained an abundance of challenging instances of MBNF, our wider searching has mainly been to find even more challenging examples. We will be happy to receive pointers to additional interesting cases.

We use metavariable to mean a variable at the meta-level which denotes something at an object-level.

The root node is on the spine. If A is applied to B by an application on the spine, the root node of A is on the spine and the root node of B is not. If a node on the spine is an abstraction each of its children is on the spine.

A balanced segment is one where each application has a matching abstraction and where each application/abstraction pair contains a balanced segment.

We largely leave it up to the reader to determine which parentheses are meta-level. If a primitive constructor (section 2.4) appears inside some arrangements with parentheses surrounding it and other arrangements without them, it usually indicates these parentheses are meta-level. Similarly, parentheses which only surround a single metavariable corresponding to an object are frequently meta-level. Parentheses surrounding syntax which is to be thought of as a sequence are normally not metalevel. To help with this ambiguity, from this point forward all parentheses appearing in arrangements inside this document are meta-level.

O 1 -R -→ O 2 is an alternative notation for (O 1 , O 2 ) ∈ R. See appendix A.4 for details.

We do not give an especially sophisticated notion of binding here. We are only interested in providing a concept of binding that can be readily grasped and is sufficiently general for wide use in a variety of grammars. The notion of equivalence we provide is intended to be used in defining other syntactic equivalences in addition to α-equivalence.

For simplicity, we do not check whether the substitution needs only to proceed into holes of c which are not subject to its bindings. This will behave well enough for our uses provided each group of names is big enough that fresh names can be found.

So the substitution must be defined for at least one of the primitive constructor decompositions to get a defined result.

By legal choice we mean a choice of metavariables matching the sets they are declared to range over and fulfilling any constraints added by any side conditions.

It is an error if there is not a unique assignment of smallest values to the declared sets. Normally, the existence of a unique assignment will be provable using a fixed point theorem like the Knaster-Tarski theorem. However, the notation allows putting strange side conditions in the constraint expressions in alternatives, and this can cause a failure.

With the Von Neumann encoding

We do not bother restricting objects to only include proper arrangements here as it does not particularly affect the logic of the proof. Provided one can pick out unique members from Symbol for left parenthesis, right parenthesis and comma, its not too hard to express what it means for an arrangement to be proper with a logical formula.

We do not call MBNF "abstract syntax," because some of it is concrete syntax.

In order to simplify the proof this model allows the use of arrangements consisting of a single pointer in the formation of objects. It is not too difficult to rule this case out.

Note that the way in which we have defined Obj and Arr is such that j ≤ i implies (Obj j ⊆ Obj i and Obj j ⊆ Obj i ). Note also that, for all limit ordinals ε ≤ κ; (Obj ε , Arr ε ) ∈ Z. Finally note that ω 2 is large enough that it has a larger cardinality than any Obj i or Arr i , so we can select some κ larger than the partition of Obj i and Arr i into the extra elements added at each stage.

A Basic Logic and Mathematics

This appendix gives a brief overview of some concepts which are common enough in mathematics, but which are often represented in different ways, to say how they are used in this paper.

A.1 Metavariable Conventions

For this section, ν stands for an arbitrary metavariable (a meta-metavariable). Statements of the form "let ν range over C" declare and define ν as a metavariable that stands for some element of the class C.

We use single letters (either Roman or Greek) for metavariables. Whenever we declare a metavariable ν as ranging over a class, this also defines as ranging over that class all variants of ν obtained by either (1) adding a subscript i ∈ N to ν to produce ν i (e.g., ν 0 , ν 1 , ν 2 , What Does This Notation Mean Anyway? Lemma B.1. Given a countable set A and a set B of all trees C such that the interior nodes of C are elements of A and the leaf nodes of C are elements of ω 1 , |B| = ℵ 1 .

Proof. Let D be the set of all trees C such that every element of C is an element of ω 1 . Since we can make a bijection between members of A to a members of ω and the function f

We can now go on to show that Object and Arrangement are well defined. We do so by producing a model within set theory that fulfils most of the constraints in section 2.1., which are written out formally in Appendix D. 16 This proof requires that the reader pick some appropriate values for Symbol, Pos, Pointer, , ǫ and B. The definition of these sets in Appendix D is adequate.

We for a given ordinal we define a set of tuples OPAC i which may be thought of as getting closer to the tuple (Object, ptr, Arrangement, Core).

Definition B.2 (OPAC). 0 Case:

Let

Let

We now define the above functions for a limit point ε. Let

Let ptr S,k ε be a bijection between S ε ⊆ Pointer and Obj ε such that for all (Obj i , ptr i , Arr i , Core i ) ∈ S,

Proof. The only way OPAC i may be empty for some i is if

We prove by induction on the size of Obj k n and Arr k n such that (Obj k n , x, Arr k n , y) ∈ OPAC n that this cannot be the case. 0 Case:

then, for all Obj k n+1 , |Obj k n+1 | ≤ ℵ 1 , provided we have some way of ordering Obj k i and Arr k i . With choice this follows quite easily from the fact that the cardinality of the set of subsets of ℵ 1 which are of cardinality less than or equal to ℵ 0 is (2 We show ∃ε; ∀i < ε;

. We note that no Arr i has ℵ 0 sub-arrangements and all such Arr i can be readily identified with some finite tree whose interior nodes are labelled corresponding the operations accenting, concatenation and the finite number of possible combinations of Subscript, superscript etc. and whose leaf nodes are labelled with members of the set ω


Chien-Liang Chen
email: clchen@globalunichip.com

Jiing-Yuan Lin
email: jylin@globalunichip.com

Youn-Long Lin
email: ylin@cs.nthu.edu.tw

Integration, Verification and Layout of a Complex Multimedia SOC

We present our experience of designing a single-chip controller for advanced digital still camera from specification all the way to mass production. The process involves collaboration with camera system designer, IP vendors, EDA vendors, silicon wafer foundry, package & testing houses, and camera maker. We also co-work with academic research groups to develop a JPEG codec IP and memory BIST and SOC testing methodology. In this presentation, we cover the problems encountered, our solutions, and lessons learned.

INTRODUCTION

Ever increasing computational demand from the application side and very deep submicron semiconductor processing from the technology side together make systemon-chip (SOC) reality and necessary. Makers of such electronics systems as PDA, cellular phone handsets, digital still camera, etc, need ASIC solutions in order to differentiate themselves from the competition and to cut cost. On the other hand, semiconductor foundry has to expand its service scope from wafer manufacturing to mask tooling, cell & I/O library, memory compiler, and up to IP such as PLL, DAC, and ADC. Therefore, there is a need to bridge the gap between system houses and wafer foundry. We call such company SOC design service provider.

An SOC design service provider takes as its inputs from the system house a specification or partially-designed prototype and delivers to its customer GDSII ready for manufacturing. Close collaboration is needed among all parties in order to successfully bring a competitive product to the market in time.

A DIGITAL STILL CAMERA SOC

Our objective was to design a single chip controller for 2million-pixel and 3-million-pixel grade DSC for mass production of 3.5 million units in a year. In order to satisfy desired functionality at low cost, the SOC was specified to include the following IPs: a hybrid RISC/DSP processor, a hardwired JPEG encoding and decoding engine, a USB 1.1. device/mini-host controller with TxRx PHY, an SD/MMC flash card host interface, an SDRAM controller, an LCD Interface, an NTSC/PAL TV encoder, a 10-bit video DAC, an 8-bit LCD DAC, and two PLLs. The IPs come from multiple sources. Each of them posts different challenge to the project team.

The hybrid RISC/DSP was not an IP at all. Actually it was a stand alone processor chip used in the previous generations of cameras. To meet high speed requirement (133MHz @ 0.25um), we have to make it a hard core before integration with others. To integrate it into the SOC, we have to collaborate with the original vendor to create synthesis, simulation and test models in addition to hardening the processor into a high-speed hard macro. The USB1.1 controller and the SD card controller are supplied by a third party vendor. They are in VHDL RTL instead of more locally popular Verilog. Therefore, mixedlanguage simulation environment has been set up.

To meet processing speed requirement of 3M pixels @ 0.1Sec and long battery life, the JPEG codec function has been implemented in a hardware accelerator. We collaborate with a university research laboratory, which will present the IP in more detail in a companion paper [START_REF] Chen | JPEG, MPEG4 & H.264 Codec IP Development[END_REF] of this session. The effort we spent was in bridging the gap between university prototype and industrial strength design.

After all IP models are made ready, whole system integration and verification is an even bigger challenge. We encountered the problem of in-consistent and in-sufficient test benches. Therefore, developing test bench as the project goes is very important. Tight co-operation among all parties and precise project management are essential to complete the integration and verification of the system.

SILICON IMPLEMENTATION

The DSC controller consists of 240K gates excluding memory macros. After whole system verification with hybrid emulation/simulation, it was implemented in TSMC 0.25um 1P5M CMOS process and packed in TFBGA256 package. It took three months for a team of six engineers to complete the Netlist-to-GDSII service. During the course, there are many changes to the spec and netlist. Therefore, the implementation team has to be flexible and adaptive to changes.

There are 30 embedded memory macros in the controller. We use an in-house memory BIST circuit generator to insert one common BIST controller, multiple sequencers, and 30 pattern generators. The MBIST is from collaboration between us and a university research laboratory, which will also describe the technology in detail in another companion paper [START_REF] Wu | SoC Testing Methodology and Practice[END_REF]. After scan insertion, the fault coverage was 93%.

The physical design of the chip was done with timingdriven placement and routing, physical synthesis, formal verification and STA QoR check.

During chip implementation, we encountered several problems:

During the course, there are 3 spec changes involving re-synthesis and FF modification, 10 netlist changes involving ECO of combinational logic part, 3 ECO changes to fix setup/hold time violation, and 13 versions of pin assignments.

There existed inconsistency between simulators/versions among customer, IP vendors and us. The customer used PC-based Verilog/ModelSim while we used NC-Verilog. This lead to extra twist during ASIC sign-off.

IP quality is less than ideal. We have to clean up many DRC/LVS violation in the database provided by the IP vendors.

The USB IP was delivered in FPGA-targeted RTL. No robust synthesis script was available and the first RTL level simulation was failed. We have to co-work with the IP vendor over 10 versions of RTL code modification or synthesis constraint updates.

Because there is no automation tool available, we manually performed many version of pin assignments to reduce the number of substrate layers from four to two resulting in packaging cost saving.

During mass production, manufacturing test uncovered that the yield killer (5% loss) was in the insufficient driving strength of an output buffer in the CPU. The chip also went through reliability test including ESD performance test, temperature cycle test, high/low temperature storage test and humidity/temperature test.

The mass production yield was enhanced from 82.7% initially to very close to foundry's yield model of 93.4% over a period of 8 months. Our measures included optimizing probe card overdrive spec, optimizing power relay waiting time, and retargeting I sat and V th by optimizing poly CD in the foundry according to results from corner lot splitting. We also corrected the insufficient driving strength problem by means of metal changes to utilize the spare cells.

We have been requested to perform failure analysis on 20 returned chips that have pins shorted to GND. After checking substrate delaminating and popped-corner using scanning acoustics tomography, we found no abnormality. Finally, by sinking 400mA of current to the corresponding pin of a good chip we concluded that the failure was due to a system board bug.

CONCLUSION

We went on to produce over three millions of the chip over 18 months. Our system customer was able take about 8% of world-wide market share during that period. We have also migrated the chip from 0.25um process to 0.18um one achieving 20% saving in die cost.

The project has successfully demonstrated that it is feasible to bridge the gap between the need of an electronics system house without IC design capability and the production capacity of a semiconductor foundry with an SOC design service provider. We have been able to leverage the experience gained and lesson learned to serve more customers and more projects such as DVD player, cellular phone set, digital TV, photo display, etc.

The project experience told us that it is quite risky to employ third party IP in a complex SOC project, especially, when the IP has not been proven in the identical design environment.

As both applications and technology become more advanced, we have expanded our IP portfolio to include MPEG4, USB2.0 and OTG, SerDes I/O and embedded Flash memory. We have also enhanced our EDA flow to be able to handle dozens of multi-million gate design at 0.13um process and below every year.

Current complex SOC projects require silicon implementation flow including virtual prototyping, signal integrity check (crosstalk, electron-migration, dynamic IR drop, de-coupling cell insertion), design for manufacturability (intra-die process variation modeling, double via, dummy metal insertion), STA sign-off with indie variation analysis, hierarchical DFT and physical implementation, low power solution (multi V t /V DD cell library, gated clock, power down isolation) and flip-chip solution.

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE