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¹), 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 TELL-formula f ∈ TELL (resp. a ASK-formula 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 string-valued 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 well-founded. 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 string-valued attribute, and a list of formulas in L3. So, these formulas represent trees, whose nodes are labeled by string-valued 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 n-ary 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 property-slot 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 non-atomic 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'_⊑₁ sg'_⊑₂.

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 non-termination of the computation of properties. So, we use a universal top-down fixpoint algorithm [LCVH92]. We adapted it as a higher-order function so that it can be applied locally in each logic functor, without requiring any global data-structure. We systematically apply it in the definition of the function props in non-atomic 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₁ 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 non-logical module containing some functor-specific values like tokens to be used as separators, for instance. These extra-parameters 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/.