A functional perspective on machine learning via
programmable induction and abduction
Steven Cheung1 , Victor Darvariu1 , Dan R. Ghica1 , Koko Muroya1,3 , andReuben N. S. Rowe2
1

University of Birmingham
2
University of Kent
3
RIMS, Kyoto University

Abstract. We present a programming language for machine learning
based on the concepts of ‘induction’ and ‘abduction’ as encountered in
Peirce’s logic of science. We consider the desirable features such a language must have, and we identify the ‘abductive decoupling’ of parameters as a key general enabler of these features. Both an idealised abductive calculus and its implementation as a PPX extension of OCaml arepresented, along with several simple examples.

1

A principled functional language for machine learning

What is the right programming language for machine learning? This question
can be answered in two ways. A first possible answer could take an algorithmic
point of view and try to identify those constructs which are most used in machinelearning programs, delivering an implementation in which the balance of various
optimisation trade-offs favours such constructs. This way of answering the question has been studied quite extensively (e.g. [1, 2]). A different methodologicalapproach to this question is to first put machine learning in a logical perspective,
to provide a guideline in the development of a programming language. Connecting deductive systems to computation is a preferred methodology of functional
programming language design [3]. This is the methodology we follow in thispaper, except we will consider inference systems beyond deduction.
The first step is, therefore, to place machine learning in a logical framework.
This is a delicate, somewhat philosophical, undertaking which may be imperfector incomplete in its representation of the extremely broad spectrum of machinelearning algorithms. However, this step must be made in order to enable themethodological machinery to crank on. We will situate our logical understanding of machine learning within C.S. Peirce’s view of deduction, induction, andabduction as the key reasoning processes in the logic of science. This view, espoused in his celebrated paper Illustrations of the Logic of Science is perhaps
not the only way in which the logic of machine learning, seen as a computational
subsidiary to the logic of science, can be understood. In fact Peirce himself revised both his position on the role of induction and abduction, and even theterminology itself. But the clarity and elegance of his Illustrations, formal andconceptual, makes it a compelling organising principle.

The second step is to suggest an informal realisability-style correspondence
between the logical and the computational, resulting in a programming language
for machine learning in which typical algorithms can be expressed concisely andelegantly4 . This is indeed a common situation when developing functional programming paradigms. The methodological principles invoked above are incorporated into a calculus, which is then implemented as an extension of the OCaml
programming language.
Contributions: We give a methodological justification for abductive inference asa logical framework for machine learning. Following an informal realisability argument for abduction we define a functional programming language for machinelearning, which we implement as a PPX extension of OCaml. The language
relies on a formal calculus of abduction which is studied elsewhere [4].

2Deduction, induction, abduction
The division of all inference into Abduction, Deduction, and Induction
may almost be said to be the Key of Logic.
C.S. Peirce

We faithfully follow Peirce’s logical analysis of scientific methodology as given
in his Illustrations of the Logic of Science. Several clarifications of terminology
first. The first one is that the term ‘logic’ must not be confused with ‘deductive
logic’. We are employing it in its broader sense, that of any system of formal
rules employed in carrying out scientific enquiry. Similarly, the term ‘induction’must not be confused with ‘mathematical’ or other kinds of deductive induction,
but with the Humean principle of ‘generalising from examples’ [5]. Finally, theterm ‘abduction’ is not used in loc. cit., but the original term ‘hypothesis’ wassubsequently replaced by the former, which became more popular.
Logical inference rules fall into two broad categories. Some rules, when correctly applied, result in conclusions which are at least as believable as the assumptions. They are ‘apodeictic’, i.e. beyond debate. These are the ‘deductive’rules, the application of general principles to specific cases. Systems of deductive
rules relate elegantly to functional programming via correspondences such as
Kleene’s proofs-as-programs (realisability) [6] or the propositions-as-types correspondence introduced by Curry and Howard [7]. Computation carried out insuch deductive functional programming languages produces definitive results.
However, these ‘analytic’ rules, and the computation inspired by them, play norole in the creation of new knowledge.
In contrast, machine learning is a style of computation characterised by the
opposite features. It is tentative, in that it produces possibly imprecise or inaccurate results. Yet it is ‘ampliative’ (or ‘synthetic’) in that it generates new
knowledge. The tentative nature of the results is a necessary consequence of
4

The Curry-Howard correspondence emphasises types, whereas realisability emphasises proofs. Because we discuss new proof rules, rather than new types, we will
prefer the realisability approach.

knowledge generation, which involves heuristics such as generalisation or guessing. The fallibility of machine learning may be unsettling, but it is an allowance
we must make for the sake of creativity. The same uncertainty also characterise
the synthetic logical rules of scientific discovery, induction and abduction. By formalising them we simply endow existing scientific practice with a computational
dimension.
Peirce’s presentation of logical concepts is syllogistic. Deduction is the application of a Rule (‘All men are mortal.’) to a Case (‘Socrates is a man.’) in orderto produce a Result (‘Socrates is mortal.’). In contrast, (scientific) induction is
the synthesis of a Rule (‘If the ball is struck, it moves.’) out of a Case (‘The ball
was struck.’) and a Result (‘The ball moved.’). Formalised, this rule is deducA∧B. In scientific practice the rule is slightly different.
tively uninteresting,A⊃B
A ∧ B ··· A ∧ B
Induction either generalises from a number of samples
A⊃B
A∧B
A⊃B
or reinforces an existing rule in light of new evidence
. The
A⊃B
strength of the evidence can be modelled more precisely either by augmenting
the logic with modalities, or quantitatively, by (frequentist) statistical inferenceor Bayesian belief revision. These lines of inquiry are investigated by a significant
literature [8].
Abduction is the third and final arrangement of Rule, Case and Result ina distinct inference rule: given a Rule and a Result we infer the Case. The
B
A⊃B. Peirce acknowlformalisation is the (deductively unsound)A
edged abduction as the rule leading to the most uncertain, the most speculative,knowledge, but also as the rule with the potential to lead to the creation of themost interesting new knowledge. In the practice of scientific discovery, abductionis the process by which we try to answer the question ‘Why?’. This rule may
seem extravagantly unsound yet it plays a crucial role in Peirce’s philosophicalunderstanding of the logic of scientific discovery.5
More succinctly, the roles of induction and abduction can be explained asfollows. Induction is a way to mechanically create models of the world from data
about the world, whereas abduction is an examination of given models in orderto understand why they work.

5

Abduction is essential in making statements about reality when we only have access to sense-data such as measurements. For example, the Result might be ‘The
thermometer reads 10◦ ’ with the Rule ‘If the temperature is 10◦ then the thermometer reads 10◦ ’. From these we can abduce the Case, that ‘The temperature is 10◦ ’.
Note that this can never be apodeictic because, for example, the thermometer may
be broken. Denying abductive reasoning and demanding the certainty of deduction
leads to universal scepticism, e.g. Descartes’s ‘evil demon’ which may subvert ourexperience of the world.

2.1

Proofs-as-programs for induction

A ∧ B ··· A ∧ B
The induction rule
has a natural computational interA⊃B
pretation as the coercion of a list of pairs of type A × B into a function A → B,
realisable by a collection of constants interpA,B : (A × B) list → A → B. It isreasonable to expect the function to be both conservative, agreeing with thearguments when specified, and ampliative, supplying new and sensible values oftype B when an unknown argument of type A is provided. This is interpolation.
Interpolation can only be computed for certain data types. In the mostgeneral case, if the type A is an order, i.e. it is equipped with a comparison
function, then the simplest and most general interpolation method is piecewise
constant interpolation. The resulting function f is constant on each intervalan ≤ a < an+1 with an , an+1 ∈ A consecutive known points, i.e. f (a) = bn foran ≤ a < an+1 . If A is an ordered field then the piecewise-constant interpolation
can be more sensible, with the segments centred in the known values, so thatfor (an−1 + an )/2 ≤ a < (an + an+1 )/2, f (a) = bn . If A is a multi-dimensional
vector field then the partition of space into regions based on distance to the given
points in which the function value is constant is the Voronoi tessellation [9].
If both A and B are fields then a variety of interpolation methods are available(trading off computational simplicity for precision) from linear interpolation,
which approximates the function as a set of line segments, to polynomial or
spline interpolations, which produce smooth functions. These methods also apply
when A is a vector field (‘multivariate interpolation’) and even if the premises
are countably many, i.e. the list of points is infinite (streams), via WhittakerShannon interpolation [10].
A∧B
A⊃B
is
The alternative presentation of the induction rule,A⊃B
more subtle because its computational interpretation suggests the need to ‘update’ a function A → B to take into account a new pair of points A × B. If
we situate ourselves in the realm of approximation, we note that a function
f : A → B can be always converted into a list of points (A × B) list via sampling,
thus reducing this rule to the previous. Concretely this would involve a familyof constants sampA,B : (A → B) → (A × B) list. A realisability-style interpretation of this rule would be more subtle because when relating lists of points andfunctions, interpolating then sampling at the same inputs produces the original
data points, but interpolating from a set of samples in general does not produce
the original function.
Finally, if we are in an approximate setting, then the computational interpretation of induction can go beyond interpolation. Interpolation is always accurate
at the interpolation points, but functions can be synthesised in ways which reduce rather than avoid error at the sampling points, such as regression [11].
Regression is a more robust way of synthesising functions because it recognises
the possibility that the sample points may incorporate noise or errors. Interpolation will over-fit the function to the points, a problem avoided by regression. In
the next section we will see that regression plays a key role in the interpretationof abduction.

A basic ‘inductive’ core functional programming language for induction could,
in principle, be designed on the basis of an applied lambda calculus with lists
and special sampA,B and interpA,B constants.
2.2

Proofs-as-programs for abduction

Induction, computationally, may be interpreted as the synthesis of functions outof data using techniques such as interpolation or regression. This is potentially
useful in the context of data science, but it is not quite machine learning. We will
see how abduction fills this role. The interpretation is rather different than in theBA⊃B
we will notcase of the induction, because in the abduction ruleA
think of A and B as data, but rather we will think of A as parameters (P ) andB as a rule (M ⊃ N ). This ‘higher-order’ version of abduction is particularly
M ⊃NP ⊃ (M ⊃ N )interesting for us:.
P
The computational interpretation is as follows. Given a parametrised function
f : P → (M → N ) and a non-parametric function g : M → N we want tofind the values of parameter p : P which makes functions f p : M → N andg : M → N be ‘as similar as possible’. One can think of g as an external
phenomenon, an experiment, or an oracle, and f as a model. By abduction weneed to find the best parameter values for the model so that the model instancef p best explains g. The process of ‘abducing the best parameters’ of a genericmodel is a general instance of a machine learning situation.
Concretely, a programming language would require a family of constants
abdP,A : A → (P → A) → P , where A is (usually) a function type. The informal semantics of abd m f is the calculation of a parameter p : P so that adefined measure of distance between f p and the reference external function m
is minimised. This is a generic optimisation problem which can be approachedin different ways depending on the types involved.
If P , the type of the parameters, is a discrete data type then combinatorial optimisation algorithms can be used to compute p. The literature on the
topic is substantial [12]. If P is a vector space then numerical approximations
such as gradient descent can be used. There is an even broader literature inthis area [13] going back to Cauchy’s pioneering work on numeric solutions tosystems of equations. Note that if the model P → A is a smooth (differentiable)
function and if the programming language has reflection [14] then gradient descent can be made very efficient by computing the differential of the function
automatically [15], otherwise it can be computed numerically [16].
An abductive programming language, i.e. a simply-typed lambda calculus
extended with a family of abduction primitives (abdP,A ), would offer the advantage of highly simplifying machine-learning programming by hiding the searchor optimisation mechanisms from the programmer. For example, considering an
oracle with signature r : float → float, a linear-regression model lc of r would beconstructed as follows (in a generic functional syntax):l (p1 , p2 ) x = p1 × x + p2

(p01 , p02 ) = abdfloat×float,float→float r l
lc = l(p01 , p02 )The resulting function lc is the concrete model, obtained from the abstract modell instantiated with abduced parameters (p01 , p02 ).
From the point of view of this computational interpretation we can see
how induction and abduction are subtly different. Both involve the synthesisof new functions, but the mechanisms are distinct. Whereas induction synthesises a function out of data using a fixed, built-in, transparent mechanism,abduction provides the means of adjusting the parameters of a programmersupplied function to best-fit an oracle. Induction and abduction can interact
to create a reference model out of sampled data rather than using the external process directly, which would be inconvenient. The combined inductionabduction function, using a collection of data points d : (A × B) list is defined asindabd d f = abdP,A→B (interpA,B d) f.
There is a similarity between this style of programming and TensorFlow [17],a successful machine-learning library, with some differences. Our ‘abduction’corresponds to ‘training’, but we impose no syntactic distinctions between afunction used as an argument to abduction or as applied to an argument. In
TensorFlow the programmer needs to explicitly create ‘sessions’ in which amodel (‘computation graph’) can be either trained or evaluated, separately. Such
distinctions are generally unpleasantly low-level.

3

Programming with induction-abduction

The considerations above highlight a programming idiom which from a realisability perspective relates induction and abduction with certain useful programming constructs. We are reassured by the resemblance of the inductive-abductive
style of programming with established frameworks such as TensorFlow. We
are proposing in fact an idealised version of such frameworks. The question we
ask is how can a conventional functional programming language be improved or
extended with inductive-abductive constructs.
Induction does not present a challenge. The interp family of constants are
simply extrinsic functions of the requisite signature. Abduction is also introduced in the same way, but programming with it turns out to be inconvenient.
The real programming language design challenge is wrestling with the bureaucratic burden of parameter management. In this section we will describe at somelength our rationale for language design, with the actual language to follow. We
iterate through key problems and informally present partial solutions, in order tohighlight the challenge faced. The definitive solution, which addresses all these
problems will be presented in the next section.
The key requirement, which will drive most of the language design, is thefact that abduction must rely on a fixed and generic optimisation algorithm. A
model P → A → B must accommodate a generic optimisation algorithm overthe space P of parameters and a norm for type B. For numeric optimisations

such as gradient descent, the space P of parameters is commonly a vector space.
The linear regression example becomes:l : vec → float → floatl v x = v[0] × x + v[1]v 0 = indabd r l
lc = l v 0
Implicit parameters Parametrising models by vectors makes for ugly syntax.
Moreover, composite models must be constructed using operations which aremanually lifted to manage parameters. Consider a model for confidence bounds
which involves two linear functions (a simple weighted regression [18]):
bound v x = (l v [0 : 1 ] x , l v [2 : 3 ] x )v 0 = indabd r boundboundc = bound v 0
where v[m : n] means taking a slice of the vector v from m to n and r some suitable reference data. The model has four parameters, which must be distributed
to the two linear bounds. However, there is a problem with this approach. Explicit decomposition of the parameter vector worsens the syntactic overhead.
More seriously, mistakes in the slicing of the vector can lead to runtime errors
which, since they involve sizes, cannot be prevented by a simple type system.
Instead, we would prefer this:bound x = (l x , l x )v 0 = indabd r boundboundc = bound {v 0 }The vector-parameter is an implicit parameter. When a concrete model is produced from the instantiation of the abstract model with the abducted parameters, they are explicitly provided. However, managing the implicit parameter inthe lifted term formers is more complex than in languages which support suchfeature syntactically [19].
In terms of implementation, it may seem possible to handle parameters in amonadic style, but we shall see soon why this solution would not be satisfactorywhen other, more subtle, requirements are taken into account.
Linear parameters Let us now turn to an issue that drives the ultimate designof the language, illustrated by our running examples:bound1 x = (λh.(h x , h x + 1 )) lbound2 x = (l x , l x + 1 )What is the dimension of the parameter vector for bound 1 and bound 2 ? In thecase of the former, it is quite obvious that the vector has two components. In
the latter, it depends on whether the programmer intended the two occurrencesof the function l to be abducted separately or together. We think there is acase for the parameters to be abducted together, so that both functions have
two parameters, not only in an attempt to conform to a beta law which is often
expected by functional programmers, but also to allow the programmer to keep
control of how many parameters are independently adjustable during abduction.
In this example, abduction will always lead to boundaries delimited by two lines
1 unit apart, i.e. fixed confidence bounds of a linear regression. In contrast, theweighted regression model can be defined with two separate parameter vectors(each of size two), v0 = [1; 0] and v1 = [1; 0]:bound x = (l {v0 } x, l {v1 } x)
In a final streamlining of the syntax, we omit parameter vectors altogether
and we only indicate by {−} that a constant is to be interpreted as a parameter,
leaving the vector of parameters everywhere implicit:
l x = {1} × x + {0}l0 x = {1} × x + {0}bound x = (l x, l0 x).
The linearity of parameter occurrences will be always observed, so that for example terms (λx.x + x){0} and {0} + {0} are distinct, because they have one,respectively two, parameters.
In general, the parameters of a model may be contributed by both arguments
and free variables, which means that parameters must be discovered not only inthe body of the function and its arguments, but also in closures. Linearity andthe need for ‘deep’ search of parameters indicates a simple syntactic solution to
be unlikely.
In conclusion, we want our running examples to be, ideally, written as:labx = a × x + b
g x = (l {1} {0}) xf x = (l {1} {0}) x
f 0 x = (l {1} {0}) x
bound w x = (f x, f 0 x)
bound l x = (g x, g x + 1)
where bound w is the four-parameter weighted regression model, and bound l
the two-parameter unit confidence interval of a linear regression.

4

The abductive calculus

We have argued that the construction of a parametrised model, which is thesecond input of the abduction abdP,A : A → (P → A) → P , can be tediousor erroneous in the absence of implicit parameter management. We would likeparameters to be implicit in construction of a parametrised model, and to becollected as a unique and opaque type for abduction.
The previous section illustrated the construction of models with implicit
parameters that are represented by specially annotated constants {k}. To enableabductive programming we propose decoupling as a key
 feature. This consists ofa family of constants decVa ,A : A → (Va → A) × Va where Va is an abstract
type indexed by a unique name a (or ‘atom’), as a mechanism to collect implicit
parameters and prepare an explicitly parametrised model.
Informally, dec m computes a pair (l : Va → A, p : Va ) by collecting all implicit parameters in m : A as the vector p and turning the model m (with implicit
parameters) into a parametrised model l : Va → A, a function on parametervectors. The name a is shared by the parameter-vector p and the parametrisedmodel l, making type Va unique for the model. For our leading example, whereπ1 is the first projection,l x = {1} × x + {0}bound x = (l x, l x + 1)
boundp = π1 (dec bound )p 0 = indabd r boundp
boundc = boundp p 0
In this section we give an overview presentation of the abductive calculus, anextension of the simply-typed lambda-calculus for abductive decoupling [4]. Let
A be a set of names (or atoms). Let (F, +, −, ×, /) be a (fixed) field and Va an
A-indexed family of opaque vector types. The types T of the calculus are definedby the grammar T ::= F | Va | T → T where a ∈ A.
0
Terms t are defined by the grammar t ::= x | λxT .t | t t | k | t $ t |0{k} | Aa,T 0 (f, x).t, where T and T are types, f and x are variables, $ ∈ Σbinary primitive operations, k ∈ F field elements, and a ∈ A names. The novel
syntactic elements of the calculus are provisional constants {k}, which serve as
implicit parameters in the above discussion, and a family of type- and nameindexed abductive decoupling functions Aa,T 0 (f, x).t. Decoupling functions are
the implicational form of the decoupling operation dec; they can be syntacticallyrelated by (Aa,T 0 (f, x).t) u ≡ (λ(f, x).t) (decVa ,T 0 u) in the presence of tuples. We
opt for the implicational form to make the scope of names explicit, as we see inthe type system below.
Let A ⊂fin A be a finite set of names, Γ a sequence of typed variables xi :Ti ,and p a sequence of elements of the field F (i.e. a vector over F). We write A ` Γ
if A is the support of Γ . The typing judgements are of shape: A | Γ | p ` t : T ,and typing derivation rules are given below.

A | Γ, x : T 0 | p ` t : T

A ` Γ, T
A | Γ, x : T | − ` x : T

0

A | Γ | p ` λxT .t : T 0 → T

A | Γ | p ` t : T0 → T A | Γ | q ` u : T0
A | Γ | p, q ` t u : TA`Γ k∈F
A|Γ |−`k:F

A | Γ | p ` t1 : T1

A`Γ
A | Γ | p ` {p} : F

A | Γ | q ` t2 : T2 $ : T1 → T2 → T ∈ Σ
A | Γ | p, q ` t1 $ t2 : T

A, a | Γ, f : Va → T 0 , x : Va | p ` t : T

A ` Γ, T 0 , T

0A | Γ | p ` Aa,T 0 (f, x).t : T → T

Note that the rules are linear with respect to the parameters p. In a derivablejudgement A | Γ | p ` t : T , the vector p gives the collection of all provisional constants from t. The decoupling function Aa,T 0 (f, x).t binds name a, so
it requires in its typing a unique vector type Va collecting all the provisional
constants. The typing rule for the function limits the scope of the name a, sothat this vector type Va cannot be used outside of the scope of the function. As
a consequence the vector type Va is unique to the decoupling function. Variables
f and x bound by the function share the type Va but this type cannot be mixed
with parameters produced by other decouplings, as they may result in vectors
with different numbers of elements. This is discussed in Sec. 6.
Employing the straightforward extension by tuples (and lists) and the syntactic sugar let x = u in t ≡ (λx.t) u, our leading example can be written in theabductive calculus as below.
let l = λa.λb.λx.a × x + b inlet f = l {1} {0} in
let bound = λx.(f x, f x + 1) in
let update = A(boundp , ).boundp (indabd r boundp ) in
update boundIts operational semantics is specified using a variation on the Geometry of Interaction [20] which relies on graph rewriting [21]. Using this semantics the calculus
is proved as sound (well-typed programs terminate with a value).
The abstract machine represents a term as a graph along the edges of whicha token travels. The routing of the token is defined by language-specific rules, as
are the rewrite rules. The presence of the token indicates unambiguously what
rule must apply, defining in effect a particular reduction strategy.
The ‘dynamic rewriting’ style of the operational semantics has several advantages which we discuss below.
Sharing of provisional constants in the graph model is naturally represented
by making provisional-constant nodes with several incoming edges. In a term
model the same can only be achieved by introducing auxiliary names, a more
complicated formalism. Moreover, provisional constants cannot be copied or discarded, but only shared at run-time, restrictions which are naturally reflected ina graph model, unlike in a term model.

Decoupling is a complex, dynamic runtime operation which in the graphmodel is surprisingly easy to formulate. Representing code and environment
jointly as a single graph removes the need for complex lookups in the formulationof this rule. This is not as convenient in conventional abstract machines, because
code and environment are separate, hindering the formulation of rules involving
both, especially the collecting and sharing of provisional constants.
In the presence of provisional constants, a program can be interpreted in both
extensional and intensional ways. For example, an extensional interpretation of{1} + {2} is a value 3, while its intensional interpretation is ‘a computation ofsummation, given two provisional constants that are currently 2 and 3.’ The
graph-rewriting abstract machine has an ability to handle both interpretations
at the same time, by separating the flow of computation (the graph) and the
input-output behaviour (the token).
The same ‘two-in-one’ graph representation also enables a direct proof ofprogram equivalence by means of bisimulation, notably by dealing with the congruence property in terms of sub-graphs.

5

DecML, a functional language for machine learning

Terms in the abductive calculus can be evaluated on-line in an experimental
graph-rewriting engine implementing the semantics directly.6 Additionally, wewant to implement a fragment of the abductive calculus as an extension of an
existing real-world functional programming language rather than as a totallynew language. The major challenge of implementing the abductive calculus is to
extract parameters, especially from closures. The semantic definition, which isa global reference-chasing operation similar to garbage collection, is not easily
implementable. It seems to require a deep and undesirable intervention on theruntime of the language. We will therefore pursue an alternative strategy, bybuilding a runtime structure for parameter management which is maintainedby instrumentation of the native code. This will make it possible to actually
maintain the model in a form in which decoupling is a trivial operation.
We implement the abductive calculus as a language extension to OCamlalong with the translation from it to standard OCaml under the PPX framework [22, Sec. 7.23].7 In addition to OCaml terms tOCaml the abductive calculus is extended with new terms t ::= tOCaml | [%pc k] | [%lift t] where, k are(floating-point) constants. If t : A then [%model t] : (dict → A)∗dict. The boundary between ‘pure’ OCaml and the abductive terms is indicated by [%model t],with abductive code inside the marker.
The tag [%model t] ensures the code t is evaluated as a term of the abductive calculus, and presents the result to the ambient OCaml code as a modelwith decoupled parameters. This will require a combination of syntactic transformations and runtime instrumentations. [%pc k] defines a provisional constant,
67

http://bit.ly/abd-vis
https://github.com/DecML/decml-ppx

while lifting [%lift k] allows identifiers from outside of the abductive fragment,
including most OCaml operators, to be used as (trivial) models.
We define a translation d−e for terms t : A of the extended abductive calculus, into terms t0OCaml of ‘lifted’ types (dict → A) ∗ dict of OCaml. The firstprojection is the model, a function parameterised by a dictionary of parameters, which is also given, as the second projection. The translation accumulates
the parameters from its sub-terms by merging their dictionaries, and it ‘lifts’
the syntactic constructs (abstraction, application, etc.) so that they match thelifted types.
The dictionary is a simple data structure that associates each provisional
constant to a unique key. By using dictionaries instead of vectors, merging two
sets of parameters is easy since we no longer need to consider their order inside
the parametrised function. Below are the required dictionary operations in thetarget language: empty denotes an empty dictionary, new key is an operationthat returns a new global key, create dict creates a single element dictionary
from a key and a float, lookup returns the value that is associated with a key ina dictionary and merge combines two compatible dictionaries by joining them.
empty : dict

new key : unit → key

new dict : key → float → dict

lookup : key → dict → float

merge : dict → dict → dict
Variable x stands for any OCaml identifier, including constants, and k for a
float. The translation is indexed by a set V of variables bound in the model:
dxeV = (fst x, snd x)(if x 6∈ V )dxeV = (λ .x, empty)(if x ∈ V )d%lift teV = (λ .t, empty)(where t is a pure OCaml term)

d%pc keV = (λq.lookup L q, new dict L k)(where L = new key ())

d(t1 , t2 )eV = (λq.((F1 q), (F2 u)), merge P1 P2 )(where (Fi , Pi ) = dti eV )dt1 t2 eV = (λq.((F1 q) (F2 u)), merge P1 P2 )(where (Fi , Pi ) = dti eV )dλx.teV = (λq.λx.F q, P )(where (F, P ) = dteV ∪{x} )In the defintion of %lift, by a ‘pure’ OCaml term we mean a term with noabductive syntax or types. In concrete DecML syntax, the leading example is:let (∗), (+), j, z, i = [%lift (∗.)], [%lift (+.)], [%pc 1.0], [%pc 0.0], [%lift 1.0] in
let l = [%model fun x → j ∗ x + z] inlet (bp, p) = [%model fun x → (l x), (l x + i)] in
let p0 = indabd r bp inlet bc = bp p0 in . . .
Induction-abduction indabd is not implemented as a constant, but it can be any
function of the right type, implementing a generic optimisation algorithm such asgradient descent. Parameter p can be supplied to this function as an argument,
if necessary, to seed the optimisation algorithm with an initial point.
This final observation also explains our decision to use the %model annotation to lift only parts of an OCaml program rather than the whole program.
Inside the abductive fragment all operations are lifted to manage parameters,
which makes them less efficient and interferes with compiler optimisation. But
once a model is created in the decoupled form then it can be processed in the
more efficient ambient language. It is particularly important that abduction,
which dominates computationally any machine learning program, can be executed natively and efficiently. The mixing of pure and instrumented code, on
the other hand, can lead to subtle typing problems which could be difficult forthe programmer to understand and fix. The limited access PPX has to typing
information makes it a challenge to give further assistance on this matter, so afuture version of this language may require substantial re-engineering.

6

Related and further work

Our work has been heavily influenced by TensorFlow [17]. We are aiming toprovide an idealised, functional version of this framework. DecML, by using thedecoupling mechanism, avoids the need to represent parameters using imperative
state, while recognising their importance (‘variables’ in TensorFlow terminology) as a distinct language entity. We also recognise the dual-use of models, indirect and training mode, but we prefer to not make this semantic distinction
syntactic. As a shallow embedding of a DSL into Python, TensorFlow must
sometimes use rather heavy-going constructs such as that of a ‘session’, which
we can afford to completely elide. Moreover, by presenting a language extension rather than an embedded DSL we avoid a host of well-known problems andpitfalls [23–25].
For reasons of space and presentational focus we have also glossed overanother significant distinction between inductive-abductive programming andTensorFlow. In the former, abduction is given as a fixed, language-specific,
construct whereas in the latter the abduction (search and optimisation) algorithm is programmable. Of course, fixing the abduction algorithm and assumingthat certain types come with fixed norms is impractical. Prolog is an example
of an abductive programming language in which abduction is implemented asa fixed resolution algorithm, which significantly narrows the applicability of thelanguage to practical problems.
However, if the programming language we are extending is rich enough (suchas OCaml), then the induction-abduction extrinsics can be simply programmed
as normal library functions. The same applies to programming the norm functions explicitly. In fact a fixed abduction construct is not actually defined in theabductive calculus [4], nor is it in DecML! We will briefly discuss some further
language design considerations for programmable abduction, which are alreadyincluded in the abductive calculus but not yet implemented in DecML.

The key requirement is that parameters are collected as an opaque vector
type, the key data type required by the formalisation of generic numeric optimisation problems. Since parameter collection and slicing mechanisms are complex,
the dimension of abducted parameter vectors and even the order of coordinates
are impossible to anticipate at compile-time. Abstracting away these details istherefore required, and any vector needs to be uniquely associated with the model
which it parametrises. Making abduction programmable also explains why we
prefer to extract, rather than discard, the current values of the parameters. They
are often used by programmers to seed the search and optimisation algorithms,
using domain-specific knowledge.
In order to prevent erroneous uses, unique and opaque vector types must be
generated for each model so that vectors produced by abduction can only be
used with the original model. The opaqueness prevents access to the representation, i.e. to the bases or the individual coordinates. Only operators which aresymmetric under permutations of bases will be allowed. Mathematically, theycorrespond to symmetric tensors, but formulated in a programmer-friendly way.
This is a real, but not onerous, restriction on the way the generic optimisation
algorithms are used. Indeed, if generic optimisation algorithms are to be used
at all it is difficult to imagine how (or why) we may want to program them sothat different axes are treated differently in the search space. As an extra bonus,
linear vector operations are efficiently programmable and easily parallelisable on
specialised architectures such as GPUs.
Our proposal focusses on the correspondence between inductive-abductive
inference rules and programming constructs in order to extract methodologicalprinciples for the design of a machine-learning-oriented programming language.
However, these correspondences are only pursued informally. A rigorous realizability definition for induction and abduction is likely to be an interesting andinstructive mathematical exercise. We plan to pursue it in the future.
Besides realisability, Curry-Howard-style correspondences can also be pursued by refining the type system to distinguish between the various modalities
arising out of inductive and abductive reasoning. The distinction between definite and tentative (or approximate) values can be handled by epistemic logics
which distinguish between ‘known’ and ‘believed’ statements. This can lead totypes for inductive-abductive programming which can track the epistemic statusof results of computations. More subtly, the analytic vs. synthetic distinction canalso be modelled by type systems [26] which can prove useful in the context ofmachine learning. This remains a longer-term project.

References
1. Chu, C.T., Kim, S.K., Lin, Y.A., Yu, Y., Bradski, G., Olukotun, K., Ng, A.Y.:
Map-reduce for machine learning on multicore. In: Advances in neural information
processing systems. (2007) 281–288
2. King, D.E.: Dlib-ml: A machine learning toolkit. Journal of Machine Learning
Research 10(Jul) (2009) 1755–1758

3. Huet, G.: Deduction and computation. In: Fundamentals of Artificial Intelligence.
Springer (1986) 38–74
4. Muroya, K., Cheung, S., Ghica, D.R.: Abductive functional programming, a semantic approach. CoRR abs/1710.03984 (2017) (Submitted for publication).
5. Howson, C.: Hume’s problem: Induction and the justification of belief. Clarendon
Press (2000)
6. Kleene, S.C.: On the interpretation of intuitionistic number theory. The Journalof Symbolic Logic 10(4) (1945) 109–124
7. Howard, W.A.: The formulae-as-types notion of construction. To HB Curry: essays
on combinatory logic, lambda calculus and formalism 44 (1980) 479–490
8. Sheridan, F.: A survey of techniques for inference under uncertainty. Artificial
Intelligence Review 5(1-2) (1991) 89–119
9. Aurenhammer, F.: Voronoi diagramsa survey of a fundamental geometric data
structure. ACM Computing Surveys (CSUR) 23(3) (1991) 345–405
10. Marks, R.: Introduction to Shannon sampling and interpolation theory. Springer
Science and Business Media (2012)
11. Vaughn, B.K.: Data analysis using regression and multilevel/hierarchical models.
Journal of Educational Measurement 45(1) (2008) 94–97
12. Ehrgott, M., Gandibleux, X.: A survey and annotated bibliography of multiobjective combinatorial optimization. OR-Spektrum 22(4) (2000) 425–460
13. Snyman, J.: Practical mathematical optimization: an introduction to basic optimization theory and classical and new gradient-based algorithms. Volume 97.
Springer Science and Business Media (2005)
14. Smith, B.C.: Reflection and semantics in Lisp. In: POPL, ACM (1984) 23–35
15. Rall, L.B.: Automatic differentiation: Techniques and applications. Springer (1981)
16. Lyness, J.N., Moler, C.B.: Numerical differentiation of analytic functions. SIAM
Journal on Numerical Analysis 4(2) (1967) 202–210
17. Abadi, M., Agarwal, A., Barham, P., Brevdo, E., Chen, Z., Citro, C., Corrado, G.S.,
Davis, A., Dean, J., Devin, M., et al.: Tensorflow: Large-scale machine learning onheterogeneous distributed systems. arXiv preprint arXiv:1603.04467 (2016)
18. Cleveland, W.S.: Robust locally weighted regression and smoothing scatterplots.
Journal of the American statistical association 74(368) (1979) 829–836
19. Lewis, J.R., Launchbury, J., Meijer, E., Shields, M.B.: Implicit parameters: Dynamic scoping with static types. In: POPL. (2000) 108–118
20. Girard, J.Y.: Geometry of interaction 1: Interpretation of System F. Studies in
Logic and the Foundations of Mathematics 127 (1989) 221–260
21. Muroya, K., Ghica, D.R.: The dynamic Geometry of Interaction machine: A callby-need graph rewriter. In: Computer Science Logic. (2017) 32:1–32:15
22. Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, D., Vouillon, J.: The OCaml
system release 4.02 (2013)
23. Svenningsson, J., Axelsson, E.: Combining deep and shallow embedding for EDSL.
In: Trends in Functional Programming. (2012) 21–36
24. Scherr, M., Chiba, S.: Implicit staging of EDSL expressions: A bridge between
shallow and deep embedding. In: ECOOP, Uppsala, Sweden. (2014) 385–410
25. Gibbons, J., Wu, N.: Folding domain-specific languages: deep and shallow embeddings (functional pearl). In: ICFP, Gothenburg, Sweden. (2014) 339–347
26. Martin-Löf, P. In: Analytic and Synthetic Judgements in Type Theory. Springer
Netherlands, Dordrecht (1994) 87–99