Towards Abductive Functional Programming
Koko Muroya, University of Birmingham

2Abstract

Abductive computation

Abduction is expressed in programs as a function, written as abd f @x -> u, which takes one argument and uses
it as two bound computations in a body expression u: aparameter collection bound to the variable x and a parameterised term bound to the variable f . When applied tosome argument t, the abduction abd f @x -> u extracts all
the provisional constants from it, turns them into definitive constants, and put them into the parameter collection x. Additionally it “lifts” the abducted term t into aparameterised term f , a function that will plug new arguments back at the sites where provisional constants used
to be in the abducted term t. For example, abduction ofa term 1 + {0} produces a parameter collection 0 and aparameterised term fun x -> 1 + x.
The intended use of abduction is to recompute newvalues of provisional constants, and to plug them backas definitive ones into the original abducted term.
1 Abduction in programming
This is done simply by function application, thanks
to the parameterising of the abducted term, like this:In logic, abduction infers a possible cause A of a given ob- abd f @x -> f (t f x) where the term t computes newservation B, knowing an implication A ⇒ B. Informally values using the parameterised term f and the parameter
speaking, this is opposite to deduction, which infers a collection x.
result B from a cause A—deduction goes along an impliA trivial but useful example of abduction iscation A ⇒ B whereas abduction goes against it. Much abd f @x -> f x, which “deprecates” a given term, i.e.
like induction, used carelessly abduction represents a fal- transforms all its provisional constants into definitive
lacy, namely that of affirming the consequent. But with ones. For example, a term (abd f @x -> f x) (1 + {0}) is
adequate restrictions in place we can show that abduction evaluated to a definitive term 1+0, and further to a result
can be both sound and useful.
value 1. Abduction also works on functions, for example a
Abductive logic programming (see [3, 2] for surveys) term (abd f @x -> f x) (fun w -> w + {0}) is deprecatedextends logic programming by allowing a logic program and evaluated to a function value fun w -> w + 0.
to contain undefined “abducible” predicates, with applications to artificial intelligence. These predicates are canTypes of collections
didates of possible causes of particular observations in the 3
behaviour of a program. Inference in abductive logic programming tells us which abducible predicates of a pro- We have seen so far example terms that contain just one
gram should hold to meet given constraints on the pro- provisional constant. If a term t has more than one program. Abductive reasoning has been used in the verifica- visional constants, abduction of it produces a parametertion of separation logic programs, allowing the improve- collection x that is literally a collection of several definiment of automatic shape analysis [1]. Facebook’s auto- tive constants. Given the collection x, the parameterised
term f made out of the abducted one t has to plug themmatic verification tool Infer1 is based on this technique.
back into the original t, in such a safe way that the appliWe here propose a new use of abduction in functional
cation f x yields exactly the deprecation of the abducted
programming, aiming at programs that modify specified
term t. For example a term (abd f @x -> f x) ({1} − {2})constants of another program. Programs can contain norshould be evaluated to 1 − 2, not to 2 − 1, which means
mal definitive ground-type constants p, as well as provithe parameter collection x has to be ordered. The size
sional ground-type constants {p} marked by curly brackof the collection also matters. If the parameter colets. It is these provisional constants that could be changed
lection is implemented as a list, one can write a termby abduction. The process of abduction itself detects all(abd f @x -> f (1 :: x)) ({1} + {2}) that tries to plug theprovisional constants in a term; it yanks them out of theextended collection 1 :: x back to the abducted term.
abducted term, and turns the abducted term into a funcTo ensure the safe restoration of a term after abduction,tion that takes a collection of parameters as an argument.
we use the type of a (fixed) field F as the ground type ofvalue, and use “vector types” Va over the ground type F.
1 http://fbinfer.com/Vectors Va are thus indexed by name a, in the sense of [5].
Abductive reasoning is a form of logical inference whichseeks to uncover all possible causes of an observation. We
show how abduction has a computational counterpart,like many other proof-theoretic concepts: namely theidentification and modification of certain constants in aterm. Abductive computation can be used to improve thebehaviour of a term in some programmer-defined sense,
like a typical workflow of optimisation problems including some machine-learning tasks. The emphasis of thisprogress report is a type system for abductive computation. It is intended to guarantee observably deterministic
behaviour of programs, even though abduction may introduce a degree of computational nondeterminism.

1

They are a type of finite-dimensional vector spaces Fnover the field F with the standard basis. Typing judgements are indexed by sets of names, in addition to theusual sets of typed variables. The rules of the system arethose of the simply-typed lambda calculus, plus a newrule for abduction:

implies t f (2, 1) = (4, 3), for example. Usual operations of a vector space should be available, that is, vector additions +a : Va → Va → Va and scalar multiplications ×a : F → Va → Va for any name a. We can additionally equip each vector type Va with inner products·a : Va → Va → F.
0What is desired but challenging is access to each co∆, a | Γ, f : Va → T , x : Va ` u : Tordinateof a collection, which naturally occurs in some∆ | Γ ` abd f @x -> u : T → T 0
optimisation algorithms. An example is numerical gradiwhere ∆ is a set of names and Γ is a set of typed variables ent descent for optimising the behaviour of a term relativexi : Ti . We require the name a in the rule to be fresh, in to identified parameters:
particular not to appear in ∆, T or T 0 .
abd f @x ->In the rule, the two bound variables f and x share thelet g = fun v -> fun e ->same vector type Va . This ensures the parameterised termf is always given a collection that has the same number(1)(f v) − (f (v + ( × e)))× e + v inof elements as the parameter collection x. The numberof parameters, i.e. the dimension of the vector space Va ,let y = foldr g x Ea in f y
is determined dynamically at runtime. For example, ina term let y = {2} in (abd f @x -> f x) ({1} + y), the where  is a constant. It updates each element of theabducted term {1}+y depends directly on the provisional parameter collection x by folding over the list of standard
constant {1} and indirectly on {2} as well. It is only basis Ea = [~e0 ; · · · ; ~en−1 ].
at runtime when the actual abducted term {1} + {2} isAlthough the computation foldl g x Ea in (1) is symdetermined.
metric, i.e. invariant under permutation of x or Ea , it
The (ordered) standard basis of the vector type Va en- turns out that the arbitrary folding over Ea is not symables the parameterised term f to know which element metric (a counterexample is the replacement of g toof a given collection fits to which place of the origi- fun v -> fun e -> (v · e) × v). This motivates us to acnal abducted term. Note that this does not immedi- commodate the following iterated vector operations, inately mean a canonical order in which parameters are dexed by the name a:assigned; any order will do, as long as both the parame+L
ter collection x and the parameterised term f respect it.
a : (Va → Va ) → Va → Va
RFor example a term (abd f @x -> f x) ({1} − {2}) can+a : Va → (Va → Va ) → Vabe evaluated to either (fun (p0 , p1 ) -> p0 − p1 ) (1, 2) or×La : (Va → F ) → Va → Va(fun (p0 , p1 ) -> p1 − p0 ) (2, 1), informally.
The last remark is regarding the freshness requirement which are three restricted versions of folding over the stanof name a in the typing rule. It ensures that two param- dard basis E .
aeter collections x and x0 generated by different abductive000
functions abd f @x -> u and abd f @x -> u always live inf +La v0 := foldr (λeλv.f (e) + v) Ea v0
different vector spaces and they are never mixed together.
Rf +a v0 := foldl (λvλe.v + f (e)) v0 Ea
This is crucial because these collections may not have thef ×Lsame number of elements, or even if they have the samea v0 := foldr (λeλv.f (e) × v) Ea v0 .
dimension they may be use a different assignment of paOur limited access to the standard basis via the iterated
rameters to coordinates.
operations still enables us to implement some optimisation algorithms, e.g. generic combinatorial optimisations
such as simulated annealing. The code (1) for numeri4 Operations on collections
cal gradient descent is indeed covered by the first iterated
As there is no canonical order in which parameters operation +L .
are assigned to bases/coordinates, implementation of
the language can opt for either a fixed order or a
non-deterministic order. In both cases the absence Referencesof canonical order leads to further restrictions on how
parameter collections may be used, in other words, [1] Cristiano Calcagno, Dino Distefano, Peter W.
O’Hearn, and Hongseok Yang. Compositional shapewhat operations on these collections can be allowed.
analysis by means of bi-abduction.
J. ACM,
The fixed order would be too intimately tied to the58(6):26:1–26:66, 2011.
concrete syntax of a program, and raise difficulty inidentifying terms (abd f @x -> f x) ({1} − {2}) and [2] Marc Denecker and Antonis C. Kakas.
Abduc(abd f @x -> f x) ((fun y -> y − {2}) {1}), for example.
tion in logic programming. In Computational Logic:
The non-deterministic order would challenge the deterLogic Programming and Beyond, Essays in Honour ofministic result of program execution.
Robert A. Kowalski, Part I, volume 2407 of Lect. Notes
The desired restriction of operations on collections apComp. Sci., pages 402–436. Springer, 2002.
pears to be the symmetricity, i.e. being invariant under
permutation of the standard basis. In our intended form [3] Antonis C. Kakas, Robert A. Kowalski, and Francescaof abduction abd f @x -> f (t f x), the symmetricity apToni. Abductive logic programming. J. Log. Comput.,plies to the term t f , meaning that t f (1, 2) = (3, 4)
2(6):719–770, 1992.
2

[4] Koko Muroya and Dan R. Ghica. The dynamic Geometry of Interaction machine: a call-by-need graphrewriter. In CSL 2017, 2017. To appear.
[5] Andrew M. Pitts. Nominal sets: names and symmetry
in computer science, volume 57 of Cambridge Tracts in
Theoretical Computer Science. Cambridge UniversityPress, 2013.

A

Operational Semantics

Operational semantics of the language is given by graphrewriting. The use of graphs instead of terms makes it
easier to handle shared intermediate evaluation results,
especially shared provisional constants, that are raisedby multiple occurrences of bound variables. Sharing is
simply represented as connection of subgraphs, while its
syntactic representation would require introducing names
and stores.
Since provisional constants are subject to abduction
and change, they cannot be freely copied or discarded inevaluation; in particular they should be shared instead ofbeing copied. For instance, a term (fun x -> x + x) {0}should not be evaluated to a term {0} + {0}, as the single provisional constant is “split” into two independent
provisional constants.
The graph rewriting semantics is defined as an abstract
machine that graphically evaluates terms in the strict way,i.e. function arguments are always evaluated before they
are passed to a function. The machine is an adaptationof our graph-rewriting abstract machine of call-by-need λcalculus [4], that can deterministically reduce a graphicalrepresentation of a term by passing a token on it. An
on-line visualiser of the graph-rewriting abstract machineis implemented2 .

2 Link to on-line visualiser: http://www.cs.bham.ac.uk/ drg/~
goa/visualiser/index.html

3