Logic and Learning

Rating:
Summary: Good introduction...ALKEMY needs more investigation
Review: This book gives an introduction to computational logic and machine learning in the context of higher-order logic, and also serves as a rudimentary introduction to functional logic programming languages. My interest in it was stirred by its emphasis on comprehensibility in learning, its attempt to discuss inductive logic programming and the construction of inductive decision trees in a higher-order logic context, and to see whether or not I could use the ALKEMY language for practical applications.

In chapter 1, the author takes the position that higher-order logic meets the needs of knowledge representation in that it can represent complex individuals, is able to formulate the hypothesis language precisely, and allows the computation of values of a function in the background theory on an individual. He also justifies the use of types in the book, claiming that such a use will result in a "substantial payoff". The author identifies seven different learning issues that he will study in the book. One of these concerns the representation of individuals. Another concerns the specification of a signature for the target function whose definition is to be induced. The third learning issue deals with the training data, each piece of data giving the value of the target function for a particular individual. The fourth issue deals with the need for a background theory, which is a collection of definitions of the functions that act on the individuals. The fifth issue concerns the hypothesis language, which specifies the functions in the background theory. The need for evaluating the predictive power of the constructed hypothesis is the sixth learning issue.The last issue concerns the requirement of comprehensibility of the hypotheses returned by the learning system. The hypotheses must provide an insight and explanation of the data, rather than merely a "black-box" with possibly high predictive power.

Chapter 2 gives an overview of the syntax and semantics of higher-order logic. The author clarifies in detail what is meant by "defined inductively", and proves a principle of induction on the structure of types. The importance of the collection of parameter-free "closed" types is brought out, and the author gives examples of various types that have been used in logic programming. Type substitutions, terms, subterms, and term substitutions are all defined in great detail, and many examples of each are given. Term substitution can be tricky and does not merely involve the replacing of a free occurrence of a variable by a term. He also shows, in the context of term substitution, that one does not need to do run-time type checking in logic programming. The model and proof theory of this theory of types is developed at the end of the chapter.

In chapter 3, the author how to represent knowledge in logic theories. For machine learning applications, a particular set of terms, called "basic terms" are used to represent individuals. Basic terms are defined in terms of default and normal terms with a suitable equivalance relation put on the normal terms. In higher order logic, sets are represented essentially as characteristic functions, i.e. as predicates. The concept of a default term arises in this method of representation, and is defined inductively in terms of default data constructors. Default terms are then used to define (inductively) "normal terms". A notion of equivalence of normal terms is defined, and a strict total order is put on the normal terms in order to allow one to select a single representative from an equivalence class. The "basic" terms are then defined. The author shows that the normal equivalence relation is the identity on basic terms, and this allows him to define a "basic form". He then shows how to obtain the basic form of a normal term. Several different metrics and kernels are defined on the basic terms.

The author addresses the construction of predicates in chapter 4, this being done incrementally via the composition of transformations. The author then defines a larger class of predicates, called the "standard predicates", along with a subclass, the "regular predicates". The "background theory" is the theory consisting of the definitions of the transformations. After placing a relation of strict total order on the standard predicates, the regular predicates are defined by induction on the number of transformations in a predicate and in terms of this ordering. Every standard predicate is shown to be equivalent to a regular predicate and an algorithm is given for constructing this regular predicate, the resulting regular predicate being called a "regularization" of the standard predicate. Then predicate rewrite systems (PRS), are studied, and related to machine learning as a generation of a search space of standard predicates.To determine when one predicate logically implies the other, the author defines an implication "preorder" on the space of predicates, which then allows the characterization of a PRS as "monotone", and a notion of "regularization" of a PRS.

The goal of the next chapter is to develop a computational formalism by viewing programs as collections of definitions or "equational theories". A computational model for programs is developed which is decidable, and which contains the familiar notions of equality, connectives and quantifiers, etc. The author introduces his notion of "programming with abstractions", which he claims allows the functional programming paradigm to be done in a logic programming style.

The last chapter is an overview of the (publically available) ALKEMY system for (binary) decision-tree learning, The author gives a detailed description of the decision-tree algorithm used by ALKEMY, which has as input a set of examples, a predicate rewrite system, and a parameter. Examples are composed of a basic term and its class, and the algorithm constructs a decision tree by labeling each leaf node of the tree but its majority class, and then performing error-complexity post-pruning on the tree. The author gives several examples of the use of ALKEMY, such as the East-West challenge game, Bongard pattern recognition, the Musk problem, mutagenesis, and a molecule recognition problem from chemistry.