Matisse:

Opl Redesigned as an Object Query Language^{∗}

Hassan Aït-Kaci

ILOG, S.A. B.P. 85 - 9, rue de Verdun 94253 Gentilly, France

                       hak@ilog.fr

February 18, 2002

Abstract

In this document, I undertake the design of the declarative part of an Opl-like language (here, provisionally called “Matisse”) using formal concepts from the state of the art in object-oriented database query languages. I start with an analysis of the constructs (data structures and operations) used by Opl for defining a model, arguing that the declarative part of Opl may be viewed essentially as a query language over complex data structures, including collections (such as lists, arrays, sets, and bags). In order to explicate the precise meaning and optimized implementation of expressions involving these constructs (such as arbitrarily nested aggregates, joins, and user-defined functions), I proceed to review prominent proposals from recent research in object query language design purporting to embody formally and efficiently queries over objects and collections thereof, and discuss their merits and shortcomings for the specific needs of a language such as Matisse. I then adapt some of these ideas to propose a core algebra and calculus with the goal of capturing all the declarative expressivity of Opl without any of its current limitations nor quirks of uniformity, trying to provide the most general, yet efficient, language conveniences.

1 Introduction

Programs expressed in the Opl language [10] typically consist of two separate parts: a model definition and an optional search specification. The model definition is purely declarative and amounts to declaring data structures and setting up a model consisting of set of algebraic constraints with, possibly, an objective “function” to optimize. The search part is not declarative and consists of explicit indications on how to proceed with searching for solutions of a defined model. We are only interested here in the purely declarative part of Opl—the model definition. Upon scrutiny, one realizes that defining a model amounts to declaring data structures and specifying a model as a syntactic object expression constructed out of these structures using data manipulation operations. Thus, the main idea of this work is based on the realization that an Opl model definition can in fact all be formulated as an expression of an object query language [11].

The motivation for redesigning the declarative part of Opl at all stems from the fact that it suffers from several undue shortcomings [15]. While several of these are cosmetic in nature, some are the result of not having recognized that the operations and data types for the representation and manipulation of data it needs have been well studied in the area of object query languages. As a result, Opl provides useful conveniences that feel very appealing to the user but unfortunately work only for very limited cases, falling short of supporting these constructs in their full generality. This state of affairs ends up frustrating the user who is led to expect much more flexibility than is actually supported, not understanding what caused a bona fide expression to be flagged as disallowed when other similar ones are allowed. My proposal is to attempt redesigning Opl to support in their full generality all the data definition and manipulation conveniences it offers, taking inspiration in recent work in object query language design.

∗This is an incomplete draft reporting work in progress.

This document is organized as follows. Section 2 briefly recounts what one needs to know about query languages. Section 3 examines Opl’s constructs for defining models and argues that it all falls within the object query language paradigm. In Section 4, I present recent work proposing formal algebras and calculi for expressing the precise semantics and efficient implementations of object query languages. In Section 5, I discuss the specific desiderata for Matisse in the light of the reviewed formalisms. In Section 6, I proceed to adapt these ideas to our needs to arrive at an algebra and a calculus sufficient to express precisely Opl constructs in their full generality, to be used as the formal basis for a kernel language into which to “desugar” a more convenient surface syntax.

2 A brief history of query languages

The relational model for databases proposed by Codd [5, 6, 7] owed its resounding success to using a simple, yet powerful, mathematical formalism to capture the representation and manipulation of data. It made a clear distinction between the formal semantics of its constructs and operations (the Relational Algebra) and the effective computation of query expressions taking their meaning in the Relational Algebra (the Relational Calculus). In its essence, the only mathematical formalism used by Relational Algebra is elementary Set Theory. This enabled expressing simply and elegantly database queries whose semantic correctness is straightforward to establish due to the pure declarativity of the Relational Algebra. It also enabled using the formal algebraic properties of its operations (such as commutativity, associativity, etc.) to optimize implementation of the Relation Calculus while provably preserving a query’s formal meaning. Thus, the Relational Calculus provides the kernel language in which to express the various constructs of a practical query language based on relations, which are ascribed a precise formal semantics in the Relational Algebra. Such a practical query language has been proposed, and well accepted, as a standard known as the Structured Query Language (SQL).^{1}

Object-oriented databases have evolved out of the relational model by allowing more flexibility in the form taken by the data and incorporating the object-oriented notions of type encapsulation and inheritance. The added flexibility consists essentially in allowing arbitrary nesting of record object structures (i.e., tuples) and collections (i.e., sets, bags, lists, etc.). In other words, whereas the relational model deals exclusively with relations over tuples of primitive types (i.e., sets of flat tuples—so-called “relational normal forms”), the object model imposes no such restriction. The other added conveniences—(polymorphic) typing, inheritance, and class/method encapsulation—have been introduced for the same obvious reasons as for general-purpose programming languages (i.e., data abstraction, reusability, modularity, etc.). As it turns out, the mere task of dealing with non-normal form objects alone in the same simple formal fashion as was done in the relational model (i.e., providing an algebra and a calculus that can be optimized thanks to the algebra’s equational theory) has been a hard task to tackle. Only recently have some elegant, yet powerful, formalisms emerged that begin to meet the challenge [1, 16, 17]. In other words, these formalisms are good candidates to stand with respect to OQL, the ODMG Object Query Language standard [2], as the relational algebra and calculus stand with respect to SQL.

1See, e.g., [12] for an excellent, easily accessible tutorial.

While the work done in the past twenty or so years in programming language design theory has made object-orientation and typing an orthogonal issue to the underlying computational model, one does need an underlying calculus to start with (e.g., in order to have C++, one needs to have C first). In other words, given a calculus, be it functional, logical, or imperative, it is not a major task to recast it as an object-oriented calculus by adapting its syntax and typing rules to deal with encapsulation and inheritance, while keeping its underlying computational model. My intention, thus, is to start with a “flat” typed object algebra and calculus rich enough to express and optimize the construction of a constraint model from a high-level definition of the kind supported by Opl, and delay incorporating true object-orientation until such a basic formalism is at hand. Indeed, providing full object-orientation for Matisse is only a second phase which should unfold relatively straightforwardly once its basic formalism has been designed.

3 Opl as an object query language

Let us consider an OPL program defining a transportation model. A certain set of products are manufactured and consumed in a set of cities. Data describing the supply is given specifying how much of each product is manufactured at each city, how much of each product is consumed at each city, and how much it costs per unit of product to be shipped from each city to each city. We want to establish how much of each good to transport between cities in such a way as to meet the demand within the supply and minimize the total cost.

The complete listing of an OPL program defining a model for a transportation problem is given in Appendix Section B. I will refer to the line numbers of that listing in the following discussion.

4 A review of object query language formalisms

In this section, I review prominent formalisms, focusing mainly on two recent proposals using the notion of comprehension syntax due to Peter Buneman et al. [1] with extensions to support arrays—a data structure of prime importance for an language with mathematical programming capabilities such as Opl. The first is due to Leonidas Fegaras and David Maier [9] and uses the notion of Monoid Comprehensions; the second is due to Leonid Libkin, Rona Machlin, and Limsoon Wong [14] and proposes a functional calculus of array objects. These two formalisms are very similar, differing mostly in their treatment of arrays (as collections in [9], and as functions in [14]). My intention is to try and merge ideas from both for our purpose.

4.1 Monoid homomorphisms and comprehensions

The formalism presented here is based on [9] and assumes familiarity with the notions and notations summarized in Appendix Section A.2. I will use the programming view of monoids exposed there using the specific notation of monoid attributes, in particular for sets, bags, and lists. I will also assume basic familiarity with naive λ-calculus and associated typing as presented in Appendix Section A.3.

4.1.1 Monoid homomorphisms

Because many operations and data structures are monoids, it is interesting to use the associated concepts as the computational building block of an essential calculus. In particular, iteration over collection types can be elegantly formulated as computing a monoid homomorphism. This notion coincides with the usual mathematical notion of homomorphism, albeit given here from an operational standpoint and biased toward collection monoids. Basically, a monoid homomorphism 𝔥𝔬𝔪_{⊕}^{⊙} maps a function f from a collection monoid ⊕ to any monoid ⊙ by collecting all the f-images of elements of a ⊕-collection using the ⊙ operation. For example, the expression 𝔥𝔬𝔪_{++}^{∪}[λx.x + 1] applied to the list [1, 2, 1, 3, 2] returns the set {2, 3, 4}. In other words, the monoid homomorphism 𝔥𝔬𝔪_{++}^{∪} of a function f applied to a list L corresponds to the following loop computation:

      result ← {};

foreach x in L do result ← result ∪ f(x);

return result;

This is formulated formally as follows:

Definition 4.1 (Monoid Homomorphism) A Monoid Homomorphism 𝔥𝔬𝔪_{⊕}^{⊙} defines a mapping from a collection homomorphism ⊕ to any monoid such that Θ_{⊕} ⊆ Θ_{⊙} by:

𝔥𝔬𝔪_{⊕}^{⊙}[f](𝔷_{⊕})  =^{def} 𝔷_{⊙}
𝔥𝔬𝔪_{⊕}^{⊙}[f](𝔲_{⊕}(x)) =^{def} f(x)
𝔥𝔬𝔪_{⊕}^{⊙}[f](x ⊕ y) =^{def} 𝔥𝔬𝔪_{⊕}^{⊙}[f](x) ⊙ 𝔥𝔬𝔪_{⊕}^{⊙}[f](y)

for any function f : α → 𝔗_{⊙}, x : α, and y : α, where 𝔗_{⊕} = ℭ_{⊕}(α).

Again, computationally, this amounts to executing the following iteration:

      result ← 𝔷_{⊙};

foreach x_{i} in 𝔲_{⊕}(x_{1}) ⊕ ⋯ ⊕ 𝔲_{⊕}(x_{n}) do result ← result ⊙ f(x_{i}); return result;

(1)

The reader may be puzzled by the condition Θ_{⊕} ⊆ Θ_{⊙} in Definition 4.1. It means that a monoid homomorphisms may only be defined from a collection monoid to a monoid that has at least the same equational theory. In other words, one can only go from an empty theory monoid, to either a {C}-monoid or an {I}-monoid, or yet to a {C, I}-monoid. This requirement is due to an algebraic technicality, and relaxing it would enable a monoid homomorphism to be ill-defined. To see this, consider going from, say, a commutative-idempotent monoid to one that is commutative but not idempotent. Let us take, for example, 𝔥𝔬𝔪_{∪}^{+}. Then, this entails:

\begin{matrix}1 = & 𝔥𝔬𝔪_{∪}^{+}[λx.1](\{a\}) \\ = & 𝔥𝔬𝔪_{∪}^{+}[λx.1](\{a\} ∪ \{a\}) \\ = & 𝔥𝔬𝔪_{∪}^{+}[λx.1](\{a\}) + 𝔥𝔬𝔪_{∪}^{+}[λx.1](\{a\}) \\ = & 1 + 1 \\ = & 2. \end{matrix}

The reader may have noticed that this restriction has the unfortunate consequence of disallowing potentially useful computations, notable examples being computing the cardinality of a set, or converting a set into a list. However, this drawback can be easily overcome with a suitable modification of the third clause in Definition 4.1, and other expressions based on it, ensuring that anomalous cases such as the above are dealt with by appropriate tests.

Also of importance for the consistency of Definition 4.1 is the fact that a non-idempotent monoid must be anti-idempotent, and a non-commutative monoid must be anti-commutative. Indeed, if ⊕ is non-idempotent as well as non-anti-idempotent (say, x_{0} ⊕ x_{0} = x_{0} for some x_{0}), then this entails:

\begin{matrix}𝔥𝔬𝔪_{⊕}^{⊙}[f](x_{0}) = & 𝔥𝔬𝔪_{⊕}^{⊙}[f](x_{0} ⊕ x_{0}) \\ = & 𝔥𝔬𝔪_{⊕}^{⊙}[f](x_{0}) ⊙ 𝔥𝔬𝔪_{⊕}^{⊙}[f](x_{0}) \end{matrix}

which is not necessarily true for non-idempotent ⊙. A similar argument may be given for commutativity. This consistency condition is in fact not restrictive operationally as it is always verified (e.g., a list will not allow partial commutation of any of its element).

Here are a few familar functions expressed with well-defined monoid homomorphisms:

length(l) = 𝔥𝔬𝔪_{++}^{+}[λx.1](l)
e ∈ s  = 𝔥𝔬𝔪_{∪}^{∨}[λx.x = e](s)
s × t  = 𝔥𝔬𝔪_{∪}^{∪}[λx.𝔥𝔬𝔪_{∪}^{∪}[λy.{⟨x, y⟩}](t)](s)
map(f, s) = 𝔥𝔬𝔪_{∪}^{∪}[λx.{f(x)}](s)
filter(p, s) = 𝔥𝔬𝔪_{∪}^{∪}[λx.𝔦𝔣 p(x) 𝔱𝔥𝔢𝔫 {x} 𝔢𝔩𝔰𝔢 {}](s).

4.1.2 Monoid comprehensions

The concept of monoid homomorphism is useful for expressing a formal semantics of iteration over collections. However, it is not very convenient as a programming construct. A natural notation for such a construct that is both conspicuous and can be expressed in terms of monoid homomorphisms is a monoid comprehension. This notion generalizes the familiar notation used for writing a set in comprehension (as opposed to writing it in extension) using a pattern and a formula describing its elements (as oppposed to listing all its elements). For example, the set comprehension {⟨x, x^{2}⟩ | x ∈ ℕ, ∃n.x = 2n} describes the set of pairs ⟨x, x^{2}⟩ (the pattern), verifying the formula x ∈ ℕ, ∃n.x = 2n (the qualifier).

This notation can be extended to any (primitive or collection) monoid ⊕. The syntax of a monoid comprehension is an expression of the form ⊕{e [] Q} where e is an expression called the head of the comprehension, and Q is called its qualifier and is a sequence q_{1}, …, q_{n}, n ≥ 0, where each q_{i} is either

• a generator of the form x ← e, where x is a variable and e is an expression; or,

• a filter ϕ which is a boolean condition.

In a monoid comprehension expression ⊕{e [] Q}, the monoid operation ⊕ is called the accumulator.

As for semantics, the meaning of a monoid comprehension is defined in terms of monoid homomorphisms.

Definition 4.2 (Monoid Comprehension) The meaning of a monoid comprehension over a monoid ⊕ is defined inductively as follows:

⊕\{e [] \}  =^{def} \{ \begin{matrix}𝔲_{⊕}(e) & if ⊕ is a collection monoid \\ e & if ⊕ is a primitive monoid \end{matrix}

⊕{e [] x ← e′, Q} =^{def} 𝔥𝔬𝔪_{⊙}^{⊕}[λx. ⊕ {e [] Q}](e′)
⊕{e [] c, Q}  =^{def} 𝔦𝔣 c 𝔱𝔥𝔢𝔫 ⊕ {e [] Q} 𝔢𝔩𝔰𝔢 𝔷_{⊕}

such that e : 𝔗_{⊕}, e′ : 𝔗_{⊙}, and ⊙ is a collection monoid.

Note that although the input monoid ⊕ is explicit, each generator x ← e′ in the qualifier has an implicit collection monoid ⊙ whose characteristics can be inferred with polymorphic typing rules.

Although Definition 4.2 can be effectively computed using nested loops (i.e., using the iteration semantics (1)), such would be in general rather inefficient. Rather, an optimized implementation can be achieved by various syntactic transformation expressed as rewrite rules. Thus, the principal benefit of using monoid comprehensions is to formulate efficient optimizations on a simple and uniform general syntax of expressions irrespective of specific monoids.

Note that relational joins are immediately expressible as monoid comprehensions. Indeed, the join of two sets S and T using a function f and a predicate p is simply:

S ▷◁_{p}^{f} T =^{def} ∪{f(x, y) [] x ← S, y ← T, p(x, y)}. (2)

Typically, a relational join will take f to be a record constructor. For example, if we write a record whose fields l_{i} have values e_{i} for i = 1, …, n, as ⟨l_{1} = e_{1}, , …, l_{n} = e_{n}⟩, then a standard relational join is obtained with, say, f(x, y) = ⟨name = y.name, age = 2 ∗ x.age⟩, and p(x, y) may be any condition such as x.name = y.name, x.age ≥ 18.

Clearly, monoid comprehensions can immediately express queries using all usual relational operators (and, indeed, object queries as well) and most usual functions. For example,

∃x ∈ s.e  =^{def} ∨{e [] x ← s}
∀x ∈ s.e  =^{def} ∧{e [] x ← s}
x ∈ s  =^{def} ∨{x = y [] y ← s}
s ∩ t  =^{def} ∪{x [] x ← s, x ∈ t}
count(a, s) =^{def} +{1 [] x ← s, x = a}

length(s) =^{def} +{1 [] x ← s}
sum(s)  =^{def} +{x [] x ← s}
max(s)  =^{def} max{x [] x ← s}
filter(p, s) =^{def} ∪{x [] x ← s, p(x)}
flatten(s) =^{def} ∪{x [] t ← s, x ← t}

Note that some of these functions will work only on appropriate types of their arguments. For example, the type of the argument of sum must be a non-idempotent monoid, and so must the type of the second argument of count. Thus, sum will add up the elements of a bag or a list, and count will tally the number of occurrences of an element in a bag or a list. Applying either sum or count to a set will be caught as a type error.

4.1.3 The monoid comprehension calculus

We are now in a position to propose a programming calculus using monoid comprehensions. Figure 1 defines an abstract grammar for an expression e of the Monoid Comprehension Calculus and amounts to adding comprehensions to an extended Typed Polymorphic λ-Calculus. Figure 2 gives the typing rules for this calculus.

e ::= ⊥  null value
| c  constant
| x  symbol
| λx.e  abstraction
| e_{1} e_{2}  application
| ⟨l_{1} = e_{1}, ⋯, l_{n} = e_{n}⟩ record
| e.l  projection
| 𝔦𝔣 e_{1} 𝔱𝔥𝔢𝔫 e_{2} 𝔢𝔩𝔰𝔢 e_{3}  conditional
| 𝔷_{⊕}  monoid identity
| 𝔲_{⊕}(e)  monoid unit injection
| e_{1} ⊕ e_{2}  monoid operation
| ⊕{e [] Q}  monoid comprehension

Figure 1: The monoid comprehension calculus

4.2 Multidimensional arrays as functions

5 Discussion

5.1 What types for Matisse?

Before we delve into redesigning a new Opl, we need to ponder its type particularities—indeed, peculiarities. The current Opl departs from conventional programming langauges when it comes to types in several respects. Figure 3 shows the types supported by Opl.

5.1.1 Primitive types 5.1.2 Object types 5.1.3 Collections types

5.2 Array types

5.2.1 First-class indexing HAK NOTE: Discuss the ZPL-region approach [3] for use in Matisse, and their sparse version [4].

\overline{Γ ⊢ ⊥ : α} for any Γ
\overline{Γ ⊢ c : τ} for any Γ, if type(a) = τ
\overline{Γ ⊢ x : τ} if Γ(x) = τ

\frac{Γ[x : τ_{1}] ⊢ e : τ_{2}}{Γ ⊢ λx.e : τ_{1} → τ_{2}}

\frac{Γ ⊢ e_{1} : τ_{1} → τ_{2}, Γ ⊢ e_{2} : τ_{1}}{Γ ⊢ e_{1} e_{2} : τ_{2}}

\frac{Γ ⊢ e_{1} : τ_{1}, ⋯, Γ ⊢ e_{k} : τ_{k}}{Γ ⊢ ⟨l_{1} = e_{1}, ⋯, l_{k} = e_{k}⟩ : ⟨l_{1} : τ_{1}, ⋯, l_{k} : τ_{k}⟩}

\frac{Γ ⊢ e : ⟨l_{1} : τ_{1}, ⋯, l_{k} : τ_{k}⟩}{Γ ⊢ e.l : τ} if l ∈ \{l_{1}, …, l_{k}\}

\frac{Γ ⊢ e_{1} : bool, Γ ⊢ e_{2} : τ, Γ ⊢ e_{3} : τ}{Γ ⊢ 𝔦𝔣 e_{1} 𝔱𝔥𝔢𝔫 e_{2} 𝔢𝔩𝔰𝔢 e_{3} : τ}

\overline{Γ ⊢ 𝔷_{⊕} : 𝔗_{⊕}} for any Γ
\frac{Γ ⊢ e : τ}{Γ ⊢ 𝔲_{⊕}(e) : ℭ_{⊕}(τ)} if ⊕ is a collection monoid
\frac{Γ ⊢ e_{1} : 𝔗_{⊕}, Γ ⊢ e_{2} : 𝔗_{⊕}}{Γ ⊢ e_{1} ⊕ e_{2} : 𝔗_{⊕}} if ⊕ is a primitive monoid
\frac{Γ ⊢ e_{1} : ℭ_{⊕}(τ), Γ ⊢ e_{2} : ℭ_{⊕}(τ)}{Γ ⊢ e_{1} ⊕ e_{2} : ℭ_{⊕}(τ)} if ⊕ is a collection monoid
\frac{Γ ⊢ e : 𝔗_{⊕}}{Γ ⊢ ⊕\{e [] \} : 𝔗_{⊕}} if ⊕ is a primitive monoid
\frac{Γ ⊢ e : τ}{Γ ⊢ ⊕\{e [] \} : ℭ_{⊕}(τ)} if ⊕ is a collection monoid
\frac{Γ ⊢ e_{2} : ℭ_{⊙}(τ_{2}), Γ[x : τ_{2}] ⊢ ⊕\{e_{1} [] Q\} : τ_{1}}{Γ ⊢ ⊕\{e_{1} [] x ← e_{2}, Q\} : τ_{1}} if Θ_{⊙} ⊆ Θ_{⊕}

\frac{Γ ⊢ e_{2} : bool, Γ ⊢ ⊕\{e_{1} [] Q\} : τ}{Γ ⊢ ⊕\{e_{1} [] e_{2}, Q\} : τ}

Figure 2: Typing rules for the Monoid Comprehension Calculus

type

basic structure range enum setof(type) array[type]

Figure 3: Opl types

5.2.2 Indexing types

5.3 Functional abstraction

6 Designing Matisse

6.1 Algebra

6.2 Semantics

6.3 Implementation

Appendix

In this part of the document, I summarize well-known notions that may be needed by some readers lacking the appropriate background. This is in order to spare those who already know this material and unclutter the main body of the text. The latter reason is also why Section B contains the complete listing of the transportation model used in the discussion of Section 3.

A Technical Background

A.1 The Relational Model

A.2 Monoids

In this section, all notions and notations relating to monoids as they are used in this paper are recalled and justified.

Mathematically, a monoid is a non-empty set equipped with an associative internal binary operation and an identity element for this operation. Formally, let S be a set, ⋆ a function from S × S to S, and ϵ ∈ S; then, ⟨S, ⋆, ϵ⟩ is a monoid iff, for any x, y, z in S:

x ⋆ (y ⋆ z) = (x ⋆ y) ⋆ z (3)

and

x ⋆ ϵ = ϵ ⋆ x = ϵ. (4)

Most familiar mathematical binary operations define monoids. For example, taking the set of natural numbers ℕ, and the set of boolean values 𝔹 = {𝔱𝔯𝔲𝔢, 𝔣𝔞𝔩𝔰𝔢}, the following are monoids:

• ⟨ℕ, +, 0⟩, • ⟨ℕ, ∗, 1⟩,

• ⟨ℕ, max, 0⟩,

• ⟨𝔹, ∨, 𝔣𝔞𝔩𝔰𝔢⟩,

• ⟨𝔹, ∧, 𝔱𝔯𝔲𝔢⟩.

The operations of these monoids are so familiar that they need not be explicated. For us, they have a “built -in” semantics that allows us to compute with them since primary school. Indeed, we shall refer to such readily interpreted monoids as primitive monoids.^{2}

Note that the definition of a monoid does not preclude additional algebraic structure. Such structure may be specified by other equations augmenting the basic monoid equational theory given by the conjunction of equations (3) and (4). For example, all five monoids listed above are commutative; namely, they also obey equation (5):

x ⋆ y = y ⋆ x (5)

for any x, y. In addition, the three last ones (i.e., max, ∨, and ∧) are also idempotent; namely, they also obey equation (6):

x ⋆ x = x (6)

for any x.

Not all monoids are primitive monoids. That is, one may define a monoid purely syntactically whose operation only builds a syntactic structure rather than being interpreted using some semantic computation. For example, linear lists have such a structure: the operation is list concatenation and builds a list out of two lists; its identity element is the empty list. A syntactic monoid may also have additional algebraic structure. For example, the monoid of bags is also defined as a commutative syntactic monoid with the disjunct union operation and the empty bag as identity. Or, the monoid of sets is a commutative and idempotent syntactic monoid with the union operation and the empty set as identity.

Because they are not interpreted, syntactic monoids pose a problem as far as representation of its elements is concerned. To illustrate this, let us consider an empty-theory algebraic structure; that is, one without any equations—not even associativity nor identity. Let us take such a structure with one binary operation ⋆ on, say, the natural numbers ℕ. Saying that ⋆ is a “syntactic” operation means that it constructs a syntactic term (i.e., an expression tree) by composing two other syntactic terms. We thus can define the set T_{⋆} of ⋆-terms on some base set, say the natural numbers, inductively as the limit ∪_{n≥0}T_{n} where,

T_{n} =^{def} \{ \begin{matrix}ℕ & if n = 0 \\ \{t_{1} ⋆ t_{2} | t_{i} ∈ T_{n−1}, i = 1, 2\} & if n > 0 \end{matrix} (7)

Clearly, the set T_{⋆} is well defined and so is the ⋆ operation over it. Indeed, ⋆ is a bona fide function from T_{⋆} × T_{⋆} to T_{⋆} mapping two terms t_{1} and t_{2} in T_{⋆} into a unique term in T_{⋆}—namely, t_{1} ⋆ t_{2}. This is why T_{⋆} is called the syntactic algebra.^{3}

2We call these monoids “primitive” following the presentation of Fegaras and Maier [9] as it adheres to a more operational (as opposed to mathematical) approach more suitable to computer-scientists. Mathematically, however, these should be called “semantic” monoids since they are interpreted by the computation semantics of their operations.

3For a fixed set of base elements and operations (which constitute what is formally called a signature), the syntactic algebra is unique (up to isomorphism). This algebra is also called the free, or the initial, algebra for its signature.

Let us now assume that the ⋆ operation is associative—i.e., that ⋆-terms verify Equation (3). Note that this equation defines a (syntactic) congruence on T_{⋆} which identifies terms such as, say, 1 ⋆ (2 ⋆ 3) and (1 ⋆ 2) ⋆ 3. In fact, for such an associative ⋆ operation, the set T_{⋆} defined in Equation (7) is not the appropriate domain. Rather, the right domain is the quotient set whose elements are (syntactic) congruence classes modulo associativity of ⋆. Therefore, this creates an ambiguity of representation of the syntactic structures.^{4}

Similarly, more algebraic structure defined by larger equational theories induces coarser quotients of the empty-theory algebra by putting together in common congruence classes all the syntactic expressions that can be identified modulo the theory’s equations. The more equations, the more ambiguous the syntactic structures of expressions. Mathematically, this poses no problem as one can always abstract away from individuals to congruence classes. However, operationally one must resort to some concrete artifact to obtain a unique representation for all members of the same congruence class. One way is to devise a canonical representation into which to transform all terms. For example, an associative operation could systematically “move” nested subtrees from its left argument to its right argument—in effect using Equation (3) as a one-way rewrite rule. However, while this is possible for some equational theories, it is not so in general—e.g., take commutativity.^{5}

From a programming standpoint (which is ours), we can abstract away from the ambiguity of canonical representations of syntactic monoid terms using a flat notation. For example, in LISP and Prolog, a list is seen as the (flat) sequence of its constituents. Typically, a programmer writes [1, 2, 1] to represent the list whose elements are 1, 2 and 1 in this order, and does not care (nor need s/he be aware) of its concrete representation. A set—i.e., a commutative idempotent syntactic monoid—is usually denoted by the usual mathematical notation {1, 2}, implicitly relying on disallowing duplicate elements, not minding the order in which the elements appear. A bag, or multiset—i.e., a commutative but non-idempotent syntactic monoid—uses a similar notation, allowing duplicate elements but paying no heed to the order in wich they appear; i.e., {{1, 2, 1}} is the bag containing 1 twice, and 2 once.

Syntactic monoids are quite useful for programming as they provide adquate data structures to represent collections of objects of a given type. Thus, we refer to them as collection monoids. Now, a definition such as Equation (7) for a syntactic monoid, although sound mathematically, is not quite adequate for programming purposes. This is because it defines the ⋆ operations on two distinct types of elements; namely, the base elements (here natural numbers) and constructed elements. In programming, it is desirable that operations be given a crisp type. A way to achieve this is by systematically “wrapping” each base element x into a term such as x⋆ϵ. This “wrapping” is achieve by associating to the monoid a function 𝔲_{⋆} from the base set into the monoid domain called its unit injection. For example, if++ is the list monoid operation for concatenating two lists, 𝔲_{++}(x) = [x] and one may view the list [a, b, c] as [a]++[b]++[c]. Similarly, the set {a, b, c} is viewed as {a} ∪ {b} ∪ {c}, and the bag {{a, b, c}} as {{a}} ⊎ {{b}} ⊎ {{c}}. Clearly, this bases the constructions on an isomorphic view of the base set rather than the base set itself, while using a uniform type for the monoid operator. Also, because the type of the base elements is irrelevant for the construction other than imposing the constraint that all such elements be of the same type, we present a collection monoid as a polymorphic data type. This justifies the formal view of monoids we give next using the programming notion of type.

4Note that this ambiguity never arises for semantic algebras whose operations are interpreted into a unique result.

5Such are important considerations in the field of term rewriting [8], where the problem of finding canonical term representations for equational theories was originally addressed by Donald Knuth and Peter Bendix in a seminal paper proposing a general effective method—the so-called Knuth-Bendix Completion Algorithm [13]. The problem, incidentally, is only semi-decidable. In other words, the Knuth-Bendix algorithm may diverge, although several interesting variations have been proposed for a wide extent of practical uses (see [8] for a good introduction and bibliography).

⊕ 𝔗_{⊕}  𝔷_{⊕}  Θ_{⊕}
+ int  0  {C}
∗ int  1  {C}
max int  0 {C, I}
∨ bool  𝔣𝔞𝔩𝔰𝔢 {C, I}
∧ bool  𝔱𝔯𝔲𝔢 {C, I}

⊕ ℭ_{⊕} 𝔗_{⊕}  𝔷_{⊕} 𝔲_{⊕}(x) Θ_{⊕}
∪ set   set(α) {} {x} {C, I}
⊎ bag   bag(α) {{}} {{x}} {C}
++ list  list(α) []  [x]  ∅

Primitive monoids  Collection monoids

Table 1: Attributes of a few common monoids

Because it is characterized by its operation ⊕, a monoid is often simply referred to as ⊕. Thus, a monoid operation is used as a subscript to denote its characteristic attributes. Namely, for a monoid ⊕,

• 𝔗_{⊕} is its type (i.e., ⊕ : 𝔗_{⊕} × 𝔗_{⊕} → 𝔗_{⊕}),

• 𝔷_{⊕} : 𝔗_{⊕} is its identity element,

• Θ_{⊕} is its equational theory (i.e., a subset of the set {C, I}, where C stands for “commutative” and I for “idempotent”);

and, if it is a collection monoid,

• ℭ_{⊕} is its type constructor (i.e., 𝔗_{⊕} = ℭ_{⊕}(α)),

• 𝔲_{⊕} : α → ℭ_{⊕}(α) is its unit injection.

Table 1 summarizes the monoid attributes of a few usual monoids.

A.3 The Typed Polymorphic λ-Calculus

We assume a set C of pregiven constants ususally denoted by a, b …, and a countably infinite set of variable symbols V usually denoted by x, y, . . .. The syntax of a term t of the λ-Calculus is given by the following grammar:

t ::= a  (a ∈ C) constant
| x  (x ∈ V) symbol
| λx.t (x ∈ V) abstraction
| t t  application

(8)

We shall call T the set of terms t defined by this grammar. These terms are also called raw terms.

An abstraction λx.t defines a lexical scope for its bound variable x, whose extent is its body t. Thus, the notion of free occurrence of a variable in a term is defined as usual, and so is the operation t_{1}[t_{2}/x] of substituting a term t_{2} for all the free occurrences of a variable x in a term t_{1}. Thus, a bound variable may be renamed to a new one in its scope without changing the abstraction.

The computation rule defined on λ-terms is the so-called β-reduction:

(λx.t_{1}) t_{2} ⟶ t_{1}[t_{2}/x].  (9)

We assume a set B of basic type symbols denoted by A, B, …, and a countably infinite set of type variables V denoted by α, β, . . .. The syntax of a type τ of the Typed Polymorphic λ-Calculus is given by the following grammar:

τ ::= A  (A ∈ B) basic type
| α  (α ∈ V) variable type
| τ → τ  function type

(10)

We shall call T the set of types τ defined by this grammar. A monomorphic type is a type that contains no variable types. Any type containing at least one variable type is called a polymorphic type.

The terms of the Typed Polymorphic λ-Calculus are only those raw terms in T that admit a well-defined type in T . Each constant in C is assumed to have a unique type in T , and we write type(a) = τ to mean that constant a has type τ.

One may assign types to symbols using a type context Γ, which is a partial function from V to T . Given a type context Γ, a variable x ∈ V and a type τ ∈ T , we define:

Γ[x : τ](y) =^{def} \{ \begin{matrix}τ & if x = y; \\ Γ(y) & if x ≠ y. \end{matrix} (11)

In other words, Γ[x : τ] coincides with Γ everywhere on V except at x, where it takes the value τ. The empty context is the function noted ∅ defined nowhere on V.

To find out whether a term t in T is well-typed, one must exhibit a type assignment that constitutes a suitable typing context for the variable symbols occurring in t, and from which one may ascribe a (unique) type for the whole term. Given a type context Γ, a term t, and a type τ, a type judgement is an expression of the form Γ ⊢ t : τ, which stands to mean that t has been deemed to have type τ when the symbols occurring in it have the types assigned to them by the context Γ. Without a type context Γ, the expression t : τ is used to mean that Γ ⊢ t : τ for some Γ.

Deriving types for terms is done using typing rules of the form:

\frac{Γ_{1} ⊢ t_{1} : τ_{n}, ⋯ Γ_{n} ⊢ t_{n} : τ_{n}}{Γ ⊢ t : τ}

which is read as follows: “t has type τ under Γ if t_{1} has type τ_{1} under Γ_{1}, …, and t_{n} has type τ_{n} under Γ_{n}.” Note that it is possible that n = 0, in which case the rule is written:

\overline{Γ ⊢ t : τ}

and it is called an axiom.

The typing rules for the Typed Polymorphic λ-Calculus are given in Figure 4. These rules can be readily translated into a Logic Programming language based on Horn-clauses such as Prolog, and used as an effective means to infer the types of expressions based on the Typed Polymorphic λ-Calculus.

The basic syntax of the Typed Polymorphic λ-Calculus may be extended with other operators and convenient data structures as long as typing rules for the new constructs are provided. Typically, one provides at least the set ℕ of integer constants and 𝔹 = {𝔱𝔯𝔲𝔢, 𝔣𝔞𝔩𝔰𝔢} of boolean constants, along with basic arithmetic and boolean operators, pairing (or tupling), a conditional operator, and a fix-point operator. The usual arithmetic and boolean operators are denoted by constant symbols (e.g., +, ∗, −, /, ∨, ∧, etc.). Let O be this set.

\overline{Γ ⊢ a : τ} for any Γ, if type(a) = τ
\overline{Γ ⊢ x : τ} if Γ(x) = τ

\frac{Γ[x : τ_{1}] ⊢ t : τ_{2}}{Γ ⊢ λx.t : τ_{1} → τ_{2}}

\frac{Γ ⊢ t_{1} : τ_{1} → τ_{2}, Γ ⊢ t_{2} : τ_{1}}{Γ ⊢ t_{1} t_{2} : τ_{2}}

Figure 4: Typing rules for the Typed Polymorphic λ-Calculus

The computation rules for these operators are based on their usual semantics as one might expect, modulo transforming the usual binary infix notation to a “curryed” application. For example, t_{1} + t_{2} is implicitly taken to be the application (+ t_{1}) t_{2}. Note that this means that all such operators are implicitly “curryed.”^{6}

For example, we may augment the grammar for the terms given in (8) as follows:

t ::= a  (a ∈ C = ℕ ∪ 𝔹 ∪ O) constant
| x  (x ∈ V)  symbol
| λx.t  (x ∈ V)  abstraction
| t t  application
| ⟨t, ⋯, t⟩  tupling
| t.n (n ∈ ℕ) projection
| 𝔦𝔣 t 𝔱𝔥𝔢𝔫 t 𝔢𝔩𝔰𝔢 t  conditional
| 𝔣𝔦𝔵 t  recursion

(12)

The computation rules for the other new constructs are:

⟨t_{1}, ⋯, t_{k}⟩.i ⟶ \{ \begin{matrix}t_{i} & if 1 ≤ i ≤ k \\ undefined otherwise \end{matrix}

𝔦𝔣 c 𝔱𝔥𝔢𝔫 t_{1} 𝔢𝔩𝔰𝔢 t_{2} ⟶ \{ \begin{matrix}t_{1} & if c = 𝔱𝔯𝔲𝔢 \\ t_{2} & if c = 𝔣𝔞𝔩𝔰𝔢 \\ undefined otherwise \end{matrix}

𝔣𝔦𝔵 t ⟶ t (𝔣𝔦𝔵 t)

(13)

To account for the new constructs, the syntax of types is extended accordingly to:

τ ::= int | bool  basic type
| α  (α ∈ V) variable type
| ⟨τ, ⋯, τ⟩  tuple type
| τ → τ  function type

(14)

6Recall that a curryed form of an n-ary function f is obtained when f is applied to less arguments than it expects; i.e., f(t_{1}, …, t_{k}), for 1 ≤ k < n. In the λ-calculus, this form is simply interpreted as the abstraction λx_{1}…. λx_{n−k}.f(t_{1}, …, t_{k}, x_{1}, …, x_{n−k}). In their fully curried form, all n-ary functions can be seen as unary functions; indeed, with this interpretation of curried forms, it is clear that f(t_{1}, …, t_{n}) = (… (f t_{1}) … t_{n−1}) t_{n}.

\overline{Γ ⊢ x : τ} if Γ(x) = τ

\frac{Γ[x : τ_{1}] ⊢ t : τ_{2}}{Γ ⊢ λx.t : τ_{1} → τ_{2}}

\frac{Γ ⊢ t_{1} : τ_{1} → τ_{2}, Γ ⊢ t_{2} : τ_{1}}{Γ ⊢ t_{1} t_{2} : τ_{2}}

\frac{Γ ⊢ t_{1} : τ_{1}, ⋯, Γ ⊢ t_{k} : τ_{k}}{Γ ⊢ ⟨t_{1}, ⋯, t_{k}⟩ : ⟨τ_{1}, ⋯, τ_{k}⟩}

\frac{Γ ⊢ t : ⟨τ_{1}, ⋯, τ_{k}⟩}{Γ ⊢ t.n : τ} if 1 ≤ n ≤ k

\frac{Γ ⊢ t_{1} : bool, Γ ⊢ t_{2} : τ, Γ ⊢ t_{3} : τ}{Γ ⊢ 𝔦𝔣 t_{1} 𝔱𝔥𝔢𝔫 t_{2} 𝔢𝔩𝔰𝔢 t_{3} : τ}

\frac{Γ ⊢ t : τ → τ}{Γ ⊢ 𝔣𝔦𝔵 t : τ}

Figure 5: Typing rules for an Extended Typed Polymorphic λ-Calculus

We are given that type(n) = int for all n ∈ ℕ and that type(𝔱𝔯𝔲𝔢) = bool and type(𝔣𝔞𝔩𝔰𝔢) = bool. The (fully curried) types of the built-in operators are given similarly; i.e., type(+) = int → (int → int), type(∨) = bool → (bool → bool), etc., … The typing rules for this extended calculus are given in Figure 5.

B A Transportation Model in Opl

[01]     enum City ...;
[02]     enum Product ...;
[03]     float+ limit = ...;
[04]
[05]     struct TableRoutesType
[06]        { Product p;
[07]          City o;
[08]          City d;
[09]          float+ cost;
[10]        };
[11]
[12]     {TableRoutesType} TableRoutes = ...;
[13]
[14]     struct Connection
[15]        { City o;
[16]          City d;
[17]        };
[18]
[19]     struct Route

[20]        { Product p;
[21]          Connection e;
[22]        };
[23]
[24]     {Route} Routes = { < p,<o,d> > | <p,o,d,c> in TableRoutes };
[25]
[26]     {Connection} Connections = { c | <p,c> in Routes };
[27]
[28]     struct Supply
[29]        { Product p;
[30]          City o;
[31]        };
[32]
[33]     {Supply} Supplies = { <p,c.o> | <p,c> in Routes };
[34]
[35]     float+ supply[Supplies] = ...;
[36]
[37]     struct Customer
[38]        { Product p;
[39]          City d;
[40]        };
[41]
[42]     {Customer} Customers = { <p,c.d> | <p,c> in Routes };
[43]
[44]     float+ demand[Customers] = ...;
[45]
[46]     float+ cost[Routes];
[47]
[48]     initialize
[49]        { forall( <p,o,d,c> in TableRoutes)
[50]              cost[< p,<o,d> >] = c;
[51]        };
[52]
[53]     {City} orig[p in Product] = { c.o | <p,c> in Routes };
[54]     {City} dest[p in Product] = { c.d | <p,c> in Routes };
[55]
[56]     {Connection} CP[p in Product] = { c | <p,c> in Routes };
[57]
[58]     assert
[59]        forall(p in Product)
[60]          sum(o in orig[p]) supply[<p,o>] = sum(d in dest[p]) demand[<p,d>];
[61]
[62]     var float+ trans[Routes];
[63]
[64]     minimize
[65]        sum(l in Routes) cost[l] * trans[l]
[66]     subject to
[67]        {
[68]          forall(p in Product, o in orig[p])
[69]              sum(<o,d> in CP[p]) trans[< p,<o,d> >] <= supply[<p,o>];
[70]
[71]          forall(p in Product, d in dest[p])
[72]              sum(<o,d> in CP[p]) trans[< p,<o,d> >] >= demand[<p,d>];
[73]
[74]          forall(c in Connections)

[75]              sum(<p,c> in Routes) trans[<p,c>] <= limit;
[77]        };

References

[1] Peter Buneman, Leonid Libkin, Dan Suciu, Val Breazu-Tannen, and Limsoon Wong. Comprehension syntax. ACM SIGMOD Record, 23(1):87–96, March 1994. (Available online^{7}).

[2] Rick Cattell, Douglas Barry, Mark Berler, Jeff Eastman, David Jordan, Craig Russell, Olaf Schadow, Torsten Stanienda, and Fernando Velez, editors. Object Data Standard—ODMG 3.0. Morgan Kaufmann, January 2000.

[3] Bradford Chamberlain, Christopher Lewis, Calvin Lin, and Lawrence Snyder. Regions: An abstraction for expressing array computation. In Proceedings of the SIGAPL/SIGPLAN International Conference on Array Programming Languages, pages 41–49, August 1999. (Available online^{8}).

[4] Bradford Chamberlain, Christopher Lewis, and Lawrence Snyder. A region-based approach for sparse parallel computing. Technical Report UW-CSE-98-11-01, University of Washington at Seattle (Computer Science), November 1998. (Available online^{9}).

[5] Edgar F. Codd. A relational model of data for large shared data banks. Communications of the ACM, 13(6):377–387, 1970.

[6] Edgar F. Codd. Extending database relations to capture more meaning. ACM Transactions on Database Systems, 4(4):397–434, 1979.

[7] Edgar F. Codd. The Relational Model for Database Management. Addison-Wesley, 1990.

[8] Nachum Dershowitz. A taste of rewriting. In Peter E. Lauer, editor, Functional Programming, Concurrency, Simulation and Automated Reasoning, pages 199–228. Springer-Verlag, 1993. (Available online^{10}).

[9] Leonidas Fegaras and David Maier. Optimizing object queries using an effective calculus. ACM Transactions on Database Systems, 25(4):?–?, December 2000. (Available online^{11}).

[10] Pascal van Hentenryck. The OPL Optimization Programming Language. The MIT Press, 1999.

[11] Andreas Heuer and Marc H. Scholl. Principles of object-oriented query languages. In H.-J. Appelrath, editor, Proceedings of the GI Conference on Database Systems for Office, Scientific, and Engineering Applications, Kaiserslautern, Germany, pages 178–197. Springer-Verlag IFB 270, 1991. (Available online^{12}).

[12] James Hoffman. Introduction to Structured Query Language. (Available online^{13}), 1996– 2001.

7http://www.acm.org/sigs/sigmod/record/issues/9403/Comprehension.ps 8http://www.cs.washington.edu/homes/echris/papers/apl99.ps 9ftp://ftp.cs.washington.edu/tr/1998/11/UW-CSE-98-11-01.PS.Z 10http://www-sal.cs.uiuc.edu/~nachum/papers/taste-fixed.ps.gz 11http://lambda.uta.edu/tods00.ps.gz 12ftp://ftp.informatik.uni-konstanz.de/pub/dbis/Publications/HS:BTW91.ps.gz 13http://w3.one.net/~jhoffman/sqltut.htm

[13] Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, UK, 1970. Reprinted in Automatic Reasoning, 2, Springer-Verlag, pp. 342– 276 (1983).

[14] Leonid Libkin, Rona Machlin, and Limsoon Wong. A query language for multidimensional arrays: Design, implementation, and optimization techniques. In Proceedings of the 1996 ACM SIGMOD International Conference on Management of Data, Montreal, Canada, pages 228–239, May 1996. (Available online^{14}).

[15] Frédéric Paulin. OPL language syntax critique and proposal for improvement. (Available online^{15}), April 2001. ILOG internal access only.

[16] Scott L. Vandenberg. Algebras for Object-Oriented Query Languages. PhD thesis, University of Wisconsin at Madison (Computer Sciences), 1993. (Available online^{16}).

[17] Limsoon Wong. Querying Nested Collections. PhD thesis, University of Pennsylvania (Computer and Information Science), 1994. (Available online^{17}).

14http://www.cs.toronto.edu/~libkin/papers/sigmod96a.ps.gz 15file:/nfs/opl/matisse/dev/opl syntax critic.html 16ftp://ftp.cs.wisc.edu/pub/tech-reports/reports/1993/tr1161.ps.Z 17ftp://ftp.cis.upenn.edu/pub/ircs/tr/94-09.ps.Z