BRICS

Basic Research in Computer Science

Formal Aspects of Polyvariant Specialization

Henning Korsholm Rohde BRICS Report Series RS-05-34 ISSN 0909-0878 November 2005 BRICS RS-05-34 H. K. Rohde: Formal Aspects of Polyvariant Specialization Copyright \begin{matrix}c \\ ◯ \end{matrix} 2005, Henning Korsholm Rohde.

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/05/34/

Formal Aspects of Polyvariant Specialization

Henning Korsholm Rohde BRICS^{∗}, Department of Computer Science University of Aarhus, Denmark

                       hense@brics.dk

November 7, 2005

Abstract

We present the first formal correctness proof of an offline polyvariant specialization algorithm for first-order recursive equations. As a corollary, we show that the specialization algorithm generates a program implementing the search phase of the Knuth-Morris-Pratt algorithm from an inefficient but binding-time-improved string matcher.

∗ Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

Contents

1 Introduction 3

2 Polyvariant specialization 4

2.1 A typed first-order language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.2 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.1.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2.2 A binding-time-annotated language . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2.2 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2.3 The specialization algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3.1 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3.2 State and effects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.3.3 The residualizing semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.4 Correctness of the algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.4.1 The transitive closure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.4.2 Symbolic unfolding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.4.3 Soundness of the residualizing semantics . . . . . . . . . . . . . . . . . . . . 16

3 Application: the Knuth-Morris-Pratt algorithm 19

4 Related work 22

5 Perspectives 23 5.1 Computational effects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 5.2 Selective bounded static variation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 5.3 Resource-bounded partial evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . 23

6 Conclusion 24

1 Introduction

Partial evaluation is a program-transformation technique characterized by constant propagation and call unfolding [13, 33]. Given a program f(x,y)=e and a value c for x, a partial evaluator (also called a program specializer) generates a program, f_{c}(y)=e', equivalent to f'(y)=f(c,y). The usefulness of partial evaluation is that f_{c}(y)=e' may, due to optimizations enabled by fixing x= c, be significantly more efficient than f'(y)=f(c,y).

Consider the power function as an example. (It will also be used to illustrate some technical aspects about the main proof in Section 2.4.2.)

            power(n,x) = if (n=0) then 1 else x*(power(n-1,x))

Fixing n = 2, a partial evaluator generates:

            power_{2}(x) = x*(x*1)

In offline partial evaluation, the decision on what can and should be reduced is taken during a so-called binding-time-analysis prephase, and represented as annotations in the program. These annotations are then blindly followed in the subsequent specialization phase. The utility of this division was demonstrated by Jones’s group [34] in connection with compiler-generation by selfapplication of the specializer, an idea originally conceived by Futamura [24].

The above example is annotated as follows (with reducible terms in italics)

power(n,x) = if (n=0) then 1 else x*(power(n−1,x))

Note that it can be annotated before the value of n is chosen. Fixing n = 2, the result of specializing the annotated program is as above.

Polyvariant specialization allows recursive functions to be indexed by their fixed arguments, and was originally conceived in Ershov’s group [11].

In the example, we may thus choose to index the recursive calls to power by n, instead of symbolically unfolding them:

            power_{2}(x) = x*(power_{1}(x))
            power_{1}(x) = x*(power_{0}(x))
            power_{0}(x) = 1

Here, symbolic unfolding is probably to be preferred to remove the overhead of function calls. To see where polyvariance makes a difference, consider the following mutually-recursive functions:

            even(n,x) = if (x=0) then true  else odd (n+1,x-1)
            odd (n,x) = if (x=0) then false else even(n−1,x-1)

Fixing n = 2 for even, a monovariant specializer using symbolic unfolding would diverge, because each function unfolds to itself with only the dynamic arguments changed. To avoid nontermination, weaker binding-time annotations must be chosen (i.e., where all terms are annotated as dynamic); the result is trivial specialization:

            even_{2}(x)  = even(2,x)
            even(n,x) = if (x=0) then true  else odd (n+1,x-1)
            odd (n,x) = if (x=0) then false else even(n-1,x-1)

In contrast, a polyvariant specializer generates:

            even_{2}(x) = if (x=0) then true  else odd_{3}(x-1)
            odd_{3}(x)  = if (x=0) then false else even_{2}(x-1)

As a footnote, the tension between ensuring termination while avoiding trivial specialization is a major issue in partial evaluation [32].

Although the above example is short, the classical example where polyvariance makes a difference is the generation of the search phase of the efficient Knuth-Morris-Pratt algorithm [35] from an inefficient string matcher [12,26].

Outline

This work presents the first formal correctness proof of an offline polyvariant specialization algorithm for typed first-order recursive equations. We work in a call-by-value denotational setting [43], where our approach – inspired by type-directed partial evaluation [14, 19, 21] – is to phrase polyvariant specialization as a non-standard, code-generating semantics (also called a residualizing semantics). This approach immediately suggests certain proof principles, namely structural induction (by compositionality) and fixed-point induction.

A priori, two issues complicate the proof:

1. We must keep track of the polyvariant element, i.e., the transitive closure of needed specialized functions. This turns out to be relatively unproblematic and isolated.

2. We must ensure that the result of symbolic unfolding is well-typed and with the right meaning. A well-known complication is that symbolic unfolding necessitates α-renaming of letexpressions to avoid variable captures. Symbolic unfolding also turns out to destroy the obvious proof approach in the denotational setting.

As an application, the specialization algorithm is shown to generate a program implementing the search phase of the Knuth-Morris-Pratt algorithm from an inefficient, but binding-time-improved, string matcher.

2 Polyvariant specialization

2.1 A typed first-order language

We consider first-order recursive equations with a call-by-value denotational semantics [20, 43]. We use standard denotational concepts throughout the paper.

2.1.1 Syntax

The language is parameterized by a signature, Σ = (B, L, C). B is a set of base types, b; L maps base types to disjoint sets of literals, l ∈ L(b); and C maps function constants, c, to function types.

Types:

GTyp :  τ ::= b | bool  (Ground types)
FTyp :  σ ::= τ_{1} * … * τ_{n}->τ  (Function types)

Terms: Let x ∈ Var and f ∈ FVar denote variables. We define expressions, equations (or functions), declarations, and programs. A notable restriction is that arguments to function calls must be variables. This restriction simplifies the formal construction, because it will eliminate the need for the partial evaluator to insert lets to avoid unsound handling of computations [9]. Hence, we effectively require that source programs have already been let-inserted (even for literals, but here only to simplify the syntax).

Exp :  e ::= l | true | false | c(e_{1},…,e_{n}) | if e_{1} then e_{2} else e_{3} |
x | let x:τ_{1} ⇐ e_{1} in e_{2} | f(x_{1}, …,x_{n})
Eqn :  q ::= f:σ(x_{1}, …,x_{n})=e
Decl :  d ::= [q_{1}, …,q_{n}]
Pgm :  p ::= local d in f

Equation names are required to be distinct within a declaration and argument names are required to be distinct within each equation.

For any a, b ∈ ℕ, let [a..b] denote {a, a + 1, …, b} if a ≤ b, and ∅ if a > b.

2.1.2 Typing

Let Γ : Var → GTyp, and Ψ : FVar → FTyp be typing environments. We define a relation, Ψ, Γ ⊢ e : τ, asserting that e is a well-typed term of type τ, in the context of Ψ and Γ. Similarly, Ψ ⊢ q : (f, σ), ⊢ d : Ψ, and ⊢ p : σ.

Ψ, Γ ⊢ e : τ

\frac{l ∈ L(b)}{Ψ, Γ ⊢ l : b}

                                 Ψ, Γ ⊢ true : bool
                                 Ψ, Γ ⊢ false : bool

\frac{C(c) = τ_{1} * … * τ_{n}->τ ∀i∈[1..n]. Ψ, Γ ⊢ e_{i} : τ_{i}}{Ψ, Γ ⊢ c(e_{1},…,e_{n}) : τ}

\frac{Ψ, Γ ⊢ e_{1} : bool Ψ, Γ ⊢ e_{2} : τ Ψ, Γ ⊢ e_{3} : τ}{Ψ, Γ ⊢ if e_{1} then e_{2} else e_{3} : τ}

\frac{Γ(x) = τ}{Ψ, Γ ⊢ x : τ}

\frac{Ψ, Γ ⊢ e_{1} : τ_{1} Ψ, Γ[x ↦ τ_{1}] ⊢ e_{2} : τ_{2}}{Ψ, Γ ⊢ let x:τ_{1} ⇐ e_{1} in e_{2} : τ_{2}}

\frac{Ψ(f) = τ_{1} * … * τ_{n}->τ ∀i∈[1..n]. Γ(x_{i}) = τ_{i}}{Ψ, Γ ⊢ f(x_{1}, …,x_{n}) : τ}

Ψ ⊢ q : (f, σ) ; \frac{σ = τ_{1} * … * τ_{n}->τ Ψ, \{x_{i} ↦ τ_{i} | i∈[1..n]\} ⊢ e : τ}{Ψ ⊢ f:σ(x_{1}, …,x_{n})=e : (f, σ)}

⊢ d : Ψ

\frac{Ψ = \{f_{i} ↦ σ_{i} | i∈[1..n]\} ∀k ∈[1..n]. Ψ ⊢ q_{k} : (f_{k}, σ_{k})}{⊢ [q_{1}, …,q_{n}] : Ψ}

⊢ p : σ

\frac{Ψ(f) = σ ⊢ d : Ψ}{⊢ local d in f : σ}

2.1.3 Semantics

Let an interpretation of the signature, I_{Σ} = (B, L, C), be given. We require that B maps each base type to a discrete cpo of values; and that L maps literals to values such that for all l ∈ L(b), L(l) ∈ B(b). For simplicity, we assume that L is surjective; i.e., that for every value v ∈ B(b) we can find a literal l ∈ L(b) such that L(l) = v.

Meaning of types:

[[b]]= B(b)
[[bool]]= 𝔹 = {tt, ff}
[[τ_{1} * … * τ_{n}->τ]]= [[[τ_{1}]] × … × [[τ_{n}]] → [[τ]]_{⊥}]

Furthermore, for all function constants c ∈ dom C, we require that C(c) ∈ [[C(c)]]. The spectrum of computational effects is here thus limited to partiality [20,38].

Meaning of typing environments:

[[Γ]] = Π_{x∈dom Γ}[[Γ(x)]] = {ρ | dom ρ = dom Γ, ∀x ∈ dom Γ. ρ(x) ∈ [[Γ(x)]]}
[[Ψ]] = Π_{f∈dom Ψ}[[Ψ(f)]] = {ξ | dom ξ = dom Ψ, ∀f ∈ dom Ψ. ξ(f) ∈ [[Ψ(f)]]}

Note that [[Ψ]] is always a pointed cpo. We write ⌊·⌋ for the inclusion from A to A_{⊥}; and for f : A → B with B pointed, we write · † f for f’s strict extension to A_{⊥}, i.e., ⊥ † f = ⊥ and ⌊a⌋ † f = f a. Let further fix(·) denote the least-fixed-point operator.

Meaning of well-typed terms: If Ψ, Γ ⊢ e : τ, we define [[e]] ∈ [[[Ψ]] → [[[Γ]] → [[τ]]_{⊥}]]. Similarly, if Ψ ⊢ q : (f, σ) then [[q]] ∈ [[[Ψ]] → [[σ]]]; if ⊢ d : Ψ then [[d]] ∈ [[Ψ]]; and if ⊢ p : σ then [[p]] ∈ [[σ]].

[[l]] ξ ρ = ⌊L(l)⌋
[[true]] ξ ρ = ⌊tt⌋
[[false]] ξ ρ = ⌊ff⌋
[[c(e_{1},…,e_{n})]] ξ ρ = [[e_{1}]] ξ ρ † λv_{1}…. [[e_{n}]] ξ ρ † λv_{n}. C(c)(v_{1}, …, v_{n})
[[if e_{1} then e_{2} else e_{3}]] ξ ρ = [[e_{1}]] ξ ρ † λb. case b of \begin{cases}tt & → [[e_{2}]] ξ ρ \\ ff & → [[e_{3}]] ξ ρ \end{cases}
[[x]] ξ ρ = ⌊ρ(x)⌋
[[let x:τ_{1} ⇐ e_{1} in e_{2}]] ξ ρ = [[e_{1}]] ξ ρ † λv. [[e_{2}]] ξ ρ[x ↦ v]
[[f(x_{1}, …,x_{n})]] ξ ρ = ξ(f)(ρ(x_{1}), …, ρ(x_{n}))
[[f:σ(x_{1}, …,x_{n})=e]] ξ = λ(v_{1}, …, v_{n}). [[e]] ξ {x_{i} ↦ v_{i} | i∈[1..n]}

If ⊢ [q_{1}, …,q_{n}] : Ψ with ∀i∈[1..n]. Ψ ⊢ q_{i} : (f_{i}, σ_{i}), note that Φ : [[Ψ]] → [[Ψ]] below is indeed a continuous operator on a pointed cpo.

[[[q_{1}, …,q_{n}]]] = (\begin{matrix}let & Φ(ξ) = \{f_{i} ↦ [[q_{i}]] ξ | i∈[1..n]\} \\ in & fix(Φ) \end{matrix} )
[[local d in f]] = [[d]](f)

We shall need some standard weakening properties:

Lemma 1 (weakening) If Ψ, Γ ⊢ e : τ and f ∉ dom Ψ then for all σ ∈ FTyp,

1. Ψ[f ↦ σ], Γ ⊢ e : τ

2. ∀g ∈ [[σ]]. [[e]] ξ ρ = [[e]] ξ[f ↦ g] ρ

Proof: Straightforward, by structural induction. □

Lemma 2 (weakening) If Ψ ⊢ q : (f′, σ′) and f ∉ dom Ψ then for all σ ∈ FTyp,

1. Ψ[f ↦ σ] ⊢ q : (f′, σ′)

2. ∀g ∈ [[σ]]. [[q]] ξ = [[q]] ξ[f ↦ g]

Proof: Follows directly from Lemma 1. □

2.2 A binding-time-annotated language

We introduce a binding-time-annotated variant of the typed first-order language. The annotations are intended to direct the specialization algorithm. As traditional we overline static constructs (understood as “to be evaluated”) and underline dynamic ones (understood as “to be residualized”).

2.2.1 Syntax

The annotated language is given with respect to the original signature, Σ = (B, L, C). Distinctness of argument and function names is again assumed.

Types:

{ \atop GTyp} :  τ̂::= \overline{τ} | \underline{τ}  (Ground types)
{ \atop FTyp} :  σ̂ ::= τ̂_{1} * … * τ̂_{n}->τ̂  (Function types)

Terms:

Êxp :  ê::= \overline{l} | \overline{true} | \overline{false} | \overline{c}(ê_{1},…,ê_{n}) | \overline{if} ê_{1} \overline{then} ê_{2} \overline{else} ê_{3} |
x | \overline{let} x:τ̂_{1} ⇐ ê_{1} \overline{in} ê_{2} | \overline{f}(x_{1}, …,x_{n})
$_{τ} ê | \underline{c}(ê_{1},…,ê_{n}) | \underline{if} ê_{1} \underline{then} ê_{2} \underline{else} ê_{3} |
\underline{let} x:τ̂_{1} ⇐ ê_{1} \underline{in} ê_{2} | \underline{f}(x_{1}, …,x_{n})
Êqn :  q̂::= f:σ̂(x_{1}, …,x_{n})=ê
D̂ecl :  d̂::= [q̂_{1}, …,q̂_{n}]
{ \atop Pgm} :  p̂::= local d̂in f

2.2.2 Typing

Let Γ̂ : Var → { \atop GTyp}, and Ψ̂ : FVar → { \atop FTyp} be typing environments. Well-typed terms (whose binding-time annotations are called congruent [33]) are defined analogously to before. We distinguish the three possible annotations for a function call: “to be unfolded” (evaluated), “to be symbolically unfolded” (reduced), or “to be residualized” (rebuilt).

Ψ̂, Γ̂ ⊢ ê: τ̂

\frac{l ∈ L(b)}{Ψ̂, Γ̂ ⊢ \overline{l} : \overline{b}}

                                 Ψ̂, Γ̂ ⊢ \overline{true} : \overline{bool}
                                 Ψ̂, Γ̂ ⊢ \overline{false} : \overline{bool}

\frac{C(c) = τ_{1} * … * τ_{n}->τ ∀i∈[1..n]. Ψ̂, Γ̂ ⊢ ê_{i} : \overline{τ}_{i}}{Ψ̂, Γ̂ ⊢ \overline{c}(ê_{1},…,ê_{n}) : \overline{τ}}

Ψ̂, Γ̂ ⊢ ê_{1} : \overline{bool} Ψ̂, Γ̂ ⊢ ê_{2} : τ̂ Ψ̂, Γ̂ ⊢ ê_{3} : τ̂

Ψ̂, Γ̂ ⊢ \overline{if} ê_{1} \overline{then} ê_{2} \overline{else} ê_{3} : τ̂

\frac{Γ̂(x) = τ̂}{Ψ̂, Γ̂ ⊢ x : τ̂}

\frac{Ψ̂(f) = \overline{τ}_{1}* … *\overline{τ}_{n}->\overline{τ} ∀i∈[1..n]. Γ̂(x_{i}) = \overline{τ}_{i}}{Ψ̂, Γ̂ ⊢ \overline{f}(x_{1}, …,x_{n}) : \overline{τ}}

\frac{Ψ̂, Γ̂ ⊢ ê_{1} : \overline{τ}_{1} Ψ̂, Γ̂[x ↦ \overline{τ}_{1}] ⊢ ê_{2} : τ̂_{2}}{Ψ̂, Γ̂ ⊢ \overline{let} x:\overline{τ}_{1} ⇐ ê_{1} \overline{in} ê_{2} : τ̂_{2}}

\frac{Ψ̂(f) = τ̂_{1}* … *τ̂_{n}->\underline{τ} ∀i∈[1..n]. Γ̂(x_{i}) = τ̂_{i}}{Ψ̂, Γ̂ ⊢ \overline{f}(x_{1}, …,x_{n}) : \underline{τ}}

\frac{Ψ̂, Γ̂ ⊢ ê: \overline{τ}}{Ψ̂, Γ̂ ⊢ $_{τ} ê: \underline{τ}}

\frac{C(c) = τ_{1} * … * τ_{n}->τ ∀i∈[1..n]. Ψ̂, Γ̂ ⊢ ê_{i} : \underline{τ}_{i}}{Ψ̂, Γ̂ ⊢ \underline{c}(ê_{1},…,ê_{n}) : \underline{τ}}

\frac{Ψ̂, Γ̂ ⊢ ê_{1} : \underline{bool} Ψ̂, Γ̂ ⊢ ê_{2} : \underline{τ} Ψ̂, Γ̂ ⊢ ê_{3} : \underline{τ}}{Ψ̂, Γ̂ ⊢ \underline{if} ê_{1} \underline{then} ê_{2} \underline{else} ê_{3} : \underline{τ}}

\frac{Ψ̂, Γ̂ ⊢ ê_{1} : \underline{τ}_{1} Ψ̂, Γ̂[x ↦ \underline{τ}_{1}] ⊢ ê_{2} : \underline{τ}_{2}}{Ψ̂, Γ̂ ⊢ \underline{let} x:\underline{τ}_{1} ⇐ ê_{1} \underline{in} ê_{2} : \underline{τ}_{2}}

\frac{Ψ̂(f) = τ̂_{1}* … *τ̂_{n}->\underline{τ} ∀i∈[1..n]. Γ̂(x_{i}) = τ̂_{i}}{Ψ̂, Γ̂ ⊢ \underline{f}(x_{1}, …,x_{n}) : \underline{τ}}

Ψ̂ ⊢ q̂: (f, σ̂) ; \frac{σ̂ = τ̂_{1} * … * τ̂_{n}->τ̂ Ψ̂, \{x_{i} ↦ τ̂_{i} | i∈[1..n]\} ⊢ ê: τ̂}{Ψ̂ ⊢ f:σ̂(x_{1}, …,x_{n})=ê: (f, σ̂)}

⊢ d̂: Ψ̂

\frac{Ψ̂ = \{f_{i} ↦ σ̂_{i} | i∈[1..n]\} ∀k ∈[1..n]. Ψ̂ ⊢ q̂_{k} : (f_{k}, σ̂_{k})}{⊢ [q̂_{1}, …,q̂_{n}] : Ψ̂}

⊢ p̂: σ̂

\frac{Ψ̂(f) = σ̂ = τ̂_{1}* … *τ̂_{n}->\underline{τ} ⊢ d̂: Ψ̂}{⊢ local d̂in f : σ̂}

Note that the typing rules disallow functions to be annotated with a static return type but dynamic arguments, since the dynamic arguments cannot currently be used in any meaningful way. In the presence of bounded static variation [33], however, this situation would change (see also Section 5.2).

2.2.3 Semantics

The intended standard semantics of the binding-time-separated language is virtually identical to the previous semantics, simply ignoring binding-time annotations and interpreting $ as identity.

This can be straightforwardly formalized as a family of erasure translations, ∥·∥, on types, terms, and typing environments, taking each construct to its unannotated counterpart. For example,

∥\underline{let} x:\underline{τ}_{1} ⇐ ê_{1} \underline{in} ê_{2}∥ = let x:τ_{1} ⇐ ∥ê_{1}∥ in ∥ê_{2}∥ and ∥$_{τ} ê∥ = ∥ê∥.

It is easy to show that well-typedness is preserved. The meaning of each annotated construct is then simply the meaning of its erasure.

The role of binding-time analysis In our formulation, a (monovariant) binding-time analyzer, bta(·) : Pgm × { \atop FTyp} → { \atop Pgm}, is thus a function satisfying that if σ̂ = τ̂_{1}* … *τ̂_{n}->\underline{τ} and ⊢ p : ∥σ̂∥ then ⊢ bta(p, σ̂) : σ̂ and ∥bta(p, σ̂)∥ = p. In particular, a binding-time analyzer must preserve meanings.

Of course, one can also write programs in { \atop Pgm} directly; writing such programs is for example done when writing macros [5].

2.3 The specialization algorithm

We define polyvariant specialization as a non-standard, residualizing semantics.

2.3.1 Notation

For residualized function calls, we need some notation that lets us separate static and dynamic arguments. Given σ̂ = τ̂_{1} * … * τ̂_{n}->\underline{τ}, we define the index of the i’th static argument, (i)\overline{σ̂}, and of the i’th dynamic argument, (i)\underline{σ̂}. For example, if σ̂ = \overline{b}_{1}*\underline{b}_{2}*\overline{b}_{3}->\underline{b} then (1)\overline{σ̂} = 1,(2)\overline{σ̂} = 3, and (1)\underline{σ̂} = 2. We formalize these indices as follows. Let first the predicates

\begin{aligned}S(τ̂) & ⇔ (∃τ. τ̂ = \overline{τ}), & S(σ̂) & ⇔ (∃τ̂_{1}, …, τ̂_{n}, τ. σ̂ = τ̂_{1} * … * τ̂_{n}->\overline{τ}) \\ D(τ̂) & ⇔ (∃τ. τ̂ = \underline{τ}), & D(σ̂) & ⇔ (∃τ̂_{1}, …, τ̂_{n}, τ. σ̂ = τ̂_{1} * … * τ̂_{n}->\underline{τ}) \end{aligned}

assert that a given type is static or dynamic, respectively. For any function type σ̂ = τ̂_{1}* … *τ̂_{n}->\underline{τ}, let |\overline{σ̂}| = |\{i ∈ [1..n] | S(τ̂_{i})\}| and |\underline{σ̂}| = |\{i ∈ [1..n] | D(τ̂_{i})\}| be the number of static and dynamic arguments, resp. Note that it is always the case that |\overline{σ̂}| + |\underline{σ̂}| = n. Define then

∀i∈[1..|\overline{σ̂}|], (i)\overline{σ̂} = min k ∈[1..n] s.t. (|\{j ∈[1..k] | S(τ̂_{j})\}| = i)
∀i∈[1..|\underline{σ̂}|], (i)\underline{σ̂} = min k ∈[1..n] s.t. (|\{j ∈[1..k] | D(τ̂_{j})\}| = i)

Given a function type σ̂, let further curryσ̂ generalize the standard binary ‘curry’ combinator, i.e., curry = λf.λx.λy.f(x, y), to static and dynamic arguments. For example, if σ̂ = \overline{b}_{1}*\underline{b}_{2}*\overline{b}_{3}->\underline{b} then curryσ̂ = λf. λ(x_{1}, x_{3}). λx_{2}. f(x_{1}, x_{2}, x_{3}). We define curryσ̂ by

curryσ̂ = λf. λ(v_{1}, …, v_{k}). λ(w_{1}, …, w_{k′}). f(u_{1}, …, u_{n})
where ∀j ∈[1..n]. (u_{j} = v_{i} ⇔ (i)\overline{σ̂} = j) ∧ (u_{j} = w_{i} ⇔ (i)\underline{σ̂} = j)

Now, given a function type σ̂ = τ̂_{1}* … *τ̂_{n}->\underline{τ}, let

\underline{σ̂} = τ̂_{(1)\underline{σ̂}}* … *τ̂_{(|\underline{σ̂}|)\underline{σ̂}}->\underline{τ}

be its residual type (i.e., σ̂ without the static arguments). Also, let (by slight abuse of notation, since we do not have product types)

[[∥\overline{σ̂}∥]] = [[∥τ̂_{(1)\overline{σ̂}}∥]] × … × [[∥τ̂_{(|\overline{σ̂}|)\overline{σ̂}}∥]]

be the set of σ̂’s evaluated static arguments.

We assume convenient names for specialized functions, i.e., f_{(v_{1},...,v_{k})}, in FVar. Let

FVar Ψ̂ = \{f_{(v_{1},...,v_{k})} | f ∈ dom Ψ̂, (v_{1}, …, v_{k}) ∈ [[∥\overline{Ψ̂(f)}∥]]\}

be the well-formed residual function names in the context of Ψ̂.

In the polyvariant specializer, the residualized function calls will refer to such residual function names. Hence, we need some notation to specify the contexts in which residualized terms are to be given meaning. We extend the notions of residual function types and currying to environments. If Ψ̂, X ⊆_{fin} FVar Ψ̂, and ξ ∈ [[∥Ψ̂∥]], let

\underline{Ψ̂}(X) = \{f_{(v_{1},...,v_{k})} ↦ \underline{Ψ̂(f)} | D(Ψ̂(f)), f_{(v_{1},...,v_{k})} ∈ X\}
curryΨ̂(ξ)(X) = {f_{(v_{1},...,v_{k})} ↦ curry_{Ψ̂(f)}(ξ(f))(v_{1}, …, v_{k}) | D(Ψ̂(f)), f_{(v_{1},...,v_{k})} ∈ X}

Note that curryΨ̂(ξ)(X) ∈ [[∥\underline{Ψ̂}(X)∥]].

2.3.2 State and effects

The residualizing semantics is phrased in so-called monadic style. We use a specific state monad to support the bookkeeping involved, layered on top of partiality (recall that partiality is the computational effect of the original language). A notable simplification of this bookkeeping is the convenient names for specialized functions, i.e., f_{(v_{1},...,v_{k})}, in FVar. Hence, we can recover the static argument values from the name of a specialized function. Accordingly, let

Δ = {{i ↦ i, seen ↦ s, pen ↦ p, res ↦ d} | i ∈ ℕ, s ∈ P_{fin}(FVar), p ∈ FVar list, d ∈ Decl}

be the cpo of states, where P_{fin}(FVar) is discretely ordered. Hence, Δ is a discrete cpo. The intended reading is that i is a counter for generating “fresh” names; seen is the set of (names of) visited equations (the so-called ‘déjà-vu’ or ‘seen-before’ list); pen is the worklist of (names of) visited but not generated equations (the so-called ‘pending’ list); and res is the generated equations.

We will find it convenient to allow manipulation of declarations as if they were lists. Also, if d = [q_{1}, …,q_{n}], and q_{i} = f_{i}:σ_{i}(x_{1}, …,x_{n})=e_{i} for all i∈[1..n], let dom d = {f_{1}, …, f_{n}} denote the set of function names.

For all cpos A and B and f ∈ [A → T B], we define

T A  = [Δ → (A × Δ)_{⊥}]
η_{A} : A → T A = λa. λδ. ⌊(a, δ)⌋
· ⋆ f : T A → T B = λt. λδ. (t δ † λ(a, δ′). f a δ′)

For static computations we need to transfer answers. This is accomplished via the monad morphism γ_{T} : A_{⊥} → T A defined as γ_{T} (v) = v † η. Note that if t δ = ⌊(a, δ)⌋ and t = γ_{T} (v) then v = ⌊a⌋. For the purpose of unique name generation, let {y_{0}, y_{1}, ...} be a countably-infinite subset of Var, such that y_{i} = y_{j} implies i = j.

We define

new : T Var  = λδ. ⌊(y_{δ(i)}, δ[i ↦ δ(i) + 1])⌋
visit : FVar → T 1 = λf. λδ. case f ∈ δ(seen) of \begin{cases}tt & → ⌊(∗, δ)⌋ \\ ff & → ⌊(∗, δ [ \begin{matrix}seen ↦ δ(seen) ∪ \{f\}, \\ pen ↦ f::δ(pen) \end{matrix} ])⌋ \end{cases}
commit : Eqn → T 1 = λq. λδ. ⌊(∗, δ[res ↦ q::δ(res)])⌋
next : T (1 + FVar) = λδ. case δ(pen) of \begin{cases}f::X & → ⌊(in_{2}(f), δ[pen ↦ X])⌋ \\ nil & → ⌊(in_{1}(∗), δ)⌋ \end{cases}
result : T Decl  = λδ. ⌊(δ(res), δ)⌋

These operations will provide adequate support for the bookkeeping involved with the polyvariant element of specialization. new returns a “fresh” variable name; visit(f) schedules f for residualization (if it has not been already); commit(q) appends q to the result (where the name of q is assumed to have been visited); next returns (and removes) the head of the pending list; and result returns the generated (i.e., committed) equations.

2.3.3 The residualizing semantics

Recall that in the source language, arguments to function calls are required to be syntactic variables. We slightly restrict the meaning of types to ensure this. Define first:

\begin{aligned}[[\overline{τ}]]_{V} & = [[τ]] \\ [[\underline{τ}]]_{V} & = Var \end{aligned}

Meaning of types:

[[\overline{τ}]]_{R} = [[τ]]
[[\underline{τ}]]_{R} = Exp
[[τ̂_{1} * … * τ̂_{n}->τ̂]]_{R} = [[[τ̂_{1}]]_{V} × … × [[τ̂_{n}]]_{V} → T [[τ̂]]_{R}]

Meaning of typing environments:

[[Γ̂]]_{R} = Π_{x∈dom Γ̂}[[Γ̂(x)]]_{R} = {ρ̂ | dom ρ̂ = dom Γ̂, ∀x ∈ dom Γ̂. ρ̂(x) ∈ [[Γ̂(x)]]_{V}}
[[Ψ̂]]_{R} = Π_{f∈dom Ψ̂}[[Ψ̂(f)]]_{R} = {ξ̂ | dom ξ̂ = dom Ψ̂, ∀f ∈ dom Ψ̂. ξ̂(f) ∈ [[Ψ̂(f)]]_{R}}

We previously assumed that each base value was represented by a literal (an extension to booleans is trivial); we now let ↓_{τ} (·) : [[τ]] → Exp pick particular such literals, i.e., for every a ∈ [[τ]], if ↓_{τ} (a) = l then [[l]] ξ ρ = ⌊a⌋.

Meaning of well-typed terms: If Ψ̂, Γ̂ ⊢ ê : τ̂, we define [[ê]]_{R} ∈ [[[Ψ̂]]_{R} → [[[Γ̂]]_{R} → T [[τ̂]]_{R}]]. Note that the only effectful operations used are new and visit.

[[\overline{l}]]_{R} ξ̂ρ̂ = η(L(l))
[[\overline{true}]]_{R} ξ̂ρ̂ = η(tt)
[[\overline{false}]]_{R} ξ̂ρ̂ = η(ff)
[[\overline{c}(ê_{1},…,ê_{n})]]_{R} ξ̂ρ̂ = [[ê_{1}]]_{R} ξ̂ρ̂⋆ λv_{1}…. [[ê_{n}]]_{R} ξ̂ρ̂⋆ λv_{n}.

γ_{T} (C(c)(v_{1}, …, v_{n}))

[[\overline{if} ê_{1} \overline{then} ê_{2} \overline{else} ê_{3}]]_{R} ξ̂ρ̂ = [[ê_{1}]]_{R} ξ̂ρ̂⋆ λb. case b of \begin{cases}tt & → [[ê_{2}]]_{R} ξ̂ρ̂ \\ ff & → [[ê_{3}]]_{R} ξ̂ρ̂ \end{cases}
[[x]]_{R} ξ̂ρ̂ = η(ρ̂(x))
[[\overline{let} x:τ̂_{1} ⇐ ê_{1} \overline{in} ê_{2}]]_{R} ξ̂ρ̂ = [[ê_{1}]]_{R} ξ̂ρ̂⋆ λv. [[ê_{2}]]_{R} ρ̂[x ↦ v]

[[\overline{f}(x_{1}, …,x_{n})]]_{R} ξ̂ρ̂ = ξ̂(f)(ρ̂(x_{1}), …, ρ̂(x_{n}))
[[$_{τ} ê]]_{R} ξ̂ρ̂ = [[ê]]_{R} ξ̂ρ̂⋆ λv. η(↓_{τ} (v))
[[\underline{c}(ê_{1},…,ê_{n})]]_{R} ξ̂ρ̂ = [[ê_{1}]]_{R} ξ̂ρ̂⋆ λe_{1}…. [[ê_{n}]]_{R} ξ̂ρ̂⋆ λe_{n}.
η(c(e_{1},…,e_{n}))
[[\underline{if} ê_{1} \underline{then} ê_{2} \underline{else} ê_{3}]]_{R} ξ̂ρ̂ = [[ê_{1}]]_{R} ξ̂ρ̂⋆ λe_{1}. [[ê_{2}]]_{R} ξ̂ρ̂⋆ λe_{2}. [[ê_{3}]]_{R} ξ̂ρ̂⋆ λe_{3}.

                                   η(if e_{1} then e_{2} else e_{3})

[[\underline{let} x:\underline{τ}_{1} ⇐ ê_{1} \underline{in} ê_{2}]]_{R} ξ̂ρ̂ = new ⋆ λy. [[ê_{1}]]_{R} ξ̂ρ̂⋆ λe_{1}. [[ê_{2}]]_{R} ξ̂ρ̂[x ↦ y] ⋆ λe_{2}.
η(let y:τ_{1} ⇐ e_{1} in e_{2})

If Ψ̂, Γ̂ ⊢ \underline{f}(x_{1}, …,x_{n}) : \underline{τ} with Ψ̂(f) = σ̂ then

\begin{aligned}[[\underline{f}(x_{1}, …,x_{n})]]_{R} ξ̂ρ̂ & = visit(f_{(ρ̂(x_{(1)\overline{σ̂}}),...,ρ̂(x_{(|\overline{σ̂}|)\overline{σ̂}}))}) ⋆ λu. \\ & η(f_{(ρ̂(x_{(1)\overline{σ̂}}),...,ρ̂(x_{(|\overline{σ̂}|)\overline{σ̂}}))}(ρ̂(x_{(1)\underline{σ̂}}), …,ρ̂(x_{(|\underline{σ̂}|)\underline{σ̂}}))) \end{aligned}

Recall above that ρ̂(x_{(1)\overline{σ̂}}) … ρ̂(x_{(|\overline{σ̂}|)\overline{σ̂}}) is simply the values of the static arguments, and ρ̂(x_{(1)\underline{σ̂}}) … ρ̂(x_{(|\underline{σ̂}|)\underline{σ̂}}) are the values (which must be variables due to [[·]]_{V}) of the dynamic arguments.

If Ψ̂ ⊢ q̂: (f, σ̂) we define [[q̂]]_{R} ∈ [[[Ψ̂]]_{R} → [[σ̂]]_{R}] by

[[f:σ̂(x_{1}, …,x_{n})=ê]]_{R} ξ̂ = λ(v_{1}, …, v_{n}). [[ê]]_{R} ξ̂{x_{i} ↦ v_{i} | i∈[1..n]}

Since the residualized meaning of a dynamic equation is an expression-generating function, we shall need a way to convert it to an equation. All we need is a function name, some distinct variables (fresh variables are fine), and some values: if D(σ̂) and g ∈ [[σ̂]]_{R}, we define ↓σ̂ (g)(·, ·) ∈ [(FVar × [[∥\overline{σ̂}∥]]) → T Eqn] by

↓σ̂ (g)(f, (v_{1}, …, v_{k})) = new ⋆ λx_{1}…. new ⋆ λx_{k′}. curryσ̂(g)(v_{1}, …, v_{k})(x_{1}, …, x_{k′}) ⋆ λe.
η(f:\underline{σ̂}(x_{1}, …,x_{k′})=e)

The output, if any, is the corresponding residual equation (note that the use of curryσ̂(g) is inessential, it is only a convenient way to properly merge the static and dynamic arguments).

If ⊢ [q̂_{1}, …,q̂_{n}] : Ψ̂ where (∀i∈[1..n]. Ψ̂ ⊢ q̂_{i} : (f_{i}, σ̂_{i})), we define [[d̂]]_{R} ∈ [[Ψ̂]]_{R} by

[[[q̂_{1}, …,q̂_{n}]]]_{R} = (\begin{matrix}let & Φ̃(ξ̂) = \{f_{i} ↦ [[q̂_{i}]]_{R} ξ̂| i∈[1..n]\} \\ in & fix(Φ̃) \end{matrix} )

We can now define our polyvariant specialization algorithm. The central part is the computation of the transitive closure of visited functions.

If ξ̂ ∈ [[Ψ̂]]_{R}, the transitive closure, closeΨ̂(ξ̂) : T Decl, is defined as follows. Let Φ be the underlying operator:

Φ(F) = next ⋆ λs. case s of \begin{cases}in_{1}(∗) & → result \\ in_{2}(f_{(v_{1},...,v_{k})}) & → ↓_{Ψ̂(f)} (ξ̂(f))(f_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k})) ⋆ λq. \\ & commit(q) ⋆ F \end{cases}

Define then

closeΨ̂(ξ̂) = fix(Φ)

It is a simple worklist algorithm, where the pending list is processed. The output, if any, is a declaration consisting of a self-contained finite set of specialized functions.

Let δ_{0} = {i ↦ 0, seen ↦ ∅, pen ↦ nil, res ↦ nil} be the initial state. If ⊢ p̂: σ̂, we define [[p̂]]_{R} ∈ [[[∥\overline{σ̂}∥]] → Pgm_{⊥}] by

[[local d̂in f]]_{R} (v_{1}, …, v_{k}) =
(visit(f_{(v_{1},...,v_{k})}) ⋆ λu. closeΨ̂([[d̂]]_{R})) δ_{0} † λ(d, δ). ⌊local d in f_{(v_{1},...,v_{k})}⌋

We will show our putative polyvariant specializer to be sound; i.e., if ⊢ p̂: σ̂ and [[p̂]]_{R}(v_{1}, …, v_{k}) = ⌊p⌋ then ⊢ p : \underline{σ̂} and [[p]] = curryσ̂([[∥p̂∥]])(v_{1}, …, v_{k}). Since the specializer blindly follows annotations, it may easily diverge. Under certain conditions, however, we can guarantee termination.

2.4 Correctness of the algorithm

The main contribution of this work, namely the proof, is quite technical. This is large due to the two major complications: keeping track of the transitive closure and taming symbolic unfolding.

2.4.1 The transitive closure

We need to keep tight control with the state, as it is passed around, to prove that closeΨ̂(ξ̂) will actually compute a transitive closure. Informally, everything will run smoothly if (1) the generation of the equations uses only new and visit (i.e., does not corrupt the bookkeeping); and (2) the initial state is not already corrupted.

To specify that only new and visit are used, we define the set of simple extensions of a state,

extΨ̂(δ) = \{δ′ | \begin{matrix}∃i ≥ δ(i). ∃f_{1}, …, f_{n} ∈ FVar Ψ̂, n ≥ 0. \\ (visit(f_{1}) ⋆ λu. … ⋆ visit(f_{n})) δ[i ↦ i] = ⌊(∗, δ′)⌋ \end{matrix} \}

Note that simple extensions are transitive: if δ′ ∈ extΨ̂(δ) and δ′′ ∈ extΨ̂(δ′) then δ′′ ∈ extΨ̂(δ).

We define a state δ to be well-formed, written wellΨ̂(δ), if the elements of δ(pen), P, are all distinct, P ∪ dom δ(res) = δ(seen) ⊆ FVar Ψ̂, and P ∩ dom δ(res) = ∅. For any typing context Ψ̂, the initial state is well-formed; and so are its simple extensions: if δ ∈ extΨ̂(δ_{0}) then wellΨ̂(δ).

Operationally, the computation of closeΨ̂(ξ̂) can be thought of as progressing through a series of well-formed states, which we will call the well-formed extensions, defined by

wextΨ̂(δ) = \{δ′ | \begin{matrix}∃δ′′ ∈ extΨ̂(δ), q_{1}, …, q_{n}, n ≥ 0, wellΨ̂(δ), wellΨ̂(δ′), wellΨ̂(δ′′). # δ′′(pen) ≥ n \\ ∧ (next ⋆ λs_{1}. commit(q_{1}) … next ⋆ λs_{n}. commit(q_{n})) δ′′ = ⌊(∗, δ′)⌋ \end{matrix} \}

where # l denotes the length of a list l. Also these extensions are transitive: if δ′ ∈ wextΨ̂(δ) and δ′′ ∈ wextΨ̂(δ′) then δ′′ ∈ wextΨ̂(δ).

We will now prove that if closeΨ̂(ξ̂) terminates then the result is indeed a transitive closure.

Lemma 3 If ⊢ d̂: Ψ̂, (visit(f) ⋆ λu. closeΨ̂(ξ̂)) δ_{0} = ⌊(d, δ′)⌋, and

∀q, f, (v_{1}, …, v_{k}), δ′′, δ′′′. (↓_{Ψ̂(f)} (ξ̂(f))(f_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k})) δ′′ = ⌊(q, δ′′′)⌋) ⇒ δ′′′ ∈ extΨ̂(δ′′)

then δ′ ∈ wextΨ̂(δ_{0}), δ′(res) = d, δ′(seen) = dom d, and ∀q ∈ δ′(res). ∃f, (v_{1}, …, v_{k}), δ′′, δ′′′.

1. ↓_{Ψ̂(f)} (ξ̂(f))(f_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k})) δ′′ = ⌊(q, δ′′′)⌋

2. δ′ ∈ wextΨ̂(δ′′′).

Proof: By fixed-point induction. Define the predicate P ⊆ T Decl by

P = \{F | \begin{matrix}∀d̂, Ψ̂, d, δ, δ′, ξ̂. \\ if ⊢ d̂: Ψ̂, wellΨ̂(δ), F (δ) = ⌊(d, δ′)⌋, and \\ a. ∀q, f, (v_{1}, …, v_{k}), δ′′, δ′′′. \\ (↓_{Ψ̂(f)} (ξ̂(f))(f_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k})) δ′′ = ⌊(q, δ′′′)⌋) ⇒ δ′′′ ∈ extΨ̂(δ′′) \\ b. ∀q ∈ δ(res). ∃f, (v_{1}, …, v_{k}), δ′′, δ′′′. \\ ↓_{Ψ̂(f)} (ξ̂(f))(f_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k})) δ′′ = ⌊(q, δ′′′)⌋ ∧ δ′ ∈ wextΨ̂(δ′′′) \\ then δ′ ∈ wextΨ̂(δ), δ′(res) = d, δ′(seen) = dom d, and \\ ∀q ∈ δ′(res). ∃f, (v_{1}, …, v_{k}), δ′′, δ′′′. \\ 1. ↓_{Ψ̂(f)} (ξ̂(f))(f_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k})) δ′′ = ⌊(q, δ′′′)⌋ \\ 2. δ′ ∈ wextΨ̂(δ′′′) \end{matrix} \} .

P is clearly pointed; it is also easily verified to be inclusive, noting that any ω-chain F_{i} will eventually stabilize for each δ due to T Decl = [Δ → (Decl × Δ)_{⊥}] being a function space with a flat co-domain. Note that condition (a.) simply require that the generation of the equations use only new and visit, and condition (b.) is only needed to make the induction go through. The lemma follows by fixed-point induction on P, using the operator Φ underlying closeΨ̂(ξ̂). □

For concrete applications, we shall also need to prove that computing the transitive closure actually terminates, if there is a finite bound X for visited functions for each set of given static parameter values (and the generation of residual functions from X does not diverge). To support the Knuth-Morris-Pratt application in Section 3, where we also want to specify size bounds of the generated programs, a simple – although technical – lemma is the most convenient:

Lemma 4 If ⊢ d̂: Ψ̂, X ⊆_{fin} FVar Ψ̂, and ∀f_{(v_{1},...,v_{k})} ∈ X, δ. (δ(seen) ⊆ X) ⇒ ∃q, δ′.

1. ↓_{Ψ̂(f)} (ξ̂(f))(f_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k})) δ = ⌊(q, δ′)⌋ ∧ δ′ ∈ extΨ̂(δ)

2. δ′(seen) ⊆ X,

then ∀δ. (δ(seen) ⊆ X ∧ wellΨ̂(δ)) ⇒ ∃d, δ′. closeΨ̂(ξ̂) δ = ⌊(d, δ′)⌋ ∧ δ′(seen) ⊆ X.

Proof: Assume that the premise holds, and let δ be given. The lemma follows by mathematical induction on |X − δ(res)|. □

Of course, finding such a finite X is undecidable in general.

2.4.2 Symbolic unfolding

Symbolic unfolding turns out to be the main source of complication, for three reasons:

1. Renaming of bound variables had to be included and must be sound (captured as ≲ ).

2. The result of unfolding must be correct (captured as ⪅ ).

3. Soundness can not be established equationally by fixed-point induction (complicating ⪅ ).

We will first consider renaming of variables. It will be useful to recall the symbolic unfolding case from the residualizing semantics:

[[\overline{f}(x_{1}, …,x_{n})]]_{R} ξ̂ρ̂ = ξ̂(f)(ρ̂(x_{1}), …, ρ̂(x_{n}))

Here ξ̂(f) is an expression-generating function. First, we must ensure that ξ̂(f) is given sound arguments (e.g., to ensure that generated expressions are not untypable).

Given Γ̂, ρ̂ ∈ [[Γ̂]]_{R}, and ρ ∈ [[∥Γ̂∥]], we define

ρ̂ ≲i ; Γ̂ ρ ⇔ (∀x ∈ dom Γ̂. S(Γ̂(x)) ⇒ ρ̂(x) = ρ(x)) ∧
(∀x ∈ dom Γ̂. D(Γ̂(x)) ⇒ ρ̂(x) ∉ {y_{i}, y_{i+1}, …}) ∧
∀x, y ∈ dom Γ̂. ρ̂(x) = ρ̂(y) ⇒ (Γ̂(x) = Γ̂(y) ∧ ρ(x) = ρ(y))

Thus, ρ̂ ≲i ; Γ̂ ρ asserts that ρ̂ is consistent with ρ, in the sense that ρ can be obtained from ρ̂ by assigning values to its variables (which must not clash with name generation).

If ρ̂ ≲i ; Γ̂ ρ, let

Γ̂_{α}(ρ̂) = {ρ̂(x) ↦ Γ̂(x) | x ∈ dom Γ̂, D(Γ̂(x))}
ρΓ̂ ; α(ρ̂) = {ρ̂(x) ↦ ρ(x) | x ∈ dom Γ̂, D(Γ̂(x))}

These functions propagate types and values through the α-renaming defined by ρ̂, that is, they describe how typing and value environments are transformed to apply to the generated expression. They are well-defined by ρ̂’s consistency with ρ. Note that ρΓ̂ ; α(ρ̂) ∈ [[∥Γ̂_{α}(ρ̂)∥]] and that static types and values are not propagated.

We shall need the following simple properties about ≲ .

Lemma 5 If ρ̂ ≲i ; Γ̂ ρ then

1. if j > i then ρ̂ ≲j ; Γ̂ ρ.

2. if v ∈ [[τ]] then (a) ρ̂[x ↦ v] ≲_{Γ̂[x↦\overline{τ}]}^{i} ρ[x ↦ v]

(b) Γ̂[x ↦ \overline{τ}]_{α}(ρ̂[x ↦ v]) = Γ̂_{α}(ρ̂)

(c) ρ[x ↦ v]_{α}^{Γ̂[x↦\overline{τ}]}(ρ̂[x ↦ v]) = ρΓ̂ ; α(ρ̂)

3. if v ∈ [[τ]] then

(a) ρ̂[x ↦ y_{i}] ≲_{Γ̂[x↦\underline{τ}]}^{i+1} ρ[x ↦ v]

(b) Γ̂[x ↦ \underline{τ}]_{α}(ρ̂[x ↦ y_{i}]) = (Γ̂_{α}(ρ̂))[y_{i} ↦ \underline{τ}]

(c) ρ[x ↦ v]_{α}^{Γ̂[x↦\underline{τ}]}(ρ̂[x ↦ y_{i}]) = (ρΓ̂ ; α(ρ̂))[y_{i} ↦ v]

4. if x ∈ dom Γ̂ then Γ̂_{α}(ρ̂)(ρ̂(x)) = Γ̂(x) and ρΓ̂ ; α(ρ̂)(ρ̂(x)) = ρ(x).

5. if (∀j ∈[1..n]. x_{j} ∈ dom Γ̂) and z_{1}, …, z_{n} are distinct variables then

(a) {z_{i} ↦ ρ̂(x_{i}) | i∈[1..n]} ≲_{{z_{i}↦Γ̂(x_{i}) | i∈[1..n]}}^{i} {z_{i} ↦ ρ(x_{i}) | i∈[1..n]}

(b) {z_{i} ↦ Γ̂(x_{i}) | i∈[1..n]}_{α}({z_{i} ↦ ρ̂(x_{i}) | i∈[1..n]}) = Γ̂_{α}(ρ̂)

(c) {z_{i} ↦ ρ(x_{i}) | i∈[1..n]}_{α}^{{z_{i}↦Γ̂(x_{i}) | i∈[1..n]}}({z_{i} ↦ ρ̂(x_{i}) | i∈[1..n]}) = ρΓ̂ ; α(ρ̂)

Proof: Straightforward in all cases. □

We now consider the two last reasons. We first illustrate the latter, technical reason: recall the power function from the introduction (glossing over syntactic restrictions),

q̂ = power(n,x) = if (n=0) then 1 else x*(power(n-1,x))

(placed in context p̂ = local\left[{ \atop q}\right] inpower) and its specialized version,

                             q = power_{2}(x) = x*(x*1)

(placed in context p = local[q]inpower_{2}). We thus have [[p̂]]_{R}(2) = ⌊p⌋. By soundness of specialization, the following equality is required to hold (unfolding the definition for curry):

[[p]] = λx. [[∥p̂∥]](2, x)

By further unfolding the definitions, we can recognize it as a relation between two fixed points,

fix(Φ′)(power_{2}) = λx. fix(Φ)(power)(2, x)

where Φ′ = λξ′. {power_{2} ↦ [[q]] ξ′} and Φ = λξ. {power ↦ [[∥q̂∥]] ξ}. The standard technique for proving such equalities is fixed-point induction, here on the pointed and inclusive relation P = {(ξ′, ξ) | ξ′(power_{2}) = λx. ξ(power)(2, x)}. But we cannot prove the inductive case, i.e., if (ξ′, ξ) ∈ P then (Φ′(ξ′), Φ′(ξ)) ∈ P, because it does not hold. The problem can be illustrated using the example, where we have by definition (simplifying the total arithmetic functions):

[[∥q̂∥]] ξ = λ(n, x). case (n = 0) of \begin{cases}tt & → 1 \\ ff & → ξ(power)(n − 1, x) † λr. ⌊x × r⌋ \end{cases}
[[q]] ξ′ = λx. ⌊x × x⌋

Then,

λx. ⊥(power)(2, x) =  ⊥  =  ⊥  = ⊥(power_{2})
λx. Φ(⊥)(power)(2, x) =  ⊥  ≠ λx. ⌊x × x⌋ = Φ′(⊥)(power_{2})
λx. Φ(Φ(⊥))(power)(2, x) =  ⊥  ≠ λx. ⌊x × x⌋ = Φ′(Φ′(⊥))(power_{2})
λx. Φ(Φ(Φ(⊥)))(power)(2, x) = λx. ⌊x × x⌋ = λx. ⌊x × x⌋ = Φ′(Φ′(Φ′(⊥)))(power_{2})

etc.

So although the desired equality certainly does hold, we cannot in general prove it by fixed-point induction alone. We can observe that fixed-point induction may give us one direction, namely

λx. fix(Φ)(power)(2, x) ⊑ fix(Φ′)(power_{2})

This direction does actually hold in general.

For the other direction, consider the residual meaning of power:

[[q̂]]_{R} ξ̂ = λ(n, x). case (n = 0) of \begin{cases}tt & → 1 \\ ff & → ξ̂(power)(n − 1, x) † λr. ⌊x*r⌋ \end{cases}

Let Φ̃ = ξ̂. {power ↦ [[q̂]]_{R} ξ̂}. Here, the symbolic unfoldings are

⊥(2, x) = ⊥  = ⊥
Φ̃(⊥)(2, x) = ⊥(1, x) † λr. ⌊x*r⌋  = ⊥
Φ̃(Φ̃(⊥))(2, x) = ⊥(0, x) † λr. ⌊x*r⌋ † λr. ⌊x*r⌋ = ⊥
Φ̃(Φ̃(Φ̃(⊥)))(2, x) = ⌊1⌋ † λr. ⌊x*r⌋ † λr. ⌊x*r⌋  = ⌊x*x*1⌋
etc.

The fallacy of the above example was to assume that the specialization terminated, thereby implicitly using fix(Φ̃) to define the operator Φ′ and thus unavoidably baking adequate symbolic unfolding into it. So while Φ^{i}(⊥) and Φ̃^{i}(⊥) are in perfect harmony, Φ^{i}(⊥) and Φ^{′i}(⊥) are not until the regular unfolding has “caught up” with the symbolic unfolding (which happens at i = 3 in the example). A central concept in the proof is precisely this relationship, written ⪅ .

Given Ψ̂, ξ̂ ∈ [[Ψ̂]]_{R}, and ξ ∈ [[∥Ψ̂∥]], we define

ξ̂ ⪅Ψ̂ ξ ⇔ (∀f ∈ dom Ψ̂. S(Ψ̂(f)) ⇒ ξ̂(f) = γ_{T} ∘ ξ(f))∧

∀f ∈ dom Ψ̂.D(Ψ̂(f)) ⇒ ∀τ̂_{1}, …, τ̂_{n}, τ, Γ̂, x_{1}, …, x_{n}, ρ̂, ρ, δ, δ′, ξ′, e. if Ψ̂(f)=τ̂_{1} * … * τ̂_{n}->\underline{τ}, dom Γ̂=\{x_{1}, …, x_{n}\}, (∀i∈[1..n]. Γ̂(x_{i}) = τ̂_{i}),

ρ̂ ≲δ(i) ; Γ̂ ρ, ξ′ ⊑ ξ, and ξ̂(f)(ρ̂(x_{1}), …, ρ̂(x_{n})) δ = ⌊(e, δ′)⌋

then δ′ ∈ extΨ̂(δ) and, letting X = δ′(seen), 1. ∥\underline{Ψ̂}(X)∥, ∥Γ̂_{α}(ρ̂)∥ ⊢ e : τ

2. [[e]] (curryΨ̂(ξ)(X)) ρΓ̂ ; α(ρ̂) = ξ(f)(ρ(x_{1}), …, ρ(x_{n}))

3. ξ′(f)(ρ(x_{1}), …, ρ(x_{n})) ⊑ [[e]] (curryΨ̂(ξ′)(X)) ρΓ̂ ; α(ρ̂)

There are four parts (beyond bookkeeping): the static case and the numbered dynamic conclusions. The static case (the first line) simply requires that ξ̂(f) is identical to ξ(f) (modulo η). The dynamic case (the remaining lines) addresses several issues, given the premise that the

symbolic unfolding of ξ̂(f) terminates and is called from some valid typing context Γ̂ with sound renaming ρ̂ ≲Γ̂ ρ. Then, (case 1.) the generated expression must be well-typed in the residual context; (case 2.) the meaning of it in this context must be equal to the meaning of the erasured function call; and (case 3.) if further ξ′ ⊑ ξ then only one direction of (case 2.) is guaranteed to hold when substituting ξ′ for ξ. We can thus recognize the two cases of symbolic unfolding mentioned above: (case 2.) can be read as ξ is “adequately unfolded” with repect to ξ̂, and (case 3.) as any ξ′ ⊑ ξ is perhaps “inadequately unfolded” with repect to ξ̂.

We can now present an outline for the soundness proof (illustrated by power).

1. Show by structural induction that, given ξ̂ ⪅ ξ, the RHS generalizes to all terms, not just the case for symbolic unfolding (Lemmas 7-10).

2. Establish [[[q̂]]]_{R} ⪅ [[∥[q̂]∥]], i.e., fix(Φ̃) ⪅ fix(Φ), by fixed-point induction (Lemma 11).

3. Use (case 3.) of the RHS, taking Φ^{i}(⊥) ⊑ fix(Φ), to show

λx. fix(Φ)(power)(2, x) ⊑ fix(Φ′)(power_{2})

by fixed-point induction. Further, Φ′({power_{2} ↦ λx. fix(Φ)(power)(2, x)}) = {power_{2} ↦ [[q]] {power_{2} ↦ λx. fix(Φ)(power)(2, x)}} = {power_{2} ↦ λx. ([[∥q̂∥]] fix(Φ))(2, x)} By (case 2.) of the RHS = {power_{2} ↦ λx. (Φ(fix(Φ))(power))(2, x)} = {power_{2} ↦ λx. fix(Φ)(power)(2, x)} By Φ(fix(Φ)) = fix(Φ) Hence, {power_{2} ↦ λx. fix(Φ)(power)(2, x)} is a fixed point of Φ′ and therefore greater than its least fixed point, fix(Φ′). Consequently,

λx. fix(Φ)(power)(2, x) ⊒ fix(Φ′)(power_{2})

This completes the key lemma (Lemma 12), which implies soundness (Theorem 1).

The typing parts are unproblematic, so is accounting for the transitive closure.

We have a technical requirement for ⪅ , namely that is admits fixed-point induction:

Lemma 6 For fixed Ψ̂, P = {(ξ̂, ξ) | ξ̂ ⪅Ψ̂ ξ} is pointed (i.e., (⊥, ⊥) ∈ P) and inclusive (i.e., closed under ω-chains).

Proof: Straightforward verification. □

Remark 1 It may be instructive to consider omitting symbolic unfolding. There would be no need for renaming, so dynamic variables could be syntactically preserved by the residualizing semantics (the restriction that function arguments must be variables also becomes unnecessary). The definitions of this section are considerably simplified:

ρ̂ ≲i ; Γ̂ ρ ⇔ ∀x ∈ dom Γ̂. S(Γ̂(x)) ⇒ ρ̂(x) = ρ(x)
Γ̂_{α}(ρ̂) = {x ↦ Γ̂(x) | x ∈ dom Γ̂, D(Γ̂(x))}
ρΓ̂ ; α(ρ̂) = {x ↦ ρ(x) | x ∈ dom Γ̂, D(Γ̂(x))}
ξ̂ ⪅Ψ̂ ξ ⇔ ∀f ∈ dom Ψ̂. S(Ψ̂(x)) ⇒ ξ̂(f) = γ_{T} ∘ ξ(f)

Most importantly, the simple fixed-point induction is now strong enough to prove correctness.

2.4.3 Soundness of the residualizing semantics

Soundness of the residualizing semantics follows the proof outline from above.

Static terms form a proper subset of the language, where the non-standard semantics agrees with the standard ones:

Lemma 7 If Ψ̂, Γ̂ ⊢ ê: \overline{τ}, ξ̂ ⪅Ψ̂ ξ, and ρ̂ ≲i ; Γ̂ ρ then [[ê]]_{R} ξ̂ρ̂ = γ_{T} ([[∥ê∥]] ξ ρ).

Proof: Straightforward, by structural induction. □

Lemma 8 If Ψ̂ ⊢ q̂: (f, σ̂), S(σ̂), and ξ̂ ⪅Ψ̂ ξ then [[q̂]]_{R} ξ̂ = γ_{T} ∘ ([[∥q̂∥]] ξ).

Proof: Follows directly from lemma 7. □

Dynamic terms and their residualized versions have the same meaning in the standard semantics, taking appropriate contexts into account.

Lemma 9 If Ψ̂, Γ̂ ⊢ ê: \underline{τ}, ξ̂ ⪅Ψ̂ ξ, ρ̂ ≲δ(i) ; Γ̂ ρ, ξ′ ⊑ ξ, and ([[ê]]_{R} ξ̂ρ̂) δ = ⌊(e, δ′)⌋ then δ′ ∈ extΨ̂(δ) and, letting X = δ′(seen), 1. ∥\underline{Ψ̂}(X)∥, ∥Γ̂_{α}(ρ̂)∥ ⊢ e : τ

2. [[e]] (curryΨ̂(ξ)(X)) ρΓ̂ ; α(ρ̂) = [[∥ê∥]] ξ ρ

3. [[∥ê∥]] ξ′ ρ ⊑ [[e]] (curryΨ̂(ξ′)(X)) ρΓ̂ ; α(ρ̂)

Proof: By structural induction, using Lemmas 1, 5(1-4), and 7. □ Lemma 10 If Ψ̂ ⊢ q̂ : (f, σ̂), D(σ̂), ξ̂ ⪅Ψ̂ ξ, ξ′ ⊑ ξ, (v_{1}, …, v_{k}) ∈ [[∥\overline{σ̂}∥]], and furthermore (↓σ̂ ([[q̂]]_{R} ξ̂)(f_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k}))) δ = ⌊(q, δ′)⌋ then δ′ ∈ extΨ̂(δ) and, letting X = δ′(seen),

1. ∥\underline{Ψ̂}(X)∥ ⊢ q : (f_{(v_{1},...,v_{k})}, ∥\underline{σ̂}∥)

2. [[q]] (curryΨ̂(ξ)(X)) = curryσ̂([[∥q̂∥]] ξ)(v_{1}, …, v_{k})

3. curryσ̂([[∥q̂∥]] ξ′)(v_{1}, …, v_{k}) ⊑ [[q]] (curryΨ̂(ξ′)(X)) Proof: Follows from Lemma 9, using Lemma 5(1-3). □

The declaration level is where all the pieces must fit together. First, we need to establish that a residualized declaration provides sound symbolic unfolding: Lemma 11 If ⊢ d̂: Ψ̂ then [[d̂]]_{R} ⪅Ψ̂ [[∥d̂∥]]. Proof: By fixed-point induction, using Lemmas 5(5), 6, 8, and 10. □

We are now in position to establish the key soundness lemma. Lemma 12 If ⊢ d̂: Ψ̂ and (visit(f) ⋆ λu. closeΨ̂([[d̂]]_{R})) δ_{0} = ⌊(d, δ)⌋ then, letting X = δ(seen),

1. ⊢ d : ∥\underline{Ψ̂}(X)∥

2. [[d]] = curryΨ̂([[∥d̂∥]])(X) Proof: Assume that ⊢ d̂: Ψ̂ and (visit(f) ⋆ λu. closeΨ̂([[d̂]]_{R})) δ_{0} = ⌊(d, δ)⌋. Note first the conditions for Lemma 3 are straightforwardly satisfied, using the simple extension part of Lemma 10 (formally triggered by Lemma 11).

(1.) We aim to establish that each equation q ∈ d is well-typed in typing context ∥\underline{Ψ̂}(X)∥ and that dom d = dom ∥\underline{Ψ̂}(X)∥ = X, i.e., that the premise for the typing rule for declarations holds.

Let q ∈ d be arbitrary. By Lemma 3(1), there is some f′ ∈ dom Ψ̂, (v_{1}, …, v_{k}), δ′′, and δ′′′ such that ↓_{Ψ̂(f′)} ([[d̂]]_{R}(f′))(f′_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k})) δ′′ = ⌊(q, δ′′′)⌋. Let Y = δ′′′(seen). By Lemma 10(1) (formally triggered by Lemma 11),

∥\underline{Ψ̂}(Y)∥ ⊢ q : (f′_{(v_{1},...,v_{k})}, \underline{σ̂})

By Lemma 3(2), Y ⊆ X, so by weakening (Lemma 2(1)),

∥\underline{Ψ̂}(X)∥ ⊢ q : (f′_{(v_{1},...,v_{k})}, \underline{σ̂})

Since q was arbitrary, each q ∈ d is well-typed in context ∥\underline{Ψ̂}(X)∥.

By Lemma 3, δ′(seen) = dom d, i.e., X = dom d.

The conclusion, ⊢ d : ∥\underline{Ψ̂}(X)∥, then follows by the typing rule for declarations.

(2.) Let Φ and Φ′ denote the operators underlying [[∥d̂∥]] and [[d]], resp. We consider each direction of the equality separately, as motivated in Section 2.4.2.

Case curryΨ̂([[∥d̂∥]])(X) ⊑ [[d]]: Let

P = \{(ξ, ξ′) ∈ [[∥Ψ̂∥]] × [[∥\underline{Ψ̂}(X)∥]] | curryΨ̂(ξ)(X) ⊑ ξ′ ∧ ξ ⊑ [[∥d̂∥]]\}

It is straightforward to verify that the predicate is pointed and inclusive. We proceed by fixed-point induction. Assume (ξ, ξ′) ∈ P.

Let f′_{(v_{1},...,v_{k})} ∈ X be arbitrary. By well-typedness of d̂, there is some q̂ ∈ d̂ and σ̂ such that Ψ̂ ⊢ q̂ : (f′, σ̂). By Lemma 3(1) and part 1, there exists q ∈ d, δ′′ and δ′′′ such that ↓σ̂ ([[d̂]]_{R}(f′))(f′_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k})) δ′′ = ⌊(q, δ′′′)⌋. Let Y = δ′′′(seen). Now,

curryσ̂([[∥q̂∥]] ξ)(v_{1}, …, v_{k}) ⊑ [[q]] curryΨ̂(ξ)(Y) By ξ ⊑ [[∥d̂∥]] and Lemmas 10(3) and 11 = [[q]] curryΨ̂(ξ)(X) By Lemmas 3(2) and 2(2) ⊑ [[q]] ξ′ By IH and monotonicity

Since f_{(v_{1},...,v_{k})} ∈ X was arbitrary,

curryΨ̂(Φ(ξ))(X) = {f_{(v_{1},...,v_{k})} ↦ curryσ̂(Φ(ξ)(f))(v_{1}, …, v_{k}) | f_{(v_{1},...,v_{k})} ∈ X} = {f_{(v_{1},...,v_{k})} ↦ curryσ̂([[∥q̂∥]] ξ)(v_{1}, …, v_{k}) | f_{(v_{1},...,v_{k})} ∈ X} ⊑ {f_{(v_{1},...,v_{k})} ↦ [[q]] ξ′ | f_{(v_{1},...,v_{k})} ∈ X} = Φ′(ξ′)

By monotonicity of Φ and the fixed-point equation, Φ(ξ) ⊑ Φ([[∥d̂∥]]) = [[∥d̂∥]]. Hence, (Φ(ξ), Φ′(ξ′)) ∈ P; we can thus conclude curryΨ̂([[∥d̂∥]])(X) ⊑ [[d]].

Case [[d]] ⊑ curryΨ̂([[∥d̂∥]])(X): The idea is to show that curryΨ̂([[∥d̂∥]])(X) is a fixed point of Φ′ and hence greater than its least fixed point, [[d]].

Let f′_{(v_{1},...,v_{k})} ∈ X be arbitrary. By well-typedness of d̂, there is some q̂ ∈ d̂ and σ̂ such that Ψ̂ ⊢ q̂ : (f′, σ̂). By Lemma 3(1) and part 1, there exists q ∈ d, δ′′ and δ′′′ such that ↓σ̂ ([[d̂]]_{R}(f′))(f′_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k})) δ′′ = ⌊(q, δ′′′)⌋. Let Y = δ′′′(seen). Thus,

curryσ̂([[∥q̂∥]] [[∥d̂∥]])(v_{1}, …, v_{k}) = [[q]] curryΨ̂([[∥d̂∥]])(Y) By Lemmas 10(2) and 11 = [[q]] curryΨ̂([[∥d̂∥]])(X) By Lemmas 3(2) and 2(2)

Since f_{(v_{1},...,v_{k})} ∈ X was arbitrary,

Φ′(curryΨ̂([[∥d̂∥]])(X)) = {f_{(v_{1},...,v_{k})} ↦ [[q]] curryΨ̂([[∥d̂∥]])(X) | f_{(v_{1},...,v_{k})} ∈ X} = {f_{(v_{1},...,v_{k})} ↦ curryσ̂([[∥q̂∥]] [[∥d̂∥]])(v_{1}, …, v_{k}) | f_{(v_{1},...,v_{k})} ∈ X} = curryΨ̂(Φ([[∥d̂∥]]))(X) = curryΨ̂([[∥d̂∥]])(X) Since [[∥d̂∥]] is a fixed point of Φ

Hence, curryΨ̂([[∥d̂∥]])(X) is a fixed point of Φ′. Consequently,

[[d]] = fix(Φ′) ⊑ curryΨ̂([[∥d̂∥]])(X)
□

Theorem 1 (soundness) If ⊢ p̂: σ̂ and [[p̂]]_{R}(v_{1}, …, v_{k}) = ⌊p⌋ then

1. ⊢ p : \underline{σ̂}

2. [[p]] = curryσ̂([[∥p̂∥]])(v_{1}, …, v_{k})

Proof: Follows directly from Lemma 12, using Lemma 3. □

3 Application: the Knuth-Morris-Pratt algorithm

String matching has been a subject to extensive investigation in partial evaluation, since Futamura in 1987 presented the method of Generalized Partial Computation [26]. His method could transform a naive, inefficient string matcher into the search phase of the ingenious Knuth-Morris-Pratt algorithm [35]. This example (now known as the “KMP-test” [41]) has since fueled numerous investigations in partial evaluation [1–4, 12, 29, 39–41]. In particular, Consel and Danvy showed that polyvariant specialization is acutally strong enough to pass the KMP-test, for certain inefficient string matchers [12]. One notable utility of the KMP-test has been to relate and distinguish various advanced program transformations with respect to how much information is propagated (and exploited) by the transformations [39,41].

However, only recently has it been shown precisely what information should be propagated to obtain the Knuth-Morris-Pratt algorithm [1]. As an amusing corollary, none of the advanced transformations that pass the KMP-test actually propagate the precise amount of information needed to exactly obtain the Knuth-Morris-Pratt algorithm [39].

The value of the formal treatment was thus to pinpoint this precise amount of information. For the purpose of analysis, a simple polyvariant specializer that actually failed the KMP-test was used [1]. The reason being that it is much easier to control the source program, which propagates collected static information about the dynamic argument by itself — a so-called binding-time-improved algorithm [12], than an advanced transformation.

From a semantic perspective, however, one piece of the formal treatment is still missing, namely a proof that applying a polyvariant specializer always gives a correct result. We are now in position to address this problem in full.

We instantiate the signature, Σ = (B, L, C), as follows:

                    B = {int, char, string}

L(int) = {…, -1, 0, 1, …}
L(char) = {a, …, z}
L(string) = {"c_{1} ⋯ c_{n}" | n ∈ ℕ, ∀i∈[1..n]. c_{i} ∈ L(char)}

                    C = {+ ↦ int*int->int, - ↦ int*int->int,

                         =_{int} ↦ int*int->bool, =_{char} ↦ char*char->bool,
                         ref ↦ string*int->char, length ↦ string->int}

The interpretation of the signature is the obvious one.

For conciseness and readability, we (1) abbreviate both =_{int} and =_{char} as =; (2) write binary function constants in infix notation; (3) assume implicit let-insertion of function arguments in a left-to-right order; and (4) write all static, reducible types and terms in italics, instead of overlining them.

We use the following inefficient string matcher, STAGED [1].

local
 main    : string*\underline{string}->\underline{int} (pat,txt)
         = \underline{match}(pat,txt,0 ,$0,length(pat),\underline{length}(txt))
 match   : string*\underline{string}*int*\underline{int}*int*\underline{int}->\underline{int} (pat,txt,j ,k,lp,lt)

= if (j =lp)

           then (k\underline{-}$j )
           else \underline{if} (k\underline{=}lt)
                \underline{then} $-1
                \underline{else} \underline{compare}(pat,txt,j ,k,lp,lt)
 compare : string*\underline{string}*int*\underline{int}*int*\underline{int}->\underline{int} (pat,txt,j ,k,lp,lt)
         = \underline{if} ($(ref (pat,j))=\underline{ref}(txt,k))
           \underline{then} \underline{match}(pat,txt,j +1 ,k\underline{+}$1,lp,lt)

\underline{else} if (j =0)

                then \underline{match}(pat,txt,0 ,k\underline{+}$1,lp,lt)

else rematch(pat,txt,j ,k,0 ,1 ,lp,lt)

rematch : string*\underline{string}*int*\underline{int}*int*\underline{int}*int*\underline{int}->\underline{int}
         (pat,txt,j ,k,jp,kp,lp,lt)

= if (kp=j)

then if ( ref (pat,jp)=ref (pat,kp))

then if (jp=0)

                   then \underline{match}(pat,txt,0 ,k\underline{+}$1,lp,lt)

else rematch(pat,txt,j ,k,0 ,(kp-jp)+1 ,lp,lt)

              else \underline{compare}(pat,txt,jp,k,lp,lt)

else if ( ref (pat,jp)=ref (pat,kp)) then rematch(pat,txt,j ,k,jp+1 ,kp+1 ,lp,lt) else rematch(pat,txt,j ,k,0 ,(kp-jp)+1 ,lp,lt)

in main

The expensive part of the computation –called backtracking– is encapsulated in the essentially static rematch function. During specialization, rematch is thus completely unfolded and the residual program runs in linear time (with a constant factor independent of the pattern pat [41]). So although inefficient, the string matcher is not particularly naive.

In contrast, more advanced program transformations such as Supercompilation [28,41,42] and Generalized Partial Computation [25–27] can pass the KMP-test from a naive (i.e., not staged), inefficient string matcher.

As an example, the result of specializing the inefficient string matcher with repect to the pattern "abaa" is shown below (we use the notational conventions from above and have further renamed all variables):

local
main_{(‘‘abaa”)}  : string->int (txt)
                 = match_{(‘‘abaa”,0,4)}(txt,0,length(txt))
match_{(‘‘abaa”,0,4)} : string*int*int->int (txt,k,lt)
                 = if k=lt then -1 else compare_{(‘‘abaa”,0,4)}(txt,k,lt)
compare_{(‘‘abaa”,0,4)} : string*int*int->int (txt,k,lt)
                 = if 'a'=ref(txt,k) then match_{(‘‘abaa”,1,4)}(txt,k+1,lt)

                                     else match_{(‘‘abaa”,0,4)}(txt,k+1,lt)

match_{(‘‘abaa”,1,4)} : string*int*int->int (txt,k,lt)
                 = if k=lt then -1 else compare_{(‘‘abaa”,1,4)}(txt,k,lt)
compare_{(‘‘abaa”,1,4)} : string*int*int->int (txt,k,lt)
                 = if 'b'=ref(txt,k) then match_{(‘‘abaa”,2,4)}(txt,k+1,lt)

                                     else compare_{(‘‘abaa”,0,4)}(txt,k,lt)

match_{(‘‘abaa”,2,4)} : string*int*int->int (txt,k,lt)
                 = if k=lt then -1 else compare_{(‘‘abaa”,2,4)}(txt,k,lt)
compare_{(‘‘abaa”,2,4)} : string*int*int->int (txt,k,lt)
                 = if 'a'=ref(txt,k) then match_{(‘‘abaa”,3,4)}(txt,k+1,lt)

                                     else match_{(‘‘abaa”,0,4)}(txt,k+1,lt)

match_{(‘‘abaa”,3,4)} : string*int*int->int (txt,k,lt)
                 = if k=lt then -1 else compare_{(‘‘abaa”,3,4)}(txt,k,lt)
compare_{(‘‘abaa”,3,4)} : string*int*int->int (txt,k,lt)
                 = if 'a'=ref(txt,k) then match_{(‘‘abaa”,4,4)}(txt,k+1,lt)

                                     else compare_{(‘‘abaa”,1,4)}(txt,k,lt)

match_{(‘‘abaa”,4,4)} : string*int*int->int (txt,k,lt)
                 = k-4
in main_{(‘‘abaa”)}

We will now show that for all patterns, our polyvariant specializer transforms the inefficient string matcher, STAGED, into a program with the above structure. The proof consists of two parts: termination of the specializer and properties of the residual programs.

We define the size of a term, | · |, in the obvious way by induction.

Theorem 2 For all strings s there exists a p such that [[STAGED]]_{R} s = ⌊p⌋ and

1. ⊢ p : string->int

2. [[p]] = curry_{string*\underline{string}->\underline{int}}([[∥STAGED∥]])(s)

3. |p| ∈ O(|s|)

Proof: Let s be arbitrary. We will establish the prerequisites for Lemma 4. Define

X = {main_{(s)}} ∪ {match_{(s,j,|s|)} | j ∈ [0..|s|]} ∪ {compare_{(s,j,|s|)} | j ∈ [0..|s| − 1]}

Clearly |X| = 1 + (|s| + 1) + |s|. Let δ be given and let Z = δ(seen) ⊆ X. Let σ̂ =

string*\underline{string}*int*\underline{int}*int*\underline{int}->\underline{int}.

Let f ∈ X be arbitrary. All cases but the last are completely straightforward.

case f = main_{(s)}: Let σ′ = string*\underline{string}->\underline{int}. Then

(↓_{σ′} ([[STAGED]]_{R}(main))(main_{(s)}, (s))) δ = ⌊(q, δ′)⌋

where δ′(seen) = Z ∪ {match_{(s,0,|s|)}}

and q = main_{(s)}: \underline{σ′} (y_{i}) = match_{(s,0,|s|)}(y_{i},0,length(y_{i})).

case f = match_{(s,j,|s|)}, j ∈ [0..|s| − 1]: Then

(↓σ̂ ([[STAGED]]_{R}(match))(match_{(s,j,|s|)}, (s, j, |s|))) δ = ⌊(q, δ′)⌋

where δ′(seen) = Z ∪ {compare_{(s,j,|s|)}}

and q = match_{(s,j,|s|)} : \underline{σ̂} (y_{i},y_{i+1},y_{i+2}) = if y_{i+1}=y_{i+2}

                       then -1

else compare_{(s,j,|s|)}(y_{i},y_{i+1},y_{i+2})

case f = match_{(s,|s|,|s|)}: Then

(↓_{σ′} ([[STAGED]]_{R}(match))(match_{(s,|s|,|s|)}, (s, |s|, |s|))) δ = ⌊(q, δ′)⌋

where δ′(seen) = Z and q =

match_{(s,|s|,|s|)} : \underline{σ̂} (y_{i},y_{i+1},y_{i+2}) = k-↓int (|s|)

case f = compare_{(s,0,|s|)}: Then, noting that |s| ≠ 0,

(↓σ̂ ([[STAGED]]_{R}(compare))(compare_{(s,0,|s|)}, (s, 0, |s|))) δ = ⌊(q, δ′)⌋

where δ′(seen) = Z ∪ {match_{(s,0,|s|)}, match_{(s,1,|s|)}} and q =

compare_{(s,0,|s|)} : \underline{σ̂} (y_{i},y_{i+1},y_{i+2})
= if ↓char (ref(s, 0))=ref(y_{i},y_{i+1})
then match_{(s,1,|s|)}(y_{i},y_{i+1}+1,y_{i+2})
else match_{(s,0,|s|)}(y_{i},y_{i+1}+1,y_{i+2})

case f = compare_{(s,j,|s|)}, j ∈ [1..|s| − 1]: This case is slightly more complicated, since we first need to know how the symbolic unfolding of rematch behaves (essentially [1, Lemma 3]). Define the termination relation Y as

Y = {(kp − jp, kp) | 0 ≤ jp ≤ kp ≤ j}

ordered by (a_{1}, b_{1}) >_{Y} (a_{2}, b_{2}) ⇔ a_{1} < a_{2} ∨ (a_{1} = a_{2} ∧ b_{1} < b_{2}). Note that (j, j) is thus the least element. By well-founded induction on Y, it is now easy to show that

[[STAGED]]_{R}(rematch)(s, y_{i}, j, y_{i+1}, jp, kp, lp, y_{i+2}) δ = ⌊(e, δ′)⌋

for some e and δ′, where either e = match_{(s,0,|s|)}(y_{i},y_{i+1}+1,y_{i+2}) and δ′(seen) = Z ∪ {match_{(s,0,|s|)}} or e = compare_{(s,jp′,|s|)}(y_{i},y_{i+1},y_{i+2}) and δ′(seen) = Z∪{compare_{(s,jp′,|s|)}}, for some jp′ ∈ [0..j]. Hence,

(↓σ̂ ([[STAGED]]_{R}(compare))(compare_{(s,j,|s|)}, (s, j, |s|))) δ = ⌊(q, δ′′)⌋

where δ′′(seen) = δ′(seen) ∪ {match_{(s,j+1,|s|)}}

and q = compare_{(s,j,|s|)} : \underline{σ̂} (y_{i},y_{i+1},y_{i+2})

= if ↓char (ref(s, j))=ref(y_{i},y_{i+1})
then match_{(s,j+1,|s|)}(y_{i},y_{i+1}+1,y_{i+2})

                                else e

Now, by Lemma 4 and the definition of [[STAGED]]_{R}, there is some p such that [[STAGED]]_{R} s = ⌊p⌋. By Theorem 1, parts (1.) and (2.) follow.

Let p = local d in f′. By Lemma 3(1), every q ∈ d is of the form

(↓σ̂ ([[STAGED]]_{R}(f))(f_{(v_{1},...,v_{k})}, (v_{1}, …, v_{k}))) δ = ⌊(q, δ′)⌋

where f_{(v_{1},...,v_{k})} ∈ X′ ⊆ X and δ(seen) ⊆ X′. Hence, we can observe by the above case analysis that the size of each q is independent of s. Since X contains at most 2|s| + 2 such equations, we have established part (3.), namely |p| ∈ O(|s|). □

Since a formal notion of “time” is outside the scope of our denotational framework, we will have to settle for some informal remarks concerning the efficiency of the specialized programs.

Given any s, it is a simple observation from the proof of Theorem 2 that when running the specialized program only a constant (i.e., independent of |s|) number of elementary operations are performed between each comparison, and that these comparisons are preserved exactly from the binding-time-improved program. From previous work [1], we know that this sequence of comparisons performed is identical to the sequence performed by the real Knuth-Morris-Pratt algorithm. Hence, the specialized program is at least as fast (asymptotically) as the linear-time Knuth-Morris-Pratt algorithm.

Note however that we use a different formal semantics than in previous work [1]. Therefore, even if we had a formal notion of time, we could not use the previous result directly.

4 Related work

Our closest related work is Filinski’s formalizations of type-directed (monovariant) partial evaluation [14, 15, 19, 21, 22]. In fact, the technical aspects of the present work are inspired by Filinski’s work: for call-by-value type-directed partial evaluation with computational effects for the simply-typed lambda calculus with constants, he uses a denotational semantics parameterized by a monad. The semantic construction of type-directed partial evaluation is a prime application of normalization by evaluation [6,7].

Not only do the correctness proofs involve more advanced techniques, e.g., logical relations due to being in a higher-order setting, but the elegant semantic construction underlying type-directed partial evaluation is on closer inspection quite different from ours: the reification functions are defined by induction on their types, and the residualizing semantics is an instance of a parameterizable, conventional monadic semantics. The latter property is the key to its efficiency, since it can therefore delegate evaluation to existing, optimizing compilers; here, the types are a crucial part of the construction (cf. the untyped setting [23]). Type-directed partial evaluation also guarantees completeness, namely that if a solution (i.e., normal form) exists at all then the algorithm will also find one (cf. our Lemma 4). Conceivably, one could mimic this construction by defining (syntactic) polyvariant normal forms with a polyvariant reduction system, and prove the polyvariant specializer complete in the above sense.

Despite the differences, type-directed partial evaluation does however not seem incompatible with polyvariance. It seems possible to introduce a new dynamic “polyvariant” fixed-point constant to the current framework, and instantiating the monadic semantics with a more complicated monad capable of handling the necessary bookkeeping, similarly to our T. The interpretation of the new constant would then compute the transitive closure, possibly restricting polyvariance to a firstorder fragment only using typing (in contrast to using the syntax grammar, as in our work).

Hatcliff and Danvy [30] have formalized a (monovariant) partial evaluator for Moggi’s computational metalanguage. The partial evaluator is proven sound with repect to an underlying operational semantics. Their formalization is evaluation-order independent and captures so-called control-based binding-time improvements (e.g., let-rearrangements) via the monadic laws.

In a small-step operational setting, they make the technical shortcut that “stuck” terms, i.e., irreducible non-values, are disallowed (and thus avoid two distinct notions of partiality, arising from both “stuck” terms and infinitely-reducing terms). This choice implies, in particular, that function constants must denote pure total functions. For example, using natural numbers, they consequently define pred(0) = 0, i.e., 0 − 1 = 0, to avoid pred(0) being “stuck”. In contrast, we explitly allow both static and dynamic primitive functions to be partial.

Later, Lawall and Thiemann re-investigated sound (monovariant) specialization, also from an operational standpoint [36]. Finally, Ager, Danvy, and the author’s treatment of the Knuth-Morris-Pratt algorithm is based on a formal semantic foundation [1]; this work was mentioned in more detail in Section 3.

5 Perspectives

The present work suggests several research directions.

5.1 Computational effects

A natural generalization is to allow arbitrary computational effects by parameterizing the source language by a monad. We not only gain expressibility, but can also keep track of dynamic computations more accurately. For the Knuth-Morris-Pratt algorithm, by the sheer possibility of making (dynamic) references to the text effectful, the residualizing semantics is forced by soundness to preserve them. Hence, the preservation of the algorithm’s trace (the sequence of these references) will be guaranteed by the specializer [1].

Other natural generalizations would be to allow higher-order functions or partially-static data structures [33]. A promising direction would be to try to integrate polyvariance into type-directed partial evaluation, as suggested in Section 4.

5.2 Selective bounded static variation

Another natural generalization is to parametrize the residualizing semantics by a monad (layered on top of the source monad). This would allow more radical program rearrangements, e.g., via the continuation monad [19]. In particular, an “unlift” operation, @, (namely bounded static variation) can be defined:

\frac{Ψ̂, Γ̂ ⊢ ê: \underline{τ} |[[∥\underline{τ}∥]]| < ∞}{Ψ̂, Γ̂ ⊢ @ê: \overline{τ}}

This rule will give rise to a lookup table in the residual program. In the realm of string matching, Danvy and the author have discovered that the key bad-character-shift heuristic of the efficient Boyer-Moore algorithm [10,31] can be seen as an instance of bounded static variation [17].

5.3 Resource-bounded partial evaluation

If we are given only limited (insufficient) resources to compute the residual program, we may consider stopping the partial evaluator prematurely. The result will then be the already completed specialized functions, some trivially specialized functions (i.e., the pending functions and values, which are scheduled for specialization), and the original program [16]. Note that such an algorithm is indifferent to whether or not the number of specialized functions is finite. We expect that the current proof can be adapted without much difficulty.

The real challenge will be to decide what should be specialized [16, 18]. Naively, we can view the pending list as a priority queue, taking the priority to be simply be the number of potential callers. Advanced profiling methods are probably preferable, particularly if they take selective bounded static variation into account. Given a sufficiently powerful profiling analysis, the idea in a nutshell is thus to focus the specialization effort (enhanced by tabulation) where it is expected to pay off most.

6 Conclusion

We have presented the first formal correctness proof of an offline polyvariant specialization algorithm for first-order recursive equations. Our approach has been to formulate the algorithm as a non-standard denotational semantics for the first-order language, and we have been able to establish correctness using mainly structural induction and fixed-point induction. The main technical challenges have been to keep track of the transitive closure and to tame symbolic unfolding.

As an application, the specialization algorithm has been shown to generate a program implementing the search phase of the Knuth-Morris-Pratt algorithm from an inefficient, but bindingtime-improved, string matcher. Here, our formalization sharpens the existing analysis of information propagation.

The present work suggests several extensions, as already mentioned in Section 5. It is also a step towards a formalization of more advanced program transformations, such as Supercompilation and Generalized Partial Computation.

Acknowledgments A special thanks to Andrzej Filinski for introducing me to formal semantics; for encouragement; and for countless deep constructive comments. I am also grateful to Olivier Danvy for his insightful comments.

References

[1] Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. On Obtaining Knuth, Morris, and Pratt’s String Matcher by Partial Evaluation. In Wei-Ngan Chin, editor, Proceedings of the ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 32–46. ACM Press, September 2002. Extended version available as technical report BRICS-RS-02-32.

[2] Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. ACM Transactions on Programming Languages and Systems, 2005. Available as technical report BRICS-RS-04-40. To appear.

[3] Torben Amtoft. Sharing of Computations. PhD thesis, University of Aarhus, Denmark, 1993. Technical report PB-453.

[4] Torben Amtoft, Charles Consel, Olivier Danvy, and Karoline Malmkjær. The abstraction and instantiation of string-matching programs. In Mogensen et al. [37], pages 332–357.

[5] Alan Bawden. Quasiquotation in Lisp. In Olivier Danvy, editor, Proceedings of the ACM SIG-PLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, Technical report BRICS-NS-99-1, University of Aarhus, pages 4–12, San Antonio, Texas, January

    1999. Available online at http://www.brics.dk/~pepm99/programme.html.

[6] Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg. Normalization by evaluation. In B. Möller and J.V. Tucker, editors, Prospects for Hardware Foundations, volume 1546 of Lecture Notes in Computer Science, pages 117–137. Springer-Verlag, 1998.

[7] Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Gilles Kahn, editor, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203–211, Amsterdam, The Netherlands, July 1991. IEEE Computer Society Press.

[8] Dines Bjørner, Andrei P. Ershov, and Neil D. Jones, editors. Partial Evaluation and Mixed Computation. North-Holland, 1988.

[9] Anders Bondorf and Olivier Danvy. Automatic autoprojection of recursive equations with global variables and abstract data types. Science of Computer Programming, 16:151–195, 1991.

[10] Robert S. Boyer and J. Strother Moore. A fast string searching algorithm. Communications of the ACM, 20(10):762–772, 1977.

[11] Mikhail A. Bulyonkov. Polyvariant mixed computation for analyzer programs. Acta Informatica, 21:473–484, 1984.

[12] Charles Consel and Olivier Danvy. Partial evaluation of pattern matching in strings. Information Processing Letters, 30(2):79–86, January 1989.

[13] Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In Susan L. Graham, editor, Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 493–501, Charleston, South Carolina, January 1993. ACM Press.

[14] Olivier Danvy. Type-directed partial evaluation. In Guy L. Steele Jr., editor, Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 242–257, St. Petersburg Beach, Florida, January 1996. ACM Press.

[15] Olivier Danvy. Type-directed partial evaluation. In John Hatcliff, Torben Æ. Mogensen, and Peter Thiemann, editors, Partial Evaluation – Practice and Theory; Proceedings of the 1998 DIKU Summer School, number 1706 in Lecture Notes in Computer Science, pages 367–411, Copenhagen, Denmark, July 1998. Springer-Verlag.

[16] Olivier Danvy, Nevin C. Heintze, and Karoline Malmkjær. Resource-bounded partial evaluation. ACM Computing Surveys, 28(2):329–332, June 1996.

[17] Olivier Danvy and Henning Korsholm Rohde. On Obtaining the Boyer-Moore String-Matching Algorithm by Partial Evaluation. Information Processing Letters. To appear.

[18] Saumya Debray. Resource-bounded partial evaluation. In Charles Consel, editor, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 179–192, Amsterdam, The Netherlands, June 1997. ACM Press.

[19] Peter Dybjer and Andrzej Filinski. Normalization and partial evaluation. In Gilles Barthe, Peter Dybjer, Luís Pinto, and João Saraiva, editors, Applied Semantics – Advanced Lectures, number 2395 in Lecture Notes in Computer Science, pages 137–192, Caminha, Portugal, September 2000. Springer-Verlag.

[20] Andrzej Filinski. Semantics of functional programming. Lecture notes, December 1998.

[21] Andrzej Filinski. A semantic account of type-directed partial evaluation. In Gopalan Nadathur, editor, Proceedings of the International Conference on Principles and Practice of Declarative Programming, number 1702 in Lecture Notes in Computer Science, pages 378– 395, Paris, France, September 1999. Springer-Verlag.

[22] Andrzej Filinski. Normalization by evaluation for the computational lambda-calculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, number 2044 in Lecture Notes in Computer Science, pages 151–165, Kraków, Poland, May 2001. Springer-Verlag.

[23] Andrzej Filinski and Henning Korsholm Rohde. Denotational Aspects of Untyped Normalization by Evaluation. RAIRO - Theoretical Informatics and Applications, 39(3):423–454, July 2005. FOSSACS’04 Special Issue. Extended version available as technical report BRICS-RS-05-4.

[24] Yoshihiko Futamura. Partial evaluation of computation process – an approach to a compilercompiler. Higher-Order and Symbolic Computation, 12(4):381–391, 1999. Reprinted from Systems · Computers · Controls 2(5), 1971.

[25] Yoshihiko Futamura, Zenjiro Konishi, and Robert Glück. WSDFU: Program transformation system based on generalized partial computation. In Mogensen et al. [37], pages 358–378.

[26] Yoshihiko Futamura and Kenroku Nogi. Generalized partial computation. In Bjørner et al. [8], pages 133–151.

[27] Yoshihiko Futamura, Kenroku Nogi, and Akihiko Takano. Essence of generalized partial computation. Theoretical Computer Science, 90(1):61–79, 1991.

[28] Robert Glück and Andrei Klimov. Occam’s razor in metacomputation: the notion of a perfect process tree. In Patrick Cousot, Moreno Falaschi, Gilberto Filé, and Antoine Rauzy, editors, Proceedings of the Third International Workshop on Static Analysis WSA’93, number 724 in Lecture Notes in Computer Science, pages 112–123, Padova, Italy, September 1993. Springer-Verlag.

[29] Bernd Grobauer and Julia L. Lawall. Partial evaluation of pattern matching in strings, revisited. Nordic Journal of Computing, 8(4):437–462, 2002.

[30] John Hatcliff and Olivier Danvy. A computational formalization for partial evaluation. Mathematical Structures in Computer Science, pages 507–541, 1997.

[31] R. Nigel Horspool. Practical fast searching in strings. Software—Practice and Experience, 10(6):501–506, 1980.

[32] Neil D. Jones. Automatic program specialization: A re-examination from basic principles. In Bjørner et al. [8], pages 225–282.

[33] Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, London, UK, 1993. Available online at

http://www.dina.kvl.dk/~sestoft/pebook/.

[34] Neil D. Jones, Peter Sestoft, and Harald Søndergaard. MIX: A self-applicable partial evaluator for experiments in compiler generation. Lisp and Symbolic Computation, 2(1):9–50, 1989.

[35] Donald E. Knuth, James H. Morris, and Vaughan R. Pratt. Fast pattern matching in strings. SIAM Journal on Computing, 6(2):323–350, 1977.

[36] Julia Lawall and Peter Thiemann. Sound specialization in the presence of computational effects. In Martin Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software, 3rd International Symposium, TACS’97, number 1281 in Lecture Notes in Computer Science, pages 227–238, Sendai, Japan, September 1997. Springer-Verlag.

[37] Torben Æ. Mogensen, David A. Schmidt, and I. Hal Sudborough, editors. The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, number 2566 in Lecture Notes in Computer Science. Springer-Verlag, 2002.

[38] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55– 92, 1991.

[39] Henning Korsholm Rohde. Measuring the propagation of information in partial evaluation. Technical Report BRICS-RS-05-26, BRICS, University of Aarhus, Denmark, August 2005.

[40] Jens Peter Secher. Driving-based Program Transformation in Theory and Practice. PhD thesis, Department of Computer Science, Copenhagen University, July 2002.

[41] Morten Heine Sørensen, Robert Glück, and Neil D. Jones. A positive supercompiler. Journal of Functional Programming, 6(6):811–838, 1996.

[42] Valentin F. Turchin. The concept of a supercompiler. ACM Transactions on Programming Languages and Systems, 8(3):292–325, 1986.

[43] Glynn Winskel. The Formal Semantics of Programming Languages. Foundation of Computing Series. The MIT Press, 1993.

Recent BRICS Report Series Publications

RS-05-34 Henning Korsholm Rohde. Formal Aspects of Polyvariant Specialization. November 2005. 27 pp.

RS-05-33 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Sumit Nain. Bisimilarity is not Finitely Based over BPA with Interrupt. October 2005. 33 pp. This paper supersedes BRICS Report RS-04-24. An extended abstract of this paper appeared in Algebra and Coalgebra in Computer Science, 1st Conference, CALCO 2005, Swansea, Wales, 3–6 September 2005, Lecture Notes in Computer Science 3629, pp. 54–68, Springer-Verlag, 2005.

RS-05-32 Anders Møller, Mads Østerby Olesen, and Michael I. Schwartzbach. Static Validation of XSL Transformations. October 2005. 50 pp.

RS-05-31 Christian Kirkegaard and Anders Møller. Type Checking with XML Schema in Xact. September 2005. 20 pp.

RS-05-30 Karl Krukow. An Operational Semantics for Trust Policies. September 2005. 38 pp.

RS-05-29 Olivier Danvy and Henning Korsholm Rohde. On Obtaining the Boyer-Moore String-Matching Algorithm by Partial Evaluation. September 2005. ii+9 pp. To appear in Information Processing Letters. This version supersedes BRICS RS-05-14.

RS-05-28 Jiří Srba. On Counting the Number of Consistent Genotype Assignments for Pedigrees. September 2005. 15 pp. To appear in FSTTCS ’05.

RS-05-27 Pascal Zimmer. A Calculus for Context-Awareness. August 2005. 21 pp.

RS-05-26 Henning Korsholm Rohde. Measuring the Propagation of Information in Partial Evaluation. August 2005. 39 pp.

RS-05-25 Dariusz Biernacki and Olivier Danvy. A Simple Proof of a Folklore Theorem about Delimited Control. August 2005. ii+11 pp. To appear in Journal of Functional Programming. This version supersedes BRICS RS-05-10.