Chapter 3 Implementation as ML Functors
Logic functors are not only formally specified, but also implemented
as modules in a programming language so that they can easily be
composed to form various executable logics. In particular logic
functors are very close to parameterized modules [Mac88a],
where modules play the role of logics as a combination of an abstract
syntax and a set of operations over this syntax, and where parameters
play the role of logics as arguments of a logic functor. These
parameterized modules are available in some ML languages, and we use
Objective CAML (OCaml^{1}), where they are
called functors. OCaml is a functional programming language that
offers a rich and safe type system, modules, (module) functors, and
even recursive module definitions.
We first define the module type, or signature, that mimicks our
definition of a logic (Section 3.1). Then we show how
easy it is to compose logic functors directly in the OCaml language,
without having to make a dedicated composer
(Section 3.2). We also explain how the type of
built logics is automatically computed from the type of logic functors
(Section 3.3). Finally we introduce some pratical
aspects of the implementation of logic functors, which were not
relevant at the theoretical level (Section 3.4).
3.1 Types and Signatures
A logic is defined as a structure L = (AS,S,P,T), where AS is the abstract syntax, S is the semantics, P is the set of
operations, and T is the type (Definition 4). All these
elements, except the semantics, are represented in the following
signature.
module type T =
sig
type t
val tell : t > bool
val ask : t > bool
val subs : t > t > bool
val top : unit > t option
val bot : unit > t option
val conj : t > t > t option
val disj : t > t > t list
val le_l : t > t > bool option
val le_u : t > t > bool option
val props : unit > props
end
T
is the name of the signature, or module type. It is composed
of a type t
, and a set of values (keyword val
). The
type t
stands for the abstract syntax AS as it
specifies a set of values, the abstract syntax trees (or internal
representation) of formulas. The values stands for operations P,
except the last one, props
, which stands for the type T of
the logic, i.e., the set of properties satisfied by the logic.
The value props
is a function that returns this set of
properties. It is a function as the type of a built logic must be
computed. This set of properties is represented as being of
type props
, which is defined below.
type requirements = string list
type props = {
st : requirements;
st' : requirements;
sg' : requirements;
cs_subs : requirements;
cp_subs : requirements;
cp'_subs : requirements;
cp_top : requirements;
cs_bot : requirements;
defst_conj : requirements;
cs_conj : requirements;
cp_conj : requirements;
cs_disj : requirements;
cp_disj : requirements;
cs_le_l : requirements;
cp_le_l : requirements;
cs_le_u : requirements;
cp_le_u : requirements;
reduced : requirements;
reduced' : requirements;
reduced_top : requirements;
reduced_bot : requirements;
reduced_right : requirements;
}
A set of properties is represented as a record, where each slot
corresponds to a property, and each value associated to a slot is a list
of requirements for this property to be true. One could think a
boolean would be enough to tell whether a property is satisfied or
not. However it appears in practice that it is very useful to know why
a property is not satisfied. In a built logic the satisfaction of a
property is a function of the satisfaction of some properties in logic
functors. More concretely, a property is satisfied if a set of
properties over some logic functors are all satisfied. So, the value
associated to a property is the subset of these properties that are
not satisfied. If this subset is empty, then the property is
satisfied. Otherwise, this means that at least one required property
is not satisfied. There may be two reasons for this:

either this required property is proved false, and then a new composition of functors has to be imagined in order to satisfy the property in the built logic,
 or there is no theorem about the required property in the type of its logic functor, and one has to be found and proved.
Examples of the building of a logic, and its adaptation to make it
satisfy some properties are given in Section 4.
The value tall
(resp. ask
) is a filter over the abstract
syntax, and enables us to test whether a formula f ∈ AS is a
TELLformula f ∈ TELL (resp. a ASKformula f ∈ ASF).
The values subs
, top
, bot
, conj
,
disj
, le_l
, le_u
stand respectively for
subsumption, tautology, contradiction, conjunction, disjunction, lower
ordering, and upper ordering. Their OCaml type is a direct translation
from Section 2.2, with the following details:

the type constructor
option
is used when the operation can return undef,
 the type constructor
list
is used to represent sets like in disjunction,
 constants like top and bottom are made functions (by adding a
unit
argument) as this is required by OCaml in order to build
recursive modules.
It can be seen that this interface can easily be extended with new
operations, and new properties. A default definition of a logic is
given below. It is useful when defining logic functors where not all
operations are defined, but which still have to match the logic
signature T
.
module Default : T =
struct
let tell f = true
let ask f = true
let subs f g = false
let top () = None
let bot () = None
let conj f g = None
let disj f g = [f; g]
let le_l f g = None
let le_u f g = None
let props () = no_props "Default"
end
The function no_props
F, where F is the name of a logic
functor, returns a record of properties where each slot is in the form
p = ["F.p"], that is no property is satisfied.
Now we have presented the signature of a logic, and its default
implementation, we give a schematic example of the implementation of a
logic functor F as a parameterized module.
module F (L : T) : T =
struct
include Default
type t = ... L.t ...
let subs f g = ... L.subs ... L.top ...
...
let props () = ... L.props ...
end
F
is the name of the functor. It takes one logic with
signature T
as a parameter, and returns another logic also with
signature T
. The returned module implements the type and values
of the signature T
as a function of the type and values of the
argument logic L
. It includes the logic Default
in order
to ensure that the signature is fully implemented, even if not all
operations are explicitly defined.
Many examples of implemented logic functors are available in the LogFun library. The module logic.ml contains types and
signatures, as well as the default logic, and a logic tester. There
are only slight variations with definitions above, such as operation
names, and the use of exceptions instead of options for partially
defined operations. These variations comes only from historical
reasons, and are only a different style of programming.
3.2 Composition of Logic Functors
While implementing a logic functor requires both logic and programming
knowledge, composing them for building customized logics is accessible
to application designers, and does not even require knowledge of the
programming language OCaml as shown in the following.
Let us first assume we have a few logic functors at disposal.
Atom
expects no argument and corresponds to the usual atoms
that are found in many logics. String
represents the concrete
domain of strings, and patterns on strings (e.g., “starts with”,
“contains”). List
is used to represent patterns on lists,
whose elements belong to its argument logic L
(in fact,
List
is a combinator of smaller functors, as can be seen in the
appendices). Finally, Prod
builds the product of 2
logics L1
, and L2
; so, its formulas are all made of a
formula from L1
and a formula from L2
.
module Atom : T = ...
module String : T = ...
module List (L : T) : T = ...
module Prod (L1 : T) (L2 : T) : T = ...
These logic functors can now be composed in a functional way,
according to their respective arity. A logic is then defined as a
OCaml module, given a name and a composition of logic functors.
module L1 : T = List (Prod Atom String)
module L2 : T = Prod (List Atom) (List String)
module rec L3 : T = Prod (Prod Atom String) (List L3)
The logic L1
enables us to represent and reason on lists of
couples, each couple being composed of an atom and a string pattern,
i.e., each couple is a stringvalued attribute. In logic L2
the
order of application of List
and Prod
is reversed so
that now formulas are the combination of a list of atoms, and a list of
string patterns. The logic L3
is an example of a recursively
defined logic, as it is used in its own definition. In such a case one
has to be cautious the recursive definition is wellfounded. This is
the case here as a list can be empty, which allows for finite
formulas, and makes operations terminate. Formulas in L3
are
the combination of a stringvalued attribute, and a list of formulas
in L3
. So, these formulas represent trees, whose nodes are
labeled by stringvalued attributes. It is useful to define such a
tree structure once for all kind of node labels. This is made possible
by defining a new logic functor as a combination of existing logic
functors, which is called a combinator. This combinator can then
be used as any other logic functor. In some way, it is only syntactic
sugar, but it improves abstraction and reusability of logic functors.
module Tree (Label : T) (Rec : T) : T = Prod Label (List Rec)
module rec L3 : T = Tree (Prod Atom String) L3
OCaml functors cannot be defined in a recursive way, so that an
additional argument Rec
is needed in the definition
of Tree
. The representation of trees can be abstracted further
by replacing the logic functor List
by an additional parameter
telling how the children of a node are organized.
module Tree (Children : functor (C : T) > T) (Label : T) (Rec : T) : T =
Prod Label (Children Rec)
From this new combinator, it is straightforward to define binary or
nary trees, simply instantiating the parameter Children
by
PairOrNil
(another combinator) or List
.
module PairOrNil (X : T) : T = Sum (Prod X X) Nil
module BinTree = Tree PairOrNil
module NaryTree = Tree List
3.3 Automatic Type Checking of Built Logics
The type checking of built logics, i.e., the computation of its set of
properties, is simply done by evaluating the function props
defined in the signature of logics. This function is coded in each
functor F as a translation of its theorems T_{F}, according to the
type props
.
In the case of an atomic functor F, the set of properties is simply
defined as a record where each propertyslot is given a value among
isok
(empty list of requirements), and requires F p
(list of one requirement "F.p", the property p is required on the
functor F). We give below the example of the functor Atom,
where the expression no_props "Atom"
returns a default set of
properties which are all required. Then only satisfied properties need
to be explicitely stated.
let props () =
{no_props "Atom" with
st' = isok;
sg' = isok;
cs_entails = isok;
cp_entails = isok;
cp'_entails = isok;
cp_top = isok;
cs_bot = isok;
defst_conj = isok;
cs_conj = isok;
cp_conj = isok;
cs_disj = isok;
cp_disj = isok;
reduced_right = isok;
}
In the case of a nonatomic functor, the set of properties is usually
defined as a function of the properties of its logic arguments. Let us
consider the example of the logic functor Sum, and one of its theorems:
sg'_{⊑}⇐ sg'_{⊑1} sg'_{⊑2}.
With the utilitary function reqand
that encodes the union of sets of requirements,
this theorem can be directly translated to
sg'_subs = reqand [a1.sg'_subs; a2.sg'_subs]
.
Now a problem comes from the fact that logics can be defined in a
recursive way. If no care is taken, this will result in an infinite
loop, and then nontermination of the computation of properties. So,
we use a universal topdown fixpoint algorithm [LCVH92]. We
adapted it as a higherorder function so that it can be applied
locally in each logic functor, without requiring any global
datastructure. We systematically apply it in the definition of the
function props
in nonatomic functors.
let fixpoint : (unit > props) > (unit > props) =
fun p >
let rec f : unit > props =
let l = ref all_props in
let is_ancestor = ref false in
let was_visited = ref false in
fun () >
if !is_ancestor (* loop detection *)
then begin (* stop recursion *)
was_visited := true;
!l end
else begin
was_visited := false;
is_ancestor := true;
let l' = p () in (* evaluation of properties *)
is_ancestor := false;
if not !was_visited or l' = !l (* stable value for props *)
then !l
else begin
l := l';
f () end (* recursive call *)
end in
f
The definition for the functor Sum can now be given in
details.
let props =
fixpoint
(fun () >
let l1 = L1.props () in
let l2 = L2.props () in
{no_props "Sum" with
st' = reqand [l1.st'; l2.st'];
sg' = reqand [l1.sg'; l2.sg'];
cs_subs = reqand [l1.cs_subs; l1.cs_bot;
l2.cs_subs; l2.cs_bot];
cp_subs = reqand [l1.cp_subs; l1.reduced_bot;
l2.cp_subs; l2.reduced_bot];
cp'_subs = reqand [l1.st'; l1.cp'_subs;
l2.st'; l2.cp'_subs];
cp_top = isok;
cs_bot = isok;
cs_conj = reqand [l1.cs_conj; l2.cs_conj];
cp_conj = reqand [l1.cp_conj; l2.cp_conj];
cs_disj = reqand [l1.cs_disj; l2.cs_disj];
cp_disj = reqand [l1.cp_disj; l2.cp_disj];
reduced = reqand [l1.reduced; l2.reduced];
reduced_top = reqand [l1.reduced_top; l2.reduced_top];
reduced_bot = reqand [l1.reduced_bot; l2.reduced_bot];
reduced_right = reqand [l1.reduced_right; l2.reduced_right];
})
3.4 Practical Aspects of Logic Functors
We must add to the above operations of an implementation, a parser and
a printer for handling the concrete syntax of formulas. Indeed, an
application should input and output formulas in a readable format.
For parsing formulas we use the stream parsers available in OCaml.
They are limited to LL_{1} grammars but can easily be modularized inside
logic functors.
It is possible to customize the concrete syntax by
passing to functors an additional parameter Param
. It is a
small nonlogical module containing some functorspecific values like
tokens to be used as separators, for instance. These extraparameters
can also be used to offer several versions of a logic functor in only
one module.
It is also possible to add other operations to logics. For instance,
we already defined operations like a refinement operator for machine
learning [FK05], or a feature extractor for navigation in
logical information systems [FR04].
 1
 See http://caml.inria.fr/.