A Semantics for Approximate Program Transformations

arXiv:1304.5531v1 [] 19 Apr 2013

Edwin Westbrook and Swarat Chaudhuri
Department of Computer Science, Rice University
Houston, TX 77005
Email: {emw4,swarat}@rice.edu
Abstract
An approximate program transformation is a transformation that can change the semantics of a program
within a specified empirical error bound. Such transformations have wide applications: they can decrease
computation time, power consumption, and memory
usage, and can, in some cases, allow implementations
of incomputable operations. Correctness proofs of approximate program transformations are by definition
quantitative. Unfortunately, unlike with standard program transformations, there is as of yet no modular
way to prove correctness of an approximate transformation itself. Error bounds must be proved for each
transformed program individually, and must be reproved each time a program is modified or a different
set of approximations are applied.
In this paper, we give a semantics that enables
quantitative reasoning about a large class of approximate program transformations in a local, composable way. Our semantics is based on a notion of
distance between programs that defines what it means
for an approximate transformation to be correct up
to an error bound. The key insight is that distances
between programs cannot in general be formulated
in terms of metric spaces and real numbers. Instead,
our semantics admits natural notions of distance for
each type construct; for example, numbers are used
as distances for numerical data, functions are used
as distances for functional data, and polymorphic
lambda-terms are used as distances for polymorphic
data. We then show how our semantics applies to two
example approximations: replacing reals with floatingpoint numbers, and loop perforation.

1. Introduction
Approximation is a fundamental concept in engineering and computer science, including notions such

as floating-point numbers, lossy compression, and approximation algorithms for NP-hard problems. Such
techniques are often used to trade off accuracy of the
result for reduced resource usage, for resources such
as computation time, power, and memory. In addition,
some approximation techniques are also used to ensure
computability. For example, true representations of
real numbers (e.g., [7], [1]), require some operations,
such as comparison, to be incomputable; floating-point
comparison, in contrast, is efficiently decidable on
modern computers.
Recently, there has been a growing interest in
language-based approximations, where approximate
program transformations are performed by the programming language environment [21], [12], [19], [18],
[4], [3], [16]. Such approaches allow the user to give an
exact program as a specification, and then apply some
set of transformations to this specification, yielding an
approximate program. The goal is for approximations
to be performed on behalf of the programmer, either
fully automatically or with only high-level input from
the user, while still maintaining a given error bound;
i.e., the goals are automation and correctness. These
goals can in turn increase programmer productivity
while helping to remove programmer errors, where
the latter can be especially important, for example, in
safety-critical systems.
This leads us to a fundamental question: what does it
mean for an approximate transformation to be correct?
A good answer to this question must surely be quantitative, since approximate transformations should not
change the output by too much; i.e., they must respect
user-specified error bounds. Correctness should also be
modular, meaning that, in settings where approximate
transformations T1 , . . . , Tk are applied together to a
program P , it should be possible to reduce the proof
of correctness of {T1 , . . . , Tk } to individual proof
obligations for the Ti s. Current formal approaches to
approximate program transformations, however, do not
permit such modular reasoning about approximations.

Typically, they are tailored to specific forms of approximation — for example, the use of floating-point
numbers or loop perforation [19] (skipping certain iterations in long-running loops). Even when multiple approximations can be combined, reasoning about them
is monolithic; in the above example, if T1 is changed
slightly, we would need to re-prove the correctness of
P with respect to not just T1 but {T1 , . . . , Tk }. In
addition, current approaches to approximate computation [2], [21], [19], [18], [4] are almost universally
restricted to first-order programs over restricted data
types.
In this work, we improve on this state of the art by
giving a general, composable semantics for program
approximation, for higher-order programs with polymorphic types. In our semantics, individual approximate transformations are proved to be quantifiably
correct, i.e., to induce a given local error expression.
Error expressions are then combined compositionally,
yielding a top-level error expression for the whole program that is built up from the errors of the individual
approximate transforms being used. This approach has
a number of benefits. First, it allows for more portable
proofs: an approximate transformation T can now be
proved correct once, and the resulting error expression
can be used many times in many different contexts.
Second, it is mechanical and opens up opportunities for
automation: approximation errors for a whole program
and a set of disparate approximate transformations are
generated simply by composing the errors of the individual transformations. Finally, our approach reduces
the correctness of approximately transformed programs
to the much easier question of whether a generated
error expression is less than or equal to a given error
bound.
The key technical insight that makes our semantics
possible is that, despite past work on using metric
spaces and real numbers in program semantics (e.g.,
[20], [15], [11]), we argue that real numbers cannot
in general capture how, for example, the output error
of a function depends on the input and its error.
Instead, our approach allows arbitrary System F types
for errors. We show that this can accurately capture
errors, for example, by using functions as errors for
functional data and polymorphic lambdas as errors for
polymorphic data. To allow this, our semantics is based
around a novel notion of an approximation type, which
is a ternary logical relation [6], [17] between exact
expressions e, approximate expressions a, and error
expressions q. In addition to the above benefits, this
approach can also handle changes of type between
exact and approximate expressions, e.g., approximating
real numbers by floating-point.

The remainder of the paper is organized as follows. Section 2 motivates our semantics with a highlevel overview. Section 3 defines our input language,
F ADT+ , which is System F with algebraic datatypes
and built-in operations. Section 4 defines our semantics
by defining the notion of approximation types mentioned above. Section 5 then shows how our semantics
of approximation types can be used to verify an
approximating compiler which compiles real numbers
into floating-point numbers and optionally performs
loop perforation [12], [19]. Note that the error bounds
created for the real to floating-point approximation
essentially yields a general approach to floating-point
error analysis [10], [5] that works for higher-order
and even polymorphic programs. Finally, Section 6
discusses related work and Section 7 concludes.

2. Approximating Programs
The goal of this work is to give a semantics for approximate transformations, which convert an exact program e into an approximate program a that, although
not identical to the e, is within some quantifiable error
bound q. Our notion of approximate transformation is
very general, but it includes at least:
Data Approximations: a uses a less exact datatype,
such as floating-point numbers instead of reals;
Approximations of Incomputable Operations: a
uses inexact but computable versions of potentially incomputable operations, such as f (n) for
finite n in place of limx→∞ f (x); and
Approximate Optimizations: a performs a cheaper,
less precise version of a computation, such as the
identity function in place of sin(x).
The point of language-based approximations is that
these transformations become part of the language
semantics, which precisely captures the relationship
between exact programs, their approximations, and the
associated error bounds.
As a simple yet illustrative example, consider an
approximate transformation that replaces the sin operator with the identity function λx. x. Such an approximation can greatly reduce computation, since sin
(for floating-point numbers) can be a costly operation,
while the identity function is a no-op. Intuitively, we
know that this change does not greatly affect the output
when x is close to 0. If, however, the output of a
call to sin is then passed to a numerically sensitive
operation, such as a reciprical, then the small change
resulting from replacing sin by the identity could lead
to a large change in the final result. Thus, our goal is
to quantify the error introduced by this approximate

Original
Program:

in

sin

output error:
err + in - sin(in)

input error: err
Approximate
Program:

in’

sin(in)

λx.x

in’

Figure 1. Error of Approximating sin with λx. x

transformation in a local, compositional way, allowing
this error to be propogated through the rest of the
program.
Figure 1 allows us to visualize the error resulting
from replacing sin with the identity function. We
assume that the input in has already been approximated, yielding an approximate input in0 with some
approximation error err. The exact output, sin(in),
gets replaced by an approximate result equal to in0 .
The error for this expression can then be calculated as
err + in − sin(in), as described in the figure.
This example leads to the following observations:
1) Errors are programs: Although the standard
approach to quantification and errors is to use
metric spaces and real numbers, the error expression err + in − sin(in) in our example depends
on both the input in and the input error err; i.e.,
it is a function, which cannot be represented by
a single real number.
2) Errors are compositional: Approximation errors in the input to sin are substituted into the
approximation error for sin itself, and this error
is in turn passed to any further approximations
that occur at a later point in the computation.
In order to formalize the relationship between programs, their approximations, and the resulting errors,
we define a semantic notion below called an approximation type. An approximation type is a form
of logical relation (see, e.g., [6], [17]), satisfying
certain properties discussed below, that relates exact
expressions e, approximate expressions a, and error
expressions q. If A is an approximation type, we write
{|a|}qA for the set of all exact expressions e related by
A to approximate expression a and error expressions
q. Thus, e ∈ {|a|}qA means that e can be approximated
by a with approximation error no greater than q when
using approximation type A.
As a first example, we define the approximation type
Fl that relates real number expressions e, floatingpoint expressions a, and non-negative real number
expressions q iff q is the distance between the e and the
real number corresponding to a. For instance, the real

number π is within error 0.1415926 . . . of the floatingpoint number 3, meaning that π ∈ {|3|}0.1415926...
Fl
holds. If the only difference between a and e is that
the former uses floating-point numbers in place of
reals, then showing e ∈ {|a|}qFl is essentially a form of
floating-point error analysis. Using Fl is more general,
however, because it allows the possibility that a performs further approximations, e.g., using the identity
in place of sin. Taking this comparison further, Fl is
specifically like an interval-based error analysis; we
examine this more closely in Section 5.2.
For functions, following Figure 1, we use an approximation type where the error of approximating a
function is itself a function, that maps exact inputs
and their approximation errors to output approximation
errors. More formally, if A1 and A2 are approximation types for the input and output of a function,
respectively, then then functional approximation type
A1 ⇒ A2 is defined such that e ∈ {|a|}qA1 ⇒A2 iff
e e1 ∈ {|a a1 |}qAe21 q1 for all e1 , a1 , and q1 such that
e1 ∈ {|a1 |}qA11 .
These notions can then be used to prove correctness
of approximate tranformations, as follows. First, the
designer of an approximate transformation gives an
approximation rule for the judgment ` e
a ≤ q : A,
stating that expressions matching e can be transformed
into a with error at most q using approximation type
A. Approximation rules are explained in more detail
below, but, as an example, our sin approximation above
can be captured as:
` sin

λx. x ≤ λx. λq. q + x − sin(x) : Fl ⇒ Fl

After formulating this rule, it must then be proved
correct, by proving that e ∈ {|a|}qA for all e, a, and
q that match the rule. As argued above, a significant
benefit of this approach is that it allows approximate
transformations to be analyzed and proved correct on
their own, without reference to the programs in which
they are being used.

3. System F as a Logical Language
In the remainder of this paper, we work in System
F with algebraic datatypes (ADTs) (see, e.g., Pierce
[13]), extended to allow uncountability and incomputability. Specifically, ADTs can have uncountably
many constructors, while built-in operations can perform potentially incomputable functions. The former is
useful for modeling the real numbers, while the latter
is useful for modeling operations on real numbers such
as comparison that are incomputable in general (e.g.,
[7], [1]). We refer to this language as F ADT+ .

The only additional technical machinery needed for
these extensions to System F is to require that all builtin functions are definable in the meta-language (set
theory or type theory). More specifically, we assume
as given some set of built-in operation symbols f ,
each with a given type τf and meta-language relation
Rf relating allowed inputs for the function defined by
f to their corresponding outputs. Further, we assume
that each Rf obeys τf and relates only one output
to any given set of inputs. The small-step evaluation
relation of System F is then be extended to allow f
applied to any values to evaluate to any output related
to those inputs by Rf . The details are straightforward
but tedious, and so are omitted here.
We use −→ to denote the small-step evaluation
relation of F ADT+ ; i.e., e −→ e0 means that e
evaluates in one step to e0 . Typing contexts Γ are
lists of type variables X that are considered in scope,
along with pairs x : τ of expression variables x
along with their types. Substitutions for expressions
e1 through en for variables x1 through xn are written
[e1 /x1 , . . . , en /xn ]. These are represented with the
letter σ, and we define capture-avoiding substitution σe
for expressions and στ for types in the usual manner.
Well-formedness of types and expressions is given
respectively by the kinding judgment Γ ` τ : ∗ and
typing judgment Γ ` e : τ , defined in the standard
manner. We write JΓ ` τ K for the set of all expressions
e such that Γ ` e : τ . Expressions or types with no
free variables are ground. Typing is extended to typing
contexts Γ and substitutions in the usual manner: ` Γ
indicates that all types in Γ are well-kinded, while
Γ ` σ : Γ0 indicates that Dom(σ) = Dom(Γ0 ), Γ `
σ(X) : ∗ for all X ∈ Dom(σ), and Γ ` σ(x) : Γ0 (x)
for all x ∈ Dom(σ). We assume all types are wellkinded and all expressions, contexts, and substitutions
are well-typed below.
We write e ↓ to denote that e is terminating. An
expression context C an expression with exactly one
occurrence of a “hole” {}, and C{e} denotes the (noncapture-avoiding) replacement of {} with e. Contextual
equivalence e1 ∼
= e2 is then defined to hold iff, for all
C and τ 0 such that · ` C{ei } : τ 0 for i ∈ {1, 2}, we
have that C{e1 } ↓ iff C{e2 } ↓. We use ⊥ to denote an
arbitrary non-terminating expression. fix(λx. x) of a
given type τ . We assume below type R of real numbers,
represented with an uncountable number of constructors, and the type R+∞ of the non-negative reals with
infinity. We use 0R for the R-constructor corresponding
to the real number 0, and ≤R , +R , and dR for the
function symbols whose functions perform real number
comparison, addition, and absolute difference, both on
R and, abusing notation slightly, on R+∞ .

Since F ADT+ can contain incomputable built-in
operations, we can additionally use it as a metalogic by embedding any relations of a given metalanguage, such as set theory or type theory, as builtin operations. We assume an ADT Prop with the
sole constructor > :: Prop, which will intuitively be
used as the type of propositions; a “true” proposition
terminates to > and a “false” one is non-terminating,
i.e., is contextually equivalent to ⊥. A meta-language
relation R can then be added to F ADT+ as a function
~ τ → Prop iff R is a set of
symbol fR of type ∀X.~
0
~
tuples hτ , ~ei such that · ` fR [τ~0 ] ~e : Prop that
is closed under contextual equivalence and contains
only terminating expressions ~e. Note that this latter
restriction is not too significant because we can always
~
use a “thunkified” relation R0 of type ∀X.(Unit
→
τ1 ) → . . . → (Unit → τn ) → Prop such that
hτ~0 , ~ei ∈ R iff hτ~0 , λx. e1 , . . . , λx. en i ∈ R. As an
example, we can immediately see that the thunkified
version of contextual equivalence itself is a relation of
type ∀X.(Unit → X) → (Unit → X) → Prop.
Lemma 1 (Consistency): For any class of built-in
operations f with functions Ff , > ∼
= ⊥ does not hold.
In the below, φ refers to expressions of type
~ τ → Prop. A constrained context is a pair hΓ; φi
∀X.~
of a context Γ and an expression φ such that Γ `
φ : Prop. A substitution σ satisfies hΓ; φi, written
σ  hΓ; φi, iff · ` σ : Γ and σ(φ) ∼
= >. We say
that hΓ; φi entails φ, written hΓ; φi ` φ true, iff
∀σ  hΓ; φi.σ(φ) ∼
= > holds. Finally, we say that σ
is a substitution from hΓ1 ; φ1 i to hΓ2 ; φ2 i, written
hΓ2 ; φ2 i ` σ : hΓ1 ; φ1 i, iff Γ2 ` σ : Γ1 and
hΓ2 ; φ2 i ` σ(φ1 ) true.

4. A Semantics of Program Approximation
In this section, we define approximation types and
illustrate them with examples. The main technical
difficulty is that the straightforward way to handle
free (expression and type) variables involves a circular
definition. Specifically, to fit with the logical relations
approach, e ∈ {|a|}qA for e, a, and q with free variables
should only hold iff σe ∈ {|σa|}σq
A for all substitutions
σ for exact variables xe , approximate variablesq xa ,
σx
and error variables xq such that σxe ∈ {|σxa |}A0 for
some approximation A0 . This defines approximation
types in terms of approximation types! To remove
this circularity, we first define approximation types
that handle a given set of free variables arbitrarily,
in Section 4.1. We then show in Section 4.2 how
to lift ground approximation types into approximation
functions, which uniformly handle any given context
of variables in the “right” way.

4.1. Approximation Types
Definition 1 (Expression-Preorder): Let Γ ` τ : ∗.
A relation ≤ is called a (Γ ` τ )-expression preorder
iff it is a preorder (reflexive and transitive) over ∼
=equivalence classes of JΓ ` τ K.
Definition 2 (Quantification Type): A Quantification type is a is a tuple Q = hΓ, Q, ≤, +, 0i of: a
typing context Γ and a type Q such that Γ ` Q : ∗; a
(Γ ` Q)-expression preorder ≤; and two expressions
+ (sometimes written in infix notation) and 0 of types
Q → Q → Q and Q (relative to Γ), respectively, such
that 0 is a least element for ≤, + is monotone with
respect to ≤ and hJΓ ` QK, +, 0i forms a monoid
with respect to the equivalence relation Q= (≤ ∩ ≥).
Stated differently, the following must hold:
Closedness: e1 , e2 ∈ JΓ ` QK implies e1 + e2 ∈
JΓ ` QK;
Monotonicity: e1 ≤ e01 and e2 ≤ e02 implies e1 +
e2 ≤ e01 + e02 ;
Leastness of 0: 0 ≤ e for all e ∈ JΓ ` QK;
Identity: e + 0 Q e for all e ∈ JΓ ` QK;
Commutativity: e1 +e2 Q e2 +e1 for ei ∈ JΓ ` QK;
and
Associativity: e1 + (e2 + e3 ) Q (e1 + e2 ) + e3 for
ei ∈ JΓ ` QK.
Such a tuple is sometimes called a Q- or (Γ ` Q)Quantification type. If Γ = · then Q is said to be
ground.
In the below, we often omit Γ when it is clear from
context, writing hQ, ≤, +, 0i. We also write QQ ,
≤Q , +Q , and IQ for the corresponding elements of
Q. We sometimes omit the Q subscript where Q can
be inferred from context. The following lemma gives
a final, implied constraint, that ⊥ is always infinity:
Lemma 2: For any quantification type Q, e ≤Q ⊥
for all e ∈ JΓ ` QK.
Example 1 (Non-Negative Reals): QR
=
hR+∞ , ≤R , +R , 0R i is a ground quantification
type that corresponds to the standard ordering and
addition on the non-negative reals.
Example 2 (Non-Negative Real Functions):
For any ground τ , hτ → R+∞ , ≤τ →R+∞
, λx1 . λx2 . λy. x1 y +R x2 y, λy. 0R i is a ground
quantification type, where addition is performed
pointwise on functions and e1 ≤τ →R+∞ e2 iff
e1 e ≤R e2 e for all ground e of type τ ; i.e., iff the
output of e1 is always no greater than that of e2 .
Definition 3 (Approximate Equality): Let Γq and
Γe be any contexts with disjoint domains, let Q be
a (Γq , Γe ` Q))-quantification type, and let E by
any type such that Γe ` E : ∗. A (Q, Γe , E)approximate equality relation is a ternary relation

e1 ≈q e2 ⊆ JΓq , Γe ` QK × JΓe ` EK × JΓe ` EK,
where q ∈ JΓq , Γe ` QK and each ei ∈ JΓe ` EK, that
satisfies the following:
Upward Closedness: e1 ≈q e2 and q ≤ q 0 implies
0
e 1 ≈q e 2 ;
Reflexivity: e1 ∼
= e2 implies e1 ≈0Q e2 ;
Symmetry: e1 ≈q e2 implies e2 ≈q e1 ;
Triangle Inequality: e1 ≈q1 e2 and e2 ≈q2 e3
implies e1 ≈q1 +q2 e3 ; and
Completeness: e1 ≈⊥ e2 for all e1 , e2 ∈ JΓ ` EK.
An approximation equality relation is ground iff
Γe = Γq = ·. In the below, we often omit Γq and Γe
when clear from context. We use a subscript to denote
which approximate equality relation is intended, as in
e1 ≈qA e2 , when it is not clear from context.
Example 3 (Reals): The relation e1 ≈qR e2 that
holds iff q ∼
= ⊥, or e1 ∼
= e2 , or |e1 − e2 | ≤R q is
a ground (R+∞ , R)-approximate equality relation that
corresponds to the standard distance over the reals.
Example 4 (Real Functions): The
relation
e1 ≈qR→R e2 that holds iff q ∼
= ⊥, or e1 ∼
= e2 ,
or |(e1 r) − (e2 r)| ≤R (q r r+ ) for all r ∈ R and
r+ ∈ R+∞ , is a ground (R → R+∞ → R+∞ , R → R)approximate equality relation, where, intuitively, the
distance between two functions e1 and e2 is given by
a function q that bounds the distance between their
outputs for each input.
Definition 4 (Approximation Type): Let Γe , Γa , and
q
Γ be three domain-disjoint contexts. A (Γe , Γa , Γq )approximation type is a tuple hQ, E, A, ≈, {| · |}· i
of: a (Γq , Γe ` Q)-quantification type Q; types E and
A, called respectively the exact and approximate types,
such that Γe ` E : ∗ and Γa ` A : ∗; a (Q, Γe , E)approximate equality relation ≈; and a mapping {|a|}q :
(JΓq , Γe ` QK × JΓa ` AK) → P(JΓe ` EK), where
q ∈ JΓq , Γe ` QK and a ∈ JΓa ` AK, that satisfies:
Error Weakening: q1 ≤ q2 implies {|a|}q1 ⊆ {|a|}q2 ;
0
Error Addition: e1 ∈ {|a|}q and e1 ≈q e2 implies
0
e2 ∈ {|a|}q+q ;
Equivalence: If q ∼
= q0 , a ∼
= a0 , and e ∼
= e0 then
q
0
0 q0
e ∈ {|a|} implies e ∈ {|a |} ;
Approximate Equality: e1 , e2 ∈ {|a|}q implies
e1 ≈q+q e2 ; and
A ground approximation type is one where Γe =
Γa = Γq = ·. In the below, we write A for approximation types, writing {|a|}qA for the set to which A maps q
and a, · ≈·A · for the approximate equality relation, EA
and AA for the exact and approximate types, QA for
the quantification type, and QA , ≤A , and +A for the
elements of QA . Again, we often omit the subscript
A when it can be inferred from context.
Example 5 (Floating-Point Numbers): Let

e ∈ {|a|}qFl iff q ∼
= ⊥, or e ∼
= ⊥ and a ∼
= ⊥,
or |e − real(a)| ≤R q where real maps (the value of)
a to its corresponding real number. We then have
that Fl = hQR , R, Fl, ≈R , {| · |}·Fl i is a ground
approximation type where a real can be approximated
by a floating-point number with an error given by the
real-number distance between the two.
Example 6 (Floating-Point Functions): Let e ∈
{|a|}qFl⇒Fl iff q ∼
= ⊥, or e ∼
= ⊥ and a ∼
= ⊥, or
0 0
0
q
e
q
e e0 ∈ {|a a0 |}Fl
for all e0 ∈ {|a0 |}qFl . We then have
that Fl ⇒ Fl = hR ⇒ R+∞ ⇒ QR , R → R, Fl →
Fl, ≈Fl⇒Fl , {| · |}·Fl⇒Fl i is a ground approximation
type, where R ⇒ R+∞ ⇒ QR is the quantification
type obtained from QR by applying the construction
of Example 2 twice. Intuitively, this approximation
type allows a real function f to be approximated by
a floating-point function f 0 with an error q whenever
q r qr bounds the error between calling f on exact real
number r and calling f 0 on a floating-point number
with at most distance qr from r.

4.2. Approximation Families
Definition 5 (Approximation Families): Let Γ =
Γe , Γa , Γq , ΓA for four domain-disjoint typing contexts
and φ be an expression such that Γ ` φ : Prop.
We say that F = hE, A, Q, 0, +, F i is a
(Γe , Γa , Γq , ΓA , φ)-approximation family iff Γe ` E :
∗, Γa ` A : ∗, Γe , Γq ` Q : ∗, Γe , Γq ` 0 : Q,
Γe , Γq ` 0 : Q → Q → Q, and F is a meta-language
function from substitutions σ such that σ  hΓ; φi to
ground approximation types A such that EA = σ(E),
AA = σ(A), QA = σ(Q), 0A = σ(0), and +A = σ(+).
We use a subscript F to denote the elements of F;
e.g., EF denotes the exact type E of F. We write F(σ)
for the approximation resulting from applying the F
component to σ. A (·, ·, ·, ·, >)-approximation family is
called ground. Note that the ground F are isomorphic
to the ground approximation types A, since, if F is
ground, then the domain of FF consists of the sole
pair h·; ·i.
We define approximation contexts Ξ with grammar:
· Ξ, (xe , xa , xq ) : F Ξ, (X e , X a , X q ) : ξ Ξ, Γ.(φ)
The form (xe , xa , xq ) : F introduces variables xe ,
xa , and xq such that xa is an approximation of xe
with error xq in some approximation returned by
approximation family F. The form (X e , X a , X q ) : ξ
introduces type variables X e , X a , and X q , along with
a variable ξ that quantifies over approximations of
X e by X a with error X q . Finally, the form Γ.(φ)
introduces additional variables in Γ and constraint φ.

More formally, let |Ξ|e , |Ξ|a , |Ξ|q , and |Ξ|A be
typing contexts that contain, respectively: all xe and
X e ; all xa and X a ; all xq , X q , and contexts Γ
in a Γ.(φ) form; and all ξ variables in Ξ. Further,
let |Ξ|p be the conjunction of the following formuq
las: xe ∈ {|xa |}x for each (xe , xa , xq ) : F; the
formula isapprox[X e , X a , X q ] stating that ξ is an
approximation of X e by X a with error X q for each
(X e , X a , X q ) : ξ; and φ for each Γ.(φ). We use
the abbreviations |Ξ|eq = |Ξ|e , |Ξ|q and |Ξ|eaqA =
|Ξ|e , |Ξ|a , |Ξ|q , |Ξ|A . The approximation context Ξ is
well-formed, written ` Ξ, iff ` |Ξ|eaqA and |Ξ|eaqA `
φ : Prop. We say F is a Ξ-approximation family,
written Ξ ` F, iff F is a (|Ξ|e , |Ξ|a , |Ξ|q , |Ξ|A , |Ξ|p )approximation family. A σ is a substitution from Ξ to
Ξ0 , written Ξ0 ` σ : Ξ, iff h|Ξ0 |eaqA ; |Ξ0 |p i ` σ :
h|Ξ|eaqA ; |Ξ|p i.
Although the functions F in approximation families
return only ground approximations, we can create nonground approximation types from F as follows. Let
Ξ be any approximation context and F be any Ξapproximation family. The notation Ξ
F then denotes the (|Ξ|e , |Ξ|a , |Ξ|q )-approximation hQ, E, A, ≈
, {| · |}· i where Q = h|Ξ|eq , QF , ≤, 0F , +F i and:
•
•
•

q1 ≤ q2 iff ∀σ  h|Ξ|eaqA ; |Ξ|p i. σq1 ≤F (σ) σq2 ;
e1 ≈q e2 iff ∀σ  h|Ξ|eaqA ; |Ξ|p i. σe1 ≈σq
F (σ)
σe2 ; and
e ∈ {|a|}q iff ∀σ  h|Ξ|eaqA ; |Ξ|p i. σe ∈
{|σa|}σq
F (σ) .

We call an approximation formed this way a Ξapproximation.
Theorem 1: If ` Ξ and Ξ ` F then Ξ
F is a
valid approximation type.
Lemma 3 (Approximation Weakening): Let Ξ ` F
and ` Ξ, Ξ0 . We then have that: Ξ, Ξ0 ` F; q1 ≤Ξ F
q2 implies q1 ≤Ξ,Ξ0 F q2 ; e1 ≈qΞ F e2 implies
e1 ≈qΞ,Ξ0 F e2 ; and e ∈ {|a|}qΞ F implies e ∈
{|a|}qΞ,Ξ0 F .
We define substitution σ(F) into approximation families as yielding the approximation family
hσE, σA, σQ, σ0, σ+, λσ 0 . F (σ 0 ◦ σ)i:
Lemma 4 (Approximation Substitution): If Ξ, Ξ0 `
F and Ξ ` σ : Ξ0 then: Ξ ` σ(F); q1 ≤Ξ,Ξ0 F q2
implies σq1 ≤Ξ σ(F ) σq2 ; e1 ≈qΞ,Ξ0 F e2 implies
q
σe1 ≈σq
Ξ σ(F ) σe2 ; and e ∈ {|a|}Ξ,Ξ0 F implies
σe ∈ {|σa|}σq
Ξ σ(F ) .
Definition 6 (Π-Approximations): If F is a Ξ0 , Ξapproximation family, then Π(Ξ).F is the Ξ0 approximation family h|Ξ|e → EF , |Ξ|a → AF , |Ξ|eq →
QF , λ|Ξ|eq . 0F , λ|Ξ|eq .+F , F 0 i where F 0 (σ) for
σ  h|Ξ0 |eaqA ; |Ξ0 |p i is defined such that: q1 ≤F 0 (σ) q2
iff q1 |Ξ|eq ≤Ξ σ(F ) q2 |Ξ|eq ; e1 ≈qF 0 (σ) e2 iff

q |Ξ|eq
q
e
σ(F ) e2 |Ξ| ; and e ∈ {|a|}F 0 (σ) iff
eq
q |Ξ|
{|a |Ξ|a |}Ξ σ(F ) . Intuitively, Π(Ξ).F forms
e

e1 |Ξ|e ≈Ξ
e

(e |Ξ| ) ∈
an approximation family where λ|Ξ| . e is approximated by λ|Ξ|a . a with error λ|Ξ|eq . q whenever e
is approximated by a with error q in approximation context Ξ. When Ξ is just the single element
(xe , xa , xq ) : F1 and F2 does not depend on the values
substituted for xe , xa , or xq , then Π(Ξ).F2 , which we
abbreviate as F1 ⇒ F2 , yields the notion of function
approximation types discussed in Section 2 and in
Example 6.
To approximate the polymorphic type ∀X.E we use
Π((X e , X a , X q ) : ξ, z 0 : X q ,
z + : X q → X q → X q .(z 0 ∼
= 0ξ ∧ z + ∼
= +ξ )).F
This approximation family quantifies over the type
variables X e , X a , and X q for the exact, approximate,
and error types, as well as over the variables z 0
and z + for the zero error and error addition of the
approximation type ξ. The latter variables are explicitly
abstracted in order to allow error expressions to refer
to them: recall that ξ is only bound in |Ξ|p , not |Ξ|q ;
i.e., error terms refer only to X e and X q , not to
ξ. Abusing notation slightly, we abbreviate the above
approximation family as Π(X, z : ξ).F.

5. Verifying an Approximating Compiler
As discussed in the Introduction, the long-term goal
of this work is to enable language-based approximations, where a compiler or other tool performs approximate transformations in a correct and automated
manner. In this section, we show how to verify such a
tool, the goal of the current work, with the semantics
given in the previous section. Specifically, we consider
a tool that performs two transformations: it compiles
real numbers into floating-point implementations; and
it optionally performs loop perforation [12], [19]. For
the current work, we assume only that our tool can be
specified with an approximate compilation judgment
Ξ ` e
a ≤ q : A such that this judgment
can be derived whenever the tool might approximate
exact expression e by a with error bound by q using
approximation type A and assumptions Ξ. Intuitively,
each rule of this judgment corresponds to an approximate transformation that the tool might perform; for
example, the approximation rule of Section 2, for
approximating sin by λx. x, might be included. We
ignore the specifics of how the tool chooses which
approximations to use where, as long as all possible
choices are contained in the approximate compilation
judgment.

To verify such a tool, we then prove soundness of
its approximate compilation judgment. Soundness here
means that Ξ ` e
a ≤ q : A implies e ∈ {|a|}qΞ A .
This can be proved in a local, modular fashion, by
verifying each approximation rule individually; more
specifically, if an approximation rule derives Ξ ` e
a ≤ q : A from assumptions Ξi ` ei
ai ≤ qi : Ai
for 1 ≤ i ≤ n and side conditions φj for 1 ≤ j ≤ m,
then the rule is correct iff e ∈ {|a|}qΞ A holds whenever
ei ∈ {|ai |}qΞii Ai for all i and φj holds for all j.
This also allows extensibility, since additional rules can
always be added as long as they are proved correct.
In the remainder of this section, we consider rules
that would be used in our example tool, including:
compositionality rules (Section 5.1); rules for replacing
real numbers by floating-point implementations (Section 5.2); and a rule for performing loop perforation
(Section 5.3).

5.1. Compositionality Rules
In order to combine errors from individual approximate transforms into a single, whole-program error, we
now introduce the compositionality rules. These rules,
given in Figure 2, are essentially the identity, stating
that each expresison construct can be approximated by
itself; however, they show how to build up and combine
error expressions for different contructs.
The first rule, A-W EAK, allows the error bound
to be weakened from q to any greater error q 0 . The
A-VAR rule approximates variable xe by xa with error
xq when these variables are associated in Ξ. The
rule A-L AM approximates a lambda-abstraction λxe . e
with a lambda-abstraction λxa . a by approximating
the body e by a, using the error function λxe . λxq . q
that abstracts over the input xe and its approximation
error xq . The A-A PP rule approximates applications
e1 e2 by applying the approximation of e1 to that
of e2 and applying the error for e1 to both e2 and
its error. The A-TL AM rule approximates polymorphic lambdas ΛX e . e by approximating the body e
in the extended approximation context Ξ, X, z : ξ,
recalling the abbreviation X, z : ξ from Section 4.2
that abstracts the various components of approximation families. A-TA PP approximates type applications
e[EF ] where the type involved is the exact type of
some approximation family F. This is accomplished
by first approximating e to some a with error q in the
polymorphic approximation Π(X, z : ξ).F 0 introduced
in Definition 6, and then applying a to the approximate
type AF of F. The error q is applied to the necessary
components of F, and the resulting approximation is
F 0 with F substituted for ξ and all the appropriate

Ξ`e

a ≤ q : F q ≤Ξ
Ξ`e
a ≤ q0 : F

F

q0

A-W EAK

e

Ξ ` λx . e
Ξ ` e1

(xe , xa , xq ) : F ∈ Ξ
A-VAR
Ξ ` xe
xa ≤ xq : F

a1 ≤ q1 : Π((xe , xa , xq ) : F).F 0 Ξ ` e2

Ξ ` e1 e2

a2 ≤ q2 : F
A-A PP

a1 a2 ≤ q1 e2 q2 : [e/x , a/x , q/xq ]F 0
e

Ξ`e

Ξ, X, z : ξ ` e
a≤q:F
A-TL AM
Ξ ` ΛX . e
ΛX a . a
e
q
0
+
≤ ΛX . ΛX . λz . λz . q : Π(X, z : ξ).F
e

a

a ≤ q : Π(X, z : ξ).F 0

Ξ`F

Ξ ` e[EF ]
a[AF ]
≤ q[EF , QF ] 0F +F : [F/ξ, . . .]F 0

A-TA PP

a ≤ q : Π((xe , xa , xq ) : F).(xe ∼
= fix e ∧ xa ∼
= fix a ∧ xq ∼
= fix(q (fix e))) ⇒ F

Ξ`e

Ξ ` fix e
Ξ`e

Ξ, x : F ` e
a ≤ q : F0
A-L AM
a
e
q
λx . a ≤ λx . λx . q : Π((xe , xa , xq ) : F).F 0

a ≤ q0 : F 0

A-F IX

fix e ≤ fix(q (fix e)) : F

∀b ∈ {True, False}.Ξ ` eb

ab ≤ qb : F

Ξ ` if e then eTrue else eFalse

∀(b, b0 ) ∈ {True, False}.eb ∈ {|ab0 |}q

q0

Ξ,b∈{|b0 |} 0 F
F

if a then aTrue else aFalse ≤ q : F

A-I F

Figure 2. Compositionality Rules for Approximate Compilation
components of F substituted for the X and z variables.
This is abbreviated as [F/ξ, . . .]F 0 .
Fixed-points fix(e) are approximated using A-F IX.
This approximates e to a with error q, applying fix
to the results in the conclusion. The approximation
family used for e is F ⇒ F, augmented with the
assumption that the inputs xe , xa , and xq are equal
to the exact, approximate, and error fix-expressions in
the conclusion of the rule.
Finally, if-expressions are approximated with A-I F.
First, each component of the if-expression is approximated; the condition can use an arbitrary approximation family F 0 , while the then and else branches
must use the same family as the whole expression. The
final condition requires that the output error q bounds
the error between the branches taken in the exact and
approximate expressions, even if one takes the then
branch and the other takes the else branch. This is
stated by quantifying over all four combinations of
True or False in the exact and approximate conditions
that meet the error q 0 computed for approximating the
if-condition, and then requiring that the corresponding
then or else branches are within error q.
Lemma 5: Each rule of Figure 2 is sound.

5.2. Floating-Point Approximation
To approximate real-number programs with their
floating-point equivalents, we use the Fl approximation type formalized in Example 5. We then add rules
Ξ`r
Ξ ` opR

real(r) ≤ |r − real(r)| : Fl
opFloat ≤ opq : Fl ⇒ Fl ⇒ Fl

for each real number r and each built-in binary operation (such as +, ∗, etc.) op, where opR and opFloat
are the version of op for reals and floating-points,
respectively, and opq is the error function calculating
the size of the interval error in the output from those
of the inputs. The error functions opq to use for the
various operations can be derived in a straightforward
manner by considering the smallest error that bounds
the difference between the real result of opr and any
potential result of opFloat on floating-point numbers
in the input interval. The infinite error ⊥ is returned
in case of overflow or Not-A-Number results. For
instance, the error +q can defined (in pseudocode) as:
+q xe xq y e y q =
let I = round([(xe − xq ) + (y e − y q ),
(xe + xq ) + (y e + y q )]) in
if ∃r ∈ I.|r| ≥ MAXFLOAT then ⊥ else
maxr0 ∈I |r0 − r|
where round rounds all reals in an interval to floatingpoint numbers (using the current rounding mode) and
MAXFLOAT is the maximum absolute value of the
floating-point representation being used. The errors for
other operations can be defined similarly.
Using these rules with the compositionality rules of
Figure 2 yields an interval-based floating-point error
analysis that works for higher-order and even polymorphic terms. Although recent work has given more
precise floating-point error analyses than intervals [10],
[5], we anticipate, as future work, that such approaches
can also be incorporated into our framework, allowing
them to be used on higher-order, polymorphic programs.
Theorem 2: The rules listed above for compiling
reals to floating-points are sound.

Ξ ` e1
a1 ≤ q1 : F ⇒ F ⇒ F
Ξ ` e2
a2 ≤ 0 : Nat
x
Ξ ` e3
a3 ≤ q3 : Nat ⇒ F e1 x ≈qΞ,x:N
F e1 bxcK
q0
red-seq e1 e2 e3 ≈Ξ F red-seq e1 de2 eK e3
Ξ ` red-seq e1 e2 e3
red-seq (λx. (a1 x)K ) (a2 /K) (λx. a3 (x ∗ K))
≤ (red-seq +F e2 (λx. (q3 bxcK 0) +F (q x)))+F q 0 : F

Figure 3. Loop Perforation

5.3. Loop Perforation
Loop perforation [12], [19] is a powerful approximate transformation that takes a loop which combines
f (0), f (1), etc., for some computationally intensive
function f , and only performs every nth iteration,
repeating the values that are computed n times. We
formalize a simplified version of loop perforation as
operating on reductions red-seq e1 e2 e3 , defined as
the function that reduces, using e1 , the sequence of
values of e3 from 0 less than or equal to e2 . The
rule in Figure 3 shows how to perforate this reduction
by first approximating each ei to some ai with error
qi . The rule requires that the number e2 of sequence
elements can be approximated with 0 error; this is
not a fundamental limitation, but is simply made here
to simplify the exposition. The approximation type
Nat is defined similarly to Fl, except that the natural
numbers are used for the exact, approximate, and error
types. Next, the rule finds an error function q that,
when applied to input x, bounds the error between
the exact sequence value e1 x and the xth value in
the perforated sequence, which can be calculated as
e1 bncK . Finally, the rule considers the fact that n
may not be an exact multiple of K, in which case the
perforated loop actually computes the result of de2 eK
iterations. An error q 0 is thus synthesized to bound the
error between this perforated result and the original
reduction. The resulting approximation then performs
the perforation computation as described above, and
the error sums the errors (q3 bxcK 0), capturing the
approximation error of a3 , with (q x), capturing the
error of using bxcK instead of x, for each value x,
and then adds the error q 0 .
Theorem 3: The rule of Figure 3 is sound.

6. Related Work
A number of recent papers relate to program approximations. Possibly the closest to this work is the
work of Reed and Pierce [16], because they consider a
higher-order (though not polymorphic) input language.
They show how to perform an approximate program
transformation that adds noise to a database query to

ensure differential privacy, i.e., that a query cannot
violate the privacy of a single individual recorded in
the database. In order to ensure that adding noise does
not change the query results too much, a type system
is used to capture functions that are K-Lipschitz,
meaning that a change of δ in the input yields a change
of at most K ∗ δ in the output. This condition can be
captured in our system by the error λxe.λxq. K ∗ xq in
an approximation of a function.
Loop perforation [12], [19] transforms certain mapreduce programs, written as for-loops in C, to perform only a subset of their iterations. Section 5.3
shows how to capture a variant of this transformation
in our system. More recent work [21] has extended
loop perforation to sampling, which takes a random
(instead of a controlled) sample of the iterations of a
loop. This work also adds substitution transformations,
where different implementations of the same basic
operations (such as sin or log) are substituted to try
to trade off accuracy for performance.
EnerJ [18] allows the programmer to specify, with
type modifiers, whether data is exact or inexact. Inexact
data means the program can tolerate errors in this data.
Such data is then stored in low-power memory, which
is cheaper but is susceptible to random bit flips.
Carbin et al. [2] present a programming model
with relaxation, where certain values in a program are
allowed to vary in a pre-defined way, to model errors.
The authors then show how to verify properties of
relaxed programs despite these errors. Although this
work addresses some of the same questions as ours,
one significant drawback is that it cannot represent
the relationship between expressions of different types,
such as real-valued functions and functions on floatingpoint numbers used to implement them.
Approximate bisimulation [9] is a new technique for
relating discrete, continuous and hybrid systems in a
manner that can tolerate errors in a system. We are
still investigating the relationships between our system
and approximate bisimulation, but one key difference
with our work is that this approach considers only
transition systems, and so cannot be applied to higherorder programs, programs with recursive data, etc.;
however, such systems still encompass the large and
practical class of control systems.
Chaudhuri et al. [4], [3] have investigated a static
analysis for proving robustness of programs, which
they then argue is a useful precondition for approximate transformations. They define robustness as the
K-Lipschitz condition, which, again, can be captured
in our system as the error λxe.λxq. K ∗ xq .
Floating-point error analysis [10], [5] bounds the
error between a floating-point program and the syntaci-

cally equivalent real-number program. We showed
how to accomplish this in our setting in Section 5.2,
yielding what we believe is the first floating-point error
analysis to work for higher-order and polymorphic
programs. Although state-of-the-art analyses use affine
expressions, instead of intervals as we used above, we
anticipate that we will be able to accommodate these
approaches in our semantics as well, thereby adapting
them to higher-order and polymorphic programs.
On a technical note, our quantification types and
approximate equality relations were inspired by Flagg
and Kopperman’s continuity spaces [8], one of the few
works that considers a more general notion of distance
than metric spaces. Specifically, the distributive lattice
completion of a quantification type corresponds exactly
to Flagg and Kopperman’s abstract notion of distance,
called a quantale. A similar transformation turns an
approximate equality relation into a continuity space,
their generalization of metric spaces.

7. Conclusion
We have introduced a semantics for approximate
program transformations. The semantics relates an
exact program to an approximation of it, and quantifies
this relationship with an error expression. Rather than
specifying errors solely with real numbers and metric
spaces, our approach is based on approximation types,
an extension of logical relations that allows us to use,
for example, functions as the errors for approximations
of functions, and polymorphic types as the errors for
polymorphic types. We then show how approximation
types can be used to verify approximate transforms in
a modular, composable fashion, by proving soundness
of each transform individually and by including a set of
compositionality rules, also proved correct, that combine errors from individual approximate transforms
into a whole-program error.

References
[1] Boehm, H.J., Cartwright, R., Riggle, M., O’Donnell,
M.J.: Exact real arithmetic: a case study in higher order
programming. In: LISP and functional programming
(1986)
[2] Carbin, M., Kim, D., Misailovic, S., Rinard, M.: Proving acceptability properties of relaxed nondeterministic
approximate programs. In: PLDI (2012)
[3] Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity analysis of programs. In: POPL (2010)
[4] Chaudhuri, S., Gulwani, S., Lublinerman, R., Navidpour, S.: Proving programs robust. In: FSE (2011)

[5] Darulova, E., Kuncak, V.: Trustworthy numerical computation in scala. In: OOPSLA (2011)
[6] Dreyer, D., Ahmed, A., Birkedal, L.: Logical stepindexed logical relations. Logical Methods in Computer
Science 7(2) (2011)
[7] Edalat, A., Potts, P.J.: A new representation for exact
real numbers. In: MFPS (2005)
[8] Flagg, B., Kopperman, R.: Continuity spaces: reconciling domains and metric spaces. Theoretical Computer
Science 1 (1997)
[9] Girard, A., Pappas, G.J.: Approximate bisimulation: a
bridge between computer science and control theory.
European Journal of Control 17(5–6), 568–578 (2011)
[10] Goubault, E., Putot, S.: Static analysis of finite precision computations. In: VMCAI (2011)
[11] Manes, E.G.: Algebraic approaches to program semantics. Springer-Verlag New York, Inc. (1986)
[12] Misailovic, S., Roy, D., Rinard, M.: Probabilistically
accurate program transformations. In: SAS (2011)
[13] Pierce, B.: Types and Programming Languages. The
MIT Press (2002)
[14] Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and
monads of probability distributions. In: POPL (2002)
[15] Reed, G.M., Roscoe, A.W.: Metric spaces as models
for real-time concurrency. In: MFPS III (1988)
[16] Reed, J., Pierce, B.C.: Distance makes the types grow
stronger: A calculus for differential privacy. In: ICFP
(2010)
[17] Reynolds, J.C.: Types, abstraction and parametric
polymorphism. Information Processing 83(1), 513–523
(1983)
[18] Sampson, A., Dietl, W., Fortuna, E., Gnanapragasam,
D., Ceze, L., Grossman, D.: Enerj: Approximate data
types for safe and general low-power computation. In:
PLDI (2011)
[19] Sidiroglou, S., Misailovic, S., Hoffmann, H., Rinard,
M.: Managing performance vs. accuracy trade-offs with
loop perforation. In: FSE (2011)
[20] Turi, D., Rutten, J.: On the foundations of final coalgebra semantics: non-well-founded sets, partial orders,
metric spaces. Mathematical. Structures in Comp. Sci.
8(5), 481–540 (1998)
[21] Zhu, Z.A., Misailovic, S., Kelner, J.A., Rinard, M.:
Randomized accuracy-aware program transformations
for efficient approximate computations. In: POPL
(2012)

