Algebraic Signatures and GEP

I've been thinking about what structure describes the expressions evolved by evolutionary algorithms like GP and GEP for a while, and it looks like algebraic signatures fit the requirements very well. Certainly we can describe a grammar and say we are evolving words in the language generated by the grammar, but that isn't really satisfying (to me). In this post I'm going to go over them again (I describe them in a previous post as well) and show that they are a very natural structure to describe the expressions evolved by genetic programs.

So, what is a signature? A signature consists of a set of types (possibly generated by a grammar) as well as a collection of function symbols and relation symbols. The function and relation symbols each have an arity (the number of arguments they take (although for now we are thinking of this as a purely syntactic system)) as well as an ordering, which says which arguments are of what type. If the arity for a function symbol is 0 than it is a constant, which allows us to specify elements of a type (a constant that has a type is an element of that type).

A signature together with a set of axioms gives a theory. This allows us to describe some theory in math (the theory of Groups, the theory of Monoids, the theory of Categories, etc) as a mathematical object. The models of the theory (the mathematical objects that embody the elements and rules of the theory) are the actual groups, monoid, categories, etc.

If a signature has only relation symbol it will give a relational theory, and if it has only functional symbols it will give an algebraic theory, which is what we are concerned with in this post. If the terms generated from the types and the function symbols can have abstractions then the theory is functional (in the terminology used in "Categories for Types").

If we take an algebraic theory with one type than the terms consist of fixed arity functional taking all arguments of one type and returning something of the same type. This fulfill the closure property for GEP (all function involve only one type). If the axioms are also provided we might be able to automate the evaluation of the expressions by reductions given by the axioms. This would mean that using GEP (or more specifically RGEP) would involve specifying the theory that we are interested in, and perhaps an interpretation of the theory in order to map the resulting expression to an object (which we can then determine the fitness of).

More generally, in Genetic Programming we may have multiple types and more complex functions, but it seems like algebraic theories will cover them. I would love if this allowed a more systematic treatment of what goes on with Genetic Programming, as I find that AI can be a little ad hoc at times compared to my other interests in category theory, type theory, and functional programming.

Learning Category Theory, functors

In many area of mathematics, especially those called "The Theory of X" for some X, we first give the motivation for X, then the construction (how an X is specified by giving the necessary objects and the axioms they obey), and then start to define properties of these Xs as well as showing what objects from other parts of math are an example of an X, then we show the mappings between Xs (the collection of such mappings may itself be an X), and then the notion of a subX (the collection of which may again be an X). We have done some of these things in this series of posts so far, and it looks like we are coming up to the mapping part. Just as in other subjects that are "sets with additional structure" (ignoring size issues as I usually will here) the mappings are functions on the underlying set that preserve the additional structure.

So, what is the underlying set? Its the set of the objects of the category. And the additional structure? The rules on the morphisms, of course! Given categories C and D, a mapping, F, between them- called a functor- gives for each object a in C an object Fa in D. If the categories are small this is literally a function. We also think of the functor as mapping a morphism, h, in C to a morphism Fh in D. In this way the functor has two "actions", one on objects and one on morphisms.

What about the additional structure then? The mapping on morphisms must obey the following laws- for all f : A -> B, g : B -> C, F(hof) = Fh o Fg (the functor F preserves composition, and for idA (the identity morphism for an object A) F(idA) = idFA (the mapping of the identity is the identity of the mapping). In other words, if morphisms compose in C then the mapped versions compose in D, and the identity morphisms of C and mapped to the ones in D.

Just as with other mapping there are a lot of things we could talk about here- invertable mappings, "surjective" mapping (epimorphisms), "injective" mappings (monomorphisms), endomorphisms, and on and on. For now I want to just talk about ways of thinking about functors and leave it at that.

One way to think of a functor is that it gives an "image" of one category in anther. Since the mapping preserves structure the image is pretty similar to the original, but it is like an interpretation of the source category in the target category. This is especially nice when thinking about mappings between mappings (a category of categories has its mappings as functors, and a category of functors has as its mappings natural transformations, a subject for a latter post) as they show the relationship between images or models of one category in another. We can then look at all ways to interpret one category in another and how they relate to each other. Hopefully I will talk about this in my posts on functional type theory.

Another way to think about them is just as the appropriate notion of mapping between the objects we are talking about. This is nice when talking about subcategories and relations between categories as it is similar to how we talk about these things in other theories. If we think of certain simple categories and all functors from or to these categories to other categories we can use functors to point out different aspects of the other category. This gives us things like a rigorous definition of the diagrams we draw.

We can think of categories as just dots and arrows, so they look like directed graphs (assuming self edges and transitivity) and maps between them are ways of placing one graph "inside of" the other in some sense.

I thinks thats all I will say about functors for now. Perhaps next time we will move on to natural transformations. If you are learning category theory, please check out the Catsters on youtube, and learn about important constructs like products/coproducts, limits/colimits, pullbacks/pushouts, etc. I will probably skip around and move too fast to cover these things, so be warned.

Functional Type Theory

In "Categories for Types" a functional type theory is given by the signature and axioms, just like an algebraic type theory. The difference is that the types and terms form a richer structure.

In addition to the ground types, defined just as in the last post, we have types generated by the grammar: T -> unit | a | TxT | T => T where a is a ground type. In other words, we chose our ground types and generate the set of types as the smallest set such that: all ground types are types, for all types A, B there is a type AxB (A cross B), and A -> B (functions from A to B), and the unit type is a type.

The terms are given just as before as well, with all variables as terms, all function symbols with arguments as terms, and all constants as terms, but we also have the unit term (), as well as all pairs of terms and projections for pairs, as well as lambda abstractions and applications of terms to terms.

This richer structure has additional rules to make abstraction and products work nicely. Notice that the terms are those of a lambda calculus with products with a simple type system with only function and product types. While the algebraic type theories where the language of categories with finite products, functional type theories are the language of cartisian closed categories (CCC). If you are familiar with CCCs, it should be clear that the types are objects, the products are the products of the category and the function types are the exponential objects- in other words the two constructions match up very nicely with each other.

This is a very cool thing for several reasons- first off I think it is neat that we have a logic (a type system) with a language for proofs (the existence of a term in a type proves that type and the corresponding proposition in the logic), secondly the term language is the lambda calculus (which is just awesome by itself) and thirdly it seems like CCC are the setting for computation and extract exactly the structure necessary to describe these systems of computation and logic.

I plan on posting about this subject more, and in particular I want to talk about higher order functional type theories and eventually omega lambda x hyperdoctrines (which is an awesome name) and domain theory as I learn about them.

Algebraic and Functional Type Theory

I've been reading "Categories for Types" for months now, and I'm finally starting to really get it. This book is great by the way- it goes over the theory of lattices, domains, posets, and categories (where it gets all the way from "what is a category" to the yoneda lemma and cartisian closed categories) before getting into type theory.

There is a chapter on algebraic type theory that goes over how to specify an algebraic theory as a syntactic system before giving it a meaning in some category. We do this in the lambda calculus, and it is a formal language and things like reductions are equivalences that we induce over words in the language so that computing equivalences tells us something in the semantics we have in mind. The fact that this is true in algebraic theories is new to me and very neat.

For example, the theory of groups is normally given by (S, +, 0, -), in additive notation, such that S is a set, + : SxS -> S, -: S -> s, 0 in S. In addition we have the axioms that make this structure into a group- let and right sided identity for 0, closure under +, the existence of inverse for all elements, and the associativity of +.

This data given as a type theory goes a little differently. First we define the Theory as a signature and its axioms. The signature has the types, in this case just the one type S, and the function symbols, their arities, and their sortings. The symbols are +, -, and e (the identity) with arities 2, 1, 0 respectively. The sorting says which arguments to the function have which types, but their is only one type here so that is pretty clear.

The axioms are a set of "equations in context". A context is of the form [(xi,Ti)], a list of variables paired with their type. Using |- for the turnstile symbol, the axioms look like "x:S, y:S, z:S |- (x+y)+z = x+(y+z):G" which is an equality of terms using the function symbol + (obviously this is the associative axiom. The theorems of the theory are the things that can be proven with the axioms and the rules for deriving true statements. Clearly all the axioms are theorems, as well as many other statements. When modeling a theory it is important to consider if the theorems of the theory are true in the model (soundness) and if the things true in (all of ) the models are present in the theory (completeness).

With this theory now given syntactically we can interpret it by giving it models as collections of objects and morphisms in a category. I will post more about this as I learn it because I think it is just incredibly interesting. This is just great material.