BRICS RS-01-25 B. Grobauer: Cost Recurrences for DML Programs BRICS

Basic Research in Computer Science

Cost Recurrences for DML Programs

Bernd Grobauer BRICS Report Series RS-01-25 ISSN 0909-0878 June 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Bernd Grobauer.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/01/25/

Cost Recurrences for DML Programs

Bernd Grobauer ^{∗}

BRICS^{†}

Department of Computer Science University of Aarhus

June, 2001

Abstract

A cost recurrence describes an upper bound for the running time of a program in terms of the size of its input. Finding cost recurrences is a frequent intermediate step in complexity analysis, and this step requires an abstraction from data to data size. In this article, we use information contained in dependent types to achieve such an abstraction: Dependent ML (DML), a conservative extension of ML, provides dependent types that can be used to associate data with size information, thus describing a possible abstraction. We systematically extract cost recurrences from first-order DML programs, guiding the abstraction from data to data size with information contained in DML type derivations.

1 Introduction

Analyzing the time complexity of a program is usually carried out in two steps. First, one establishes an upper bound of the program’s running time as a function of the size of its input. Second, one approximates the growth of this extracted bounding function, thus determining the complexity class of the program. The first step requires an abstraction from data to data size. Information contained in dependent types can be used to achieve such an abstraction. In this article, we show how to automatically extract time bounds from first-order programs written in Dependent ML (DML), an extension of ML that provides a limited form of dependent types. If a bound is successfully extracted, we can guarantee that it is a recurrence, i.e., an equation defining a function in terms of its result on smaller inputs. A recurrence that describes an upper bound for the running time of a program is called a cost recurrence.

∗

Ny Munkegade, Building 540, 8000 Aarhus C, Denmark.

E-mail: grobauer@brics.dk

†

Basic Research in Computer Science (www.brics.dk),

funded by the Danish National Research Foundation.

Limits and achievements of automated cost analysis Automated cost analyses have inherent limits. For example, finding a cost recurrence for a program is at least as hard as proving termination of the program. Also, finding good approximations for the growth of recurrences (or, in general, almost any kind of function) is known to be a hard problem.

Nevertheless, automated methods for cost analysis have been proposed. One choice is to restrict the class of programs such that termination is guaranteed, and the extracted time bounds can easily be approximated. For example, Reistad and Gifford [7] consider functional programs without general recursion, using only combinators such as map and zip. Methods that treat more general programs, as for example proposed by Le Métayer [4] and Rosendahl [8], usually focus on extracting a cost program p^{c}; if p^{c} terminates, it calculates an upper bound for the running time of a program p. Transforming p^{c} may yield a version compact enough to read off the complexity class of p. If not, p^{c} still may be useful for more empirical attempts to determine the time complexity of p, such as plotting input size against the running time calculated by p^{c}.

Dependent ML DML, which was developed by Xi [12, 16] in his PhD thesis, extends ML with a limited form of dependent types: A DML type can be enriched with indices taken from a constraint domain (e.g., integers equipped with their usual operations, with linear (in)equalities as constraints). For example, the data type of lists can be enriched with a notion of length or a data type of trees with a notion of height. The type language is expressive enough to encode well-formedness criteria, such as a tree being balanced. DML function types can express non-trivial properties, for example that a list is always mapped to a list of the same length, or that a function with a balanced tree as input always returns a balanced tree.

The design philosophy of DML is to use type-checking for the verification of non-trivial correctness properties of ML programs—every valid ML program is a valid DML program, because DML extends ML conservatively. For example, to verify that a program for inserting an element into a balanced tree indeed returns a balanced tree, the user needs to (1) enrich a data type of trees such that only balanced trees are accepted, and (2) declare in a type annotation that the insert function maps balanced trees to balanced trees. A range of similar examples convincingly demonstrates that DML is a useful tool for practical programming [12, 13, 15, 16].

This work We use information contained in DML type derivations to extract cost recurrences from DML programs. With DML types, data can be associated with a measure of data size, which essentially describes an abstraction from data to data size that is necessary for extracting a cost recurrence. For example, enriching the data type of lists with a notion of length describes an abstraction from lists to their length. More intricate measures—the high expressiveness of DML types allows the user to tailor measures to each situation. In many cases, measures with several components (e.g., for trees, the pair of height and number of leaves) prove to be useful. Size measures often coincide with shape information for data that is useful for verifying program properties by DML type-checking. Therefore, in many cases, DML types that express correctness properties of a program can be reused for establishing the complexity of the program.

We allow recurrences to contain logical formulas, which are used to restrict arguments that cannot be completely determined. Thus, logical information contained in DML type derivations about such arguments can be included in cost recurrence rather than approximating them in an ad-hoc way. Compared with other methods that extract executable cost bounds—and therefore are required to carry out approximations—we leave the choice of how to approximate to the user, thus separating concerns between extracting a cost recurrence and solving it.

We combine the extraction of a cost bound with a check whether the result is indeed a recurrence: The information contained in DML type derivations facilitates a check of whether the size measure decreases for each recursive call under a wellfounded ordering. In other words, the user has to choose a size measure that constitutes a termination order for the program in question. This is no limitation compared to other methods: Because finding a cost bound entails a termination proof, in all methods for cost analysis a termination proof needs to be found in some way. It is an asset of using DML that the termination proof can be concisely encoded through the size measure.

An example Consider a zip function written in ML:

  fun zip lp =
   case lp of
      (nil,nil) => nil
    | (cons(x,xs),cons(y,ys)) => cons((x,y),zip(xs,ys))

DML offers the possibility to annotate zip with a type containing an enriched version of lists. We enrich the data type of lists with a notion of length; the type of α-typed lists consisting of n elements is written as α list(n). Obviously, zip should take two lists of equal length and return a list of the same length. DML type checking validates that zip has the type

Π n : ℕ . α list(n) × β list(n) → (α × β)list(n).

Intuitively, Π can be read as “for all”.^{1} In ML, a pair of two lists with different lengths could be passed to zip, which would result in a runtime error. In DML, the given type of zip allows zip only to be called with two lists of equal length. The type also shows that the resulting list is of the same length as the input lists.

1Formally, Π introduces a dependent product, i.e., a product where the value of the first component (here n) determines the type of the second component (here the function from a pair of lists of length n to a list of length n). Dependent products are also called Π-types.

Let us measure running time as the number of calls to user-defined functions, giving each call a cost of one unit. The resulting recurrence describes the number of calls to zip as a function of the length of the two input lists:

zip^{c}(n) = \begin{cases}n = 0 → 0 \\ n > 0 → 1 + zip^{c}(n − 1) \end{cases}

This cost recurrence is extracted from a DML type derivation for zip. In the type derivation, the arguments to zip—two lists—are associated with an index n that represents their length. Using this information, the extraction algorithm abstracts from the lists to their length n. For example, the case expression is turned into a conditional by inferring for each branch a condition on n that has to hold if the pattern is matched. Similarly, the algorithm derives from the type derivation that the recursive call of zip has a list of length n − 1 as argument, and thus generates a call zip^{c}(n − 1). Obviously, n − 1 < n, so the extracted bound is a recurrence.

The recurrence can easily be solved: zip^{c}(n) = n.

The remainder of the article The article is structured as follows: Section 2 gives an introduction to DML, Section 3 presents an intuitive account of our method for extracting cost recurrences and gives several examples, Section 4 contains a formal account, Section 5 treats related work, and Section 6 concludes. Appendix A gives a short overview over the formal definition of DML, and Appendix B contains details of the formal development of this work.

2 Background: Dependent ML

DML provides dependent types in which type index objects are limited to some constraint domain C. Type checking for DML is decidable; it is based on solving constraints in C. For dependently typed languages with significantly more expressive types (e.g., Cayenne [1]) type checking is undecidable.

We consider an effect-free fragment of DML. As constraint domain, we choose integers, constrained by linear (in)equalities—we write ℤ both for the sort of integers and the constraint domain. In the following, we present a short introduction to programming in DML and sketch the formal specification of DML. The latter forms the basis for the formal development presented in Section 4.

2.1 A programmer’s view of DML

The only new aspect for an ML programmer is the extended type system, which contains type indices, in the present case integers.

2.1.1 Enriched recursive data types

As indicated in the example in Section 1, in DML a list type can be enriched with a notion of length, enabling us to express the type of α-typed lists of n elements as α list(n). The DML data-type definition is

  datatype α list with ℕ =
     nil(0)
   | Π n : ℕ . cons(n + 1) of α × α list(n)

It is obtained from an ordinary definition of lists in ML by making the following additions:

1. The phrase “with ℕ” has been added. This signifies that the data type of lists is to be enriched with one index and that this index is restricted to the sort of natural numbers. The constraint language of DML allows the definition of subsorts of an already defined sort: ℕ stands for {k : ℤ | k ≥ 0}.

2. Constructors and occurrences of “list” are augmented with an index. The constructor nil is indexed with 0, thus defining the empty list to be of type α list(0). A list built with cons is of type α list(n + 1), provided that cons was applied to an element of type α list(n). Hence, cons is indexed with n + 1.

3. The definition of the cons case exhibits a quantification over an index variable n. This index variable is necessary to express the dependence between the index of cons and the index of the list appearing in its branch. The quantification restricts the index variable to the sort of natural numbers.

Similarly, we can define the data type of a list of lists α llist(m,n) as

  datatype α llist with (ℕ,ℕ) =
     lnil(0,0)

| Π m, n_{1}, n_{2} : ℕ . lcons(m + 1,n_{1} + n_{2}) of

                    α list(n_{1}) × α llist(m,n_{2})

The first index stands for the number of inner lists and the second index for the total number of elements the inner lists contain.

The example of lists provides some intuition of how to define enriched recursive data types in two steps: First, decide on the number of indices to be used in the data type, along with the sorts the indices are to be restricted to. Second, annotate each constructor with the appropriate indices. When an index of a constructor depends on indices of recursive data types that appear under that constructor, introduce new index variables using quantification. An index can be defined as a function of other indices using all operations of the constraint domain.

In the introduction we mentioned that enriched data types can encode wellformedness criteria. As an example, we define a data type of height-balanced trees, i.e., the height difference between the two children of a node can be at most one:

  datatype α HBtree with (ℕ,ℕ) =
     Leaf(0,0)

| Π s_{1}, s_{2}, h_{1} : ℕ . Π h_{2} : {k : ℕ | h_{1} − 1 ≤ k ≤ h_{1} + 1}. Node(1 + max(h_{1}, h_{2}), s_{1} + s_{2} + 1) of

       α HBtree(h_{1},s_{1}) × α × α HBtree(h_{2},s_{2})

We use two indices, where the first represents the height of the tree and the second represents the number of elements stored in the tree. When defining a node, we require for the heights h_{1} and h_{2} of the subtrees, that they differ by at most one. This can be achieved by (1) defining a sort of natural numbers k that differ by at most one from h_{1}, and (2) restricting h_{2} to this new sort. As a consequence, only two trees with a height difference of at most one can be the children of a node, i.e., only height-balanced trees can have type α HBtree.

Note that for defining a new sort, all predicates and operations of the chosen constraint domain can be used. In the case of height-balanced trees, we use −, +, and ≤.

2.1.2 DML function types

As in ML, a data-type definition gives rise to type declarations for its constructors. For example, the definition of enriched lists presented above yields a type α list(0) for the constructor nil, and the type

Π n : ℕ . α × α list(n) → α list(n + 1)

for the constructor cons.

Figure 1 shows three functions operating on the data types defined in Section 2.1.1, together with their DML types:

• append takes two lists of n_{1} and n_{2} elements, respectively, and returns a list of n_{1} + n_{2} elements.

• flatten takes a list of lists that contain a total number of n elements, and returns a list of n elements

• occurs takes a string and a balanced tree, and returns a truth value, according to whether the string is stored in the tree or not (assuming a sorted balanced tree).

The DML types of append, flatten and occurs add shape information to the respective ML type of each function: In the case of append and flatten, we learn about the shape of the result, i.e., how long the output list is. For occurs, the DML type restricts the input tree to trees of a special shape, namely balanced trees.

So far, the output indices in the DML type of a function could always be specified as a function of the input indices. For relational dependencies, DML offers existential types. These allow one to restrict the index of an output to a sort—because sorts can be defined in terms of already declared indices, relational dependencies can be expressed.

append : Π n_{1}, n_{2} : ℕ . α list(n_{1}) × α list(n_{2}) → α list(n_{1} + n_{2})

  fun append lp =
   case lp of
      (nil,l2) => l2
    | (cons(x,xs),l2) => cons(x,append(xs,l2))

flatten : Π m, n : ℕ . α llist(m,n) → α list(n)

  fun flatten ll =
   case ll of
      lnil => nil
    | lcons(xs,rest) => append(xs,flatten rest)

occurs : Π h, s : ℕ . string × string HBtree(h,s) → bool

  fun occurs(e,t) =
   case t of
      Leaf => false
    | Node(t1,e',t2) => if e = e'
                        then true
                        else if e < e'
                             then occurs(s,t1)
                             else occurs(s,t2)

Figure 1: Some functions with their DML types

Consider, for example, a function that inserts a string into a balanced tree. Depending on how the tree is rebalanced, the result can be a tree of equal height or a tree higher by one. Similarly, the number of elements in the tree stays equal if the element to be inserted already was in the tree, otherwise the number is increased by one. A valid DML type for a correct insert function on height-balanced trees is as follows:

Π h, s : ℕ . string × HBtree(h,s) →
∃ h′ : {k : ℕ | h ≤ k ≤ h + 1} .
∃ s′ : {k : ℕ | s ≤ k ≤ s + 1} .
HBtree(h′,s′)

The type of the output tree restricts height and size to be either equal or larger by one than the height and size of the input tree, respectively.

2.2 A formal specification of DML

In the theoretical development of DML [12], three languages are defined, whose interplay is displayed graphically in Figure 2.

• ML_{0} basically is an extension of Mini-ML with general pattern matching. It formalizes a manageable subset of ML.

[figure: e^{∗} : τ; eval; ||·||; e : σ; eval; e′ : τ; |·|; type elaboration; v^{∗} : τ; ||·||; v : σ; \overbrace{DML_{0}^{Π}(C)}; \overbrace{ML_{0}}; \overbrace{DML_{0}(C)}]

Figure 2: Interplay of languages

• DML_{0}^{Π}(C) is an explicitly typed language with dependent types, i.e., types that are indexed with elements from a constraint domain C. Its syntax is that of ML_{0}, adding abstraction over index variables and application of an expression to index expressions. A canonical erasure || · || that removes index-related syntax both from the term and the type language, maps DML_{0}^{Π}(C) into ML_{0}. The erasure commutes with evaluation.

• DML_{0}(C) enriches ML_{0} with dependent types; it has the same type language as DML_{0}^{Π}(C). DML_{0}(C) requires type-annotations only for recursive definitions. An erasure on the type language extends to an erasure | · | that maps DML_{0}(C) into ML_{0}. A type-elaboration algorithm maps a DML_{0}(C) program with correct type annotations into DML_{0}^{Π}(C) such that (1) the type annotations are preserved and (2) the erasure of both terms results in the same ML_{0} term.

DML_{0}^{Π}(C) allows easy type-checking, because it is explicitly typed and indices are part of the term language. For the same reason, however, DML_{0}^{Π}(C) is impractical for actual programming. Instead, the user works with DML_{0}(C), which corresponds to the language, the example programs of Section 2.1.2 are given in: Their displayed DML-types are the type-annotations that are required for the implicit recursive definitions. Type-checking is carried out by a type elaboration algorithm [12, Chapter 4], evaluation by applying the erasure and the ML_{0} evaluation mechanism.

In the following, we first give some basic facts about constraint domains and the constraint language used to express the index objects for DML types. We then briefly describe DML_{0}^{Π}(C).^{2} The description glosses over many details—we refer the reader to Xi’s PhD thesis [12] for the complete picture.

2For simplicity, we restrict the presentation to the monomorphic case without existential types—polymorphism and existential types are treated in extensions of DML_{0}^{Π}(C).

2.2.1 Constraints in DML

A constraint domain C is defined by (1) a signature Σ that declares a base sort along with basic operations and predicates and (2) a Σ-structure. For example, for the constraint domain ℤ, the signature declares the base sort ℤ and the usual operations (+, −, mod, etc.) and predicates (<, ≥, etc.) over integers; the Σ-structure is given by the standard model of integers.

sorts  γ ::= b ||| 1 ||| γ_{1} × γ_{2} ||| {a : γ | P }
propositions P ::= ⊤ ||| ⊥ ||| i = j ||| p(i) ||| P_{1} ∧ P_{2} ||| P_{1} ∨ P_{2}
objects  i, j ::= a ||| f(i) ||| ⟨⟩ ||| ⟨i, j⟩ ||| fst(i) ||| snd(i)
contexts  ϕ ::= · ||| ϕ, a : γ ||| ϕ, P

Figure 3: Constraint language

DML uses the constraint language defined in Figure 3 to express the index objects for DML types. New sorts can be defined by pairing already defined sorts or restricting an already defined sort with a sort proposition. Sort propositions are built from the basic predicates p of the constraint domain. Index sorts serve as types for index objects, in which basic operations f of the constraint domain can appear. An index context is given as a collection of index propositions and type declarations for index variables.

DML type-checking requires a constraint solver that is able to handle constraints of the form

Φ ::= ⊤ ||| ⊥ ||| i = j ||| p(i) ||| Φ_{1} ∧ Φ_{2} ||| Φ_{1} ∨ Φ_{2} ||| ∀a: γ.Φ ||| ∃a: γ.Φ

Constraint satisfaction under a given index context, which is written as ϕ ⊧ Φ, is defined in the canonical way.

2.2.2 The language DML_{0}^{Π}(C)

A grammar of the DML_{0}^{Π}(C) syntax is given in Figure 4.

τ ::= δ(i) ||| 1 ||| (τ_{1} × τ_{2}) ||| (τ_{1} → τ_{2}) ||| Π a : γ . τ
e ::= x ||| ⟨⟩ ||| ⟨e_{1}, e_{2}⟩ ||| c[i_{1}] … [i_{n}] ||| c[i_{1}] … [i_{n}](e)

||| (case e of ms) ||| (lam x : τ . e) ||| e_{1}(e_{2}) ||| let x = e_{1} in e_{2} end ||| (fix x : τ.e) ||| (λa : γ . e) ||| e[i]

p ::= x ||| c[a_{1}] … [a_{n}] ||| c[a_{1}] … [a_{n}](p) ||| ⟨⟩ ||| ⟨p_{1}, p_{2}⟩
ms ::= p ⇒ e ||| p ⇒ e | ms

Figure 4: Syntax of DML_{0}^{Π}(C)

In the grammar of the type language, δ(i) stands for a data type δ that is indexed with index object i. The DML data-type declaration of an enriched data type δ(i) yields constructor types of form Π a_{1} : γ_{1}… Π a_{k} : γ_{k} . τ → δ(i) for constructors without argument such as nil, and Π a_{1} : γ_{1}… Π a_{k} : γ_{k} . τ → δ(i) for constructors with argument such as cons. Several examples of types appeared in Section 2.1.2.

In addition to the usual constructs, the term language provides abstraction over index variables (λa : γ . e) and application of an expression to an index object (e[i]). Furthermore, a constructor c of a recursive data type only appears with a number of index arguments—index variables when appearing in a pattern p and index objects otherwise. The number and sorts of index arguments is determined by the constructor type, which is inferred from the corresponding data type definition (see Section 2.1.2).

A typing judgment for DML_{0}^{Π}(C) has the form

ϕ; Γ ⊢ e: τ,

where ϕ is an index context and Γ a normal context; an overview over the typing rules for DML_{0}^{Π}(C) is presented in Appendix A.1.

Substitutions play a central role in the formalization of DML: They are used both in the definition of the typing system and the semantics (Appendix A.2). A substitution can both affect index variables and normal variables:

θ ::= [] ||| θ[a ↦ i] ||| θ[x ↦ e]

For a substitution θ, its restriction to index variables is referred to as θ_{ϕ}, its restriction to normal variables as θ_{Γ}.

The application of a substitution θ to a term t is written t[θ]. With θ_{1} ∘ θ_{2} we denote the substitution mapping t to (t[θ_{1}])[θ_{2}]; with θ_{1}θ_{2} we denote the substitution that behaves like θ_{1} on all variables in dom(θ_{1})\dom(θ_{2}), and like θ_{2} on all other variables.

3 Extracting cost recurrences

We first give an intuitive account of our method for extracting cost recurrences from DML programs, deferring a formal treatment to Section 4. We then present examples illustrating some distinctive features of the method.

3.1 The intuition behind extracting cost recurrences

We extract cost recurrences from first-order DML programs of the form

F_{1}:Π a_{0} : γ_{0}… Π a_{j_{1}} : γ_{j_{1}} . (ρ_{10} × ρ_{11} ⋯ × ρ_{1l_{1}}) → ρ_{1}

  fun F_{1}(x_{0},x_{1},. . .,x_{l_{1}}) = e_{1}

⋮ F_{k}:Π a_{0} : γ_{0}… Π a_{j_{k}} : γ_{j_{k}} . (ρ_{k0} × ρ_{k1} ⋯ × ρ_{kl_{k}}) → ρ_{k}

  fun F_{k}(x_{0},x_{1},. . .,x_{l_{k}}) = e_{k}

where we write ρ ::= δ(i) ||| 1 ||| (ρ_{1} × ρ_{2}) for first-order types; also data-type constructors are only allowed to take first-order arguments. Because indices are used to abstract from data to data size, we require that (1) all sorts γ have been constructed only with subsorts of ℕ and (2) data types are enriched such that for any i, all indices appearing in a branch of a data type δ(i) must be bounded.^{3}

We count cost in terms of the number of calls to user-defined functions F and to constructors c, assigning a cost of c_{F} and c_{c} for each call, respectively. c_{F} and c_{c} are constants of the domain in which cost is measured, e.g., the natural numbers.

The first step of extracting a cost recurrence from a DML program is type elaboration, which yields a DML_{0}^{Π}(ℤ) program.^{4}

Example For the append function from Figure 1, type elaboration yields the DML_{0}^{Π}(ℤ) program displayed in Figure 5. Type elaboration makes the indices explicit in the term language: index variables n_{1} and n_{2} are abstracted over; pattern matching against cons introduces a new index variable n′_{1}; cons and the recursive call of append are passed index objects that describe the length of the respective list arguments passed to cons and append. Because DML_{0}^{Π}(ℤ) is monomorphic, assume that the data type list has been defined for a fixed type of elements, say string. The constructors nil and cons then are typed as follows:

nil : list(0)
cons : Π n : ℕ . string × list(n) → list(n + 1)

fix append : Π n_{1} : ℕ . Π n_{2} : ℕ . list(n_{1}) × list(n_{2})
→ list(n_{1} + n_{2}).

λn_{1} : ℕ . λn_{2} : ℕ . lam lp : list(n_{1}) × list(n_{2}) .

case lp of

⟨nil, l_{2}⟩ ⇒ l_{2}
| ⟨cons[n′_{1}]⟨x, xs⟩, l_{2}⟩ ⇒
cons[n′_{1} + n_{2}]⟨x, append[n′_{1}][n_{2}]⟨xs, l_{2}⟩⟩

Figure 5: The append function in DML_{0}^{Π}(C)

We now describe intuitively how the extraction algorithm works. Note that all steps can be carried out automatically; for manipulating constraints, the algorithm uses a constraint solver for ℤ.

3More precisely speaking, every constructor type Π a_{1} : γ_{1}… Π a_{k} : γ_{k} . ρ → δ(i) must be such that for a fixed δ(i), there are only finitely many z_{1}, … z_{k} such that c[z_{1}] … [z_{k}] is of type ρ → δ(i). This condition is met for every data-type definition in which the indices convey size information: structures of a given size cannot contain substructures of arbitrary size.

4Because type elaboration as defined by Xi [12, Chapter 4] works on DML_{0}(C) programs, the program has to be rewritten in DML_{0}(ℤ). This is easily done by replacing the ML function-definition syntax with a recursive definition (keyword fix), a lambda-abstraction (keyword lam), and a case expression with a single pattern, and declaring F_{1} … F_{k} in a row of nested let-statements.

The type of each function determines the arguments of the corresponding recurrence equation. A function

F : Π a_{0} : γ_{0}… Π a_{l} : γ_{l} . ρ_{1} → ρ_{2}

gives rise to a recurrence equation F^{c} with a_{0} … a_{l} as formal parameters.

Example (cont.) For append, a recurrence equation append^{c} with formal parameters n_{1} and n_{2} is extracted.

The extraction algorithm works on the body of the function definitions. The issues that have to be dealt with are

1. How to treat case expressions?

2. How to treat index variables introduced by pattern matching?

3. How to assign and add up cost?

How to treat case expressions? To abstract from data to data size, we need to turn case expressions, which examine data, into conditionals that examine data size. Such a transformation can be achieved using information contained in the DML_{0}^{Π}(ℤ) type derivation: During type checking, constraints over the index objects in the program are collected in an index context. Consider a branch of a case expression over some type ρ. The type derivation contains a collection of constraints that have to be satisfied when entering the branch, i.e., when the pattern of the branch is matched. By projecting out these constraints over the index variables contained in ρ, i.e., eliminating all other index variables, a guard for the corresponding branch of a conditional can be derived.

Example (cont.) The case expression in append is type-checked under the index context

ϕ = n_{1} : ℕ, n_{2} : ℕ

For the two branches, additional constraints are generated:

• For the branch with pattern ⟨nil, l_{2}⟩, the index context n_{1} = 0 is generated.

• For the branch with pattern ⟨cons[n′_{1}]⟨x, xs⟩, l_{2}⟩, the index context n′_{1} : ℕ, n_{1} = n′_{1} + 1 is generated.

From the conjunction of ϕ and the newly generated index context of each branch, we can derive a condition in terms of n_{1} and n_{2} by projecting out over n_{1} and n_{2}: The result is n_{1} = 0 for the first branch and n_{1} > 0 for the second branch.

In general, it is possible that the generated guards overlap, even though the patterns of the case expression are mutually exclusive. When, during the evaluation of a recurrence equation, more than one guard is satisfied, all possible branches are evaluated and the maximum value is returned.

How to treat index variables introduced by pattern matching? A pattern can introduce new index variables; these index variables may appear within the branch guarded by the pattern, and thus also may play a role in the corresponding conditional branch of the extracted recurrence equation. Often, we can eliminate such index variables by deriving equality constraints that define a new index variable in terms of other index variables. If not, then the constraints can be used to derive a restriction for the values of the new index variables. This restriction is inserted into the extracted conditional branch.

Example (cont.) The second branch of the case expression in append introduces the new index variable n′_{1}. The constraints allow us to derive that n′_{1} = n_{1} − 1, so n′_{1} can be eliminated.

How to count and add up cost? When extracting a cost recurrence, we need to count every call to a user-defined function F with a cost of c_{F} and every use of a constructor c with a cost of c_{c}. Consider first a constructor c without arguments: In the cost recurrence, we simply replace c[i_{1}] … [i_{k}] with c_{c}. For constructors with arguments c[i_{1}] … [i_{k}](e) and function calls F [i_{1}] … [i_{k}](e), the cost incurred by e also needs to be taken into account. Hence, we first extract a recurrence-equation expression t that represents the cost of evaluating the argument, and then add it to the cost incurred by the function call:

• The total cost of c[i_{1}] … [i_{k}](e) is t + c_{c}

• The total cost of F [i_{1}] … [i_{k}](e) is t + c_{F} + (F^{c}i_{1} … i_{k}), where F^{c}i_{1} … i_{k} is a call to the cost recurrence extracted for F.

In our cost model, constants and variables can be accessed without cost, and therefore are turned into the constant 0 when extracting a cost recurrence.

Example (ended) We now assemble all the pieces of a cost recurrence for append. If we assign a cost of one unit to recursive calls of append and assume the use of cons to be cost free, then the cost of append is described by

append^{c} n_{1} n_{2} = \begin{cases}n_{1} = 0 → 0 \\ n_{1} > 0 → 1 + append^{c}(n_{1} − 1) n_{2} \end{cases}

(In the second branch, we have removed additions of zero that resulted from the variables x, xs and l_{2}, and the application of constructor cons.)

3.2 Example: Flattening a list of lists

The flatten function (see Figure 1) is an interesting problem for extracting a cost recurrence because of the choice of size measure for the input: The size of a list of lists is measured both in terms of the number of inner lists and the total number of elements contained in the inner lists.

We measure cost in terms of calls to user-defined functions. Our method yields the following cost recurrence:^{5}

flatten^{c} m n = \begin{cases}m = 0 ∧ n = 0 → 0 \\ m > 0 → 2 + append^{c} n_{1} n_{2} \\ + flatten^{c} (m − 1) n_{2} \end{cases}

where n_{1} + n_{2} = n

Here, a restriction n_{1} + n_{2} = n for the new variables n_{1} and n_{2} introduced by pattern matching has been inserted by the extraction algorithm—neither n_{1} nor n_{2} can be eliminated automatically.

Using the equation append^{c} n_{1} n_{2} = n_{1} derived in Section 3.1, we can rewrite the cost recurrence for flatten as

flatten^{c} m n = \begin{cases}m = 0 ∧ n = 0 → 0 \\ m > 0 → 2 + n_{1} \\ + flatten^{c} (m − 1) n_{2} \end{cases}

where n_{1} + n_{2} = n

It is easy to see that the maximal cost incurred by n_{1} in the second branch, added over all recursive calls, is n; all in all, we can approximate the cost of flatten as flatten^{c}(m, n) = 2m + n.

The size measure chosen here for a list of lists is intuitive and seems to be crucial for deriving a useful bound. Yet it is unclear how this measure could be be defined without the expressiveness offered by DML types, e.g., when using abstract-interpretation techniques [8].

3.3 Example: Searching a balanced tree

The occurs function (see Figure 1) provides an example of how two cost bounds in terms of different size measures can be obtained: one in terms of the height of a tree, and one in terms of the number of elements stored in a tree. The latter bound is obtained by reasoning with DML type guarantees—we profit from the fact that DML can express properties of the input that are not inferable from the code.

Our method yields the following cost recurrence for occurs:

occurs^{c} h s = \begin{cases}h = 0 ∧ s = 0 → 0 \\ h > 0 ∧ s > 0 → \begin{cases}0 \\ \{ & \begin{matrix}1 + occurs^{c} h_{1} s_{1} \\ 1 + occurs^{c} h_{2} s_{2} \end{matrix} \end{cases} \end{cases}

where h_{1} − 1 ≤ h_{2} ≤ h_{1} + 1
∧ max(h_{1}, h_{2}) + 1 = h
∧ s_{1} + s_{2} + 1 = s

5Here and in all the following recurrences we have simplified additions of constants.

(Each if expression gives rise to a guardless conditional, because no restrictions on indices can be inferred from its test expression.)

The recurrence looks more daunting than it is: It keeps track both of the height and the number of elements in the tree, but it is easy to see that the number of elements is of no consequence to the result of the cost recurrence. Approximating both h_{1} and h_{2} with h − 1 gives rise to a simple recurrence equation whose solution is occurs^{c}(h, s) = h.

The complication of eliminating size information could have been avoided by chosing a tree type which only keeps track of the height of a tree. Also keeping track of the number of elements, however, allows us to derive a cost measure in terms of the number of elements rather than the height of the tree. The crucial observation to make is that DML data-type definitions give rise to induction principles for proving relations among the indices of a data type. The definition of HBtree, for example, yields the following induction schema:

For R ∈ ℕ × ℕ, if

1. R(0, 0)

2. if for all h_{1}, h_{2}, s_{1}, s_{2} with h_{1} − 1 ≤ h_{2} ≤ h_{1} + 1, R(h_{1}, s_{1}) and

R(h_{2}, s_{2}) it follows that R(max(h_{1}, h_{2}) + 1, s_{1} + s_{2} + 1)

then whenever a value has type HBtree(h,s), the relation R(h, s)

holds.

Using this induction schema, one can show that s ≥ 2^{h} − 1 for any heightbalanced tree with height h and size s. Taking the logarithm, we see that h ≤ log(s + 1); combining this with the cost recurrence occurs^{c}(h, s) = h, we derive that the cost of occurs is logarithmic in s. This derivation is fully formal, i.e., based only on assumptions explicit in the types or the extracted recurrence.

3.4 Example: Merge sort

Merge sort provides an example of how the extraction algorithm preserves useful information contained in a program’s DML type.

An implementation of merge sort in DML is given in Figure 6 (adapted from the distribution of de Caml, a DML prototype [11]): Function initlist converts the list to be sorted into a list of lists such that each of these lists is sorted and has length two (apart from a possible last singleton list). Function merge2 goes through a list of lists, merging every two adjacent lists into one. Function mergeall iterates the application of merge2 until a single list is obtained. The types of initlist and merge2 capture the fact that the size measure that steers the recursion is continually halved—the index expression ⌈n/2⌉ can be encoded as div(n, 2) + mod(n, 2) in the integer constraint domain we are working with.

We extract cost recurrences (Figure 7a), this time counting the number of comparisons (counting calls to primitive functions works the same as counting calls to user-defined functions). The recurrences for merge^{c}, initlist^{c} and merge2^{c}(m, n) are easy to approximate, yielding a simplified set of recurrences

merge : Π n_{1}, n_{2} : ℕ . list(n_{1}) × list(n_{2}) → list(n_{1} + n_{2})

fun merge lp =
 case lp of
    (nil, l2) => l2
  | (l1, nil) => l1
  | (cons(h1,t1),cons(h2,t2)) =>
      if h1 < h2 then cons(h1,merge(t1,l2))
                 else cons(h2,merge(l1,t2))

initlist : Π n : ℕ . list(n) → llist(⌈n/2⌉,n)

fun initlist l =
 case l of
    nil => lnil
  | cons(_,nil) => lcons(l, lnil)
  | cons(e1,cons(e2, rest)) =>
      lcons(if e1 < e2
            then cons(e1,cons(e2,nil))
            else cons(e2,cons(e1,nil)),
            initlist rest)

merge2 : Π m, n : ℕ . llist(m,n) → llist(⌈m/2⌉,n)

fun merge2 ll =
 case ll of
    lnil => ll
  | lcons(_,lnil) => ll
  | lcons(l1,lcons(l2,rest)) =>
        lcons(merge(l1,l2),merge2 rest)

mergeall : Π m, n : ℕ . llist(m,n) → list(n)

mergeall ll =
 case ll of
    lnil => nil
  | lcons(l,lnil) => l
  | lcons(_,lcons(_,_)) => mergeall(merge2 ll)

msort : Π n : ℕ . list(n) → list(n)

msort l = mergeall(initlist l)

Figure 6: Merge sort in DML

displayed in Figure 7b. Notice how the information about halving the length of the list of lists captured in the type of merge2 appears in mergeall^{c} m n. The solution of this recurrence equation is well-known to be O(n log m), which gives an overall complexity for msort of O(n log n).

An extraction scheme without access to such high-level information as provided by DML types might still provide enough implicit information in the

merge^{c} n_{1} n_{2} = n_{1} = 0 → 0 n_{2} = 0 → 0

n_{1} > 0 ∧ n_{2} > 0 → 1 + \begin{cases}merge^{c} (n_{1} − 1) n_{2} \\ merge^{c} n_{1} (n_{2} − 1) \end{cases}

initlist^{c} n = n = 0 → 0 n = 1 → 0 n > 1 → 1 + initlist^{c} (n − 2)

merge2^{c} m n = m = 0 ∧ n = 0 → 0 m = 1 → 0 m > 1 → merge^{c} n_{1} n_{2} + merge2^{c} (m − 2) n_{3}

where n_{1} + n_{2} + n_{3} = n

mergeall^{c} m n = m = 0 ∧ n = 0 → 0 m = 1 → 0 m > 1 → merge2^{c} m n + mergeall^{c}(⌈m/2⌉) n

msort^{c} n = initlist^{c} n + mergeall^{c} (⌈n/2⌉) n

a: Extracted cost recurrences

merge^{c} n_{1} n_{2} = n_{1} + n_{2}

initlist^{c} n = ⌊n/2⌋

merge2^{c} m n = n

mergeall^{c} m n = \begin{cases}m ≤ 1 → 0 \\ m > 1 → n + mergeall^{c} (⌈m/2⌉) n \end{cases}

msort^{c} n = ⌊n/2⌋ + mergeall^{c} (⌈n/2⌉) n

b: Approximated cost recurrences

Figure 7: Cost recurrences for merge sort

extracted cost bound to derive the same bound, but the reasoning over the cost recurrence would be more involved. Basically, information about argument sizes that is encoded in the DML type and carried over into the cost recurrence with our method, would first have to be (re)proven for the cost bound.

4 Formal development

We now formally define the method for extracting cost recurrences from DML programs. The development is based on the theoretical view of DML presented in Section 2.2 and therefore only treats a monomorphic version of DML without existential types. Extending the development into a polymorphic setting is straightforward and has been omitted for the sake of conciseness. For simplicity, the formalization also does not treat mutual recursion. Extracting a cost bound from mutually recursive programs works exactly the same, but checking whether an extracted bound is indeed a recurrence becomes somewhat more tricky. For the latter, techniques such as presented in Xi’s latest work [14] could be used (see Section 5).

A first assessment shows that our method can also be extended to existential types in a straightforward way. Essentially, the application of a function that returns a value of existential type introduces a new index variable that can be treated in the same way as new index variables introduced by pattern matching.

We start by defining the first-order fragment of DML treated by our method. For this fragment, we introduce a cost measure using a monadic translation with a cost monad. After defining a language of recurrence equations, we present the extraction algorithm. We prove its correctness by showing that extraction, if successful, indeed yields an upper bound with respect to the cost model defined by the monadic translation.

4.1 A first-order fragment of DML

As pointed out in Section 3.1, the first step of extracting cost recurrences from a first-order DML_{0}(ℤ) program is type-elaboration, which results in a DML_{0}^{Π}(ℤ) program of the form given in Figure 8 (we abbreviate a row of abstractions over a_{0} : γ_{0}, … a_{l} : γ_{l} with λa⃗ : γ⃗, and ⟨x_{0}, ⟨x_{1}, …, ⟨x_{i−1}, x_{i}⟩⟩⟩ with ⟨x_{0}, …, x_{i}⟩). The extraction algorithm to be presented in Section 4.4 therefore operates on the language defined in Figure 8 (cf. the full language in Figure 4).

The original semantics of DML (see Appendix A.2) is defined as a natural semantics: e ⟶ v means that e evaluates under environment Θ to value v. The semantics has a rule ev-fix for unfolding fixed-point definitions to handle recursion. For the first-order fragment of DML with its restricted form of function definition and function application used here, it is convenient to define a semantics that handles recursion using an environment of function definitions. We define a modified semantics: e ⟶_{Θ} v means that e evaluates under environment Θ to value v, where Θ is a substitution mapping function names to their definitions. We show the following theorem:

Theorem 1 Let p be a program of the form given in Figure 8. Then p ⟶ v in the standard semantics iff p ⟶_{[]} v in the modified semantics.

The definition of the modified semantics and the proof of Theorem 1 are deferred to Appendix B.1. let F_{1} = fix F_{1} : Π a_{0} : γ_{0}… Π a_{l_{1}} : γ_{l_{1}} . ρ_{11} → ρ_{12}.

λa⃗ : γ⃗ . lam x : ρ_{11} . body

⋮

F_{k} = fix F_{k} : Π a_{0} : γ_{0}… Π a_{l_{k}} : γ_{l_{k}} . ρ_{k1} → ρ_{k2}.

λa⃗ : γ⃗ . lam x : ρ_{k1} . body

in e end

a: Def. of functions F_{1} … F_{k} in DML_{0}^{Π}(ℤ)
body ::= case x of ⟨x_{0}, …, x_{i_{k}}⟩ ⇒ e
e ::= x ||| ⟨⟩ ||| ⟨e_{1}, e_{2}⟩ ||| c[i_{1}] … [i_{n}] ||| c[i_{1}] … [i_{n}](e)

||| (case e of ms) ||| let x = e_{1} in e_{2} end ||| F_{i}[i_{1}] … [i_{n}](e)

p ::= x ||| c[a_{1}] … [a_{n}] ||| c[a_{1}] … [a_{n}](p) ||| ⟨⟩ ||| ⟨p_{1}, p_{2}⟩
ms ::= p ⇒ e ||| p ⇒ e | ms

b: Grammar of function bodies

Figure 8: A first-order fragment of DML_{0}^{Π}(ℤ)

4.2 Measuring cost of computation

One way of introducing a cost measure into functional programs is the monadic translation [6] with a cost monad. It is well-known that state can be added to a program by (1) performing a monadic translation with the state monad [10] and (2) taking the term model of the result, i.e., expanding the monadic constructs inserted by the translation to code. Similarly, using the cost monad instead of the state monad, we can transform a program such that a cost counter is maintained.

The cost monad pairs computations that result in a value of type τ with a second component of a type C that expresses the cost of the computation; all we need to know is that C is an ordered Abelian monoid^{6} (C, +, 0, ≤). We write C α as a type abbreviation for α×C. A call-by-value monadic translation with a cost monad that is based on C turns a function of type Π a_{0} : γ_{0}… Π a_{k} : γ_{k} . ρ_{1} → ρ_{2} into a function of type Π a_{0} : γ_{0}… Π a_{k} : γ_{k} . ρ_{1} → C ρ_{2}. The intended meaning is that the transformed function not only returns the result value, but also the cost of computing it.

The cost monad can be defined by specifying two language constructs, val^{C} and let^{C}, which a monadic translation inserts into a program text. The typing rule for val^{C} is

6In an ordered monoid, the ordering ≤ is compatible with the monoid’s operation, i.e., if a ≤ b then a + c ≤ b + c. Relevant examples of ordered monoids are (ℕ, +, 0, ≤) and (ℝ, +, 0, ≤).

ϕ; Γ ⊢ e: ρ

(ty-monadic-val)

ϕ; Γ ⊢ val^{C} e: C ρ

The construct val^{C} is used to inject a value v : ρ into C ρ as ⟨v, 0⟩—values do not require any computation and thus incur no cost. The typing rule for let^{C} is

ϕ; Γ ⊢ e_{1} : C ρ_{1} ϕ; Γ, x : ρ_{1} ⊢ e_{2} : C ρ_{2}

(ty-monadic-let)

ϕ; Γ ⊢ let^{C} x = e_{1} in e_{2} end : C ρ_{2}

In (let^{C} x = e_{1} in e_{2} end), the expression e_{1} is evaluated to a result v_{1} wrapped with a cost z_{1}. To calculate e_{2}, the unwrapped v_{1} is used, yielding ⟨v_{2}, z_{2}⟩. The final result of the let expression is ⟨v_{2}, z_{1} + z_{2}⟩.

The monadic translation provides only the infrastructure for tracking cost, but does not assign costs to any program constructs. This assignment of costs is done by inserting a monadic construct cost_{z} with typing rule

ϕ; Γ ⊢ e: C ρ z ∈ C

(ty-monadic-cost)

ϕ; Γ ⊢ cost_{z} e: C ρ

into the transformed program. cost_{z} is particular to the cost monad: It adds z to the cost component of the value it is applied to.

A cost-conscious version of a program, i.e., a program that keeps track of the cost incurred by calls to user-defined functions and uses of constructors, is generated as follows: We first perform a monadic translation of the program and then enclose (1) each application of a user-defined function F with cost_{c_{F}}, and (2) each application of a constructor c with cost_{c_{c}}.

Figure 9 displays the combined translation (·)^{∗} for function bodies. A program p of the form given in Figure 8 is translated into p^{∗} by applying the monadic translation to all function bodies and the body of the program, and changing every result type ρ_{l2} in the type annotation of the fixed-point definition to C ρ_{l2}. The cost-conscious version can easily be expressed in DML_{0}^{Π}(C): Figure 10 shows how to expand val^{C}, let^{C} and cost_{z}.

The following theorem shows that the cost translation is well-behaved:

Theorem 2 Let ·; · ⊢ p : ρ be derivable. Then

1. judgment ·; · ⊢ p^{∗} : C ρ is derivable.

2. p ⟶_{[]} v iff p^{∗} ⟶_{[]} ⟨v, z⟩ for some z ∈ C.

The proof is deferred to Appendix B.2.

4.3 A language of recurrence equations

The language of recurrence equations is based on the natural numbers part ℕ of the constraint domain ℤ and the cost domain C. Natural numbers and tuples thereof serve as abstractions of input size, and therefore are used as arguments of recurrence equations. The result of a recurrence equation represents cost of computation and is expressed in C.

x^{∗}  = val^{C} x
⟨⟩^{∗}  = val^{C} ⟨⟩
⟨e_{1}, e_{2}⟩^{∗}  = let^{C} x_{1} = e_{1}^{∗} in
let^{C} x_{2} = e_{2}^{∗}
in val^{C} ⟨x_{1}, x_{2}⟩ end
(c[i_{1}] … [i_{k}])^{∗}  = cost_{c_{c}} (val^{C} (c[i_{1}] … [i_{k}]))
(c[i_{1}] … [i_{k}](e))^{∗}  = let^{C} x = e^{∗}
in cost_{c_{c}} (val^{C} (c[i_{1}] … [i_{k}](x))) end
(case e of ms)^{∗}  = let^{C} x = e^{∗}
in case x of ms^{∗} end
(p ⇒ e | ms)^{∗}  = p ⇒ e^{∗} | ms^{∗}
(let x = e_{1} in e_{2} end)^{∗} = let^{C} x = e_{1}^{∗}
in e_{2}^{∗} end
(F [i_{1}] … [i_{k}](e))^{∗}  = let^{C} x = e^{∗}
in cost_{c_{c}} (F [i_{1}] … [i_{k}](x)) end

Figure 9: Monadic translation of function bodies

val^{C} e  ≡ ⟨e, 0⟩
let^{C} x = e_{1} ≡ case e_{1} of
in e_{2}  ⟨x, z_{1}⟩ ⇒ case e_{2} of
end  ⟨v, z_{2}⟩ ⇒ ⟨v, z_{1} + z_{2}⟩
cost_{z} e  ≡ case e of
⟨x, z′⟩ ⇒ ⟨x, z + z′⟩

Figure 10: Monadic constructs as syntactic sugar

4.3.1 Syntax and types

We describe a system of recurrence equations with the language given in Figure 11. Because we extract recurrences from programs that are not mutual recursive, neither is a system of recurrence equations, i.e., a body t_{l} may only contain recurrence-equation names F_{1}^{c} … F_{l}^{c}. Conditionals, which so far have been pretty printed, are introduced with the keyword cond followed by a number of branches. Within a branch, the first constraint Φ_{1} represents the guard of the branch, whereas the second constraint Φ_{2} represents a where-clause. The scope of the quantification (we write a⃗ : σ⃗ as shorthand for the quantification over variables a_{1} : σ_{1} … a_{k} : σ_{k}) extends both over Φ_{2} and the branch body t. For ∀a⃗ : σ⃗.Φ_{2} we require that for any interpretation of its free variables, there are only finitely many instantiations of a⃗ such that Φ_{2} is satisfied; this requirement is met for recurrence equations extracted from DML programs in which the data types are enriched in a sensible way as required in Section 3.1.

index types  σ ::= ℕ ||| 1 ||| σ_{1} × σ_{2}
types  ν ::= C ||| σ → ν
definitions  𝔈 ::= F_{1}^{c} a_{0} a_{1} … a_{l_{1}} = t_{1}
⋮
F_{k}^{c} a_{0} a_{1} … a_{l_{k}} = t_{k}
body  t ::= z ||| t_{1} + t_{2} ||| F^{c} i⃗ ||| (cond brs)
index objects i, j ::= a ||| f(i) ||| ⟨⟩ ||| ⟨i, j⟩ ||| fst(i) ||| snd(i)
branches  brs ::= br ||| br | brs
branch  br ::= (Φ_{1} → ∀a⃗ : σ⃗.Φ_{2} → t)

Figure 11: Syntax of recurrence equations

The rationale behind the shape of recurrence equation types is that for a function F_{l} of type

Π a_{0} : γ_{0} . Π a_{1} : γ_{1}… Π a_{k} : γ_{k} . ρ_{1} → ρ_{2},

the associated cost recurrence F_{l}^{c} should have type

γ̃_{0} → γ̃_{1} → … γ̃_{k} → C,

where ˜ · maps an index sort to the associated index type. For example {a : ℕ × ℕ | fst(a) ≤ snd(a)} is mapped to ℕ × ℕ.

The formal definition of ˜ · and its extension to contexts Γ is deferred to Appendix B.3.1.

The body of a recurrence equation F_{k}^{c} is typed using the judgment

φ; Δ ⊢ e: ν

in which φ maps index types σ to index variables, and Δ assigns recurrenceequation types to function names. Figure 12 gives typing rules, all of which are straightforward. So are the rules for checking the type of an index object (φ ⊢ i : σ) and the wellformedness of a constraint (φ ⊢ Φ), which have been omitted.

Based on the typing rules for the body of a recurrence equation, we define what it means for a system of recurrence equations to be well-typed with respect to the program they have been extracted from.

Definition 3 Let p be a program and context Γ assign every F_{l} defined in p to its declared type. A system of recurrence equations 𝔈 is well-typed with respect to p if for every

F : Π a_{0} : γ_{0} . Π a_{1} : γ_{1}… Π a_{k} : γ_{k} . ρ_{1} → ρ_{2}

defined in p , for the extracted recurrence equation

F^{c} a_{0} … a_{k} = t

we have

a_{0} : γ̃_{0}, …, a_{k} : γ̃_{k}; Γ̃ ⊢ t: C.

(ty-re-const)

φ; Δ ⊢ z : C

φ; Δ ⊢ e_{1} : C φ; Δ ⊢ e_{2} : C

(ty-re-plus)

φ; Δ ⊢ e_{1} + e_{2} : C

\begin{matrix}Δ(F) = σ_{0} → … → σ_{k} → C \\ φ ⊢ i_{0} : σ_{0} … φ ⊢ i_{k} : σ_{k} \end{matrix}

\overline{(ty-re-app)}

φ; Δ ⊢ F^{c} i_{0} … i_{k} : C

φ ⊢ Φ_{11} φ, a⃗_{1} : σ⃗_{1} ⊢ Φ_{12} φ, a⃗_{1} : σ⃗_{1}; Δ ⊢ e_{1} : C

⋮

φ ⊢ Φ_{k1} φ, a⃗_{k} : σ⃗_{k} ⊢ Φ_{k2} φ, a⃗_{k} : σ⃗_{k}; Δ ⊢ e_{k} : C (ty-re-cond)

φ; Δ ⊢ (cond Φ_{11} → ∀a⃗_{1} : σ⃗_{1}.Φ_{12} → e_{1}
⋮
| Φ_{k1} → ∀a⃗_{k} : σ⃗_{k}.Φ_{k2} → e_{k}) : C

Figure 12: Typing rules for recurrence equations

4.3.2 Semantics

We give a simple denotational semantics to the language of recurrence equations. A recurrence equation defining a function of type

σ_{0} → σ_{1} → … σ_{k} → C

is interpreted in the function domain

[I[[σ_{0}]] → I[[σ_{1}]] → … I[[σ_{k}]] → C_{⊥}].

(Because all I[[σ_{l}]] are discrete cpos, such functions are necessarily continuous).

Here I[[·]] is the canonical semantics given to ground index objects i and index types σ by the constraint domain ℤ; for an index substitution θ that maps index

T [[z]]Ψθ = ⌞z⌟
T [[t_{1} + t_{2}]]Ψθ = T [[t_{1}]]Ψθ +_{⊥} T [[t_{2}]]Ψθ
T [[F_{l}^{c} i_{0} … i_{k}]]Ψθ = Ψ(F_{l}^{c}) (I[[i_{0}[θ]]]) … (I[[i_{k}[θ]]])
T [[cond br_{0} | … | br_{k}]]Ψθ = max_{⊥}{B[[br_{0}]]Ψθ, …, B[[br_{k}]]Ψθ}

B[[(Φ_{1} → ∀a⃗ : σ⃗.Φ_{2} → t)]]Ψθ = \begin{cases}⌞0⌟ if |̸= Φ_{1}[θ] \\ max_{⊥}\{T [[t]]Ψθ[a⃗ ↦ z⃗] | \\ z⃗ ∈ I[[σ⃗]] ∧ Φ_{2}[θ[a⃗ ↦ z⃗]]\} \\ if ⊧ Φ_{1}[θ] \end{cases}

Figure 13: Semantics of recurrence equations

variables to ground index objects, we write I[[θ]] for the corresponding mapping into ℤ. With C_{⊥} we denote the domain that results from interpreting C as a discrete domain and lifting it in the canonical way—in the semantics definition we also mark operations on C that have been lifted in the canonical way by subscripting them with ⊥.

Figure 13 gives a semantics T [[·]]Ψθ for recurrence-equation expressions, where Ψ is a mapping from recurrence-equation names to functions and θ an index substitution that maps index variables to ground index objects. The semantics treats a conditional by taking the maximum of the values returned by the branches of the conditional. If the guard of a branch does not hold, the branch returns 0. Otherwise, all possible values for the universally quantified index variables in the branch are tried out and the maximum is returned. Because, as required in Section 4.3.1, there is at most a finite number of such values, the semantics of a branch is well-defined (we assume that max_{⊥}∅ = ⌞0⌟).

Given the definition of a recurrence equation

F^{c}a_{0} a_{1} … a_{k} = t

and a mapping Ψ that ranges over all names of recurrence-equations declared previously to F^{c} (recall that we do not consider mutually recursive systems of recurrence equations), then the semantics of the defined function is the fixed point of the functional

λF.λn_{0} n_{1} … n_{k}.T [[t]](Ψ[F^{c} ↦ F])[a_{0}, …, a_{k} ↦ n_{0}, … n_{k}].

This semantics of a single recurrence equation extends naturally to a system 𝔈 of recurrence equations and yields a mapping from recurrence-equation names to functions; we write S[[𝔈]].

4.4 The extraction algorithm

We extract cost recurrences from DML_{0}^{Π}(ℤ) type derivations. A DML_{0}^{Π}(ℤ) typing judgment is of the form

ϕ; Γ ⊢ e: τ,

where ϕ is an index context and Γ is a variable context (see Appendix A.1 for details). The central part of the extraction algorithm operates on the type derivations for the bodies of function definitions F_{1} … F_{n}: From an expression e of first-order type that occurs within the body of a function definition, a recurrence-equation expression t of type C is extracted. The algorithm is defined in form of a judgment

ϕ; Γ ⊢ e: ρ ▶ t.

Consider the following definition of a function F (see Figure 8):

let F = fix F : Π a_{0} : γ_{0}… Π a_{l} : γ_{l} . ρ_{1} → ρ_{2}.
λa⃗ : γ⃗ . lam x : ρ_{1} . case x of ⟨x_{0}, …, x_{k}⟩ ⇒ e

Assuming that e is typed as ϕ; Γ ⊢ e : ρ_{2}, the extracted recurrence equation is F^{c} a_{0} … a_{l} = t, where t results from ϕ; Γ ⊢ e : ρ_{2} ▶ t.

Before we give a complete description of the extraction of cost recurrences, we examine how an index context can be turned into a constraint over the declared index variables.

4.4.1 Turning an index context into a constraint

DML_{0}^{Π}(ℤ) expressions are typed under a “normal” context and an index context of form

ϕ ::= · ||| ϕ, a : γ ||| ϕ, P

(See Figure 3). Basically, the index context collects constraints over index variables. It is straightforward to define a function C that rewrites an index context ϕ into a constraint Φ such that sort definitions are “flattened out”, i.e.,

C(a : {k : ℕ | k > 0}, b : {k : {k′ : ℕ | k′ > 1} | k ≥ a}) = a > 0 ∧ b > 1 ∧ b ≥ a

A precise definition of C is deferred to Appendix B.3.2.

A useful operation over constraints is to project out a certain set of variables, i.e., “hide” all remaining variables by existential quantification. We write ∃a⃗.Φ for the constraint that results from existentially quantifying over the variables a⃗ in Φ. With a constraint solver such as used for DML type-checking, existentially quantified variables usually are simplified away.

Often equalities can be derived from a constraint Φ. Let a⃗ be a subset of the free variables in Φ; we define a substitution θ := mk subst a⃗(Φ) as follows: For all a ∈ a⃗ such that i is an index expression without free variables in a⃗, and a = i can be derived from Φ, we have θ(a) = i.

ϕ; Γ ⊢ e: τ_{1} ▶ t ϕ ⊧ τ_{1} ≡ τ_{2}
\overline{(extr-eq)}
ϕ; Γ ⊢ e: τ_{2} ▶ t
\overline{(extr-var)}

ϕ; Γ ⊢ x: τ ▶ 0

\overline{(extr-unit)}
ϕ; Γ ⊢ ⟨⟩: 1 ▶ 0

ϕ; Γ ⊢ e_{1} : τ_{1} ▶ t_{1} ϕ; Γ ⊢ e_{2} : τ_{2} ▶ t_{2}

\overline{(extr-pair)}

ϕ; Γ ⊢ ⟨e_{1}, e_{2}⟩: τ_{1} × τ_{2} ▶ t_{1} + t_{2}

ϕ; Γ ⊢ e_{1} : ρ_{1} ▶ t_{1} ϕ; Γ, x : ρ_{1} ⊢ e_{2} : ρ_{2} ▶ t_{2}

\overline{(extr-let)}

ϕ; Γ ⊢ let x = e_{1} in e_{2} end : ρ_{2} ▶ t_{1} + t_{2}

ϕ; Γ ⊢ e: ρ_{1} ▶ t
\overline{(extr-app)}

ϕ; Γ ⊢ F [i_{1}] … [i_{k}](e) : ρ_{2} ▶ t + c_{F} + (F^{c}i_{1} … i_{k})

(ty-cons-wo)

ϕ; Γ ⊢ c[i_{1}] … [i_{n}] : ρ ▶ c_{c}

ϕ; Γ ⊢ e: τ ▶ t

\overline{(ty-cons-w)}

ϕ; Γ ⊢ c[i_{1}] … [i_{n}](e) : ρ ▶ t + c_{c}

ϕ; Γ ⊢ e: ρ′ ▶ t

ϕ; Γ ⊢ (p_{0} ⇒ e_{0}) : ρ′ ⇒ ρ ▶ br_{1}

⋮

ϕ; Γ ⊢ (p_{k} ⇒ e_{k}) : ρ′ ⇒ ρ ▶ br_{k} \overline{(ty-case)}

ϕ; Γ ⊢ (case e of p_{0} ⇒ e_{0} | … | p_{k} ⇒ e_{k}) : ρ

▶ t + (cond br_{1} | br_{2} | … | br_{k})

p ↓ ρ′ ▷ (ϕ′; Γ′) ϕ, ϕ′; Γ, Γ′ ⊢ e: ρ ▶ t Φ_{1} = ∃(dom(ϕ, ϕ′)\var(ρ′)).C(ϕ, ϕ′) θ = mk subst_{dom(ϕ′)}(C(ϕ′)) Φ_{2} = ∃(dom(θ)).C(ϕ′)

\overline{(ty-branch)}

ϕ; Γ ⊢ (p ⇒ e) : ρ′ ⇒ ρ

▶ Φ_{1} → ∀(dom(ϕ′)\dom(θ)).Φ_{2} → t[θ]

Figure 14: Extraction algorithm 4.4.2 Definition of the extraction algorithm

The definition of the judgment ϕ; Γ ⊢ e: ρ ▶ t is given in Figure 14. Most rules are fairly straightforward:

• Accessing a variable or the unit value has no cost.

• For pairs and let expressions, the total cost is the sum of the costs incurred by their subexpressions.

• The cost of executing a user-defined function F has three components: the cost of evaluating its argument, the cost c_{F} of calling the function, and the cost incurred by evaluating the function. For the latter component, a recursive call with the appropriate arguments is generated.

• The use of a constructor c costs c_{c} plus the cost of evaluating a possible argument.

A case expression is handled by converting it into a conditional. The real heart of the algorithm is the rule that handles branches of case expressions. This rule extracts a conditional branch from a type derivation for

ϕ; Γ ⊢ (p ⇒ e) : ρ′ ⇒ ρ.

This judgment types the branch of a case expression that matches a pattern p against a value of type ρ′; the expression e in the branch has the same type ρ as the total case expression. We go through the premises of the corresponding extraction rule one by one:

1. The judgment p ↓ ρ′ ▷ (ϕ′; Γ′) (see Figure 16 on page 34) is defined as part of the DML_{0}^{Π}(C) type-checking rules. It generates an index context ϕ′ and a variable context Γ′ that describe the index variables and normal variables occurring in the pattern p.

For example, after translation into DML_{0}^{Π}(ℤ), the pattern of the second branch in flatten (Section 3.2) is lcons[m′][n_{1}][n_{2}]⟨xs, rest⟩; typechecking under index context ϕ = m : ℕ, n : ℕ generates the following index context:

ϕ′ = m′ : ℕ, n_{1} : ℕ, n_{2} : ℕ, m = m′ + 1, n = n_{1} + n_{2}.

2. DML_{0}^{Π}(C) type-checking types the branch expression under the contexts ϕ, ϕ′ and Γ, Γ′. From the resulting type derivation, a recurrence-equation expression t is extracted.

For the second branch of flatten, this yields

t = 2 + (append^{c} n_{1} n_{2}) + (flatten^{c} m′ n_{2})

3. The guard of the branch Φ_{1} is derived by projecting out from C(ϕ, ϕ′) over the index variables contained in ρ′.

In flatten, the only index variable in ρ′ = llist(m,n) are m and n; projecting them out yields m > 0. For n there is no information, because we only know that n ∈ ℕ, and (as pointed out in Section 3.1) we require all indices to be of subsorts of ℕ anyways.

4. All index variables declared in ϕ′ that can be expressed in terms of index variables from ϕ should be are eliminated using substitution θ: In the branch returned by the rule, the body is t[θ] rather than t.

For the second branch of flatten, we can infer that m′ = m − 1, so θ = [m′ ↦ m − 1].

5. Index variables declared in ϕ′ for which no equality constraint can be derived have to be restricted. This is done by (1) hiding the variables dom(θ) via existential quantification in C(ϕ′), and (2) universally quantifying over the remaining variables of dom(ϕ′), binding variables both in Φ_{2} and in t[θ]. Conjuncts in Φ_{2} containing none of the universally quantified variables can be dropped (such conjuncts are guaranteed to be satisfied whenever Φ_{1} is satisfied).

For the second branch of flatten, existential quantification over m′ in ϕ′ yields, after normalization, m > 0 ∧ n = n_{1} + n_{2}. We universally quantify over n_{1} and n_{2}, and drop the conjunct m > 0.

To complete the running example: The second branch of flatten gives rise to the following branch of the conditional in flatten^{c}:

m > 0 → ∀n_{1}, n_{2} : ℕ.n_{1} + n_{2} = n →
2 + (append^{c} n_{1} n_{2}) + (flatten^{c} (m − 1) n_{2})

4.4.3 Checking whether the bound is a recurrence

It remains to check whether we really extract a recurrence, i.e., a function defined in terms of its value on smaller arguments. For the presented language without mutual recursion (for handling mutual recursion, Xi’s most recent work [14] could be adapted—see Section 5), this can be conveniently done during extraction when generating a recursive call F^{c} i_{1} … i_{k} inside the body that defines F^{c} a_{1} … a_{k}: The extraction yields a recurrence if for every such call,

⟨i_{1}, …, i_{n}⟩ < ⟨a_{1}, …, a_{n}⟩

can be derived from the collected constraints for a well-founded order < on tuples. In practice, one could for example fix the usual lexicographic ordering, requiring the user to enrich data correspondingly, or leave the user a choice as to which ordering should be used.

4.4.4 Correctness

Theorem 4 Let functions F_{1}, …, F_{k} be a well-typed block of function definitions. Let 𝔈 be the system of recurrence equations for F_{1}^{c}, …, F_{k}^{c} extracted from these definitions. Let p be a well-typed program consisting of these function definitions F_{1}, …, F_{k} and a program body F_{l}[z_{1}] … [z_{l′}](u), where z_{1}, …, z_{l′} are ground index objects and u is a value. Then:

1. 𝔈 is well-typed with respect to p.

2. If T [[F_{l}^{c} z_{1} … z_{l′}]](S[[𝔈]])[] = ⌞z′⌟ for some z′ ∈ C, then there exists a value v and a z ∈ C with z ≤ z′ such that p^{∗} evaluates to ⟨v, z⟩.

3. If the test described in Section 4.4.3 has been performed during the extraction of 𝔈, then the denotation of F_{l}^{c}z_{1} … z_{k} under environment S[[𝔈]] is guaranteed to yield ⌞z′⌟ for some z′ ∈ C rather than ⊥.

Part 1 and 3 of the theorem capture that the extracted system of cost bounds is well-formed: The system is well-typed, and the application of a bound F_{l}^{c}, to some legal input z_{1}, … z_{l} (legal in the sense that F_{l}[z_{1}] … [z_{l}](u) type-checks for some u) is well-defined. Because the translation (·)^{∗} (see Section 4.2) captures our cost model—in the translated program, a cost counter z is calculated together with the actual result—part 2 states that this bound indeed is a cost bound for the execution of F_{l}[z_{1}] … [z_{l}](u). The proof of Theorem 4 is deferred to Appendix B.4.

5 Related work

We discuss related work regarding automated complexity analysis and type systems.

Le Métayer’s ACE system [4] automatically extracts cost bounds for a subset of FP, expressing the extracted bounds as FP programs. The system is based on program transformation. The first step transforms the original program into a step-counting version, i.e., a program that takes the same arguments, but returns the cost of computation for these arguments rather than the result. Conceptually, this transformation corresponds to a monadic translation with the cost monad as presented in Section 4.2, where the cost component is projected out from the final result. Subsequent transformation steps try to transform the step-counting version into a composition of a cost bound and a measure function, where the measure function is composed from selector functions and the length function for lists. The principal goal of the ACE system is to eliminate recursion in the cost bound, which corresponds to solving recurrences; the system’s library holds more than 1000 transformation rules, many of them tailored to recognize patterns of recursion. The process of finding a measure function is interleaved with the process of eliminating recursion and cannot easily be decoupled. Pointing the system to a given measure thus seems difficult. In contrast, our method separates concerns: The user can specify an appropriate measure using dependent types, but no attempts are made to solve the extracted cost recurrence.

Sands [9] treats cost analysis for higher-order call-by-name languages: Cost bounds are extracted by program transformation and reasoning over programs; his method can be seen as an extension of Le Métayer’s overall approach. Sands focuses on the complications for cost analysis caused by higher-order functions and call-by-name evaluation. No special concern is given to the abstraction of data to data size, which is the main concern of our work.

Rosendahl [8] develops a system that uses abstract interpretation and program transformation techniques to extract cost bounds from a first-order subset of Scheme. An abstract interpretation is used to extend the set of S-expressions with partially known structures—unknown parts of a structure are represented by a special token that stand for all possible structures. Size measures are expressed through “inverse size functions”: For a given size, an inverse size function returns a partially known structure that approximates all data structures of that size. For example, for lists, the inverse size function generates for size n a list containing n times the special token representing all possible structures. An initial cost bound for a program is achieved by (1) composing a suitable inverse size function with the abstract interpretation of the step-counting version of the program and (2) taking the term model. Program transformation is then used to simplify this initial cost bound as much as possible. Liu and Gómez [5] propose a method based on Rosendahl’s work in which they use advanced program-transformation techniques to make the cost bound more efficient and more accurate. Both methods requires the user to define the abstraction from data to data size. However, with dependent types, measures can be expressed that are impossible to define with an inverse size function—the measure used in Section 3.2 for analyzing flatten is one example.

Reistad and Gifford [7] use an effect type system for automatically inferring cost estimates of functional programs written with combinators such as map and fold. Two indexed data-types, lists and vectors, are built into the type system. The effects associated with function types are cost expressions that may depend on indices of list/vector arguments and on cost expressions associated with function arguments. The main focus of Reistad and Gifford is to guide parallelization of programs with the inferred cost estimates.

Crary and Weirich [3] present a decidable type system for the specification and certification of resource consumption in the setting of Typed Assembly Language. The type system simulates dependent types using sum and inductive kinds. Essentially, it allows the user to annotate function arrows with resource bounds (e.g., time bounds or space bounds) in terms of the shape of data arguments and of cost bounds associated with function arguments. The focus lies on the certification of resource bounds through type checking rather than the derivation of resource bounds.

Chin and Khoo [2] propose sized types in which size information is expressed with Presburger formulas. They use a a constraint solver to infer size information. It is very likely that complexity analysis in the style of this paper could be integrated into their setting.

Recently, Xi [14] presented an extension of the DML type system that allows program termination verification. The basic observation is the same as for our work, namely that DML types can be used to encode a notion of input size. For each function, the programmer supplies a metric in terms of the input indices; if type checking succeeds, the metrics are guaranteed to specify a termination order. Both higher-order functions and general recursion are handled. We believe that our work would benefit substantially from reformulating it in this extended type system: As an immediate benefit, extracted cost bounds could be easily verified to be recurrences also for general recursion. Also an extension of this work to higher-order functions, if possible, should be easier within Xi’s new type system, though of course our work handles defunctionalized programs (à la Reynolds) and thus, indirectly, higher-order functions.

6 Conclusion

We have presented a method for automatically extracting cost recurrences from first-order DML programs. The distinct feature of our method is the use of dependent types to describe a size measure that abstracts from data to data size. The user has to choose an appropriate size measure for our method to successfully extract a cost recurrence. Because of the high expressiveness of its types, DML offers high flexibility for tailoring size measures. The required DML type annotations usually are easy to find: Because size measures encode shape information of data types, they closely correspond to the programmer’s intuitive understanding of how his program works. Our method harnesses this intuition for automatic cost analysis.

Acknowledgments I am indebted to Olivier Danvy, Julia Lawall and Zhe Yang for their encouragement and fruitful discussions on the subject of this work. Further thanks are due to Olivier Danvy, Andrzej Filinski and Julia Lawall for their numerous constructive comments. I am also grateful to the anonymous referees and Neil Jones for further comments.

References

[1] Lennart Augustsson. Cayenne—a language with dependent types. In Paul Hudak and Christian Queinnec, editors, Proceedings of ICFP’98, pages 239–250, Baltimore, Maryland, September 1998. ACM Press.

[2] Wei-Ngan Chin and Siau-Cheng Khoo. Calculating sized types. Higher-Order and Symbolic Computation, 14(2/3), 2001. To appear.

[3] Karl Crary and Stephanie Weirich. Resource bound certification. In Thomas Reps, editor, Proceedings of POPL’00, pages 184–198, Boston Massachusetts, January 2000. ACM Press.

[4] Daniel Le Métayer. ACE: An automatic complexity evaluator. ACM Transactions on Programming Languages and Systems, 10(2):248–266, April 1988.

[5] Yanhong Annie Liu and Gustavo Gómez. Automatic accurate time-bound analysis for high-level languages. In Frank Mueller and Azer Bestavros, editors, Proceedings of the ACM SIGPLAN 1998 Workshop on Languages, Compilers, and Tools for Embedded Systems (LCTES), number 1474 in LNCS, pages 31–40, Montréal, Canada, June 1998. Springer-Verlag.

[6] Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science, pages 14–23, Pacific Grove, California, June 1989. IEEE Computer Society Press.

[7] Brian Reistad and David K. Gifford. Static dependent costs for estimating program execution time. In Carolyn L. Talcott, editor, Proceedings of LFP’94, LISP Pointers, Vol. VII, No. 3, Orlando, Florida, June 94. ACM Press.

[8] Mads Rosendahl. Automatic complexity analysis. In Joseph E. Stoy, editor, Proceedings of the Conference on Functional Programming Languages and Computer Architecture ’89, pages 144–156, London, September 1989. ACM Press.

[9] David Sands. Calculi for Time Analysis of Functional Programs. PhD thesis, Department of Computing, Imperial College, University of London, September 1990.

[10] Philip Wadler. The essence of functional programming. In Andrew W. Appel, editor, Proceedings of POPL’92, pages 1–14, Albuquerque, New Mexico, January 1992. ACM Press.

[11] Hongwei Xi. de Caml. A prototype implementation of DML, based on

Caml-light. Available from http://www.ececs.uc.edu/~hwxi/DML/DML.
html.

[12] Hongwei Xi. Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, 1998.

[13] Hongwei Xi. Dependently typed data structures. In Chris Okasaki, editor, Proceedings of Workshop of Algorithmic Aspects of Advanced Programming Languages (WAAAPL ’99), pages 17–32, Paris, September 1999. Available

from http://www.cs.columbia.edu/~cdo/waaapl99.pdf.

[14] Hongwei Xi. Dependent types for program termination verification. In Proceedings of 16th IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, June 2001. IEEE Computer Society Press.

[15] Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Keith D. Cooper, editor, Proceedings of PLDI’98, pages 249–257, Montreal, June 1998. ACM Press.

[16] Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Alex Aiken, editor, Proceedings of POPL’99, pages 214–227, San Antonio, Texas, January 1999. ACM Press.

A DML

In the following we give a short overview over the formalization of DML_{0}^{Π}(C) that is used in this article. We gloss over details such as type-formation rules, well-formedness of contexts, and type-equivalence. The complete formalization can be found in Xi’s PhD thesis [12, Chapters 2–4].

A.1 DML typing rules

A typing judgment for DML_{0}^{Π}(C) has the form

ϕ; Γ ⊢ e: τ,

where ϕ is an index context and Γ a (normal) context; typing is with respect to a signature S that assigns types to constructors. In the following, we focus on typing rules that treat indices—the remaining rules are fairly standard.

The treatment of indices is based on a judgment ϕ ⊢ i : γ that expresses that i : γ can be derived from the index context ϕ; to establish this judgment, constraint solving is required. The judgment is used, for example, to express type-soundness of an index substitution θ under a context ϕ as ϕ ⊢ θ : ϕ′ (Figure 15a), which basically says that, assuming the context given by ϕ substitution θ assigns to all index variables declared in ϕ′ an index object of the declared sort. The following lemma [12, Chapter 3] shows a useful link between typesoundness with respect to an index context ϕ and satisfyability with respect to ϕ:

Lemma 5 Let ϕ and ϕ′ be index contexts and θ an index substitution such that ϕ ⊢ θ : ϕ′ is derivable. Then, if ϕ, ϕ′ ⊧ Φ is derivable, also ϕ ⊧ Φ[θ] is derivable.

Figure 15b defines a corresponding judgment for general substitutions; it is straightforward to show that if ϕ; Γ ⊢ θ : (ϕ′; Γ′) holds for a substitution θ, then ϕ ⊢ θ_{ϕ} : ϕ′ holds for its restriction θ_{ϕ} to index variables.

Figure 16 and Figure 17 on page 36 display the typing rules for DML_{0}^{Π}(C). The judgment p ↓ τ ▷ (ϕ; Γ) defined in Figure 16 on the following page is used for typing pattern matching over an expression of type τ: Type information about variables and index variables occurring in pattern p is gathered. Figure 17 on page 36 defines the “top-level” typing judgment ϕ; Γ ⊢ e : τ for DML_{0}^{Π}(C). The rule for type equality ty-eq uses a judgment ϕ ⊧ τ_{1} ≡ τ_{2} that is defined as

(isubst-empty)

ϕ ⊢ [] : ·

ϕ ⊢ θ : ϕ′ ϕ ⊢ i : γ[θ]

(isubst-ivar)

ϕ ⊢ θ[a ↦ i] : ϕ′, a : γ ϕ ⊢ θ : ϕ′ ϕ ⊧ P [θ]

(subst-iprop)

ϕ ⊢ θ : ϕ′, P

a: Type-soundness of an index substitution

(subst-empty)

ϕ; Γ ⊢ [] : (·; ·)

ϕ; Γ ⊢ θ : (ϕ′; Γ′) ϕ; Γ ⊢ e: τ[θ]

\overline{(subst-var)}

ϕ; Γ ⊢ θ[x ↦ e] : (ϕ′; Γ′, x : τ) ϕ; Γ ⊢ θ : (ϕ′; Γ′) ϕ ⊢ i : γ[θ]

(subst-ivar)

ϕ; Γ ⊢ θ[a ↦ i] : (ϕ′, a : γ; Γ′) ϕ; Γ ⊢ θ : (ϕ′; Γ′) ϕ ⊧ P [θ]

(subst-iprop)

ϕ; Γ ⊢ θ : (ϕ′, P; Γ′) b: Type-soundness of a substitution (general) Figure 15: Type-soundness of a substitution

\overline{(pat-var)} ; x ↓ τ ▷ (·; x : τ) \overline{(pat-unit)} ; ⟨⟩ ↓ 1 ▷ (·; ·)

p_{1} ↓ τ_{1} ▷ (ϕ_{1}; Γ_{1}) p_{2} ↓ τ_{2} ▷ (ϕ_{2}; Γ_{2})

\overline{(pat-prod)}

⟨p_{1}, p_{2}⟩ ↓ τ_{1} × τ_{2} ▷ (ϕ_{1}, ϕ_{2}; Γ_{1}, Γ_{2}) S(c) = Π a_{1} : γ_{1}… Π a_{k} : γ_{k} . δ(i)

(pat-cons-wo)

c[a_{1}] … [a_{k}] ↓ δ(j) ▷ (a_{1} : γ_{1}, …, a_{k} : γ_{k}, i = j; ·) S(c) = Π a_{1} : γ_{1}… Π a_{k} : γ_{k} . τ → δ(i) p ↓ τ ▷ (ϕ; Γ)

(pat-cons-w)

c[a_{1}] … [a_{k}](p) ↓ δ(j) ▷ (a_{1} : γ_{1}, …, a_{k} : γ_{k}, i = j, ϕ; Γ) Figure 16: Typing rules for patterns in DML_{0}^{Π}(C) the congruent extension of ϕ ⊧ i = j from index objects to types. The rules ty-cons-wo, ty-cons-w and ty-iapp, for constructors and application to an index object, respectively, examine whether index objects are indeed of the required sort; when typing a constructor, the judgment for establishing type soundness of index substitutions is used to account for possible sequential dependencies among the sorts pertaining to the arguments of the constructor.

The following theorem [12, Chapter 4] shows that types are preserved under a type-sound substitution.

Theorem 6 (Substitution) If ϕ, ϕ′; Γ, Γ′ ⊢ e: τ and ϕ; Γ ⊢ θ : (ϕ′; Γ′) are derivable, then ϕ; Γ ⊢ e[θ] : τ[θ] is derivable.

A.2 DML semantics

Figure 18 on page 37 describes a natural semantics for DML_{0}^{Π}(C): e ⟶ v means that e reduces to a value v, where

v ::= c[i_{1}] … [i_{k}] ||| c[i_{1}] … [i_{k}](v) ||| ⟨⟩ ||| ⟨v_{1}, v_{2}⟩ ||| (lam x : τ . e) ||| (λa : γ . v).

Notice that type indices are never evaluated. The language design decision is that there is no direct interaction between indices and code execution; type indices are used only for type-checking.

The rule that describes the semantics of a case expression makes use of a judgment match(v, p) ⟹ θ defined in Figure 19 on page 38: If a value v matches a pattern p, a substitution for the free variables in p is returned. Notice that the semantics of case expressions is nondeterministic: an arbitrary matching arm is picked.

Xi [12, Chapter 4] proves the following theorem connecting the type system and the semantics:

Theorem 7 (Relating types and semantics) 1. Assume that there is no a ∈ dom(ϕ) that occurs in pattern p. If ϕ; Γ⊢ v:τ, p ↓ τ ▷ (ϕ′; Γ′) and match(p, v) ⟹ θ, then ϕ; Γ ⊢ θ : (ϕ′; Γ′) is derivable.

2. Given e,v in DML_{0}^{Π}(C) such that e ⟶ v is derivable. If ϕ; Γ ⊢ e : τ is derivable, then ϕ; Γ ⊢ v : τ is derivable.

ϕ; Γ ⊢ e: τ_{1} ϕ ⊧ τ_{1} ≡ τ_{2} ; \overline{(ty-eq)} ; ϕ; Γ ⊢ e: τ_{2} Γ(x) = τ ; \overline{(ty-var)} ; ϕ; Γ ⊢ x: τ

\begin{matrix}S(c) = Π a_{1} : γ_{1}… Π a_{k} : γ_{k} . δ(i) \\ ϕ ⊢ [a_{1}, …, a_{k} ↦ i_{1}, …, i_{k}] : (a_{1} : γ_{1}, …, a_{k} : γ_{k}) \end{matrix}

(ty-cons-wo)

ϕ; Γ ⊢ c[i_{1}] … [i_{k}] : δ(i[a_{1}, …, a_{k} ↦ i_{1}, …, i_{k}])

S(c) = Π a_{1} : γ_{1}… Π a_{k} : γ_{k} . τ → δ(i) ϕ ⊢ [a_{1}, …, a_{k} ↦ i_{1}, …, i_{k}] : (a_{1} : γ_{1}, …, a_{k} : γ_{k})

ϕ; Γ ⊢ e: τ[a_{1}, …, a_{k} ↦ i_{1}, …, i_{k}] \overline{(ty-cons-w)}

ϕ; Γ ⊢ c[i_{1}] … [i_{k}](e) : δ(i[a_{1}, …, a_{k} ↦ i_{1}, …, i_{k}])

\overline{(ty-unit)} ; ϕ; Γ ⊢ ⟨⟩: 1 ϕ; Γ ⊢ e_{1} : τ_{1} ϕ; Γ ⊢ e_{2} : τ_{2} \overline{(ty-prod)}

ϕ; Γ ⊢ ⟨e_{1}, e_{2}⟩: τ_{1} × τ_{2}
ϕ; Γ ⊢ e: τ′

ϕ; Γ ⊢ (p_{1} ⇒ e_{1}) : τ′ ⇒ τ

⋮

ϕ; Γ ⊢ (p_{k} ⇒ e_{k}) : τ′ ⇒ τ \overline{(ty-case)}

ϕ; Γ ⊢ (case e of p_{1} ⇒ e_{1} | … | p_{k} ⇒ e_{k}) : τ

p ↓ τ′ ▷ (ϕ′; Γ′) ϕ, ϕ′; Γ, Γ′ ⊢ e: τ

\overline{(ty-branch)}

ϕ; Γ ⊢ (p ⇒ e) : τ′ ⇒ τ

ϕ, a : γ; Γ ⊢ e: τ

\overline{(ty-ilam)}

ϕ; Γ ⊢ (λa : γ . e) : Π a : γ . τ ϕ; Γ ⊢ e: Π a : γ . τ ϕ ⊢ i : γ

\overline{(ty-iapp)}

ϕ; Γ ⊢ e[i] : τ[a ↦ i]
ϕ; Γ, x : τ_{1} ⊢ e: τ_{2}

\overline{(ty-lam)}

ϕ; Γ ⊢ (lam x : τ_{1} . e) : τ_{1} → τ_{2} ϕ; Γ ⊢ e_{1} : τ_{1} → τ_{2} ϕ; Γ ⊢ e_{2} : τ_{1}

\overline{(ty-app)}

ϕ; Γ ⊢ e_{1}(e_{2}) : τ_{2}

ϕ; Γ ⊢ e_{1} : τ_{1} ϕ; Γ, x : τ_{1} ⊢ e_{2} : τ_{2}

\overline{(ty-let)}

ϕ; Γ ⊢ let x = e_{1} in e_{2} end : τ_{2}

ϕ; Γ, f : τ ⊢ e: τ
\overline{(ty-fix)}
ϕ; Γ ⊢ (fix f : τ.e) : τ

Figure 17: Typing rules for DML_{0}^{Π}(C)

(ev-cons-wo)

c[i_{1}] … [i_{k}] ⟶ c[i_{1}] … [i_{k}]

e ⟶ v
\overline{(ev-cons-w)}

c[i_{1}] … [i_{k}](e) ⟶ c[i_{1}] … [i_{k}](v)

e_{1} ⟶ v_{1} e_{2} ⟶ v_{2}
\overline{(ev-prod)}
⟨e_{1}, e_{2}⟩ ⟶ ⟨v_{1}, v_{2}⟩

e_{0} ⟶ v_{0} match(v_{0}, p_{l}) ⟹ θ for some 1 ≤ l ≤ k e_{l}[θ] ⟶ v

\overline{(ev-case)}

case e_{0} of (p_{1} ⇒ e_{1} | … | p_{k} ⇒ e_{k}) ⟶ v

e ⟶ v

\overline{(ev-ilam)}

(λa : γ . e) ⟶ (λa : γ . v)

e ⟶ (λa : γ . v)

\overline{(ev-iapp)}

e[i] ⟶ v[a ↦ i]

\overline{(ev-lam)}

(lam x : τ . e) ⟶ (lam x : τ . e)

e_{1} ⟶ (λx : τ . e) e_{2} ⟶ v_{2} e[x ↦ v_{2}] ⟶ v

\overline{(ev-app)}
e_{1}(e_{2}) ⟶ v

e_{1} ⟶ v_{1} e_{2}[x ↦ v_{1}] ⟶ v

\overline{(ev-let)}

let x = e_{1} in e_{2} end ⟶ v

\overline{(ev-fix)}

(fix f : τ.e) ⟶ e[f ↦ (fix f : τ.e)]

Figure 18: Natural Semantics of DML_{0}^{Π}(C)

\overline{(mat-var)}

match(x, v) ⟹ [x ↦ v]

\overline{(mat-unit)}

match(⟨⟩, ⟨⟩) ⟹ []

match(p_{1}, v_{1}) ⟹ θ_{1} match(p_{2}, v_{2}) ⟹ θ_{2}

\overline{(mat-prod)}

match(⟨p_{1}, p_{2}⟩, ⟨v_{1}, v_{2}⟩) ⟹ θ_{1}θ_{2}

(mat-cons-wo)

match(c[a_{1}] … [a_{k}], c[i_{1}] … [i_{k}]) ⟹ [a_{1} ↦ i_{1}, …, a_{k} ↦ i_{k}]

match(p, v) ⟹ θ

(mat-cons-w)

match(c[a_{1}] … [a_{k}](p), c[i_{1}] … [i_{k}](v)) ⟹ θ[a_{1} ↦ i_{1}, …, a_{k} ↦ i_{k}]

Figure 19: Semantics of pattern matching in DML_{0}^{Π}(C)

B Formal development

B.1 A modified semantics a first-order fragment of DML

Figure 20 displays a modified semantics in which an environment of function definitions is maintained. Rule ev-mod-fundef shows how the environment is built up from function definitions, rule ev-mod-fapp shows how the environment is used. The judgment match(v, p) ⟹ θ in rule ev-mod-case is defined as in the standard semantics (see Figure 19 on the page before): If value v can be matched against pattern p, the corresponding substitution θ of the free variables in p is returned.

We present a proof of Theorem 1 on page 18, which states that the origi-

(ev-mod-cons-wo)

c[i_{1}] … [i_{k}] ⟶_{Θ} c[i_{1}] … [i_{k}]

e ⟶_{Θ} v

(ev-mod-cons-w)

c[i_{1}] … [i_{k}](e) ⟶_{Θ} c[i_{1}] … [i_{k}](v)

e_{1} ⟶_{Θ} v_{1} e_{2} ⟶_{Θ} v_{2}

(ev-mod-prod)

⟨e_{1}, e_{2}⟩ ⟶_{Θ} ⟨v_{1}, v_{2}⟩

e_{0} ⟶_{Θ} v_{0}
match(v_{0}, p_{l}) ⟹ θ for some 1 ≤ l ≤ k
e_{l}[θ] ⟶_{Θ} v

(ev-mod-case)

case e_{0} of (p_{1} ⇒ e_{1} | … | p_{k} ⇒ e_{k}) ⟶_{Θ} v

e_{1} ⟶_{Θ} v_{1} e_{2}[x ↦ v_{1}] ⟶_{Θ} v

(ev-mod-let)

let x = e_{1} in e_{2} end ⟶_{Θ} v

e ⟶_{Θ[F ↦e_{F}]} v

(ev-mod-fundef)

let F = fix F : τ.e_{F} in e end ⟶_{Θ} v

e ⟶_{Θ} v′
Θ(F) = λa⃗ : γ⃗ . lam x : ρ . body
body[a⃗ ↦ i⃗][x ↦ v′] ⟶_{Θ} v

(ev-mod-fapp)

F [i⃗](e) ⟶_{Θ} v

Figure 20: Natural Semantics of first-order fragment of DML nal semantics of DML_{0}^{Π}(C) from Appendix A.2 and the modified semantics of Figure 20 on the page before are equivalent.

Given a program p of the form described in Figure 8 on page 19, the modified semantics builds up an environment from the function definitions in p (rule evmod-fundef), while the original semantics accumulates a substitution (rule evlet). The judgment ⊢ Θ : Γ (Figure 21) is used to establish the well-formedness of an environment Θ and to type the functions contained in it.

(ty-env-nil)

⊢ [] : ·

⊢ Θ : Γ ·; Γ, F : τ ⊢ λa⃗ : γ⃗ . lam x : ρ_{F} . body_{F} : τ

(ty-env-cons)

⊢ Θ[F ↦ λa⃗ : γ⃗ . lam x : ρ_{F} . body_{F}] : Γ, F : τ

Figure 21: Typing an environment

We further use a mapping (·)^{∘} to relate the environment of the modified semantics with the substitution of the original semantics. Given an environment ⊢ Θ : Γ, the substitution Θ^{∘} is defined as follows:

\begin{aligned}([])^{∘} & = & [] \\ (Θ[F ↦ e])^{∘} & = & [F ↦ fix F : Γ(F).e] ∘ Θ^{∘} \end{aligned}

The following lemma relates the modified semantics with the original semantics.

Lemma 8 Let ⊢ Θ : Γ_{F} and let e be a body expression such that ϕ; Γ_{F} , Γ⊢ e:ρ is derivable. Then e[Θ^{∘}] ⟶ v iff e ⟶_{Θ} v.

Proof: The proof of the lemma is conducted by structural induction over the derivation e[Θ^{∘}] ⟶ v (proving the implication from left to right) and e ⟶_{Θ} v (right to left).

We show the implication from left to right, examining the last rule in a derivation of e[Θ^{∘}] ⟶ v. For rules ev-cons-wo, ev-cons-w, ev-prod, ev-case and ev-let, the lemma follows immediately by induction hypothesis. For rules evilam, ev-iapp, ev-app and ev-fix observe, that because of the restricted shape of e (see Figure 8 on page 19), only rule ev-ilam can occur as the last rule in a derivation e[Θ^{∘}] ⟶ v, namely for e = F [i⃗](e′). Assume therefore that (F [i⃗](e′))[Θ^{∘}] ⟶ v is derivable; an analysis of the shape of the corresponding derivation (see Figure 18 on page 37 for the rules) shows that for some value v_{1} there are derivations of e′[Θ^{∘}] ⟶ v_{1} and body[a⃗ ↦ i⃗][x ↦ v_{1}][Θ^{∘}] ⟶ v. Using the induction hypothesis, we can derive that body[a⃗ ↦ i⃗][x ↦ v_{1}] ⟶_{Θ} v, from which it follows easily with rule ev-mod-fapp (Figure 20 on the preceding page) that F [i⃗](e′) ⟶_{Θ} v.

The other direction of the implication follows similarly. □

We are now in a position to prove Theorem 1 on page 18.

Proof: Let program p be of the form given in Figure 8 on page 19 with function definitions F_{l} = fix F_{l} : τ_{l}.e_{l} for 0 ≤ l ≤ k and program body e. With the typing rules ty-let and ty-fix (Figure 17 on page 36) and the rules from Figure 21 on the preceding page a straightforward induction over the number of function definitions shows that

⊢ (F_{1} : τ_{1}, …, F_{k} : τ_{k}) : \overbrace{[F_{1} ↦ e_{1}, …, F_{k} ↦ e_{k}]}^{=:Θ}.

Further, examining the modified and original semantics, we see:

p ⟶ v iff e[Θ^{∘}] ⟶ v
p ⟶_{[]} v iff e ⟶_{Θ} v

With Lemma 8 on the page before it follows that p ⟶ v iff p ⟶_{[]} v. □

B.2 The monadic translation

We present a proof of Theorem 2 on page 20, which states that the monadic translation preserves types and semantics.

B.2.1 The monadic translation preserves types

The following Lemma expresses the validity of the typing rules given for val^{C}, let^{C} and cost in Section 4.2 with respect to the expansion of these constructs as given in Figure 10 on page 21.

Lemma 9 The typing rules for val^{C}, let^{C} and cost as given in Section 4.2 are admissible (assuming that val^{C}, let^{C} and cost are expanded as described in Figure 10 on page 21).

Proof: Straightforward by constructing the corresponding type derivations. □

The first part of Theorem 2 on page 20 follows immediately from the following lemma.

Lemma 10 For an expression e, if ϕ; Γ ⊢ e: ρ is derivable, then ϕ; Γ^{∗} ⊢ e^{∗} : C ρ is derivable, where Γ^{∗} results from Γ by wrapping the result type of every function declared in Γ with C .

Proof: The proof is conducted by structural induction on the derivation of ϕ; Γ ⊢ e: ρ (typing rules in Figure 17 on page 36). If the last rule of the derivation is (ty-eq), then the lemma follows immediately by induction hypothesis. Otherwise, because the remaining rules are syntax directed, we proceed by examining all possible expressions e.

We present one interesting case, namely a function call ϕ; Γ ⊢ F [i⃗](e) : ρ. Examining the possible derivations, we see that there exists ρ_{1} such that ϕ; Γ ⊢ F [i⃗] : ρ_{1} → ρ and ϕ; Γ ⊢ e: ρ_{1} are derivable. The monadic translation of F [i⃗](e) is

let^{C} x = e^{∗}
in cost_{c_{c}} (F [i⃗](x)) end

Because of Lemma 9 on the page before, rule ty-monadic-let (Section 4.2) is admissible, hence we need to find derivations of ϕ; Γ ⊢ e^{∗} : C ρ_{1} and ϕ; Γ^{∗}, x : ρ_{1} ⊢ cost_{c_{F}} (F [i⃗](x)) : C ρ. The former follows by induction hypothesis, the latter is easily derived using rule ty-monadic-cost and the fact that ϕ; Γ ⊢ F [i⃗] : ρ_{1} → ρ is derivable. □

B.2.2 The monadic translation preserves semantics

In order to prove the second part of Theorem 2 on page 20, namely that the monadic translation preserves semantics, we need the following lemma:

Lemma 11 Let ⊢ Θ : Γ_{F} and ϕ; Γ_{F} , Γ ⊢ e : ρ be derivable. Then e ⟶_{Θ} v iff there exists a z ∈ C such that e^{∗} ⟶_{Θ^{∗}} ⟨v, z⟩ is derivable (where Θ^{∗}(F) = Θ(F)^{∗} for all F ∈ dom(Θ)).

Proof: The proof is conducted by structural induction over e ⟶_{Θ} v (proving the implication from left to right) and over e^{∗} ⟶_{Θ^{∗}} ⟨v, z⟩ (right to left).

We show the case of a function call F [i⃗](e). Assume that there exists a derivation of F [i⃗](e) ⟶_{Θ} v. Rule inversion with ev-mod-fapp (Figure 20 on page 39) shows that there exists a value v′ such that e ⟶_{Θ} v′ and body[a⃗ ↦ i⃗][x_{1} ↦ v′] ⟶_{Θ} v are derivable, where Θ(F) = λa⃗ : γ⃗ . lam x : ρ . body. Consider now the translated term (F [i⃗](e))^{∗} where the monadic constructs have been expanded as shown in Figure 10 on page 21:

case e^{∗} of
⟨x_{1}, z_{1}⟩ ⇒ case (case F [i⃗](x_{1}) of ⟨x_{3}, z_{3}⟩ ⇒ ⟨x_{3}, z_{3} + c_{F} ⟩) of
⟨x_{2}, z_{2}⟩ ⇒ ⟨x_{2}, z_{1} + z_{2}⟩

By induction hypothesis, we know that there is a z′_{1} such that e^{∗} ⟶_{Θ^{∗}} ⟨v′, z′_{1}⟩; with ev-mod-case it follows that we need to show a derivation of F [i⃗](v′) ⟶_{Θ^{∗}} ⟨v, z′_{3}⟩ for some z′_{3} ∈ C. Such a derivation can be constructed using ev-mod-fapp and a derivation body^{∗}[a⃗ ↦ i⃗][x_{1} ↦ v′] ⟶_{Θ^{∗}} ⟨v, z′_{3}⟩, which exists by induction hypothesis. □ We are now in a position to prove the second part of Theorem 2 on page 20:

Proof: Let program p be of the form given in Figure 8 on page 19 with function definitions F_{l} = fix F_{l} : τ_{l}.e_{l} for 0 ≤ l ≤ k and program body e. Let

\begin{aligned}Γ & := & F_{1} : τ_{1}, …, F_{k} : τ_{k} \\ Θ & := & [F_{1} ↦ e_{1}, …, F_{k} ↦ e_{k}] \end{aligned}

Inspecting the type derivation of p it is easy to see that ⊢ Θ : Γ and ·; Γ⊢ e:ρ are derivable. From the semantics we know that p ⟶_{[]} v and p^{∗} ⟶_{[]} ⟨v′, z⟩ iff e ⟶_{Θ} v and e^{∗} ⟶_{Θ^{∗}} ⟨v′, z⟩, respectively. With Lemma 11 on the page before we have that e ⟶_{Θ} v iff e^{∗} ⟶_{Θ^{∗}} ⟨v, z⟩, which concludes the proof. □

B.3 Extraction of recurrence equations—preliminaries

B.3.1 An erasure from index sorts to index types

The erasure ˜ · maps an index sort to its associated index type by removing all constraint-related information. It is defined as follows:

\begin{aligned}ℕ̃ & = & ℕ \\ ˜1 & = & 1 \\ { \atop γ_{1} × γ_{2}} & = & γ̃_{1} × γ̃_{2} \\ { \atop \{a : γ | P \}} & = & γ̃ \end{aligned}

For a context Γ that maps function names to types we define Γ̃ such that

Γ̃(F^{c}) = γ̃_{0} → γ̃_{1} → … γ̃_{k} → C

if

Γ(F) = Π a_{0} : γ_{0} . Π a_{1} : γ_{1}… Π a_{k} : γ_{k} . ρ_{1} → ρ_{2}.

For an index context ϕ we define ϕ̃ as follows:

\begin{aligned}˜ · & = & · \\ { \atop ϕ, a : γ} & = & ϕ̃, a : γ̃ \\ ϕ̃, P & = & ϕ̃ \end{aligned}

The following lemma shows that the erasure preserves type soundness of index substitutions.

Lemma 12 If ϕ ⊢ θ : ϕ′ is derivable, then ϕ̃ ⊢ θ : ϕ̃′ is derivable.

Proof: With a straightforward induction over the structure of sort γ, it is easy to show that if ϕ ⊢ i : γ is derivable, then ϕ̃ ⊢ i : γ̃ is derivable. Using this fact, one then can show the lemma with a straightforward induction over the length of ϕ′. □

B.3.2 Flattening index contexts into constraints

The algorithm for extracting cost recurrences uses a function C to rewrite an index context into a conjunctive constraint by flattening subsort definitions. A declaration i : {k : γ | P } is rewritten with the conjunction of (1) the constraints imposed by the declaration i : γ and (2) the index proposition P [k ↦ i]. The resulting constraint Φ := C(ϕ) is a quantifier-free conjunction of equality constraints and index propositions:^{7}

\begin{aligned}C(·) & = & ⊤ \\ C(ϕ, i : 1) & = & C(ϕ) \\ C(ϕ, i : ℕ) & = & C(ϕ) \\ C(ϕ, i : γ_{1} × γ_{2}) & = & C(ϕ, fst(i) : γ_{1}, snd(i) : γ_{2}) \\ C(ϕ, i : \{k : γ | P \}) & = & C(ϕ, i : γ) ∧ P [k ↦ i] \\ C(ϕ, P) & = & C(ϕ) ∧ P \\ C(ϕ, i = j) & = & C(ϕ) ∧ (i = j) \end{aligned}

C is well-defined: Assuming a straightforward weight-function for sort definitions, a termination order for C(ϕ) can be given as the lexicographic order of the sum of the weights of all sort definitions in ϕ and the length of ϕ.

The following lemma expresses a useful correspondence between ϕ and C(ϕ):

Lemma 13 Let ϕ and ϕ′ be index contexts and θ an index substitution such that dom(θ) = dom(ϕ′). Then

ϕ ⊢ θ : ϕ′ iff ϕ ⊧ C(ϕ′)[θ].

Proof: We conduct the proof by structural induction over ϕ. In the base case, ϕ = ·, we have ϕ ⊢ [] : · and ϕ ⊧ ⊤[θ] for all substitutions θ. Both directions follow immediately (using dom(θ) = dom(ϕ′) from right to left).

A non-empty index context has form ϕ, a : γ or ϕ, P. We examine the first of these cases, the second case follows by similar reasoning.

We have to show that

ϕ ⊢ θ[a ↦ i] : ϕ′, a : γ iff ϕ ⊧ C(ϕ′, a : γ)[θ[a ↦ i]],

which is equivalent to

(ϕ ⊢ θ : ϕ′ and ϕ ⊢ i : γ[θ]) iff (ϕ ⊧ C(ϕ′)[θ] and ϕ ⊧ C(a : γ)[θ[a ↦ i]]).

Assuming that for all i and γ

ϕ ⊢ i : γ iff ϕ ⊧ C(a : γ)[a ↦ i],  (*)

we can conclude the proof using the induction hypothesis.

7Because of the way C handles product sorts, it actually is defined on contexts that assign sorts to index objects rather than only index variables.

It remains to show Equation (*). We use induction over the structure of γ and demonstrate the case of a sort definition of form {k : γ | P }: We have to show that

ϕ ⊢ i : {k : γ | P } iff ϕ ⊧ C(a : {k : γ | P })[a ↦ i]

Assuming the left-hand side, it follows with rule-inversion that ϕ ⊢ i : γ and ϕ ⊧ P [k ↦ i]. Using the induction hypothesis, we further can derive that ϕ ⊧ C(a : γ)[a ↦ i], so obviously ϕ ⊧ (C(a : γ ∧ P [k ↦ a]))[a ↦ i], which is equivalent to ϕ ⊧ (C(a : {k : γ | P }))[a ↦ i]. The direction from right to left follows with similar reasoning steps. □

B.4 Extraction of recurrence equations—correctness

In this section, we present a proof of the correctness of the extraction algorithm for recurrence equations, as stated in Theorem 4 on page 29. As the theorem is in three parts, we divide the proof into three parts.

B.4.1 The result of extraction is well-typed

The first part of Theorem 4 on page 29 follows directly from a lemma that relates the type derivation of a function body to the type derivation of the extracted recurrence-equation term.

Lemma 14 If ϕ; Γ ⊢ e: ρ ▶ t is derivable for an expression e, then ϕ̃; Γ̃ ⊢ t: C is derivable.

Proof: The proof is conducted by structural induction over the type derivation of e. In case the last rule of the type derivation is ty-eq, then the lemma follows by induction hypothesis. Because the remaining typing rules for DML_{0}^{Π}(C) are syntax directed, we proceed by examining the different syntactic forms of e as given by the grammar in Figure 8 on page 19. We show the case of a function call F [i_{0}] … [i_{k}] e; all other cases can be shown in a similar way.

For a function call F [i_{0}] … [i_{k}](e) , the extracted recurrence-equation term is t := t′ + c_{F} + (F^{c} i_{0} … i_{k}) where t′ has been extracted from e. The last rule of the type derivation must be ty-app, i.e., for some ρ_{1}, ρ_{2} there exist derivations

ϕ; Γ ⊢ e: ρ_{1}  (1)
ϕ; Γ ⊢ F [i_{0}] … [i_{k}] : ρ_{1} → ρ_{2}  (2)

Analyzing the shape of a type derivation for t, we see that we need to show

ϕ̃; Γ̃ ⊢ t′ : C  (1′)
ϕ̃ ⊢ i_{0} : γ̃_{0} … ϕ̃ ⊢ i_{k} : γ̃_{k},  (2′)

assuming that Γ(F) = Π a_{0} : γ_{0}… Π a_{k} : γ_{k} . ρ′_{1} → ρ′_{2}. From (1), we can show (1′) using the induction hypothesis. From (2), we can derive (2′): With a straightforward induction on k one can show that (2) implies

ϕ ⊢ [a_{0} ↦ i_{0}, …, a_{k} ↦ i_{k}] : (a_{0} : γ_{0}, …, a_{k} : γ_{k}).

With Lemma 12 on page 43, it follows that

ϕ̃ ⊢ [a_{0} ↦ i_{0}, …, a_{k} ↦ i_{k}] : (a_{0} : γ̃_{0}, …, a_{k} : γ̃_{k}),

which, because there are no dependencies between two index types γ̃_{l} and γ_{l′}, implies (2′). □

B.4.2 The result of extraction is a cost bound

We need to show that the cost of executing F [i⃗] v for some user-defined function F and some value v is bounded by F^{c} i⃗, where F^{c} is the cost recurrence extracted for F. We start with Lemma 15, which says that when extracting a recurrenceequation term t from a DML expression e, then t defines a bound for e under the assumption that all calls to user-defined functions in e are bounded correctly by the corresponding calls to F^{c} in t.

Lemma 15 Let ϕ; Γ_{F} , Γ ⊢ e : ρ ▶ t be derivable. Let θ be a substitution such that θ_{ϕ} substitutes index variables for ground terms, θ_{Γ} substitutes (normal) variables for values, and ·; Γ_{F} ⊢ θ : (ϕ; Γ) is derivable, i.e., θ is type-sound with respect to ϕ and Γ. Let Θ be an environment such that ⊢ Θ : Γ_{F} is derivable. Let Ψ be a mapping from dom(Γ_{F}) to functions such that

1. if Γ_{F} (F) = Π a_{0} : γ_{0}… Π a_{l} : γ_{l} . ρ_{1} → ρ_{2} then

Ψ(F^{c}) ∈ [I[[γ̃_{0}]] → … → I[[γ̃_{l}]] → C_{⊥}]

2. if F [i⃗](u) type-checks under Γ_{F} and T [[F^{c} i⃗]]Ψ[] = ⌞z⌟ then

F [i⃗](u) ⟶_{Θ^{∗}} ⟨u′, z′⟩ with z′ ≤ z.

Then if T [[t]]Ψ(I[[θ_{ϕ}]]) = ⌞z⌟, then e^{∗}[θ] ⟶_{Θ^{∗}} ⟨v′, z′⟩ with z′ ≤ z.

Proof: We use structural induction over the type derivation of e. In case the last rule of the type derivation is ty-eq, then the lemma follows by induction hypothesis. Because the remaining typing rules for DML_{0}^{Π}(C) are syntax directed, we proceed by examining the different syntactic forms of e as given by the grammar in Figure 8 on page 19. We show two interesting cases: function application and case expression.

For a function application F [i⃗](e), the extracted recurrence-equation term is t + c_{F} + F^{c} i⃗, where t has been extracted from e. We express (F [i⃗](e))^{∗}, (see Figure 9 on page 21 for the definition of the monadic translation (·)^{∗}) as a DML program by removing syntactic sugar introduced in the translation (see Figure 10 on page 21) and examine the shape of a possible derivation for

(F [i⃗](e))^{∗}[θ] ⟶_{Θ^{∗}} ⟨v′, z′⟩.

It is easy to see that such a derivation can exist only if there are z′_{F} , z′_{e} ∈ C such that z′ = z′_{F} + c_{F} + z′_{e} and the following two assumptions hold:

(1) For some value v_{e}, there is a derivation e^{∗}[θ] ⟶_{Θ^{∗}} ⟨v_{e}, z′_{e}⟩.

(2) There is a derivation F [i⃗[θ]] v_{e} ⟶_{Θ^{∗}} ⟨v′, z′_{F} ⟩.

Assume now that T [[t + c_{F} + F^{c} i⃗]]Ψ(I[[θ_{ϕ}]]) = ⌞z⌟; using the semantics definition from Figure 13 on page 24 the following three facts follow easily:

(1′) For some z_{e} ∈ C we have T [[t]]Ψ(I[[θ_{ϕ}]]) = ⌞z_{e}⌟.

(2′) For some z_{F} ∈ C, we have T [[F^{c} i⃗]]Ψ(I[[θ_{ϕ}]]) = ⌞z_{F} ⌟.

(3′) We have z = z_{F} + c_{F} + z_{e}.

Using the induction hypothesis and (1′), we can deduce (1) for some z′_{e} ≤ z_{e}. From (2′), it follows by assumption that (2) holds for some z′_{F} ≤ z_{F}; this is because T [[F^{c} i⃗]]Ψ(I[[θ_{ϕ}]]) is equivalent to T [[F^{c} (i⃗[θ_{ϕ}])]]Ψ[]. Finally, using (3′) we can infer that z′ ≤ z, which concludes the proof for this case.

For a case expression of form (case e of p_{0} ⇒ e_{0} | … p_{k} ⇒ e_{k}), the extracted recurrence-equation term is

t + (cond br_{0} | … | br_{k})

where t is extracted from e by

ϕ; Γ_{F} , Γ ⊢ e: ρ′ ▶ t

and every br_{j} from the type-derivation of a branch (p_{j} ⇒ e_{j}) as

Φ_{j1} → ∀(dom(ϕ′_{j})\dom(θ_{j})).Φ_{j2} → t[θ_{j}]

where

p ↓ ρ′ ▷ (ϕ′_{j}; Γ′_{j})
ϕ, ϕ′_{j}; Γ, Γ′_{j} ⊢ e_{j} : ρ ▶ t_{j}
Φ_{j1} = ∃(dom(ϕ, ϕ′_{j})\var(ρ′)).C(ϕ, ϕ′_{j})
θ_{j} = mk subst_{dom(ϕ′_{j})}(C(ϕ′_{j}))
Φ_{j2} = ∃(dom(θ_{j})).C(ϕ′_{j})

Like before, we examine the shape of a possible derivation for

(case e of p_{0} ⇒ e_{0} | … p_{k} ⇒ e_{k})^{∗}[θ] ⟶_{Θ^{∗}} ⟨v′, z′⟩,

and see that such a derivation can exist only if there are z′_{e}, z′_{b} ∈ C such that z′ = z′_{e} + z′_{b} and the following two assumptions hold:

(1) For some value v_{e}, there is a derivation e^{∗}[θ] ⟶_{Θ^{∗}} ⟨v_{e}, z′_{e}⟩.

(2) For some j with 0 ≤ j ≤ k for which match(p_{j}, v_{e}) ⟹ θ′ is derivable, there is a derivation e_{j}^{∗}[θ ∘ θ′] ⟶_{Θ^{∗}} ⟨v′, z′_{b}⟩.

Assume now that T [[t + (cond br_{0} | … | br_{k})]]Ψ(I[[θ_{ϕ}]]) = ⌞z⌟; using the semantics definition from Figure 13 on page 24 we can deduce the following facts:

(1′) For some z_{e} ∈ C we have T [[t]]Ψ(I[[θ_{ϕ}]]) = ⌞z_{e}⌟.

(2′) There is some z_{b} ∈ C such that for every branch br_{j}

Φ_{j1} → ∀(dom(ϕ′_{j})\dom(θ_{j})).Φ_{j2} → t[θ_{j}]

we have that if ⊧ Φ_{j1}[θ_{ϕ}] then for all z⃗ with ⊧ Φ_{j2}[θ_{ϕ}[a⃗ ↦ z⃗]] there is z_{B} ≤ z_{b} such that T [[t_{j}[θ_{j}]]]Ψ(I[[θ_{ϕ}[a⃗ ↦ z⃗]]]) = ⌞z_{B}⌟

(3′) We have z = z_{e} + z_{b}.

Using the induction hypothesis and (1′), we can deduce (1) for some z′_{e} ≤ z_{e}. In the following, we prove (2), using the induction hypothesis and (2′):

• We first show that whenever match(p_{j}, v_{e}) ⟹ θ′ is derivable, then ⊧ Φ_{j1}[θ_{ϕ}], i.e., the precondition for (2’) holds.

We examine the form of Φ_{j1} = ∃b⃗, c⃗.C(ϕ, ϕ′_{j}), where b⃗ are the variables in dom(ϕ′_{j}) and c⃗ are the variables in dom(ϕ)\var(ρ′). We need to show

⊧ (∃b⃗, c⃗.C(ϕ, ϕ′_{j}))[θ_{ϕ}].

In fact, θ_{ϕ} and θ′_{ϕ} hold witnesses for b⃗ and c⃗, respectively: By assumption, we have ·; Γ_{F} ⊢ θ : (ϕ; Γ), which implies ⊢ θ_{ϕ} : ϕ. Further, with the first part of Theorem 7 on page 35, it follows that ϕ ⊢ θ_{j}_{ϕ} : ϕ′. Using Lemma 13 on page 44, we derive ⊧ C(ϕ)[θ_{ϕ}] and ϕ ⊧ C(ϕ′_{j})[θ′_{ϕ}]. With Lemma 5 on page 33, we then can derive ⊧ (C(ϕ′_{j})[θ′_{ϕ}])[θ_{ϕ}], so all in all we have we have ⊧ C(ϕ, ϕ′_{j})[θ′_{ϕ} θ_{ϕ}], which implies ⊧ (∃b⃗, c⃗.C(ϕ, ϕ′_{j}))[θ_{ϕ}].

• With similar reasoning, we show that whenever match(p_{j}, v_{e}) ⟹ θ′ is derivable, then ⊧ Φ_{j2}[θ_{ϕ}[a⃗ ↦ θ′_{ϕ}(a⃗)]] (where a⃗ := dom(ϕ′_{j})\dom(θ_{j})) holds, so with (2′) it follows that

T [[t_{j}[θ_{j}]]]Ψ(I[[θ[a⃗ ↦ θ′_{ϕ}(a⃗)]]]) = ⌞z_{B}⌟ for some z_{B} ≤ z_{b}.  (*)

• Knowing (*), we can show (2) by induction hypothesis if

T [[t_{j}[θ_{j}]]]Ψ(I[[θ_{ϕ}[a⃗ ↦ θ′_{ϕ}(a⃗)]]]) = T [[t_{j}]]Ψ(I[[θ_{ϕ} ∘ θ′_{ϕ}]]).

With a straightforward structural induction over t_{j} we can show that

T [[t_{j}[θ_{j}]]]Ψ(I[[θ_{ϕ}[a⃗ ↦ θ′_{ϕ}(a⃗)]]]) = T [[t_{j}]]Ψ(I[[θ_{j} ∘ θ_{ϕ}[a⃗ ↦ θ′_{ϕ}(a⃗)]]])

It remains to show that b[θ_{j} ∘ θ_{ϕ}[a⃗ ↦ θ′_{ϕ}(a⃗)]] = b[θ_{ϕ} ∘ θ′_{ϕ}] for all b ∈ dom(θ ∘ θ′). Some reasoning about the domains of the comprised substitutions allows us to rearrange their composition and show instead that

b[(θ_{j} ∘ [a⃗ ↦ θ′_{ϕ}(a⃗)])θ_{ϕ}] = b[θ′_{ϕ} θ_{ϕ}]  (**)

For b ∈ a⃗ and b ∈ dom(θ) there is nothing to show. Consider now b ∈ dom(θ_{j}). By definition of θ_{j} we know that ϕ′ ⊧ b = b[θ_{j}]. Using Lemma 5 on page 33 on ⊢ θ_{ϕ} : ϕ and ϕ ⊢ θ_{j}_{ϕ} : ϕ′_{j} (established above), we can derive that b[θ_{j} ∘ θ′_{ϕ} ∘ θ_{ϕ}] = b[θ′_{ϕ} ∘ θ_{ϕ}]. Equation (**) follows with some basic reasoning about substitutions.

Now, with (3′) and the fact that z_{B} ≤ z_{b}, it follows that z′ ≤ z, which concludes the proof for this case. □ We have shown that extracting a recurrence-equation term t from a DML expression e yields a valid bound under the assumption that we have a valid bound F^{c} for every user-defined function F called in e. We now show that the semantics of a recurrence equation G^{c}, which is based on the recurrence-equation term extracted from the body of a user-defined function G (see Section 4.3.2), indeed defines a bound for G.

Lemma 16

Let (fix G : Π a⃗ : γ⃗ . ρ_{1} → ρ_{2}.lam x : ρ_{1} . case x of ⟨x_{0}, …, x_{k}⟩ ⇒ e) be typable under Γ_{F} and let

·; Γ_{F} , G : Π a⃗ : γ⃗ . ρ_{1} → ρ_{2}, x : ρ_{1}, x_{0} : ρ_{1}^{0}, …, x_{k} : ρ_{1}^{k} ⊢ e : ρ_{2} ▶ t

be derivable. Let Θ be an environment such that ⊢ Θ : Γ_{F} is derivable. Let Ψ be a mapping from dom(Γ_{F}) to functions such that

1. if Γ_{F} (F) = Π a_{0} : γ_{0}… Π a_{l} : γ_{l} . ρ_{1} → ρ_{2} then

Ψ(F^{c}) ∈ [I[[γ̃_{0}]] → … → I[[γ̃_{l}]] → C_{⊥}]

2. if F [i⃗](u) type-checks under Γ_{F} and T [[F^{c} i⃗]]Ψ[] = ⌞z⌟ then

F [i⃗](u) ⟶_{Θ^{∗}} ⟨u′, z′⟩ with z′ ≤ z.

Let further

φ := fix(λF.λn⃗.T [[t]](Ψ[G^{c} ↦ F])[a⃗ ↦ n⃗])
Θ_{1} := Θ[G ↦ lam x : ρ_{1} . case x of ⟨x_{0}, …, x_{k}⟩ ⇒ e]

Then, if G[i⃗](u) type-checks under Γ_{F} , G : Π a⃗ : γ⃗ . ρ_{1} → ρ_{2} and

T [[G^{c} [i⃗]]](Ψ[G^{c} ↦ φ])[] = ⌞z⌟,

we have G[i⃗](u) ⟶_{Θ_{1}}^{∗} ⟨v′, z′⟩ with z′ ≤ z.

Proof: We use fixed-point induction over the definition of φ. For the base case, we have

T [[G [i⃗]]](Ψ[G^{c} ↦ φ])[] = ⊥,

so the lemma is vacuously true. For the induction step, assume that for φ′, if G[i⃗](u) type-checks under Γ_{F} , G : Π a⃗ : γ⃗ . ρ_{1} → ρ_{2} and

T [[G^{c} [i⃗]]](Ψ[G^{c} ↦ φ′])[] = ⌞z⌟,

we have G[i⃗](u) ⟶_{Θ_{1}}^{∗} ⟨v′, z′⟩ with z′ ≤ z. We have to show that if

T [[G [i⃗]]](Ψ[G^{c} ↦ λn⃗.T [[t]](Ψ[G^{c} ↦ φ′])[a⃗ ↦ n⃗]])[] = ⌞z⌟  (1)

then

G[i⃗] u ⟶_{Θ_{1}}^{∗} ⟨v′, z′⟩  (2)

with z′ ≤ z.

Using the definitions of the denotational semantics (Figure 13 on page 24) of recurrence equations and operational semantics of DML (Figure 20 on page 39), we see that Equations (1) and (2) are equivalent to

T [[t]](Ψ[G^{c} ↦ φ′])[a⃗ ↦ I[[i⃗]]] = ⌞z⌟  (1’)
e^{∗}[a⃗ ↦ i⃗][x ↦ u][x_{0} ↦ fst(u)] … [x_{k} ↦ snd^{k}(u)] ⟶_{Θ_{1}}^{∗} ⟨v′, z′⟩ (2’)

We can use Lemma 15 on page 46; its preconditions are satisfied:

• From the fact that G[i⃗](u) type-checks under Γ_{F} , G : Π a⃗ : γ⃗ . ρ_{1} → ρ_{2}, we can deduce that the substitution

[a⃗ ↦ i⃗][x ↦ u][x_{0} ↦ fst(u)] … [x_{k} ↦ snd^{k}(u)]

is type-sound with respect to a⃗ : γ⃗ and x : ρ_{1}, x_{0} : ρ_{1}^{0}, …, x_{k} : ρ_{1}^{k}.

• The environment (Ψ[G^{c} ↦ φ′]) has the required properties, for F^{c} ∈ dom(Θ) by assumption, and for G^{c} by induction hypothesis.

□

Part 2 of Theorem 4 on page 29 follows from Lemma 16 on the preceding page with a straightforward induction proof over the number of user-defined functions in program p.

B.4.3 Result of extraction is a recurrence

The intuition behind the test described in Section 4.4.3 of whether the extracted cost bound is a recurrence is to use the constraint information contained in DML_{0}^{Π}(C) type derivations for showing that the argument on each recursive call decreases. Without further proof, however, such an argument only shows the termination of the examined DML program. We further need to argue that conclusions drawn from constraint information about index arguments to recursive function calls also holds for arguments to the corresponding calls occurring within an occurrence equation:

Theorem 17 Assume that the extraction algorithm annotates every call F^{c} i⃗ with the index context it was extracted under, i.e., ϕ′; Γ′ ⊢ F [i⃗](e′) : ρ′ gives rise to F^{c,ϕ′}i⃗, and that the semantics T [[·]] ignores such annotations. If ϕ; Γ⊢ e:ρ ▶ t and ⊢ θ : ϕ, then, in the unfolded definition of T [[t]]Ψθ, for all applications Ψ(F^{c,ϕ′}) I[[i⃗[θ′]]] we have ⊢ θ′ : ϕ′.

Proof: As in the proof of Lemma 15 on page 46, we use structural induction over the type derivation of e. The only interesting case is that of a case expression case e of p_{0} ⇒ e_{0} | … p_{k} ⇒ e_{k}. The extracted recurrence-equation term is

t + (cond br_{0} | … | br_{k})

where t is extracted from e by

ϕ; Γ_{F} , Γ ⊢ e: ρ′ ▶ t

and every br_{j} from the type-derivation of a branch (p_{j} ⇒ e_{j}) as

Φ_{j1} → ∀(dom(ϕ′_{j})\dom(θ_{j})).Φ_{j2} → t[θ_{j}]

where

p ↓ ρ′ ▷ (ϕ′_{j}; Γ′_{j})
ϕ, ϕ′_{j}; Γ, Γ′_{j} ⊢ e_{j} : ρ ▶ t_{j}
Φ_{j1} = ∃(dom(ϕ, ϕ′_{j})\var(ρ′)).C(ϕ, ϕ′_{j})
θ_{j} = mk subst_{dom(ϕ′_{j})}(C(ϕ′_{j}))
Φ_{j2} = ∃(dom(θ_{j})).C(ϕ′_{j})

For T [[t]]Ψθ we can simply use the induction hypothesis. For the conditional, however, we have to examine all possible calculations T [[t_{j}[θ_{j}]]]Ψ(θ[a⃗ ↦ z⃗]) (with a⃗ := dom(ϕ′_{j})\dom(θ_{j})). With a straightforward structural induction on t_{j} one can show that

T [[t_{j}[θ_{j}]]]Ψ(θ[a⃗ ↦ z⃗]) = T [[t_{j}]]Ψ(θ_{j} ∘ (θ[a⃗ ↦ z⃗])).

To use the induction hypothesis, it remains to show that ⊢ (θ_{j} ∘ θ[a⃗ ↦ z⃗]) : (ϕ, ϕ′_{j}), which follows with a short derivation using Lemma 13 on page 44 and the assumptions about ϕ, ϕ′_{j}, θ, θ_{j}, and z⃗. □

Theorem 17 shows that index-based reasoning about the index arguments to functions in a DML program carry over to the corresponding recurrence equation, hence the third part of Theorem 4 on page 29 holds.

Recent BRICS Report Series Publications

RS-01-25 Bernd Grobauer. Cost Recurrences for DML Programs. June 2001. 51 pp. Extended version of a paper to appear in Leroy, editor, Proceedings of the 6th ACM SIGPLAN International Conference on Functional Programming, 2001.

RS-01-24 ZoltánÉsik and Zoltán L. Németh. Automata on Series-Parallel Biposets. June 2001. 15 pp. To appear in Kuich, editor, 5th International Conference, Developments in Language Theory DLT ’01 Proceedings, LNCS, 2001.

RS-01-23 Olivier Danvy and Lasse R. Nielsen. Defunctionalization at Work. June 2001. Extended version of an article to appear in Søndergaard, editor, 3rd International Conference on Principles and Practice of Declarative Programming, PPDP ’01 Proceedings, 2001.

RS-01-22 Zoltán Ésik. The Equational Theory of Fixed Points with Applications to Generalized Language Theory. June 2001. 21 pp. To appear in Kuich, editor, 5th International Conference, Developments in Language Theory DLT ’01 Proceedings, LNCS, 2001.

RS-01-21 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. Equational Theories of Tropical Semirings. June 2001. 52 pp. Extended abstracts of parts of this paper have appeared in Honsell and Miculan, editors, Foundations of Software Science and Computation Structures, FoSSaCS ’01 Proceedings, LNCS 2030, 2000, pages 42–56 and in Gaubert and Loiseau, editors, Workshop on Max-plus Algebras and their Applications to Discrete-event Systems, Theoretical Computer Science, and Optimization, MAX-PLUS ’01 Proceedings, IFAC (International Federation of Automatic Control) IFAC Publications, 2001.

RS-01-20 Catuscia Palamidessi and Frank D. Valencia. A Temporal Concurrent Constraint Programming Calculus. June 2001. 31 pp.

RS-01-19 Jiří Srba. On the Power of Labels in Transition Systems. June 2001. 23 pp. Full and extended version of Larsen and Nielsen, editors, Concurrency Theory: 12th International Conference, CONCUR ’01 Proceedings, LNCS, 2001.