Analytical Differential Calculus with Integration

Han Xu #
Department of Computer Science and Technology, Peking University, Beijing, China

Zhenjiang Hu #
Key Laboratory of High Confidence Software Technologies (MoE),
Department of Computer Science and Technology, Peking University, Beijing, China

Abstract
Differential lambda-calculus was first introduced by Thomas Ehrhard and Laurent Regnier in 2003.
Despite more than 15 years of history, little work has been done on a differential calculus with
integration. In this paper, we shall propose a differential calculus with integration from a programming
point of view. We show its good correspondence with mathematics, which is manifested by how
we construct these reduction rules and how we preserve important mathematical theorems in our
calculus. Moreover, we highlight applications of the calculus in incremental computation, automatic
differentiation, and computation approximation.

2012 ACM Subject Classification Software and its engineering → General programming languages;
Software and its engineering → Functional languages

Keywords and phrases Differential Calculus, Integration, Lambda Calculus, Incremental Computa-
tion, Adaptive Computing

Digital Object Identifier 10.4230/[Link].2021.143

Category Track B: Automata, Logic, Semantics, and Theory of Programming

Related Version Full Version: [Link]

1 Introduction

Differential calculus has more than 15 years of history in computer science since the pioneer
work by Thomas Ehrhard and Laurent Regnier [9]. It is, however, not well-studied from
the perspective of programming languages; we would expect the profound connection of
differential calculus with important fields such as incremental computation, automatic
differentiation and self-adjusting computation just like how mathematical analysis connects
with mathematics. We want to understand what is the semantics of the derivative of a
program and how we can use these derivatives to write a program. That is, we wish to have
a clear description of derivatives and introduce integration to compute from operational
derivatives to the program.
The two main lines of the related work are the differential lambda-calculus [9, 8] and the
change theory [7, 4, 5]. On one hand, the differential lambda-calculus uses linear substitution
to represent the derivative of a term. For example, given a term x ∗ x (i.e., x2 ), with the
differential lambda-calculus, we may use the term ∂x∗x ∂x · 1 to denote its derivative at 1. As
there are two alternatives to substitute 1 for x in the term x ∗ x, it gives (1 ∗ x) + (x ∗ 1)
(i.e., 2x) as the derivative (where + denotes “choice”).
Despite that the differential lambda-calculus provides a concise way to analyze the
alternatives of linear substitution on a lambda term, there is a gap between analysis on terms
and computation on terms. For instance, let +′ denote our usual addition operator, and +
′
′ ′
denote the choice of linear substitution. Then we have that ∂x+ x
∂x · 1 = (1 + x) + (x + 1),
′
which is far away from the expected 1 + 1. Moreover, it offers no method to integrate over a
∂t
derivative, say ∂x · y.
© Han Xu and Zhenjiang Hu;
EA

licensed under Creative Commons License CC-BY 4.0

TC S

48th International Colloquium on Automata, Languages, and Programming (ICALP 2021).

Editors: Nikhil Bansal, Emanuela Merelli, and James Worrell; Article No. 143; pp. 143:1–143:20
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
143:2 Analytical Differential Calculus with Integration

On the other hand, the change theory gives a systematic way to define and propagate
(transfer) changes. The main idea is to define the change of function f as Derive f , satisfying

f (x ⊕ ∆x) = f (x) ⊕ (Derive f ) x ∆x.

where ⊕ denotes an updating operation. It reads that the change over the input x by ∆x
results in the change over the result of f (x) by (Derive f ) x ∆x. While change theory
provides a general way to describe changes, the changes it described are differences (deltas)
instead of derivatives. It is worth noting that derivative is not the same as delta. For example,
by change theory, we can deduce that f (x) will be of the form of x ∗ x + C if we know
(Derive f ) x ∆x = 2 ∗ x ∗ ∆x + ∆x ∗ ∆x, but we cannot deduce this form if we just know
that its derivative is 2 ∗ x, because change theory has no concept of integration or limits.
Although a bunch of work has been done on derivatives [9, 8, 7, 4, 19, 16, 21, 10, 1],
there is unfortunately, as far as we are aware, little work on integration. It may be natural
to ask what a derivative really means if we cannot integrate it. If there is only a mapping
from a term to its derivative without its corresponding integration, how can we operate on
derivatives with a clear understanding of what we actually have done?
In this paper1 , we aim at a new differential framework, having dual mapping between
derivatives and integrations. With this framework, we can manifest the power of this dual
mapping by proving, among others, three important theorems, namely the Newton-Leibniz
formula, the Chain Rule and the Taylor’s theorem.
Our key idea can be illustrated by a simple example. Suppose we have a function f map-
ping from an n-dimensional space to an m-dimensional space. Then, let x be (x1 , x2 , ..., xn )T ,
and f (x) be (f1 (x), f2 (x), ..., fm (x))T . Mathematically, we can use a Jacobian matrix A to
represent its derivative, which satisfies the equation
 ∂f ∂f1 ∂f1

1
∂x1 ∂x2 · · · ∂x n
 ∂f2 ∂f2 ∂f2 
· · · ∂x
 ∂x1 ∂x
f (x + ∆x) − f (x) = A∆x + o(∆x), where A =  2 n

 ··· ··· ··· ··· 

∂fm ∂fm
∂x1 ∂x2 · · · ∂f
∂xn
m

However, computer programs usually describe computation over data of some structure,
rather than just scalar data or matrix. In this paper, we extend the idea and propose a new
calculus that enables us to perform differentiation and integration on data structures. Our
main contributions are summarized as follows.
To our knowledge, we have made the first attempt of designing a calculus that provides
both derivative and integral. It is an extension of the lambda-calculus with five new
operators including derivatives and integrations. We give clear semantics and typing
rules, and prove that it is sound and strongly normalizing. (Section 2)
We prove three important theorems and highlight their practical application for incre-
mental computation, automatic differentiation, and computation approximation.
R t ∂t
We prove the Newton-Leibniz formula: t12 ∂y |x dx = t[t2 /y] ⊖ t[t1 /y], which is also
known as Second Fundamental Theorem of Calculus. It shows the duality between
derivatives and integrations, and can be used for incremental computation. (Section 3)
We prove the Chain Rule: ∂f ∂x (g x)
|t1 ∗ t = ∂f∂yy |g t1 ∗ ( ∂g∂zz |t1 ∗ t). It says
∀x, ∀x0 , (f (g(x)))′ ∗ x0 = f ′ (g(x)) ∗ g ′ (x) ∗ x0 , and can be used for incremental compu-
tation and automatic differentiation. (Section 4)

1
A full version of this paper is available at [Link]
H. Xu and Z. Hu 143:3

Terms t ::= c constants of interpretable type

| x variable
| λx : T. t lambda abstraction
| tt function application
| (t1 , t2 , . . . , tn ) | πj t n-tuple and projection
| t⊕t addition
| t⊖t subtraction
| t∗t multiplication
∂t
| ∂x |t derivative
Rt
| t
t dx integration
| inl t | inr t left/right injection
| case t of inl x1 ⇒ t | inr x2 ⇒ t case analysis
| f ix t fix point

Types T ::= B base type

| (T1 , T2 , . . . , Tn ) product type
| T →T function type
| T +T sum type

Contexts Γ ::= ∅ empty context

| Γ, x : T variable binding

Figure 1 Calculus Syntax.

∞
1 (k)
t0 ) ∗ (t ⊖ t0 )k . Different from
P
We prove the Taylor’s Theorem: f t = k! (f
k=0
that one of the differential lambda-calculus [9], this Taylor’s theorem manifests res-
ults of computation instead of analysis on occurrence of terms. It can be used for
approximation of a function computation. (Section 5)

2 Calculus

In this section, we shall give a clear definition of our calculus with both derivatives and
integration. We explain important insights in our design, and prove some useful properties
and theorems that will be used later.

2.1 Syntax
Our calculus, as defined in Figure 1, is an extension of the simply-typed lambda calculus [20].
Besides the usual constant, variable, lambda abstraction, function application, and tuple, it
∂t
introduces five new operations: addition ⊕, subtraction ⊖, multiplication ∗, derivative ∂x |t
Rt
and integration t t dx. The three binary operations, namely ⊕, ⊖, and ∗, are generalizations
of those from our mathematics. Intuitively, x ⊕ ∆ is for updating x with change ∆, ⊖ for
canceling updates, and * for distributing updates. We build up terms from terms of base
types (such as R, C), and on each base type we require these operations satisfy the following
properties:

ICALP 2021
143:4 Analytical Differential Calculus with Integration

c:T ∈Γ x:T ∈Γ
(TCon) (TVar)
Γ ⊢ c: T Γ ⊢ x: T
Γ ⊢ t : T1 Γ ⊢ t : T2
(TInl) (TInr)
Γ ⊢ inl t : T1 + T2 Γ ⊢ inr t : T1 + T2
Γ ⊢ t1 : T ∗ Γ ⊢ t2 : T ∗ Γ ⊢ t1 : T ∗ Γ ⊢ t2 : T ∗
(TAdd) (TSub)
Γ ⊢ t1 ⊕ t2 : T ∗ Γ ⊢ t1 ⊖ t2 : T ∗
Γ, x : T1 ⊢ t : T2 Γ ⊢ t1 : T1 → T2 Γ ⊢ t2 : T1
(TAbs) (TApp)
Γ ⊢ λx : T1 . t : T1 → T2 Γ ⊢ t1 t2 : T2
Γ ⊢ t: T →T Γ ⊢ t1 : T1 Γ, x : T1 ⊢ t2 : T2
(TFix) ∂t2 ∂T2
(TDer)
Γ ⊢ f ix t : T Γ ⊢ ∂x |t1 : ∂T1
∀j ∈ [1, n], Γ ⊢ tj : Tj ∀j ∈ [1, n], Γ ⊢ t : (T1 , T2 , ..., Tn )
Γ ⊢ (t1 , t2 , ..., tn ) : (T1 , T2 , ..., Tn ) Γ ⊢ πj t : Tj
(TPair) (TProj)
∗
∂T
Γ ⊢ t1 : ∂T Γ ⊢ t2 : T
(TMul)
Γ ⊢ t1 ∗ t2 : T ∗
∗
Γ ⊢ t1 : T Γ ⊢ t2 : T Γ, x : T ⊢ t : ∂T
∂T
Rt (TInt)
Γ ⊢ t12 t dx : T ∗
Γ, x1 : T1 ⊢ t1 : T Γ, x2 : T2 ⊢ t2 : T Γ ⊢ t : T1 + T2
(TCase)
Γ ⊢ case t of inl x1 ⇒ t1 | inr x2 ⇒ t2 : T

Figure 2 Typing Rules.

The addition and multiplication are associative and commutative, i.e., (a ⊕ b) ⊕ c =

a ⊕ (b ⊕ c), a ⊕ b = b ⊕ a, (a ∗ b) ∗ c = a ∗ (b ∗ c), a ∗ b = b ∗ a.
The addition and the subtraction are cancellable, i.e., (a ⊕ b) ⊖ b = a and (a ⊖ b) ⊕ b = a.
The multiplication is distributive over addition, i.e., a ∗ (b ⊕ c) = a ∗ b ⊕ a ∗ c.

▶ Example 1 (Basic Operations on Real Numbers). For real numbers r1 , r2 ∈ R, we have the
following definitions.

r1 ⊕ r2 = r1 + r2
r1 ⊖ r2 = r1 − r2
r1 ∗ r2 = r1 r2
R t2
We use ∂t∂x |t2 to denote derivative of t1 over x at point t2 , and
1
t1
t dx to denote
integration of t over x from t1 to t2 .

2.2 Typing
As defined in Figure 1, we have base types (denoted by B), tuple types, function types, and
sum type. To make our later typing rules easy to understand, we introduce the following
type notations.

Type T ∗ ::= B base type

∗ ∗ ∗
| (T , T , ..., T ) product type
| T → T∗ arrow type
H. Xu and Z. Hu 143:5

T ∗ means the types that are addable (i.e., updatable through ⊕). We view the addition
between functions, tuples and base type terms as valid, which will be showed by our reduction
rules later. But here, we forbid the addition and subtraction between sum types because we
view updates such as inl 0⊕inr 1 as invalid. If we want to update the change to a term of sum
types anyway, we may do case analysis such as case t of inl x1 ⇒ inl (x1 ⊕ ...) | inr x2 ⇒
(x2 ⊕ ...).
Next, we introduce two notations for derivatives on types:
∂T
= T,
∂B
∂T ∂T ∂T ∂T
=( , , ..., ).
∂(T1 , T2 , ..., Tn ) ∂T1 ∂T2 ∂Tn
The first notation says that with the assumption that differences (subtraction) of values
of base types are of base types, the derivative over base types has no effect on the result
type. And, the second notation resembles partial differentiation. Note that we do not
consider derivatives on functions because even for functions on real numbers, there is no
good mathematical definition for them yet. Therefore, we do not have a type notation for
∂T
∂(T1 →T2 ) . Besides, because we forbid the addition and subtraction between the sum types,
we will iew the differentiation of the sum types as invalid, so we do not have notations for
∂T
∂(T1 +T2 ) either.
Figure 2 shows the typing rules for the calculus. The typing rules for constant, variable,
lambda abstraction, function application, tuple, and projection are nothing special. The
typing rules for addition and subtraction are natural, but the rest three kinds of rules are
more interesting. Rule TMul the typing rule for t1 ∗ t2 . If t1 is a derivative of T1 over T2 , and
t2 is of type T2 , then multiplication will produce a term of type T1 . This may be informally
△Y
understood from our familiar equation △X ∗ △X = △Y . Rule TDer shows introduction
of the derivative type through a derivative operation, while Rule TInt cancellation of the
derivative type through an integration operation.

2.3 Semantics
We will give a two-stage semantics for the calculus. At the first stage, we assume that all
the constants (values and functions) over the base types are interpretable in the sense there
is a default well-defined interpreter to evaluate them. At the second stage, the important
part of this paper, we define a set of reduction rules and use the full reduction strategy
to compute their normal form, which enjoys good properties of soundness, confluence, and
strong normalization.
More specifically, after the full reduction of a term in our calculus, every subterm (now in
a normal form of interpretable types) outside the lambda function body will be interpretable
on base types, which will be proved in the full version. In other words, our calculus helps to
reduce a term to a normal form which is interpretable on base types, and leave the remaining
evaluations to interpretation on base types. We will not give reduction rules to the operations
on base types because we do not want to touch on implementations of primitive functions on
base types.
For simplicity, in this paper we will assume that the important properties such as the
Newton-Leibniz formula, the Chain Rule, and the Taylor’s theorem, are satisfied by all the
primitive functions and their closures through addition, subtraction, multiplication, derivative
and integration. This assumption may seem too strong, since not all primitive functions on
base types meet this assumption. However, it would make sense to start with the primitive
functions meeting these requirements to build our system, and extend it later with other
primitive functions.

ICALP 2021
143:6 Analytical Differential Calculus with Integration

t0 : B
∂(t1 ,t2 ,...,tn )
(EAppDer1)
∂x |t0 → ( ∂t ∂t2 ∂tn
∂x |t0 , ∂x |t0 , ..., ∂x |t0 )
1

t0 : B
∂inl/inr t
(EAppDer2)
∂t
∂x |t0 → inl/inr ∂x |t0
t0 : B
∂(λy:T.t)
(EAppDer3)
∂t
∂x |t0 → λy : T. ∂x |t0
∀i ∈ [1, n], ti∗ = (t1 , t2 ..., ti−1 , xi , ti+1 ..., tn )
(EAppDer4)
∂t
→ ( ∂t[t∂x
∂x |(t1 ,t2 ,...,tn )
1∗ /x]
1
|t1 , ∂t[t∂x
2∗ /x]
2
|t2 , ..., ∂t[t∂x
n∗ /x]
n
|tn )
t1 , t2 : B
R t2 Rt Rt Rt (EAppInt1)
(t , t , ...t1n )dx → ( t12 t11 dx, t12 t12 dx, ..., t12 t1n dx)
t1 11 12
t1 , t2 : B
R t2 R t2 (EAppInt2)
t1
inl/inr t dx → inl/inr t1
t dx
t1 , t2 : B
R t2 R t2 (EAppInt3)
t1
λy : T2 .tdx → λy : T2 . t1
tdx
∀i ∈ [1, n], ti∗ = (t21 ..., t2i−1 , xi , t1i+1 ..., t1n )
R (t21 ,t22 ,...,t2n ) Rt R t2n
(t11 ,t12 ,...t1n )
tdx → t1121 π1 (t[t1∗ /x])dx1 ⊕ ... ⊕ t1n πn (t[tn∗ /x])dxn
(EAppInt4)

Figure 3 Reduction Rules for Derivative and Integration.

2.4 Reduction Rules

Our calculus is an extension of simply-typed lambda-calculus. Our lambda abstraction and
application are nothing different from the simply-typed lambda calculus, and we have the
reduction rule:

(λx : T. t)t1 → t[t1 /x].

We use an n-tuple to model structured data and projection πj to extract j-th component
from a tuple, and we have the following reduction rule:

πj (t1 , t2 , ...tn ) → tj .

Similarly, we have reduction rules for the case analysis:

case (inl t) of inl x1 ⇒ t1 | inr x2 ⇒ t2 → t1 [t/x1 ]

case (inr t) of inl x1 ⇒ t1 | inr x2 ⇒ t2 → t2 [t/x2 ]

Besides, we introduce fix-point operator to deal with recursion:

fix f → f (fix f )

It is worth noting that tuples, having a good correspondence in mathematics, should be

understood as structured data instead of high-dimensional vectors because there are some
operations that are different from those in mathematics. As will be seen later, there is
difference between our multiplication and matrix multiplication, and derivative and integration
on tuples of tuples has no correspondence to mathematical objects.
H. Xu and Z. Hu 143:7

The core reduction rules in our calculus are summarized in Figure 3, which define three
basic cases for both reducing derivative terms and integration terms. For derivative, we use
∂t
∂x |t0 to denote the derivative of t over x at point t0 , and we have four reduction rules:

Rule EAppDer1 is to distribute point t0 : B into a tuple. This resembles the case in
mathematics; if we have a function f defined by f (x) = (f1 (x), f2 (x), . . . , fm (x))T , its
derivative will be ( ∂f1 ∂f2 ∂fm T
∂x , ∂x , . . . , ∂x ) . For example, if we have a function f : R → (R, R)
defined by f (x) = (x, x ∗ x), then its derivative will be (1, 2 ∗ x).
Rule EAppDer2 is similar to Rule EAppDer1.
Rule EAppDer3 is to distribute point t0 : B into a lambda abstraction. Again this is
very natural in mathematics. For example, for function f (x) = λy : B. x ∗ y, then we
would have its derivative on x as λy : B.y.
Rule EAppDer4 is to deal with partial differentiation, similar to the Jacobian matrix in
mathematics (as shown in the introduction). For example, if we have a function that maps
a pair (x, y) to (x ∗ x, x ∗ y ⊕ y), which may be written as λz : (B, B). (π1 z ∗ π1 z, (π1 z ∗
π2 z ⊕ π2 z)) then we would have its derivative ∂(f∂zz) |(x,y) as ((2 ∗ x, y), (0, x ⊕ 1)).
Similarly, we can define four reduction rules for integration. Rules EAppInt1,EAppInt2
and EAppInt3 are simple. Rule EAppInt4 is worth more explanation. It is designed to
establish the Newton-Leibniz formula
Z t2
∂t
|x dx = t[t2 /y] ⊖ t[t1 /y]
t1 ∂y

when t1 and t2 are tuples:

Z (t21 ,t22 ,...,t2n )
∂t
|x dx = t[(t21 , t22 , ..., t2n )/y] ⊖ t[(t11 , t12 , ..., t1n )/y].
(t11 ,t12 ,...,t1n ) ∂y

So we design the rule to have

∂t[(t21 , ..., t2(j−1) , x′j , t1(j+1) , ..., t1n )/y]

Z t2j Z (t21 ,...,t2(j−1) ,t2j ,t1(j+1) ,...,t1n )
∂t
′ | xj dxj = |x dx.
t1j ∂x j (t21 ,...,t2(j−1) ,t1j ,t1(j+1) ,...,t1n ) ∂y
∂t
Notice that under our evaluation rules on derivative, πj ( ∂x |x=(x1 ,x2 ,...,xn ) ) will be equal to
the derivative of t to its j-th parameter xj , so the integration will lead us to the original t.
Finally, we discuss the reduction rules for the three new binary operations, as summarized
in Figure 4. The addition ⊕ is introduced to support the reduction rule of integration. It is
also useful in proving the theorem and constructing the formula. We can understand the
two reduction rules for addition as the addition of high-dimension vectors and functions
respectively. Similarly, we can have two reduction rules for subtraction ⊖. The operator ∗ was
introduced as a powerful tool for constructing the Chain Rule and the Taylor’s theorem. The
first two reduction rules can be understood as multiplications of a scalar with a function and a
high-dimension vector respectively, while the last one can be understood as the multiplication
on matrix. For example, we have

((1, 4), (2, 5), (3, 6)) ∗ (7, 8, 9) = (50, 122)

which corresponds to the following matrix multiplication.

 
  7  
1 2 3   50
8 =
4 5 6 122
9

ICALP 2021
143:8 Analytical Differential Calculus with Integration

(t11 , ..., t1n ) ⊕ (t21 , ..., t2n ) → (t11 ⊕ t21 , ..., t1n ⊕ t2n ) (EAppAdd1)

(λx : T. t1 ) ⊕ (λy : T. t2 ) → λx : T. (t1 ⊕ t2 [y/x]) (EAppAdd2)

(t11 , ..., t1n ) ⊖ (t21 , ..., t2n ) → (t11 ⊖ t21 , ..., t1n ⊖ t2n ) (EAppSub1)

(λx : T. t1 ) ⊖ (λy : T. t2 ) → λx : T. (t1 ⊖ t2 [y/x]) (EAppSub2)

t0 : B
(EAppMul1)
(t1 , t2 , ..., tn ) ∗ t0 → (t1 ∗ t0 , t2 ∗ t0 , ..., tn ∗ t0 )
t0 : B
(EAppMul2)
(λx : T.t) ∗ t0 → λx : T.(t ∗ t0 )
t0 : B
(EAppMul3)
(inl/inr t) ∗ t0 → inl/inr (t ∗ t0 )
t1 : (t11 , t12 , ...t1n ), t2 : (t21 , t22 , ...t2n )
(EAppMul4)
t1 ∗ t2 → (t11 ∗ t21 ) ⊕ (t12 ∗ t22 ) ⊕ ... ⊕ (t1n ∗ t2n )

Figure 4 Reduction Rules for Addition, Subtraction and Multiplication.

It is worth noting that while they are similar, ∗ is different from the matrix multiplication
operation. For example, we cannot write x as an m-dimensional vector (or m ∗ 1 matrix) in
Taylor’s theorem because no matrix A is well-performed under A ∗ x ∗ x, but we can write
Taylor’s Theorem easily under our framework. In the matrix representation, the number of
rows of the first matrix and the number of columns of the second matrix must be equal so
that we can perform multiplication on them. This means, we can only write case m = 1’s
Taylor’s theorem in matrices, while our version can perform for any tuples.

2.5 Properties
Next, we prove some properties of our calculus. The proof is rather routine with some small
variations.

▶ Lemma 2 (Properties). This calculus has the properties of progress, preservation and
confluence. Moreover, if a term t does not contain subterms f ix t′ , then t is strong
normalizable.

Proof. Full proof is in the full version, which is adapted from the standard proof. ◀

2.6 Term Equality

We need to talk a bit more on equality because we do not consider reduction or calculation
on primitive functions. This notion of equality has little to do with our evaluation but has
a lot to do with the equality of primitive functions. Using this notion of equality, we can
compute the result from completely different calculations. This will be used in our later
proof of the three theorems.
Since we have proved the confluence property, we know that every term has at most one
normal form after reduction. Thus, we can define our equality based on their normal forms;
the equality between unnormalizable terms is undefined.
H. Xu and Z. Hu 143:9

▶ Definition 3 (Term Equality). An open term t1 is said to be equal to a term t2 , if and only
if for all free variables x1 , x2 , ..., xn in t1 and t2 , for all closed and weak-normalizable term
ui whose type is the same as that of xi , we have t1 [u1 /x1 , ..., un /xn ] = t2 [u1 /x1 , ..., un /xn ].
A closed-term t1 = t2 , if their normal forms n1 and n2 have the relation that n1 = n2 ,
where a normal form n1 is said to be equal to another normal form n2 , if they satisfy one of
the following rules:
(1) n1 is a of type iB (Type iB is used to capture terms with base type constants and
functions, being defined by iB = iB → iB | B). A normal form of type iB is interpretable
by the base type interpreter. Detailed proof is in the full version), then n2 has to be of
the same type, and under the base type interpretation, n1 is equal to n2 ;
(2) n1 is (t1 , t2 , ..., tn ), then n2 has to be (t′1 , t′2 , ..., t′n ), and ∀j ∈ [1, n], tj is equal to t′j ;
(3) n1 is λx : T.t, then n2 has to be λy : T.t′ (y can be x), and n1 x is equal to n2 x.
(4) n1 is inl t′1 , then n2 has to be inl t′2 , and t′1 is equal to t′2 .
(5) n1 is inr t′1 , then n2 has to be inr t′2 , and t′1 is equal to t′2 .

▶ Lemma 4. The equality is reflexive, transitive and symmetric for weak-normalizable terms.

Proof. Based on the equality of terms of base types, we can prove it by induction. ◀

▶ Lemma 5. The equality is consistent, e.g., we can not prove equality between arbitrary
two terms.

Proof. Notice that except for the equality introduced by the base type interpreter, other
equality inferences all preserve the type. So for arbitrary t1 of type (B, B) and t2 of type B,
we can not prove equality between them. ◀

Next we give some lemmas that will be used later in our proof. It is relatively unimportant
to the mainline of our calculus, so we put their proofs in the full version.

▶ Lemma 6. If t1 ρ∗ t′1 , t2 ρ∗ t′2 , then t1 [t2 /x]ρ∗ t′1 [t′2 /x].

▶ Lemma 7. If t1 = t′1 , t2 = t′2 , then t1 ⊕ t2 = t′1 ⊕ t′2 .

▶ Lemma 8. For a term t, for any subterm s, if the term s’=s, then t[s’/s]=t. (We only
substitute the subterm s, but not other subterms same as s)

▶ Lemma 9. If t1 ∗ (t2 ⊕ t3 ) and (t1 ∗ t2 ) ⊕ (t1 ∗ t3 ) are weak-normalizable, then t1 ∗ (t2 ⊕ t3 ) =

(t1 ∗ t2 ) ⊕ (t1 ∗ t3 ).

▶ Lemma 10. If (t1 ⊖t2 )⊕(t2 ⊖t3 ) and t1 ⊖t3 are weak-normalizable, then (t1 ⊖t2 )⊕(t2 ⊖t3 ) =
t1 ⊖ t3 .

3 Newton-Leibniz’s Formula
The first important theorem we will give is the Newton-Leibniz’s formula, which ensures the
duality between derivatives and integration. This theorem lays a solid basis for our calculus.
R t ∂t
▶ Theorem 11 (Newton-Leibniz). Let t contain no free occurrence of x, and both t12 ∂y |x dx
and t[t2 /y] ⊖ t[t1 /y] are well-typed and weak-normalizable. Then we have
Z t2
∂t
|x dx = t[t2 /y] ⊖ t[t1 /y].
t1 ∂y

ICALP 2021
143:10 Analytical Differential Calculus with Integration

Proof. If t1 , t2 or t is not closed, then we need to prove ∀u1 , ..., un , we have

Z t2
∂t
( |x dx)[u1 /x1 , ..., un /xn ] = (t[t2 /y] ⊖ t[t1 /y])[u1 /x1 , ..., un /xn ].
t1 ∂y

By freezing u1 , ..., un , we can apply the substitution [u1 /x1 , ..., un /xn ] to make every term
closed. So, for simplicity, we will assume t, t1 and t2 to be closed.
We prove this by induction on types.

Case: t1 ,t2 and t are of base types. By the confluence lemma, we know there exists the
R t ∂t R t′ ′
normal form t′ , t′1 and t′2 of the term t, t1 and t2 . Also, we know t12 ∂y |x dx = t′2 ∂t ∂y |x dx
′ ′ ′ ′
R t′2 ∂t1 ′
and t[t2 /y] ⊖ t[t1 /y] = t [t2 /y] ⊖ t [t1 /y]. Since on base types we have t′ ∂y |x dx =
1
R t ∂t
t′ [t′2 /y] ⊖ t′ [t′1 /y], we have t12 ∂y |x dx = t[t2 /y] ⊖ t[t1 /y].
Case: t1 ,t2 are of base types, t is of type (T1 , T2 , ..., Tn ). By the confluence lemmas, there
exist a normal form (t′11 , t′12 , ..., t′1n ) for t. Using Rules (EAppInt1) and (EAppDer1),
we know
R t2 ∂t R t ∂(t′ ,t′ ,...,t′1n )
t1 ∂y x
| dx = t12 11 12 |x dx
R t2 ∂t′11 ∂y∂t′12 ∂t′
= t1 ( ∂y |x , ∂y |x , ..., ∂y1n |x )dx
R t ∂t′ R t ∂t′ R t ∂t′
= ( t12 ∂y11 |x dx, t12 ∂y12 |x dx, ..., t12 ∂y1n |x dx)

On the other hand, we have

t[t2 /y] ⊖ t[t1 /y]

= (t′11 [t2 /y], t′12 [t2 /y], ..., t′1n [t2 /y]) ⊖ (t′11 [t1 /y], t′12 [t1 /y], ..., t′1n [t1 /y])
= (t′11 [t2 /y] ⊖ t′11 [t1 /y], t′12 [t2 /y] ⊖ t′12 [t1 /y], ..., t′1n [t2 /y] ⊖ t′1n [t1 /y])
R t2 ∂t′1j
By induction, we have ∀j ∈ [1, n], t1 ∂y |x dx = t′1j [t2 /y] ⊖ t′1j [t1 /y] , so we have proven
the case.
Case: t1 ,t2 are of base types, t is of type A → B. By Lemma 8, we can use λz : A.t z (for
simiplicity, we use λz : A.t′ where t′ = t z) to substitute for t, where z is a fresh variable.
Now, we have for any u,
Rt Rt ′
∂t
( t12 ∂y |x dx) u = ( t12 ∂λz:A.t
∂y |x dx) u
R t2 ∂t′
= λz : A.( t1 ∂y |x dx) u
R t ′ [u/z]
= t12 ∂t ∂y |x dx

and on the other hand, since z is free in t1 and t2 , we have

(t[t2 /y] ⊖ t[t1 /y]) u = ((λz : A.t′ )[t1 /y] ⊖ (λz : A.t′ )[t2 /y]) u
= λz : A.(t′ [t2 /y] ⊖ t′ [t1 /y]) u
= (t′ [t2 /y] ⊖ t′ [t1 /y])[u/z]
= (t′ [u/z])[t2 /y] ⊖ (t′ [u/z])[t1 /y]
R t2 ∂t′ [u/z]
By induction (on B), we know t1 ∂y |x dx = (t′ [u/z])[t2 /y] ⊖ (t′ [u/z])[t1 /y], thus we
have proven the case.
Case: t1 ,t2 are of base types, t is of type T1 + T2 . This case is impossible because the
righthand term is not well-typed.
H. Xu and Z. Hu 143:11

Case: t1 ,t2 are of type (T1 , T2 , ..., Tn ), t is of any type T . By using the confluence lemma,
we know there exist the normal forms (t′11 , t′12 , ..., t′1n ) and (t′21 , t′22 , ..., t′2n ) for t1 and t2
respectively.
Applying Rules (EAppDer3) and (EAppInt3), we have
R t2 ∂t
R (t′21 ,t′22 ,...,t′2n )
∂t
| dx
t1 ∂y x
= | dx
(t′ ,t′12 ,...,t′1n ) ∂y x
11
R t′21
= π ( | [(x1 , t′12 , ...t′1n )/x])dx1 ⊕ · · · ⊕
t′11 1 ∂y x
∂t
R t′2n
π ( ∂t | [(t′21 , t′22 , ..., xn )/x])dxn
t′1n n ∂y x

Notice that there is no occurrence of x in t, so we have

R t′2j
t′1j
∂t
πj ( ∂y |x [(t′21 , t′22 , ..., t′2(j−1) , xj , t′1(j+1) , ..., t′1n )/x])dxj
R t′2j ∂t
= t′ πj ( ∂y |(t′21 ,t′22 ,...,t′2(j−1) ,xj ,t′1(j+1) ,...,t′1n ) )dxj
1j
R t′2j ∂t[t(j−1)∗ /y]
= t′ πj ( ∂t[t∂x 1∗ /y]
1
|t′21 , ∂t[t∂x
2∗ /y]
2
|t′22 , ..., ∂x j−1
|t′2(j−1) ,
1j
∂t[tj∗ /y] ∂t[t(j+1)∗ /y]
∂x′j |xj , ∂x j+1
|t′1(j+1) , ..., ∂t[t∂x
n∗ /y]
n
|t′1n )dxj
R t′2j ∂t[(t′21 ,t′22 ,...,t′2(j−1) ,x′j ,t′1(j+1) ,...,t′1n )/y]
= t′1j ∂x′j |xj dxj

By induction (on the case where t1 , t2 are of type Tj , t is of type T ), we have

R t′2j ∂t[(t′21 ,t′22 ,...,t′2(j−1) ,x′j ,t′1(j+1) ,...,t′1n )/y]
t′1j ∂x′j |xj dxj
= (t[(t21 , t22 , ..., t2(j−1) , xj , t1(j+1) , ..., t′1n )/y])[t′2j /x′j ] ⊖
′ ′ ′ ′ ′

(t[(t′21 , t′22 , ..., t′2(j−1) , x′j , t′1(j+1) , ..., t′1n )/y])[t′1j /x′j ]
= (t[(t′21 , t′22 , ..., t′2(j−1) , t′2j , t′1(j+1) , ..., t′1n )/y]) ⊖
(t[(t′21 , t′22 , ..., t′2(j−1) , t′1j , t′1(j+1) , ..., t′1n )/y])

Note that the last equation holds because x′j is a fresh variable and t has no occurrence
of x′j .
Now we have the following calculation.
R t2∂t
| dx
t1 ∂y x
= { all the above }
((t[(t′21 , t′12 , ..., t′1n )/y]) ⊖ (t[(t′11 , t′12 , ..., t′1n )/y])) ⊕
((t[(t′21 , t′22 , ..., t′1n )/y]) ⊖ (t[(t′21 , t′12 , ..., t′1n )/y])) ⊕ · · · ⊕
((t[(t′21 , t′22 , ..., t′2n )/y]) ⊖ (t[(t′21 , t′22 , ..., t′1n )/y]))
= { Lemma 10 }
(t[(t′21 , t′22 , ..., t′2n )/y]) ⊖ (t[(t′11 , t′12 , ..., t′1n )/y])
= { Lemma 6 }
t[t2 /y] ⊖ t[t1 /y]

Thus we have proven the theorem. ◀

Application: Incremental Computation

A direct application is incrementalization [17, 7, 11]. Given a function f (x), if the input x is
changed by ∆, then we can obtain its incremental version of f (x) by f ′ (x, ∆).

f (x ⊕ ∆) = f (x) ⊕ f ′ (x, ∆)

ICALP 2021
143:12 Analytical Differential Calculus with Integration

where f ′ satisfies that

Z x⊕∆
∂f (x)
f ′ (x, ∆) = |x dx.
x ∂x

▶ Example 12 (Averaging a Pair of Real numbers). As a simple example, consider the average
of a pair of real numbers

average :: (R, R) → R
average = λx.(π1 (x) + π2 (x))/2

Suppose that we want to get an incremental computation of average at x = (x1 , x2 ) when

the first element x1 is changed to x1 + d while the second component x2 is kept the same.
The incremental computation is defined by
Z x⊕(d,0)
∂average(x) d
inc(x, d) = average(x, (d, 0)) = |x dx =
x ∂x 2

which is efficient.

4 Chain Rule
The Chain Rule is another important theorem of the relation between function composition
and derivatives. This Chain Rule in our calculus has many important applications in
automatic differentiation and incremental computation.

▶ Theorem 13 (Chain Rule). Let f : T1 → T , g : T2 → T1 . If both ∂f ∂x (g x)

|t1 ∗ t and
∂f y ∂g z
∂y |(g t1 ) ∗ ( ∂z |t1 ∗ t) are well-typed and weak-normalizable. Then for any t, t1 : T2 , we have

∂f (g x) ∂f y ∂g z
|t1 ∗ t = |(g t1 ) ∗( |t ∗ t).
∂x ∂y ∂z 1

Proof. Like in the proof of Theorem 11, for simplicity, we assume that f , g, t and t1 are
closed. Furthermore, we assume that t and t1 are in normal form. We prove this by induction
on types.

Case T, T2 are base types, and T1 is any type. To be well-typed, T1 must contain no →
or + type. So for simplicity, we suppose T1 to be (B, B, B, ..., B) of n-tuples, but the
technique below can be applied to any T1 type (such as tuples of tuples) that makes the
term well-typed.
First we notice that

gz = (π1 (g z), π2 (g z), ..., πn (g z))

= ((λb′ : B.π1 (g b′ )) z, (λb′ : B.π2 (g b′ )) z, ..., (λb′ : B.πn (g b′ )) z)

and for any j, we notice that πj (g b′ ) has only one free variable of base type, so it can
be reduced to a normal form, say Ej , of base type. Let gj be λb′ : [Link] , then we have
g z = (g1 z, g2 z, ..., gn z).
Next, we deal with the term f :

f = λa : T1 . (f a)
= λa : T1 . ((λy1 : B. λy2 : B., ...λyn : B. (f (y1 , y2 , ..., yn ))) π1 (a) π2 (a)... πn (a))
H. Xu and Z. Hu 143:13

and we know that (f (y1 , y2 , ..., yn )) only contains base type free variables, so it can be
reduced to a base type normal form, say N , so we have

f = λa : T. ((λy1 : B.λy2 : B., ...λyn : B. N ) π1 (a) π2 (a)... πn (a)).

Now, we can calculate as follows:

∂f (g x)
∂x |t1 ∗ t
= ∂(λa:T.(λy1 :B.λy2 :B.,...λyn :B.N ) π1∂x (a) π2 (a)... πn (a)) (g1 x,g2 x,...,gn x)
|t1 ∗t
∂(λy1 :B.λy2 :B.,...λyn :B.N ) (g1 x) (g2 x)... (gn x)
= ∂x |t1 ∗ t
= ∂N [(g1 x)/y1 ,(g2 ∂xx)/y2 ,...(gn x)/yn ]
|t1 ∗ t

∂f y ∂g z
∂y |(g t1 ) ∗ ( ∂z |t1 ∗ t)
= ∂f∂yy |(g1 t1 ,g2 t1 ,...,gn t1 ) ∗ ( ∂(g1 z,g2 z,...,gn z)
∂z |t1 ∗ t)
∂f y
= ∂y |(g1 t1 ,g2 t1 ,...,gn t1 ) ∗ ( ∂g∂z
1 z
|t1 ∗ t, ∂g∂z
2 z
|t1 ∗ t, ..., ∂g∂z
n z
|t1 ∗ t)
∂(λy1 :B.λy2 :B.,...λyn :B.N ) π1 (y) π2 (y)... πn (y)
= ∂y |(g1 t1 ,g2 t1 ,...,gn t1 ) ∗

( ∂g∂z
1 z
|t1 ∗ t, ∂g∂z
2 z
|t1 ∗ t, ..., ∂g∂z
n z
|t1 ∗ t)
∂N [y1′ /y1 ,g2 t1 /y2 ,...,gn t1 /yn ] ′
∂N [g1 t1 /y1 ,g2 t1 /y2 ,...,yn /yn ]
=( ∂y1′ |g1 t1 , ..., ′
∂yn |gn t1 )∗

( ∂g∂z
1 z
|t1 ∗ t, ∂g∂z
2 z
|t1 ∗ t, ..., ∂g∂z
n z
|t1 ∗ t)
∂N [y1′ /y1 ,g2 t1 /y2 ,...,gn t1 /yn ]
=( ∂y1′ |g1 t1 ∗ ( ∂g∂z
1 z
|t1 ∗ t)) ⊕ ...⊕
′
∂N [g1 t1 /y1 ,g2 t1 /y2 ,...,yn /yn ]
( ′
∂yn |gn t1 ∗ ( ∂g∂z
n z
|t1 ∗ t))

Notice that by the base type interpretation, f (g1 (x), g2 (x), ..., gn (x)) = f1′ (g1 (x), g2 (x), ...,
gn (x)) ∗ g1′ (x) + f2′ (g1 (x), g2 (x), ..., gn (x)) ∗ g2′ (x) + ... + fn′ (g1 (x), g2 (x), ..., gn (x)) ∗ gn′ (x)
where fj′ means the derivative of f to its j-th parameter, so we get the following and
prove the case.
∂N [(g1 x)/y1 ,(g2 x)/y2 ,...(gn x)/yn ]
∂x |t1 ∗ t
∂N [y1′ /y1 ,g2 t1 /y2 ,...,gn t1 /yn ]
=( ∂y1′ |g1 t1 ∗ ( ∂g∂z
1 z
|t1 ∗ t)) ⊕ ...⊕
′
∂N [g1 t1 /y1 ,g2 t1 /y2 ,...,yn /yn ]
( ′
∂yn |gn t1 ∗ ( ∂g∂z
n z
|t1 ∗ t))

Case T2 is base type, T1 is any type, T is A → B. We prove that for any u of type A, we
have ( ∂f ∂x
(g x)
|t1 ∗ t) u = ( ∂f∂yy |(g t1 ) ∗ ( ∂g∂zz |t1 ∗ t)) u.
First, let f = λx : T1 .(f x) u, g ′ = g, then by induction we have
′

∂f ′ (g ′ x) ∂f ′ y ′

∂x |t1 ∗t= ∂y |(g t1 )

′ ∗ ( ∂g∂z z |t1 ∗ t)

that is, we have

( ∂f (g x) u
∂x |t1 ∗ t) = ( ∂f∂yy u |(g t1 ) ∗ ( ∂g∂zz |t1 ∗ t))

Then, we prove ( ∂f (g x) u
∂x |t1 ∗ t) = ( ∂f ∂x
(g x)
|t1 ∗ t) u by the following calculation.

( ∂f ∂x
(g x)
|t1 ∗ t) u = ( ∂λa:A.(f∂x(g x)) a |t1 ∗ t) u
= (λa : A.( ∂(f (g ∂x
x)) a
|t1 ∗ t)) u
∂f (g x) u
= ( ∂x |t1 ∗ t)

ICALP 2021
143:14 Analytical Differential Calculus with Integration

Next, we prove ( ∂f∂yy |(g t1 ) ∗ ( ∂g∂zz |t1 ∗ t)) u = ∂f∂yy u |(g t1 ) ∗ ( ∂g∂zz |t1 ∗ t). For simplicity,
we assume T1 to be (B, B, B, ..., B) of n-tuples (the technique below can be applied to
any T1 type which makes the term well-typed).
On one hand, by substituting (g1 z, g2 z, ..., gn z) for g z, we have

( ∂f∂yy |(g t1 ) ∗ ( ∂g∂zz |t1 ∗ t)) u

= ∂f∂yy |(g1 t1 ,g2 t1 ,...,gn t1 ) ∗ ( ∂(g1 z,g2∂zz,...,gn z) |t1 ∗ t) u
= ( ∂f (y1 ,g2 ∂yt1 ,...,gn t1 )
′ |g1 t1 ∗ ( ∂g∂z
1 z
|t1 ∗ t) ⊕ ...⊕
1
∂f (g1 t1 ,g2 t1 ,...,yn )
∂yn′ |gn t1 ∗ ( ∂g∂z
n z
|t1 ∗ t)) u

Since
f (g1 t1 , g2 t1 , ..., gj−1 t1 , yj , gj+1 t1 , ..., gn t1 )
= λa : A.f (g1 t1 , g2 t1 , ..., gj−1 t1 , yj , gj+1 t1 , ..., gn t1 ) a

which will be denoted as λa : A.t∗j , we continue the calculation as follows.

( ∂f∂yy |(g ∂g z
t1 ) ∗ ( ∂z |t1 ∗ t)) u
∂λa:A.t∗ ∂λa:A.t∗
= ( ∂y1 1 |g1 t1 ∗ ( ∂g∂z 1 z
|t1 ∗ t) ⊕ ... ⊕ ∂yn n |gn t1 ∗ ( ∂g∂z
n z
|t1 ∗ t)) u
∂t∗ ∂t∗
= λa : A.( ∂y11 |g1 t1 ∗ ( ∂g∂z
1 z
|t1 ∗ t)) ⊕ ... ⊕ ( ∂ynn |gn t1 ∗ ( ∂g∂z
n z
|t1 ∗ t)) u
∂t∗
1 [u/a] ∂g1 z ∂t∗
n [u/a]
= ∂y1 |g1 t1 ∗ ( ∂z |t1 ∗ t) ⊕ ... ⊕ ∂yn |gn t1 ∗ ( ∂g∂z
n z
|t1 ∗ t)

On the other hand, we have

( ∂f∂yy u |(g t1 ) ∗ ( ∂g∂zz |t1 ∗ t))

= ∂f∂yy u |(g1 t1 ,g2 t1 ,...,gn t1 ) ∗ ( ∂(g1 z,g2∂zz,...,gn z) |t1 ∗ t)
= ∂f (y1 ,g2 ∂yt1 ,...,gn t1 ) u
1
|g1 t1 ∗ ( ∂g∂z
1 z
|t1 ∗ t) ⊕ ...⊕
∂f (g1 t1 ,g2 t1 ,...,yn ) u
∂yn |gn t1 ∗ ( ∂g∂z
n z
|t1 ∗ t)
∂(λa:A.t∗1) u ∂(λa:A.t∗n) u
= ∂y1 |g1 t1 ∗ ( ∂g∂z
1 z
|t1 ∗ t) ⊕ ... ⊕ ∂yn |gn t1 ∗ ( ∂g∂z
n z
|t1 ∗ t)
∗ ∗
∂t1 [u/a] ∂g1 z ∂tn [u/a] ∂gn z
= ( ∂y1 |g1 t1 ∗ ( ∂z |t1 ∗ t)) ⊕ ... ⊕ ( ∂yn |gn t1 ∗ ( ∂z |t1 ∗ t))

Therefore, we have proven the case.

Case T2 is base type, T1 is any type, T is (T1 , T2 , ..., Tn ). We need to prove that for all j,
we have πj ( ∂f ∂x
(g x)
|t1 ∗ t) = πj ( ∂f∂yy |(g t1 ) ∗ ( ∂g∂zz |t1 ∗ t)). We may follow the proof for the
case when T has type A → B. Let f ′ = λx : T1 . πj (f x), g ′ = g, by induction, we have
∂πj (f (g x)) ∂πj (f y)
∂x |t1 ∗t= ∂y |(g t1 ) ∗ ( ∂g∂zz |t1 ∗ t)

The rest of the proof is similar to that for the case when T = A → B.
Case T2 is base type, T1 is any type, T is T1 + T2 . Notice that T1 has to be base type to
be well-typed. But either the case, the proof is similar to the case when T = A → B.
Case T2 , T1 and T are any type. Notice that T2 does not contain no → or + to be
well-typed (i.e., no derivative over function types). We have proved the case when T2 is
base type, and we assume that T2 has type (T1 , T2 , ..., Tn ). Suppose the normal form of
t1 is (t′11 , t′12 , ..., t′1n ) and the normal form of t is (t′21 , t′22 , ..., t′2n ), Then
∂f (g x)
∂x |t1 ∗ t
= ∂f ∂x
(g x)
|(t′11 ,t′12 ,...,t′1n ) ∗ (t′21 , t′22 , ..., t′2n )
∂f (g (x1 ,t′12 ,...,t′1n )) ∂f (g (t′11 ,t′12 ,...,xn ))
=( ∂x1 |t′11 , ..., ∂xn |t′1n ) ∗ (t′21 , ..., t′2n )
∂f (g (x1 ,t′12 ,...,t′1n )) ∂f (g (t′ ′
11 ,t12 ,...,xn )) ′
=( ∂x1 |t′11 ∗ t′21 ) ⊕ ... ⊕ ( ∂xn |t1n ∗ t′2n )
H. Xu and Z. Hu 143:15

On the other hand, we can use Lemma 9 (i.e., t1 ∗ (t2 ⊕ t3 ) = (t1 ∗ t2 ) ⊕ (t1 ∗ t3 )) to do
the following calculation.
∂f y ∂g z
∂y |(g t1 ) ∗ ( ∂z |t1 ∗ t)
∂g (x1 ,t′12 ,...,t′1n ) ∂g (t′11 ,t′12 ,...,xn )
= ∂f∂yy |(g t1 ) ∗ (( ∂x1 |t′11 ∗ t′21 ) ⊕ ... ⊕ ( ∂xn |t′1n ∗ t′2n ))
∂f y ∂g (x1 ,t′12 ,...,t′1n )
= ∂y |(g t1 ) ∗ ( ∂x1 |t′11 ∗ t′21 ) ⊕ ...⊕
′ ′
∂f y ∂g (t11 ,t12 ,...,xn )
∂y |(g t1 ) ∗ ( ∂xn |t′1n ∗ t′2n )

Now by induction using f ′ = f, g ′ = λx : Tj .g (t′11 , t′12 , ..., t′1(j−1) , x, t′1(j+1) , ..., t′1n ), we
have
∂f (g (t′11 ,t′12 ,...,t′1(j−1) ,xj ,t′1(j+1) ...,t′1n )
∂xj |t′1j ∗ t′2j
′ ′
∂g (t11 ,t12 ,...,t′1(j−1) ,xj ,t′1(j+1) ...,t′1n )
= ∂f∂yy |(g′ t′1j ) ∗ ( ∂xj |t′1j ∗ t′2j )
′ ′ ′ ′ ′
∂g (t11 ,t12 ,...,t1(j−1) ,xj ,t1(j+1) ...,t1n )
= ∂f∂yy |(g t1 ) ∗ ( ∂xj |t′1j ∗ t′2j )

Therefore by Lemma 7, we have proven the case.

Thus we have proven the theorem. ◀

Application: Automatic Differentiation

The Chain Rule provides another way to compute the derivatives. There are many applications
of the chain rule, and here we give an example of how to associate it with the automatic
differentiation [10].

▶ Example 14 (AD). This is an example from [10]. Let sqr and magSqr be defined as follows.

sqr :: R→R
sqr a = a∗a
magSqr :: (R, R) → R
magSqr (a, b) = sqr a ⊕ sqr b

⊕t2 )
First of all, let t1 and t2 two pairs, then it is easy to prove that ∂(t1∂x |t3 = ∂t ∂t2
∂x |t3 ⊕ ∂x |t3 .
1

Next, we can perform automatic differentiation on magSqr by the following calculation.

∂(magSqr x)
∂x |(a,b) ∗ t
∂(sqr(π1 x)⊕sqr(π2 x))
= ∂x |(a,b) ∗ t
∂(sqr y) ∂(π1 x) ∂(sqr y)
= ∂y |π1 (a,b) ∗ ( ∂x |(a,b) ∗ t) ⊕ ∂y |π2 (a,b) ∗ ( ∂(π 2 x)
∂x |(a,b) ∗ t)
= 2 ∗ a ∗ ((1, 0) ∗ t) ⊕ 2 ∗ b ∗ ((0, 1) ∗ t)

Now, because the theorem applies for any t of pair type, we use (1, 0) and (0, 1) to
∂(magSqr x)
substitute for t respectively, and we will get ∂x |(a,b) = (2 ∗ a, 2 ∗ b), which means
its derivative to a is 2 ∗ a and its derivative to b is 2 ∗ b.

5 Taylor’s Theorem
In this section, we discuss Taylor’s Theorem, which is useful to give an approximation of
a k-order differentiable function around a given point by a polynomial of degree k. In
programming, it is important and has many applications in approximation and incremental
computation.

ICALP 2021
143:16 Analytical Differential Calculus with Integration

First of all, we introduce some high-order notations.

∂ n−1 t1
∂ 0 t1 ∂ n t1 ∂ |x
∂xn−1
∂x0 |t2 = t1 ∂xn |t2 = ∂x |t2
t ∗ t01 = t t ∗ tn1 = (t ∗ t1 ) ∗ tn−1
1
f 0
= f f n
= (f ′ )n−1
(λx : T. t)′ ∂t
= λx : T. ∂x |x

Now our Taylor’s Theorem can be expressed as follows.

∞
1 (k)
t0 ) ∗ (t ⊖ t0 )k are weak-
P
▶ Theorem 15 (Taylor’s Theorem). If both f t and k! (f
k=0
normalizable, then

∞
X 1 (k)
f t= (f t0 ) ∗ (t ⊖ t0 )k .
k!
k=0

Proof. Like in the proof of Theorem 11, for simplicity, we assume that f , g, t and t1 are
closed. Furthermore, we assume that t and t1 are in normal form. We prove it by induction
on the type of f : T → T ′ .

Case T ′ is a base type. T must contain no → by our typing, so for simplicity, we suppose
T to be (B, B, ..., B). Using the same technique in Theorem 13, we assume f to be

f = λx : T. (λx1 : B. λx2 : B., ...λxn : B. N ) π1 (x) π2 (x)... πn (x)

(denoted by f = λx : T. t2 later), t to be (t11 , t12 , ..., t1n ), and t0 to be (t21 , t22 , ..., t2n ),
where each tij is a normal form of base type. Then we have

(f (n) t0 ) ∗ (t ⊖ t0 )n
n
= ∂∂xtn2 |t0 ∗ (t ⊖ t0 )n
∂ n−1 t2 ∂ n−1 t2
∂ | ∂ |
∂xn−1 (x1 ,t22 ,...,t2n ) ∂xn−1 (t21 ,t22 ,...,xn )
=( ∂x1 |t21 , ..., ∂xn |t2n ) ∗ (t ⊖ t0 )n
∂ n−1 t2 ∂ n−1 t2
∂ | ∂ |
∂xn−1 (x1 ,t22 ,...,t2n ) ∂xn−1 (t21 ,t22 ,...,xn )
=( ∂x1 |t21 ∗ (t11 ⊖ t21 ) ⊕ ... ⊕ ∂xn |t2n
∗(t1n ⊖ t2n )) ∗ (t ⊖ t0 )n−1
∂ n−2 t2 ∂ n−2 t2
∂ | ∂ |
n−2 (x1 ,t22 ,...,t2n ) n−2 (x1 ,t22 ,...,xn )
∂( ∂x ∂x1 |x1 ,..., ∂x ∂xn |t2n )
= (( ∂x1 |t21 ) ∗ (t11 ⊖ t21 ) ⊕ ...⊕
∂ n−2 t2 ∂ n−2 t2
∂ | ∂ |
n−2 (x1 ,t22 ,...,xn ) ∂xn−2 (t21 ,t22 ,...,xn ) |
∂( ∂x ∂x1 |t 21 ,..., ∂xn xn )
( ∂xn |t2n )
∗(t1n ⊖ t2n )) ∗ (t ⊖ t0 )n−1
∂ n−2 t2
∂ |
∂ ∂xn−2 (x1 ,t22 ,...,t2n ) |
x1
= (( ∂x1
∂x1 |t21 ) ∗ (t11 ⊖ t21 )2 ⊕ ...⊕
∂ n−2 t2
∂ |
∂ ∂xn−2 (x1 ,t22 ,...,xn ) |
∂x1 t21
(( ∂xn |t2n ) ∗ (t1n ⊖ t2n )) ∗ (t11 ⊖ t21 ),
H. Xu and Z. Hu 143:17

∂ n−2 t2
∂ |
∂ ∂xn−2 (x1 ,x2 ,...,t2n ) |
∂x2 t22
(( ∂x1 |t21 ) ∗ (t11 ⊖ t21 )) ∗ (t12 ⊖ t22 ) ⊕ ...⊕
∂ n−2 t2
∂ |
∂ ∂xn−2 (t11 ,x2 ,...,xn ) |
∂x2 t22
(( ∂xn |t2n ) ∗ (t1n ⊖ t2n )) ∗ (t12 ⊖ t22 ),
...
∂ n−2 t2
∂ |
∂ ∂xn−2 (x1 ,t22 ,...,xn ) |
∂xn t2n
(( ∂x1 |t21 ) ∗ (t11 ⊖ t21 )) ∗ (t1n ⊖ t2n ) ⊕ ...⊕
∂ n−2 t
2|
∂
∂ ∂xn−2 (t11 ,t22 ,...,xn ) |
xn
( ∂xn
∂xn |t2n ) ∗ (t1n ⊖ t2n )2 ) ∗ (t ⊖ t0 )n−2
= ...

∂
As seen in the above, every time we decompose a ∂x i
|(...) , apply Rule EAppDer1,
and then make reduction with Rule EAppMul3 to lower down the exponent of (t ⊖
t0 )n . Finally, we will decompose the last derivative and get the term t2 in the form of
t2 [t′21 /x1 , t′22 /x2 , ..., t′2n /xn ] where ∀j ∈ [1, n], t′2j is either t2j or xj .
Note that on base type we assume that we have Taylor’s Theorem:
∞ n
X 1 X ∂ k
f (x0 + h) = f (x0 ) + ( hi ) f (x0 )
k! i=1 ∂xi
k=1

where x0 and h is an n-dimensional vector, and xj , hj is its projection to its j-th

dimension.
n
1 ∂ k
So we have (f (k) t0 ) ∗ (t ⊖ t0 )k corresponds to the k-th addend k!
P
( hi ∂x i
) f (x0 ).
i=1
Case: T ′ is function type A → B. Similar to the proof in Theorem 13, for all u of type A,
we define f ∗ = λx : T. f x u, and by using the inductive result on type B, we can prove
the case simiarly as that in Theorem 13.
Case: T ′ is a tuple type (T1 , T2 , T3 , ...). Just define f ∗ = λx : T. πj (f x) to use inductive
result. The rest is simple.
Case: T ′ is a tuple type T1 + T2 . This case is impossible because the righthand is not
well-typed.
Thus we have proven the theorem. ◀

Application: Polynomial Approximation

Taylor’s Theorem has many applications. Here we give an example of using Taylor’s Theorem
for approximation. Suppose there is a point (1, 0) in the polar coordinate system, and we
want to know where the point will be if we slightly change the radius r and the angle θ.
Since it is extremely costive to compute functions such as sin() and cos(), Taylor’s Theorem
enables us to make a fast polynomial approximation.

▶ Example 16. Let function polar2catesian be defined by

polar2cartesian :: (R, R) → (R, R)

polar2cartesian(r, θ) = (r ∗ cos(θ), r ∗ sin(θ))

ICALP 2021
143:18 Analytical Differential Calculus with Integration

We show how to expand polar2cartesian(r, θ) at (1, 0) up to 2nd-order derivative. Since

∂(polar2cartesian(x))
∂x |(1,0) = ∂(π1 x∗cos(π2 x),π
∂x
1 x∗sin(π2 x)
|(1,0)
∂(x1 ∗cos(0),x1 ∗sin(0)) ∂(1∗cos(x2 ),1∗sin(x2 ))
=( ∂x1 |1 , ∂x2 |0 )
= ((1, 0), (0, 1))

we have

∂(polar2cartesian(x))
∂x |(1,0) ∗ (∆r, ∆θ) = (∆r, ∆θ).

Again, we have

1 ∂ (polar2cartesian(x))
2

2 ∂x2 |(1,0) ∗ (∆r, ∆θ)2 = (((0, 0), (0, 1)), ((0, 1), (−1, 0))) ∗ (∆r, ∆θ)2
= (− 21 ∆θ2 , ∆r ∗ ∆θ).

Combining the above, we can use (1⊕∆r⊖ 21 ∆θ2 , ∆θ⊕∆r∗∆θ) to make an approximation
to polar2cartesian(1 + ∆r, ∆θ).

6 Related Work
Differential Calculus and The Change Theory. The differential lambda-calculus [9, 8]
has been studied for computing derivatives of arbitrary higher-order programs. In the
differential lambda-calculus, derivatives are guaranteed to be linear in its argument, where
the incremental lambda-calculus does not have this restriction. Instead, it requires that the
function should be differentiable. The big difference between our calculus and differential
lambda calculus is that we perform computation on terms instead of analysis on terms.
The idea of performing incremental computation using derivatives has been studied by
Cai et al. [7], who give an account using change structures. They use this to provide a
framework for incrementally evaluating lambda calculus programs. It is shown that the work
can be enriched with recursion and fix-point computation [4]. The main difference between
our work and change theory is that we describe changes as mathematical derivatives while
the change theory describe changes as (discrete) deltas.

Incremental/Self-Adaptive Computation. Paige and Koenig [19] present derivatives for a

first-order language with a fixed set of primitives for incremental computation. Blakeley et
al. [16] apply these ideas to a class of relational queries. Koch [14] guarantees asymptotic
speedups with a compositional query transformation and delivers huge speedups in realistic
benchmarks, though still for a first-order database language. We have proved Taylor’s
theorem in our framework, which provides us with another way to perform finite difference
on the computation.
Self-adjusting computation [2] or adaptive function programming [3] provides a dynamic
approach to incrementalization. In this approach, programs execute on the original input in
an enhanced runtime environment that tracks the dependencies between values in a dynamic
dependence graph; intermediate results are memoized. Later, changes to the input propagate
through dependency graphs from changed inputs to results, updating both intermediate and
final results; this processing is often more efficient than recomputation. Mathematically,
self-adjusting computations corresponds to differential equations (The derivative of a function
can be represented by the computational result of function), which may be a future work of
our calculus.
H. Xu and Z. Hu 143:19

Automatic Differentiation. Automatic differentiation [12] is a technique that allows for

efficiently computing the derivative of arbitrary programs, and can be applied to probabilistic
modeling [15] and machine learning [6]. This technique has been successfully applied to some
higher-order languages [21, 10]. As pointed out in [4], while some approaches have been
suggested [18, 13], a general theoretical framework for this technique is still a matter of open
research. We prove the chain rule inside our framework, which lays a foundation for our
calculus to perform automatic differentiation. And with more theorems in our calculus, we
expect more profound applications in differential calculus.

7 Conclusion

In this paper, we propose an analytical differential calculus which is equipped with integration.
This calculus, as far as we are aware, is the first one that has well-defined integration, which has
not appeared in both differential lambda calculus and the change theory. Our calculus enjoys
many nice properties such as soundness and strong normalizing, and has three important
theorems, which have profound applications in computer science. Also, our calculus is highly
extendable, it would be easy for users to add new features and prove more theorems inside
our calculus.

References
1 Martín Abadi and Gordon D. Plotkin. A simple differentiable programming language.
Proceedings of the ACM on Programming Languages, 4(POPL):1–28, January 2020. doi:
10.1145/3371106.
2 Umut A. Acar, Amal Ahmed, and Matthias Blume. Imperative self-adjusting computation. In
George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California,
USA, January 7-12, 2008, pages 309–322. ACM, 2008.
3 Umut A. Acar, Guy E. Blelloch, and Robert Harper. Adaptive functional programming. In
John Launchbury and John C. Mitchell, editors, Conference Record of POPL 2002: The
29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR,
USA, January 16-18, 2002, pages 247–259. ACM, 2002.
4 Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, and C.-H. Luke Ong. Fixing
incremental computation - derivatives of fixpoints, and the recursive semantics of datalog.
In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on
Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and
Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings,
volume 11423 of Lecture Notes in Computer Science, pages 525–552. Springer, 2019.
5 Mario Alvarez-Picallo and C. H. Luke Ong. The difference lambda-calculus: A language for
difference categories, 2020. arXiv:2011.14476.
6 Atilim Gunes Baydin, Barak A. Pearlmutter, Alexey Andreyevich Radul, and Jeffrey Mark
Siskind. Automatic differentiation in machine learning: a survey. J. Mach. Learn. Res.,
18:153:1–153:43, 2017.
7 Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, and Klaus Ostermann. A theory of changes
for higher-order languages: incrementalizing λ-calculi by static differentiation. In Michael F. P.
O’Boyle and Keshav Pingali, editors, ACM SIGPLAN Conference on Programming Language
Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014,
pages 145–155. ACM, 2014.
8 Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antide-
rivatives. Math. Struct. Comput. Sci., 28(7):995–1060, 2018.

ICALP 2021
143:20 Analytical Differential Calculus with Integration

9 Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci.,
309(1-3):1–41, 2003.
10 Conal Elliott. The simple essence of automatic differentiation. Proc. ACM Program. Lang.,
2(ICFP):70:1–70:29, 2018.
11 Paolo G. Giarrusso, Yann Régis-Gianas, and Philipp Schuster. Incremental \lambda -calculus
in cache-transfer style - static memoization by program transformation. In Luís Caires, editor,
Programming Languages and Systems - 28th European Symposium on Programming, ESOP
2019, Held as Part of the European Joint Conferences on Theory and Practice of Software,
ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture
Notes in Computer Science, pages 553–580. Springer, 2019.
12 Andreas Griewank and Andrea Walther. Evaluating derivatives - principles and techniques of
algorithmic differentiation, Second Edition. SIAM, 2008.
13 Robert Kelly, Barak A. Pearlmutter, and Jeffrey Mark Siskind. Evolving the incremental λ
calculus into a model of forward automatic differentiation (AD). CoRR, abs/1611.03429, 2016.
arXiv:1611.03429.
14 Christoph Koch. Incremental query evaluation in a ring of databases. In Jan Paredaens and
Dirk Van Gucht, editors, Proceedings of the Twenty-Ninth ACM SIGMOD-SIGACT-SIGART
Symposium on Principles of Database Systems, PODS 2010, June 6-11, 2010, Indianapolis,
Indiana, USA, pages 87–98. ACM, 2010.
15 Alp Kucukelbir, Dustin Tran, Rajesh Ranganath, Andrew Gelman, and David M. Blei.
Automatic differentiation variational inference. J. Mach. Learn. Res., 18:14:1–14:45, 2017.
16 Per-Åke Larson and Jingren Zhou. Efficient maintenance of materialized outer-join views. In
Rada Chirkova, Asuman Dogac, M. Tamer Özsu, and Timos K. Sellis, editors, Proceedings
of the 23rd International Conference on Data Engineering, ICDE 2007, The Marmara Hotel,
Istanbul, Turkey, April 15-20, 2007, pages 56–65. IEEE Computer Society, 2007.
17 Yanhong A. Liu. Efficiency by incrementalization: An introduction. High. Order Symb.
Comput., 13(4):289–313, 2000. doi:10.1023/A:1026547031739.
18 Oleksandr Manzyuk. A simply typed λ-calculus of forward automatic differentiation. Electronic
Notes in Theoretical Computer Science, 286:257–272, 2012. Proceedings of the 28th Conference
on the Mathematical Foundations of Programming Semantics (MFPS XXVIII).
19 Robert Paige and Shaye Koenig. Finite differencing of computable expressions. ACM Trans.
Program. Lang. Syst., 4(3):402–454, 1982.
20 Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.
21 Jeffrey Mark Siskind and Barak A. Pearlmutter. Nesting forward-mode AD in a functional
framework. High. Order Symb. Comput., 21(4):361–376, 2008.