1 Getting Started

In this chapter we start programming in OCaml. We use an interactive

tool called an interpreter that checks and executes the declarations of a
program one by one. We concentrate on recursive functions on integers
computing things like powers, integer quotients, digit sums, and integer
roots. We also formulate a general algorithm known as linear search
as a higher-order function. We follow an approach known as functional
programming where functions are designed at a mathematical level using
types and equations before they are coded in a concrete programming
language.

1.1 Programs and Declarations

An OCaml program is a sequence of declarations, which are executed

in the order they are written. Our first program
let a = 2 * 3 + 2
let b = 5 * a

consists of two declarations. The first declaration binds the identifier a

to the integer 8, and the second declaration binds the identifier b to
the integer 40. This is clear from our understanding of the arithmetic
operations “+” and “∗”.
To learn programming in OCaml, you want to use an interactive
tool called an interpreter.1 The user feeds the interpreter with text.
The interpreter checks that the given text can be interpreted as a pro-
gram formulated correctly according to the rules of the programming
language. If this is the case, the interpreter determines a type for every
identifier and every expression of the program. Our example program
is formulated correctly and the declared identifiers a and b both receive
the type int (for integer). After a program has been checked success-
fully, the interpreter will execute it. In our case, execution will bind the
identifier a to the integer 8 and the identifier b to the integer 40. After
the program has been executed successfully, the interpreter will show
the values it has computed for the declared identifiers. If a program
is not formulated correctly, the interpreter will show an error message
indicating which rule of the language is violated. Once the interpreter
1
A nice browser-based interpreter is https://try.ocamlpro.com.

1
 1 Getting Started

has checked and executed a program, the user can extend it with further
declarations. This way one can write the declarations of a program one
by one.
At this point you want to start working with the interpreter. You
will learn the exact rules of the language through experiments with the
interpreter guided by the examples and explanations given in this text.
Here is a program redeclaring the identifier a:
let a = 2 * 3 + 2
let b = 5 * a
let a = 5
let c = a + b

The second declaration of the identifier a shadows the first declaration

of a. Shadowing does not affect the binding of b since it is obtained
before the second declaration of a is executed. After execution of the
program, the identifiers a, b, and c are bound to the integers 5, 40,
and 45, respectively.
The declarations we consider in this chapter all start with the key-
word let and consist of a head and a body separated by the equality
symbol “=”. Keywords cannot be used as identifiers. The bodies of
declarations are expressions. Expressions can be obtained with iden-
tifiers, constants, and operators. The nesting of expressions can be
arranged with parentheses. For instance, the expression 2 · 3 + 2 − x
may be written with redundant parentheses as ((2 · 3) + 2) − x. The
parentheses in 2 · (x + y) − 3 are not redundant and are needed to make
the expression x + y the right argument of the product with the left
argument 2.
Every expression has a type. So far we have only seen expressions
of the type int. The values of the type int are integers (whole num-
bers . . . , −2, −1, 0, 1, −2, . . . ). In contrast to the infinite mathematical
type Z, OCaml’s type int provides only a finite interval of machine
integers realized efficiently by the hardware of the underlying com-
puter. The endpoints of the interval can be obtained with the predefined
identifiers min_int and max_int. All machine operations respect this
interval. We have max_int + 1 = min_int, for instance.2
When we reason about programs, we will usually ignore the machine
integers and just assume that all integers are available. As long as the

2
It turns out that different interpreters realize different intervals for machine integers,
even on the same computer. For instance, on the author’s computer, in October
2021, the browser-based Try OCaml interpreter realizes max_int as 231 − 1 =
2147483647, while the official OCaml interpreter realizes max_int as 261 − 1 =
4611686018427387903.

2
 1 Getting Started

numbers in a concrete computation are small enough, this simplification

does not lead to wrong conclusions.
Every programming language provides machine integers for effi-
ciency. There are techniques for realizing much larger intervals of in-
tegers based on machine integers in programming languages.

Exercise 1.1.1 Give an expression and a declaration. Explain the

structure of a declaration. Explain nesting of expressions. Give a type.

Exercise 1.1.2 To what value does the program

let a = 2 let a = a * a let a = a * a

bind the identifier a?

Exercise 1.1.3 Give a machine integer x such that x + 1 < x.

1.2 Functions and Let Expressions

Things become interesting once we declare functions. The declaration

let square x = x * x

declares a function

square : int → int

squaring its argument. The identifier square receives a functional type

int → int describing functions that given an integer return an integer.
Given the declaration of square, execution of the declaration
let a = square 5

binds the identifier a to the integer 25.

Can we compute a power x8 with just three multiplications? Easy,
we just square the integer x three times:
let pow8 x = square (square (square x))

This declaration gives us a function pow8 : int → int.

Another possibility is the declaration
let pow8' x =
let a = x * x in
let b = a * a in
b * b

3
 1 Getting Started

declaring a function pow8 ′ : int → int doing the three multiplications

using two local declarations. Local declarations are obtained with let
expressions

let d in e

combining a declaration d with an expression e using the keywords

let and in. Note that the body of pow ′ nests two let expressions as
let d1 in (let d2 in e). OCaml lets you write redundant parentheses
marking the nesting (if you want to). Let expressions must not be con-
fused with top-level declarations (which don’t use the keyword in).

Exercise 1.2.1 Write a function computing x5 with just 3 multiplica-

tions. Write both a version with square and a version with local dec-
larations. Write the version with local declarations with and without
redundant parentheses marking the nesting.

1.3 Conditionals, Comparisons, and Booleans

The declaration
let abs x = if x < 0 then -x else x

declares a function abs : int → int returning the absolute value of an

integer (e.g., abs(−5) = 5). The declaration of abs uses a compari-
son x < 0 and a conditional formed with the keywords if, then, and
else. We call the expression after the if keyword the condition. The
expression following the then keyword is called the consequence and
the expression after the else keyword is called the alternative. If the
condition evaluates to true, the consequence is evaluated. Otherwise,
the alternative is evaluated.
The declaration
let max x y : int = if x <= y then y else x

declares a function max : int → int → int computing the maximum

of two numbers. This is the first function we see taking two argu-
ments. There is an explicit return type specification in the dec-
laration (appearing as “ : int”), which is needed so that max receives
the correct type.3

3
The complication stems from the design that in OCaml comparisons like ≤ also
apply to types other than int.

4
 1 Getting Started

Given max, we can declare a function

let max3 x y z = max (max x y) z

returning the maximum of three numbers. This time no re-

turn type specification is needed since max forces the correct type
max3 : int → int → int → int.
Next, we declare a three-argument maximum function using a local
declaration:
let max3 x y z : int =
let a = if x <= y then y else x in
if a <= z then z else a

There is a type bool having two values true and false called booleans.
The comparison operator “≤” used for max (written “<=” in OCaml) is
used with the functional type int → int → bool saying that an expression
e1 ≤ e2 where both subexpressions e1 and e2 have type int has type bool.

The declaration
let test (x : int) y z = if x <= y then y <= z else false

declares a function test : int → int → int → bool testing whether its
three arguments appear in order. The type specification given for
the argument x is forces test to receive the correct type. Alternatively,
type specifications could be given for one or all of the other arguments.

Exercise 1.3.1 Declare minimum functions analogous to the maximum

functions declared above. For each declared function give its type (before
you check it with the interpreter). Also, write the declarations with and
without redundant parentheses to understand the nesting.

Exercise 1.3.2 Declare functions int → int → bool providing the com-
parisons x = y, x ̸= y, x < y, x ≤ y, x > y, and x ≥ y. Do this by
just using conditionals and comparisons x ≤ y. Then realize x ≤ y with
x ≤ 0 and subtraction.

5
 1 Getting Started

1.4 Recursive Power Function

Our next goal is a function computing powers xn using multiplication.

We recall that powers satisfy the equations

x0 = 1
xn+1 = x · xn

Using the equations, we can compute every power xn where n ≥ 0. For

instance,

23 = 2 · 22 2nd equation
1
= 2·2·2 2nd equation
= 2 · 2 · 2 · 20 2nd equation
= 2·2·2·1 1st equation
= 8

The trick is that the 2nd equation reduces larger powers to smaller pow-
ers, so that after repeated application of the 2nd equation the power x0
appears, which can be computed with the 1st equation. What we see
here is a typical example of a recursive computation.
Recursive computations can be captured with recursive functions.
To arrive at a function computing powers, we merge the two equations
for powers into a single equation using a conditional:

xn = if n < 1 then 1 else x · xn−1

We now declare a recursive function implementing this equation:

let rec pow x n =
if n < 1 then 1
else x * pow x (n - 1)

The identifier pow receives the type pow : int → int → int. We say
that the function pow applies itself. Recursive function applications are
admitted if the declaration of the function uses the keyword rec.
We have demonstrated an important point about programming at
the example of the power function: Recursive functions are designed at
a mathematical level using equations. Once we have the right equations,
we can implement the function in any programming language.

6
 1 Getting Started

To understand how a recursive function is evaluated by the interpreter,

it can be helpful to look at an execution trace. An execution trace
shows a step-by-step evaluation of an expression. Consider the following
execution trace for pow 5 2:

pow 5 2 = if 2 < 1 then 1 else 5 · pow 5 (2 − 1)

= if false then 1 else 5 · pow 5 (2 − 1)
= 5 · pow 5 (2 − 1)
= 5 · pow 5 1
= 5 · (if 1 < 1 then 1 else 5 · pow 5 (1 − 1))
= 5 · (if false then 1 else 5 · pow 5 (1 − 1))
= 5 · (5 · pow 5 (1 − 1))
= 5 · (5 · pow 5 0)
= 5 · (5 · if 0 < 1 then 1 else 5 · pow 5 (0 − 1))
= 5 · (5 · if true then 1 else 5 · pow 5 (0 − 1))
= 5 · (5 · 1)
=5·5
= 25

For visual clarity, each evaluated expression is underlined. We observe

that whenever the interpreter encounters a conditional, it starts by eval-
uating the condition, and depending on that, it either evaluates the con-
sequence or the alternative. Similarly, whenever a function application
is encountered, its arguments are fully evaluated before the function
itself is applied to them. We will see these rules again once we start
implementing an interpreter for Mini-OCaml in Chapter 5.
Execution traces tend to grow long quickly. Because of that, we
introduce the notion of reduced execution traces. In reduced execu-
tion traces, only function applications are considered. See this example
of a reduced execution trace for pow 5 2:

pow 5 2 = 5 · pow 5 1
= 5 · (5 · pow 5 0)
= 5 · (5 · 1)
= 25

Again, the expressions evaluated in each step are underlined.

7
 1 Getting Started

1.5 Integer Division

Given two integers x ≥ 0 and y > 0, there exist unique integers k, r ≥ 0

such that

x = k·y+r

and

r<y

We call k the quotient and r the remainder of x and y. For instance,

given x = 11 and y = 3, we have the quotient 3 and the remainder 2
(since 11 = 3 · 3 + 2). We speak of integer division, or division with
remainder, or Euclidean division.
We may also characterize the quotient as the largest number k such
that k · y ≤ x, and define the remainder as r = x − k · y.
There is a nice geometrical interpretation of integer division. The
idea is to place boxes of the same length y next to each other into a
shelf of length x. The maximal number of boxes that can be placed into
the shelf is the quotient k and the length of the space remaining is the
remainder r = x − k · y < y. For instance, if the shelf has length 11
and each box has length 3, we can place at most 3 boxes into the shelf,
with 2 units of length remaining.4
Given that x and y uniquely determine k and r, we are justified in
using the notations x/y and x % y for k and r. By definition of k and r,
we have

x = (x/y) · y + x % y

and

x%y < y

for all x ≥ 0 and y > 0.

From our explanations it is clear that we can compute x/y and x % y
given x and y. In fact, the resulting operations x/y and x % y are es-
sential for programming and are realized efficiently for machine integers
on computers. We refer to the operations as division and modulo, or
just as “div” and “mod”. Accordingly, we read the applications x/y and
x % y as “x div y” and “x mod y”. OCaml provides both operations as
primitive operations using the notations x/y and x mod y.
4
A maybe simpler geometrical interpretation of integer division asks how many boxes
of height y can be stacked on each other without exceeding a given height x.

8
 1 Getting Started

Digit sum
With div and mod we can decompose the decimal representation of
numbers. For instance, 367 % 10 = 7 and 367/10 = 36. More generally,
x % 10 yields the last digit of the decimal representation of x, and x/10
cuts off the last digit of the decimal representation of x.
Knowing these facts, we can declare a recursive function computing
the digit sum of a number:
let rec digit_sum x =
if x < 10 then x
else digit_sum (x / 10) + (x mod 10)

For instance, we have digit_sum 367 = 16. We note that digit_sum

terminates since the argument gets smaller upon recursion.

Exercise 1.5.1 (First digit) Declare a function that yields the first
digit of the decimal representation of a number. For instance, the first
digit of 367 is 3.

Exercise 1.5.2 (Maximal digit) Declare a function that yields the

maximal digit of the decimal representation of a number. For instance,
the maximal digit of 376 is 7.

Digit reversal
We now write a function rev that given a number computes the number
represented by the reversed digital representation of the number. For
instance, we want rev 76 = 67, rev 67 = 76, and rev 7600 = 67. To
write rev, we use an important algorithmic idea. The trick is to have an
additional accumulator argument that is initially 0 and that collects
the digits we cut off at the right of the main argument. For instance,
we want the (reduced) execution trace

rev ′ 456 0 = rev ′ 45 6 = rev ′ 4 65 = rev ′ 0 654 = 654

for the helper function rev ′ with the accumulator argument.

We declare rev and the helper function rev ′ as follows:
let rec rev' x a =
if x <= 0 then a
else rev' (x / 10) (10 * a + x mod 10)
let rev x = rev' x 0

We refer to rev ′ as the worker function for rev and to the argument a
of rev ′ as the accumulator argument of rev ′ . We note that rev ′ ter-
minates since the first argument gets smaller upon recursion.

9
 1 Getting Started

Greatest common divisors

Recall the notion of greatest common divisors. For instance, the greatest
common divisor of 34 and 85 is the number 17. In general, two numbers
x, y ≥ 0 such that x + y > 0 always have a unique greatest common
divisor. We assume the following rules for greatest common divisors
(gcds for short):5
1. The gcd of x and 0 is x.
2. If y > 0, the gcd of x and y is the gcd of y and x % y.
The two rules suffice to declare a function gcd : int → int → int com-
puting the gcd of two numbers x, y ≥ 0 such that x + y > 0:
let rec gcd x y =
if y < 1 then x
else gcd y (x mod y)

The function terminates for valid arguments since (x % y) < y for x ≥ 0

and y ≥ 1.
Computing div and mod with repeated subtraction
We can compute x/y and x % y using repeated subtraction. To do so,
we simply subtract y from x as long as we do not obtain a negative
number. Then x/y is the number of successful subtractions and b is the
remaining number.
let rec my_div x y = if x < y then 0 else 1 + my_div (x - y) y
let rec my_mod x y = if x < y then x else my_mod (x - y) y

We remark that both functions terminate for x ≥ 0 and y > 0 since the
first argument gets smaller upon recursion.

Exercise 1.5.3 (Execution Traces)

Give a full exection trace for each the following applications:

rev ′ 67 1 gcd 8 12

Additionally, give reduced execution traces for these applications:

rev ′ 678 0 rev ′ 6780 0 gcd 90 120 gcd 153 33 my_mod 17 5

We remark that the functions rev ′ , gcd, and my_mod employ a special
form of recursion known as tail recursion. We will discuss tail recursion
in Section 1.11.

5
We will prove the correctness of the rules in a later chapter.

10
 1 Getting Started

1.6 Mathematical Level versus Coding Level

When we design a function for OCaml or another programming lan-

guage, we do this at the mathematical level. The same is true when
we reason about functions and their correctness. Designing and rea-
soning at the mathematical level has the advantage that it serves all
programming languages, not just the concrete programming language
we have chosen to work with (OCaml in our case). Given the design of
a function at the mathematical level, we refer to the realization of the
function in a concrete programming language as coding. Programming
as we understand it emphasizes design and reasoning over coding.
It is important to distinguish between the mathematical level and
the coding level. At the mathematical level, we ignore the type int of
machine integers and instead work with infinite mathematical types. In
particular, we will use the types

N : 0, 1, 2, 3, . . . natural numbers
+
N : 1, 2, 3, 4, . . . positive integers
Z : . . . , −2, −1, 0, 1, 2, . . . integers
B : false, true booleans

When starting with the design of a function, it is helpful to fix a

mathematical type for the function. Once the type is settled, we can
collect equations the function should satisfy. The goal here is to come
up with a collection of equations that is sufficient for computing the
function.
For instance, when we design a power function, we may start with
the mathematical type

pow : Z → N → Z

and the equation

pow x n = xn

Together, the type and the equation specify the function we want to
define. Next we need equations that can serve as defining equations
for pow. The specifying equation is not good enough since we assume,
for the purpose of the example, that the programming language we want
to code in doesn’t have a power operator. We now recall that powers xn
satisfy the equations

x0 = 1
xn+1 = x · xn

11
 1 Getting Started

In Section 1.4 we have already argued that rewriting with the two equa-
tions suffices to compute all powers we can express with the type given
for pow. Next we adapt the equations to the function pow we are de-
signing:

pow x 0 = 1
pow x n = x · pow x (n − 1) if n > 0

The second equation now comes with an application condition re-

placing the pattern n + 1 in the equation xn+1 = x · xn .
We observe that the equations are exhaustive and disjoint, that is,
for all x and n respecting the type of pow, the left side of one and only
one of the equations applies to the application pow x n. We choose
the equations as defining equations for pow and summarize our design
with the mathematical definition

pow : Z → N → Z
pow x 0 := 1
pow x n := x · pow x (n − 1) if n > 0
Note that we write defining equations with the symbol “:=” to mark
them as defining.
We observe that the defining equations for pow are terminating.
The termination argument is straightforward: Each recursion step
issued by the second equation decreases the second argument n by 1.
This ensures termination since a chain x1 > x2 > x3 > · · · of natural
numbers cannot be infinite.
Next we code the mathematical definition as a function declaration
in OCaml:
let rec pow x n =
if n < 1 then 1
else x * pow x (n - 1)

The switch to OCaml involves several significant issues:

1. The type of pow changes to int → int → int since OCaml has no
special type for N (as is typical for execution-oriented programming
languages). Thus the OCaml function admits arguments that are
not admissible for the mathematical function. We speak of spurious
arguments.
2. To make pow terminating for negative n, we return 1 for all n < 1.
We can also use the equivalent comparison n ≤ 0. If we don’t scare
away from nontermination for spurious arguments, we can also use
the equality test n = 0.

12
 1 Getting Started

3. The OCaml type int doesn’t give us the full mathematical type Z of
integers but just a finite interval of machine integers.
When we design a function, there is always a mathematical level
governing the coding level for OCaml. One important point about the
mathematical level is that it doesn’t change when we switch to another
programming language. In this text, we will concentrate on the mathe-
matical level.
When we argue the correctness of the function pow, we do this at
the mathematical level using the infinite types Z and N. As it comes
to the realization in OCaml, we just hope that the numbers involved
for particular examples are small enough so that the difference between
mathematical arithmetic and machine arithmetic doesn’t show. The
reason we ignore machine integers at the mathematical level is simplicity.

1.7 More about Mathematical Functions

We use the opportunity and give mathematical definitions for some func-
tions we already discussed. A mathematical function definition consists
of a type and a system of defining equations.
Remainder

% : N → N+ → N
x % y := x if x < y
x % y := (x − y) % y if x ≥ y

Recall that N+ is the type of positive integers 1, 2, 3, . . . . By using the

type N+ for the divisor we avoid a division by zero.
Digit sum

D: N→N
D(x) := x if x < 10
D(x) := D(x/10) + (x % 10) if x ≥ 10
Digit Reversal

R: N→N→N
R 0 a := a
R x a := R (x/10) (10 · a + (x % 10)) if x > 0
A system of defining equations for a function must respect the type
specified for the function. In particular, the defining equations must be
exhaustive and disjoint for the type specified for the function.

13
 1 Getting Started

Often, the defining equations of a function will be terminating for

all arguments. This is the case for each of the three function defined
above. In each case, the same termination argument applies: The first
argument, which is a natural number, is decreased by each recursion
step.
Curly braces
We can use curly braces to write several defining equations with the
same left-hand side with just one left-hand side. For instance, we may
write the defining equations of the digit sum function as follows:

x if x < 10
D x :=
D(x/10) + (x % 10) if x ≥ 10

Total and partial functions

Functions where the defining equations terminate for all arguments are
called total, and function where this is not the case are called partial.
Most mathematical functions we will look at are total, but there are
a few partial functions that matter. If there is a way to revise the
mathematical definition of a function such that the function becomes
total, we will usually do so. The reason we prefer total functions over
partial functions is that equational reasoning for total functions is much
easier than it is for partial functions. For correct equational reasoning
about partial functions we need side conditions making sure that all
function applications occurring in an equation used for reasoning do
terminate.
We say that a function diverges for an argument if it does not
terminate for this argument. Here is a function that diverges for all
numbers smaller than 10 and terminates for all other numbers:

f : N→N
f (n) := f (n) if n < 10
f (n) := n if n ≥ 10

Exercise 1.7.1 Define a function N → N that terminates for even num-

bers and diverges for odd numbers.

Graph of a function
Abstractly, we may see a function f : X → Y as the set of all argument-
result pairs (x, f (x)) where x is taken from the argument type X. We
speak of the graph of a function. The graph of a function completely
forgets about the definition of the function.

14
 1 Getting Started

When we speak of a mathematical function in this text, we always

include the definition of the function with a type and a system of defining
equations. This information is needed so that we can compute with the
function.
In noncomputational mathematics, one usually means by a function
just a set of argument-result pairs.
GCD function
It is interesting to look at the mathematical version of the gcd function
from Section 1.5:

G: N→N→N
G x 0 := x
G x y := G y (x % y) if y > 0

The defining equations are terminating since the second argument is

decreased upon recursion (since x % y < y if y > 0). Note that the type
of G admits x = y = 0, a case where no greatest comon divisor exists.

1.8 A Higher-Order Function for Linear Search

A boolean test for numbers is a function f : int → bool expressing a

condition for numbers. If f (k) = true, we say that k satisfies f .
Linear search is an algorithm that given a boolean test f : int → bool
and a number n computes the first number k ≥ n satisfying f by check-
ing f for
k = n, n + 1, n + 2, . . .
until f is satisfied for the first time. We realize linear search with an
OCaml function

first : (int → bool) → int → int

taking the test as first argument:

let rec first f k =
if f k then k
else first f (k + 1)

Functions taking functions as arguments are called higher-order func-

tions. Higher-order functions are a key feature of functional program-
ming.
Recall that we have characterized in Section 1.5 the integer quotient
x/y as the maximal number k such that k · y ≤ x. Equivalently, we may

15
 1 Getting Started

characterize x/y as the first number k ≥ 0 such that (k + 1) · y > x

(recall the shelf interpretation). This gives us the equation

x/y = first (λk. (k + 1) · y > x) 0 if x ≥ 0 and y > 0 (1.1)

The functional argument of first is described with a lambda expres-

sion
λk. (k + 1) · y > x
Lambda expressions are a common mathematical notation for describing
functions without giving them a name.6
We use (1.1) to declare a function

div : int → int → int

computing quotients x/y:

let div x y = first (fun k -> (k + 1) * y > x) 0

From the declaration we learn that OCaml writes lambda expressions

with the words “fun” and “->”. Here is a reduced execution trace show-
ing how quotients x/y are computed with first:

div 11 3 = first (λk. (k + 1) · 3 > 11) 0 1 · 3 ≤ 11

= first (λk. (k + 1) · 3 > 11) 1 2 · 3 ≤ 11
= first (λk. (k + 1) · 3 > 11) 2 3 · 3 ≤ 11
= first (λk. (k + 1) · 3 > 11) 3 4 · 3 > 11
= 3

We remark that first is our first inherently partial function. For

instance, the function

first (λk. false) : N → N

diverges for all arguments. More generally, the application first f n

diverges whenever there is no k ≥ n satisfying f .
Exercise 1.8.1 Declare a function div ′ such that div x y = div ′ x y 0
by specializing first to the test λk. (k + 1) · y > x.

Exercise 1.8.2 Declare a function sqrt : N → N such that sqrt(n2 ) = n

for all n. Hint: Use first.

Exercise 1.8.3 Declare a terminating function bounded_first such that

bounded_first f n yields the first k ≥ 0 such that k ≤ n and k satisfies f .
6
The greek letter “λ” is pronounced “lambda”. Sometimes lambda expressions λx.e
are written with the more suggestive notation x 7→ e.

16
 1 Getting Started

1.9 Partial Applications

Functions described with lambda expressions can also be expressed with

declared functions. To have an example, we declare div with first and a
helper function test replacing the lambda expression:
let test x y k = (k + 1) * y > x
let div x y = first (test x y) 0

The type of the helper function test is int → int → int → bool. Applying
test to x and y yields a function of type int → bool as required by first.
We speak of a partial application. Here is a reduced execution trace
showing how quotients x/y are computed with first and test:

div 11 3 = first (test 11 3) 0 1 · 3 ≤ 11

= first (test 11 3) 1 2 · 3 ≤ 11
= first (test 11 3) 2 3 · 3 ≤ 11
= first (test 11 3) 3 4 · 3 > 11
= 3

We may describe the partial applications of test with equivalent lambda

expressions:

test x y = λk. (k + 1) · y > x

test 11 3 = λk. (k + 1) · 3 > 11

We can also describe partial applications of test to a single argument

with equivalent lambda expressions:

test x = λyk. (k + 1) · y > x = λy. λk. (k + 1) · y > x

test 11 = λyk. (k + 1) · y > 11 = λy. λk. (k + 1) · y > 11

Note that lambda expressions with two argument variables are nota-
tion for nested lambda expressions with single arguments. We can also
describe the function test with a nested lambda expression:

test = λxyk. (k + 1) · y > x = λx. λy. λk. (k + 1) · y > x

Following the nesting of lambda expressions, we may see applications

and function types with several arguments as nestings of applications
and function types with single arguments:

e1 e2 e3 = (e1 e2 ) e3
t1 → t2 → t3 = t1 → (t2 → t3 )

17
 1 Getting Started

Note that applications group to the left and function types group to the
right.
We have considered equations between functions in the discussion of
partial applications of test. We consider two functions as equal if they
agree on all arguments. So functions with very different definitions may
be equal. In fact, two functions are equal if and only if they have the
same graph. We remark that there is no algorithm deciding equality of
functions in general.

Exercise 1.9.1
a) Write λxyk. (k + 1) · y > x as a nested lambda expression.
b) Write test 11 3 10 as a nested application.
c) Write int → int → int → bool as a nested function type.

Exercise 1.9.2 Express the one-argument functions described by the

expressions x2 , x3 and (x+1)2 with lambda expressions in mathematical
notation. Translate the lambda expressions to expressions in OCaml and
have them type checked. Do the same for the two-argument function
described by the expression x < k 2 .

Exercise 1.9.3 (Sum functions)

a) Define a function N → N computing the sum 0 + 1 + 2 + · · · + n of
the first n numbers.
b) Define a function N → N computing the sum 0 + 12 + 22 + · · · + n2
of the first n square numbers.
c) Define a function sum : (N → N) → N → N computing for a given
function f the sum f (0) + f (1) + f (2) + · · · + f (n).
d) Give partial applications of the function sum from (c) providing spe-
cialized sum functions as asked for by (a) and (b).

1.10 Inversion of Strictly Increasing Functions

A function f : N → N is strictly increasing if

f (0) < f (1) < f (2) < · · ·

Strictly increasing functions can be inverted using linear search. That

is, given a strictly increasing function f : N → N, we can construct a
function g : N → N such that g(f (n)) = n for all n. The construction is
explained by the equation

first (λk. f (k + 1) > f (n)) 0 = n (1.2)

18
 1 Getting Started

which in turn gives us the equation

(λx. first (λk. f (k + 1) > x) 0) (f (n)) = n (1.3)

For a concrete example, let f (n) := n2 . (1.3) tells us that

g(x) := first (λk. (k + 1)2 > x) 0

is a function N → N such that g(n2 ) = n for all n. Thus we know that

sqrt x := first (λk. (k + 1)2 > x) 0

√
computes integer square roots ⌊ 2 x⌋. For instance, we have sqrt(1) = 1,
sqrt(4) = 2, and sqrt(9) = 3. The floor operator ⌊x⌋ converts a real
number x into the greatest integer y ≤ x.
Exercise 1.10.1 Give a reduced execution trace for sqrt 10.

Exercise 1.10.2 Declare a function sqrt ′ such that sqrt x = sqrt ′ x 0

by specializing first to the test λk. (k + 1)2 > x.

Exercise 1.10.3 The ceiling operator ⌈x⌉ converts a real number

into the least integer y such that x ≤ y.
√
a) Declare a function computing rounded down cube roots ⌊ 3 x⌋.
√
b) Declare a function computing rounded up cube roots ⌈ 3 x ⌉.

Exercise 1.10.4 Let y > 0. Convince yourself that λx. x/y inverts the
strictly increasing function λn. n · y.

Exercise 1.10.5 Declare inverse functions for the following functions:

a) λn.n3
b) λn.nk for k ≥ 2
c) λn.k n for k ≥ 2

Exercise 1.10.6 Declare a function inv : (N → N) → (N → N) that

given a strictly increasing function f yields a function inverting f . Then
express the functions from exercise 1.10.5 using inv.

Exercise 1.10.7 Let f : N → N be strictly increasing. Convince your-

self that the functions

λx. first (λk. f (k) = x) 0

λx. first (λk. f (k) ≥ x) 0
λx. first (λk. f (k + 1) > x) 0

all invert f and find out how they differ.

19
 1 Getting Started

1.11 Tail Recursion

A special form of functional recursion is tail recursion. Tail recursion

matters since it can be executed more efficiently than general recursion.
Tail recursion imposes the restriction that recursive function applica-
tions can only appear in tail positions where they directly yield the
result of the function. Hence recursive applications appearing as part of
another application (operator or function) are not tail recursive. Typical
examples of tail recursive functions are the functions rev ′ , gcd, my_mod,
and first we have seen before. Counterexamples for tail recursive func-
tions are the recursive functions pow (the recursive application is nested
into a product) and my_div (the recursive application is nested into a
sum).
Tail recursive functions have the property that their execution can be
traced in a simple way. For instance, we have the tail recursive reduced
execution trace

gcd 36 132 = gcd 132 36

= gcd 36 24
= gcd 24 12
= gcd 12 0
= 12

For functions where the recursion is not tail recursive, traces look more
complicated, for instance

pow 2 3 = 2 · pow 2 2
= 2 · (2 · pow 2 1)
= 2 · (2 · (2 · pow 2 0))
= 2 · (2 · (2 · 1))
= 8

In imperative programming languages tail recursive functions can be

expressed with loops. While imperative languages are designed such
that loops should be used whenever possible, functional programming
languages are designed such that tail recursive functions are preferable
over loops.
Often recursive functions that are not tail recursive can be reformu-
lated as tail recursive functions by introducing an extra argument serving
as accumulator argument. Here is a tail recursive version of pow :
let rec pow' x n a =

20
 1 Getting Started

if n < 1 then a
else pow' x (n - 1) (x * a)

We explain the role of the accumulator argument with a reduced execu-

tion trace:

pow ′ 2 3 1 = pow ′ 2 2 2
= pow ′ 2 1 4
= pow ′ 2 0 8
= 8

Exercise 1.11.1 (Factorials) In mathematics, the factorial of a pos-

itive integer n, denoted by n!, is the product of all positive integers less
than or equal to n:

n! = n · (n − 1) · · · · · 2 · 1

For instance,

5! = 5 · 4 · 3 · 2 · 1 = 120

In addition, 0! is defined as 1. We capture this specification with a

recursive function defined as follows:

!:N→N
0! := 1
(n + 1)! := (n + 1) · n!

a) Declare a function fac : int → int computing factorials.

b) Define a tail recursion function f : N → N → N such that n! = f 1 n.
c) Declare a tail recursive function fac ′ : int → int → int such that
fac ′ 1 computes factorials.

1.12 Tuples

Sometimes we want a function that returns more than one value. For
instance, the time for a marathon may be given with three numbers in
the format h : m : s, where h is the number of hours, m is the number
of minutes, and s is the number of seconds the runner needed. The time
of Eliud Kipchoge’s world record in 2018 in Berlin was 2 : 01 : 39. There
is the constraint that m < 60 and s < 60.

21
 1 Getting Started

OCaml has tuples to represent collections of values as single values.

To represent the marathon time of Kipchoge in Berlin, we can use the
tuple

(2, 1, 39) : int × int × int

consisting of three integers. The product symbol “×” in the tuple type
is written as “*” in OCaml. The component types of a tuple are not
restricted to int, and there can be n ≥ 2 positions, where n is called
the length of the tuple. We may have tuples as follows:

(2, 3) : int × int

(7, true) : int × bool
((2, 3), (7, true)) : (int × int) × (int × bool)

Note that the last example nests tuples into tuples. We mention that
tuples of length 2 are called pairs, and that tuples of length 3 are called
triples.
We can now write two functions

sec : int × int × int → int

hms : int → int × int × int

translating between times given in total seconds and times given as

(h, m, s) tuples:
let sec (h,m,s) = 3600 * h + 60 * m + s
let hms x =
let h = x / 3600 in
let m = (x mod 3600) / 60 in
let s = x mod 60 in
(h,m,s)

Exercise 1.12.1
a) Give a tuple of length 5 where the components are the values 2 and 3.
b) Give a tuple of type int × (int × (bool × bool)).
c) Give a pair whose first component is a pair and whose second com-
ponent is a triple.

Exercise 1.12.2 (Sorting triples) Declare a function sort sorting

triples. For instance, we want sort (3, 2, 1) = (1, 2, 3). Designing such
a function is interesting. Given a triple (x, y, z), the best solution we
know of first ensures y ≤ z and then inserts x at the correct position.
Start from the code snippet

22
 1 Getting Started

let sort (x,y,z) =

let (y,z) = if y <= z then (y,z) else (z, y) in
if x <= y then ?. . .?
else ?. . .?

where the local declaration ensures y ≤ z using shadowing.

Exercise 1.12.3 (Medians) The median of three numbers is the num-

ber in the middle. For instance, the median of 5, 0, 1 is 1. Declare a
function that takes three numbers and yields the median of the num-
bers.

1.13 Exceptions and Spurious Arguments

What happens when we execute the native operation 5/0 in OCaml?

Execution is aborted and an exception is reported:
Exception: Division_by_zero

Exceptions can be useful when debugging erroneous programs. We will

say more about strings and exceptions in later chapters.
There is no equivalent to exceptions at the mathematical level. At
the mathematical level we use types like N+ or side conditions like y ̸= 0
to exclude undefined applications like x/0.
When coding a mathematical function in OCaml, we need to replace
mathematical types like N with the OCaml type int. This introduces
spurious arguments not anticipated by the mathematical function.
There are different ways to cope with spurious arguments:
1. Ignore the presence of spurious arguments. This is the best strategy
when you solve exercises in this text.
2. Use a wrapper function raising exceptions when spurious arguments
show up. The wrapper function facilitates the discovery of situations
where functions are accidentally applied to spurious arguments.
As an example, we consider the coding of the mathematical remainder
function

rem : N → N+ → N
rem x y := x if x < y
rem x y := rem (x − y) y if x ≥ y

as the OCaml function

let rec rem x y = if x < y then x else rem (x - y) y

23
 1 Getting Started

receiving the type int → int → int. In OCaml we now have the spurious
situation that rem x 0 diverges for all x ≥ 0. There other spurious
situations whose analysis is tedious since machine arithmetic needs to
be taken into account. Using the wrapper function
let rem_checked x y =
if x >=0 && y > 0 then rem x y
else invalid_arg "rem_checked"

all spurious situations are uniformly handled by throwing the exception

Invalid_argument "rem_checked"

There are several new features here:

• The lazy boolean and connective x >= 0 && y > 0 tests two condi-
tions and is equivalent to if x >= 0 then y > 0 else false.
• There is the string "rem_checked". Strings are values like integers
and booleans and have type string.
• The predefined function invalid_arg raises an exception saying that
rem_checked was called with spurious arguments.7
When an exception is raised, execution of a program is aborted and the
exception raised is reported.
We use the opportunity and introduce the lazy boolean connec-
tives as abbreviations for conditionals:

e1 && e2 ⇝ if e1 then e2 else false lazy and

e1 || e2 ⇝ if e1 then true else e2 lazy or

Exercise 1.13.1 Consider the declaration

let eager_or x y = x || y

Find expressions e1 and e2 such that the expressions e1 || e2 and

eager_or e1 e2 behave differently. Hint: Choose a diverging expres-
sion for e2 and keep in mind that execution of a function application
executes all argument expressions. In contrast, execution of a condi-
tional if e1 then e2 else e3 executes e1 and then either e2 or e3 , but
not both.

Exercise 1.13.2 (Sorting triples) Recall exercise 1.12.2. With lazy

boolean connectives a function sorting triples can be written without
much thinking by doing a naive case analysis considering the alternatives
x is in the middle or y is in the middle or z is in the middle.

7
OCaml says “invalid argument” for “spurious argument”.

24
 1 Getting Started

1.14 Polymorphic Functions

Consider the declaration of a projection function for pairs:

let fst (x,y) = x

What type does fst have? Clearly, int × int → int and bool × int → bool
are both types admissible for fst. In fact, every type t1 × t2 → t1
is admissible for fst. Thus there are infinitely many types admissible
for fst.
OCaml solves the situation by typing fst with the polymorphic type

∀αβ. α × β → α

A polymorphic type is a type scheme whose quantified variables (α

and β in the example) can be instantiated with all types. The instances
of the polymorphic type above are all types t1 × t2 → t1 where the
types t1 and t2 can be freely chosen. When a polymorphically typed
identifier is used in an expression, it can be used with any instance of its
polymorphic type. Thus fst (1 , 2 ) and fst (true, 5 ) are both well-typed
expressions.
Here is a polymorphic swap function for pairs:
let swap (x,y) = (y,x)

OCaml will type swap with the polymorphic type

∀αβ. α × β → β × α

This is in fact the most general polymorphic type that is admissible

for swap. Similarly, the polymorphic type given for fst is the most
general polymorphic type admissible for fst. OCaml will always derive
most general types for function declarations.
Exercise 1.14.1 Declare functions admitting the following polymor-
phic types:
a) ∀α. α → α
b) ∀αβ. α → β → α
c) ∀αβγ. (α × β → γ) → α → β → γ
d) ∀αβγ. (α → β → γ) → α × β → γ
e) ∀αβ. α → β

1.15 Iteration

Given a function f : t → t, we write f n (x) for the n-fold application

of f to x. For instance, f 0 (x) = x, f 1 (x) = f (x), f 2 (x) = f (f (x)),

25
 1 Getting Started

and f 3 (x) = f (f (f (x))). More generally, we have

f n+1 (x) = f n (f x)

Given an iteration f n (x), we call f the step function and x the start
value of the iteration.
With iteration we can compute sums, products, and powers of non-
negative integers just using additions x + 1:

x + n = x + 1 · · · + 1 = (λa.a + 1)n (x)

n · x = 0 + x · · · + x = (λa.a + x)n (0)
xn = 1 · x · · · · x = (λa.a · x)n (1)

Exploiting commutativity of addition and multiplication, we arrive at

the defining equations

succ x := x + 1
add x n := succ n (x)
mul n x := (add x)n (0)
pow x n := (mul x)n (1)

We define a polymorphic iteration operator

iter : ∀α. (α → α) → N → α → α
iter f 0 x := x
iter f (n + 1) x := iter f n (f x)

so that we can obtain iterations f n (x) as applications iter f n x of the

operator. Note that the function iter is polymorphic, higher-order, and
tail-recursive. In OCaml, we will use the declaration
let rec iter f n x =
if n < 1 then x
else iter f (n - 1) (f x)

Functions for addition, multiplication, and exponentiation can now

be declared as follows:
let succ x = x + 1
let add x y = iter succ y x
let mul x y = iter (add y) x 0
let pow x y = iter (mul x) y 1

Note that these declarations are non-recursive. Thus termination needs

only be checked for iter, where it is obvious (2nd argument is decreased).

26
 1 Getting Started

Exercise 1.15.1 Declare a function testing evenness of numbers by it-

erating on booleans. What do you have to change to obtain a function
checking oddness?

Exercise 1.15.2 We have the equation

f n+1 (x) = f (f n (x))

providing for an alternative, non-tail-recursive definition of an itera-

tion operator. Give the mathematical definition and the declaration in
OCaml of an iteration operator using the above equation.

1.16 Iteration on Pairs

Using iteration and successor as basic operations on numbers, we have

defined functions computing sums, products, and powers of nonnegative
numbers. We can also define a predecessor function8

pred : N+ → N
pred (n + 1) := n

just using iteration and successor (the successor of an integer x is x + 1).

The trick is to iterate on pairs. We start with the pair (0, 0) and iterate
with a step function f such that n + 1 iterations yield the pair (n, n + 1).
For instance, the iteration

f 5 (0, 0) = f 4 (0, 1) = f 3 (1, 2) = f 2 (2, 3) = f (3, 4) = (4, 5)

using the step function

f (a, k) = (k, k + 1)

yields the predecessor of 5 as the first component of the computed pair.

More generally, we have

(n, n + 1) = f n+1 (0, 0)

We can now declare a predecessor function as follows:

let pred n = fst (iter (fun (a,k) -> (k, succ k)) n (0,0))

Iteration on pairs is a powerful computation scheme. Our second

example concerns the sequence of Fibonacci numbers

0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, . . .

8
the predecessor of an integer x is x − 1.

27
 1 Getting Started

which is well known in mathematics. The sequence is obtained by start-

ing with 0, 1 and then adding new elements as the sum of the two pre-
ceding elements. We can formulate this method as a recursive function

fib : N → N
fib(0) := 0
fib(1) := 1
fib (n + 2) := fib (n) + fib (n + 1)

Incidentally, this is the first recursive function we see where the recursion
is binary (two recursive applications) rather than linear (one recursive
application). Termination follows with the usual argument that each
recursion step decreases the argument.
If we look again at the rule generating the Fibonacci sequence, we
see that we can compute the sequence by starting with the pair (0, 1)
and iterating with the step function f (a, b) = (b, a + b). For instance,

f 5 (0, 1) = f 4 (1, 1) = f 3 (1, 2) = f 2 (2, 3) = f (3, 5) = (5, 8)

yields the pair (fib(5), fib(6)). More generally, we have

(fib(n), fib(n + 1)) = (λ(a, b).(b, a + b))n (0, 1)

Thus we can declare an iterative Fibonacci function as follows:

let fibi n = fst (iter (fun (a,b) -> (b, a + b)) n (0,1))

In contrast to the previously defined function fib, function fibi requires

only tail recursion as provided by iter.

Exercise 1.16.1 Declare a function computing the sum 0+1+2+ · · · +n

by iteration starting from the pair (0, 1).

Exercise 1.16.2 Declare a function f : N → N computing the sequence

0, 1, 1, 2, 4, 7, 13, . . .

obtained by starting with 0, 1, 1 and then adding new elements as the

sum of the three preceding elements. For instance, f (3) = 2, f (4) = 4,
and f (5) = 7.

Exercise 1.16.3 Functions defined with iteration can always be elab-

orated into tail-recursive functions not using iteration. If the iteration
is on pairs, one can use separate accumulator arguments for the compo-
nents of the pairs. Follow this recipe and declare a tail-recursive function
fib′ such that fib′ n 0 1 = fib(n).

28
 1 Getting Started

Exercise 1.16.4 Recall the definition of factorials n! from exer-

cise 1.11.1.
a) Give a step function f such that (n!, n) = f n (1, 0).
b) Declare a function faci computing factorials with iteration.
c) Declare a tail-recursive function fac ′ such that fac ′ n 1 0 = n!. Follow
the recipe from exercise 1.16.3.

1.17 Computing Primes

A prime number is an integer greater 1 that cannot be obtained as

the product of two integers greater 1. There are infinitely many prime
numbers. The sequence of prime numbers starts with

2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, · · ·

We want to declare a function nth_prime : N → N that yields the el-

ements of the sequence starting with nth_prime 0 = 2 . Assuming a
primality test prime : int → bool, we can declare nth_prime as follows:
let next_prime x = first prime (x + 1)
let nth_prime n = iter next_prime n 2

Note that next_prime x yields the first prime greater than x. Also note
that the elegant declarations of next_prime and nth_prime are made
possible by the higher-order functions first and iter.
It remains to come up with a primality test (a test checking
whether an integer is a prime number). Here are 4 equivalent char-
acterizations of primality of x assuming that x, k, and n are natural
numbers:
1. x ≥ 2 ∧ ∀ k ≥ 2. ∀ n ≥ 2. x ̸= k · n
2. x ≥ 2 ∧ ∀ k, 2 ≤ k < x. x % k > 0
3. x ≥ 2 ∧ ∀ k > 1, k 2 ≤ x. x % k > 0
√
4. x ≥ 2 ∧ ∀ k, 1 < k ≤ 2 x. x % k > 0
Characterization (1) is close to the informal definition of prime numbers.
Characterizations (2), (3), and (4) are useful for our purposes since they
can be realized algorithmically. Starting from (1), we see that x − 1 can
be used as an upper bound for k and n. Thus we have to test x = k · n
only for finitely many k and n, which can be done algorithmically. The
next thing we see is that is suffices to have k because n can be kept
implicit using the remainder operation. Finally, we see that it suffices
to test for k such that k 2 ≤ x since we can assume n ≥ k. Thus we can
√
sharpen the upper bound from x − 1 to 2 x.

29
 1 Getting Started

Here we choose the second characterization to declare a primality

test in OCaml and leave the realization of the computationally faster
fourth characterization as an exercise.
To test the bounded universal quantification in the second charac-
terization, we declare a higher-order function

forall : int → int → (int → bool) → bool

such that

forall m n f = true ←→ ∀k, m ≤ k ≤ n. f k = true

using the defining equations9


true m>n
forall m n f :=
f m && forall (m + 1) n f m≤n

The function forall terminates since |n + 1 − m| ≥ 0 decreases with

every recursion step.
We now define a primality test based on the second characterization:

prime x := x ≥ 2 && forall 2 (x − 1) (λk. x % k > 0)

The discussion of primality tests makes it very clear that program-

ming involves mathematical reasoning.
Efficient primality tests are important in cryptography and other
areas of computer science. The naive versions we have discussed here
are known as trial division algorithms and are too slow for practical
purposes.

Exercise 1.17.1 Express forall with iter.

Exercise 1.17.2 Declare a test exists : int → int → (int → bool) → bool
such that exists m n f = true ←→ ∃k, m ≤ k ≤ n. f k = true in two
ways:
a) Directly following the design of forall.
b) Using forall and boolean negation not : bool → bool.

Exercise 1.17.3 Declare a primality test based on the fourth charac-

√
terization (i.e., upper bound 2 x). Convince yourself with an OCaml
√
interpreter that testing with upper bound 2 x is much faster on large
primes (check 479,001,599 and 87,178,291,199).
9
We use the curly brace as an abbreviation to write two equations as a single equa-
tion.

30
 1 Getting Started

Exercise 1.17.4 Explain why the following functions are primality

tests:
a) λx. x ≥ 2 && first (λk. x % k = 0) 2 = x
b) λx. x ≥ 2 && (first (λk. k 2 ≥ x || x % k = 0) 2)2 > x
Hint for (b): Let k be the number the application of first yields. Distin-
guish three cases: k 2 < x, k 2 = x, and k 2 > x.
Exercise 1.17.5 Convince yourself that the four characterization of
primality given above are equivalent.

1.18 Polymorphic Exception Raising and Equality Testing

Recall the predefined function invalid_arg discussed in Section 1.13.

Like every function in OCaml, invalid_arg must be accommodated with
a type. It turns out that the natural type for invalid_arg is a polymor-
phic type:
invalid_arg : ∀α. string → α
With this type an application of invalid_arg can be typed with whatever
type is required by the context of the application. Since evaluation of
the application raises an exception and doesn’t yield a value, the return
type of the function doesn’t matter for evaluation.
Like functions, operations must be accommodated with types. So
what is the type of the equality test? OCaml follows common math-
ematical practice and admits the equality test for all types. To this
purpose, the operator testing equality is accommodated with a poly-
morphic type10 :
= : ∀α. α → α → bool
The polymorphic type promises more than the equality test delivers.
There is the general problem that a meaningful equality test for functions
cannot be realized computationally. OCaml bypasses the problem by
the crude provision that an equality test on functions raises an invalid
argument exception.
We assume that functions at the mathematical level always return
values and do not raise exceptions. We handle division by zero by assum-
ing that it returns some value, say 0. Similarly, we handle an equality
test for functions by assuming that it always returns true. When reason-
ing at the mathematical level, we will avoid situations where the ad hoc
definitions come into play, following common mathematical practice.
10
In fact, OCaml also equips the less-than test (<) with the same polymorphic type
and lifts this test to compound types such as tuples and constructor types.

31
 1 Getting Started

1.19 Summary

After working through this chapter you should be able to design and code
functions computing powers, integer quotients and remainders, digit
sums, digit reversals, and integer roots. You should understand that
the design of functions happens at a mathematical level using mathe-
matical types and equations. A given design can then be refined into
a program in a given programming language. In this text we are us-
ing OCaml as programming language, assuming that this is the first
programming language you see.11
You also saw a first higher-order function first, which can be used to
obtain integer quotients and integer roots with a general scheme known
as linear search. You will see many more examples of higher-order func-
tions expressing basic computational schemes.
The model of computation we have assumed in this chapter is rewrit-
ing with defining equations. In this model, recursion appears in a natural
way. You will have noticed that recursion is the feature where things get
really interesting. We also have discussed tail recursion, a restricted form
of recursion with nice properties we will study more carefully as we go
on. All recursive functions we have seen in this chapter have equivalent
tail recursive formulations (often using an accumulator argument).
Finally, we have seen tuples, which are compound values combining
several values into a single value.

11
Most readers will have done some programming in some programming language
before starting with this text. Readers of this group often face the difficulty that
they invest too much energy on mapping back the new things they see here to the
form of programming they already understand. Since functional programming is
rather different from other forms of programming, it is essential that you open
yourself to the new ideas presented here. Keep in mind that a good programmer
quickly adapts to new ways of thinking and to new programming languages.

32