Therefore, BIC pens are the best pens for pen flipping tricks. QED.
Each of the genetic operators has to be reinterpreted using this representation. We can't change the population directly, as it has no mutable structure (real functions have no internal state), but we can wrap it up in other functions that enact changes. Let go through the three main operators- mutation, crossover, and selection.
Mutation requires that some small number of bits are flipped. These bits can be represented by a set of integer pairs specifying not the bits values, but rather their location. There value is not important in the representation. If we make such a set of random pairs, we can create a function that takes as an argument a function representing a population, and returns a function representing the new population. This new function will use the old function to get the value of a particular location, but if the coordinate requested is also in the set of mutated coordinates then it will flip the result before returning it. This means that we use the old population's values, but wrap the function up in case we need to change its specific locations.
Crossover can be represented by a list of triples. The first two numbers are the crossed pair, and the third in the triple is the cut point between the two individuals. Of course, some individuals will not be crossed at all, and their cut points will be 0. Again, the actual genetic material of the individuals does not matter, only the place that the cut point occurs. This list of triples can be used to wrap up the function representing the population, such that to get a particular coordinate one has to check the respective triple and cut point, and get the value from the previous population. If the requested value is before the cut, we get it from the first individual, and if it is after the cut point then we get it from the second individual.
Selection is particularly easy to represent. Each selected individual- regardless of the selection mechanism- gets its index recorded in a list as long as the population. This list is like a switch board- when an index is requested, the index from the previous population is returned based on the value in this list. So to get the first individual in the new population, we return the individual in the previous population whose index is recorded in the first position of this list. If we don't want to make the choose of the actual individual, as we will see at the end of the post, we can just use tournament selection and record the tournaments, deciding the winners when we have the individuals. Something similar is possible with roulette wheel where we record value from 0 to 1 and use them as the spins for the wheel.
With all the genetic operators represented this way, we simply have to create a population function and wrap it up in higher order functions again and again to perform a run of the algorithm. This turns out not be be terribly fast in my trials, as after a couple of operators there are a large number of bit flips, checks, and indirections necessary to get the value of a location. I've tried several things to make it faster, but at least the naive implementation does not appear to scale well. It is still an interesting idea, however. If the population where somehow very sparse it might even save space, as you only have to record changes, not all the actual bits. In fact, if the population started out completely uniform- for example all bits are set to 0- such as before the initialization step, then the population could be represented by a very concise function- the constantly 0 function. This requires a fixed constant amount of memory, which might be a huge win in some cases.
Unfortunately I have not been able to get this idea to be any better then the usual way of doing a GA. The only thing that it has lead to is an idea about investigating the effect of the initial population on the resulting population. If all the generations where generated as I've described (and not necessarily stored wrapped up in a function, but rather just as the data structures) then a run could be performed many times. If we generate some population, and then run the same GA many times with the same mutations, crossovers, and selections, then we could flip each bit one at a time and see how it effects the resulting population. This would tell us if some bits where more important then others. The coolest thing would be a "heat map" were each bit in the original population is replaced with a color based on how many bits in the final population it effected. This would be really cool to look at, if nothing else.
One of the funny things I've seen about it is that it is possible to get this compilation error: "Universe Inconsistency". Is this not the most intimidating error possible? The universe is inconsistent? Oh god. What do we do? Luckily all this mean is that the stratification of the type Type, which occurs behind the scenes, failed because of some definition. Stratifying Type allows the calculus to remain predicative without making the user manage the infinite hierarchy of universes indexed by the natural numbers.
There are two languages in Coq- Gallina, the term language, and the administration language called the Vernacular.
I need to do a sample project to evaluate the tool, so I've chosen a very simple one- I'm translating the untyped lambda calculus into the system SKI. Its a simple translation on inductive datatypes. I'm not sure how to show that the translation makes any sense- my first thought was some proof of extensional equality, but I don't think thats really possible. I suppose something might be possible, but I can't think of anything that doesn't require reducing lambda terms into a normal form, which is, in general, impossible. I'm sure I'm missing something here.
Coinductive types are pretty neat. They are often infinite, and yet in Coq programs using them must always halt. This is handled by rules on their use that ensure they do not cause some potentially unbounded recursion (co-recursion?). This certainly forbids some programs that would have been terminating, but in this sort of thing we are willing to give up some generality for strong normalization.
Speaking of strong normalization, while the actual logic of the system is intuisionistic, it is possible to do classical proofs. Adding the LEM (Law of the Excluded Middle) to a module does not break the whole system, but I don't know how it interacts with the assurance of termination or the types of proofs possible.
So yea, Coq is pretty awesome. So are the other systems built using the CoC like Adga and Epigram, I only chose Coq because it is a proof assistant and so seems more closely connected to AI to me. It really is amazing to see it prove things, and interactive sessions seem like a conversation with a computer that is capable of fairly complex proof techniques.
System F does not correspond to what you normally hear called second order logic, which may be called second order predicate logic, but rather to (the implication fragment of) second order propositional logic. Interestingly Haskell's concept of a type class gives us predicates, which makes it more like first order predicate logic, which is awesome.
So, we have two tools- implication in the form of lambda abstractions written as ->, and universal quantification in the form of type abstraction. In the simply typed lambda calculus we could specify the identity function as (\x:a.x) read as "for x of type a, x" which has no effect on its arguments. The problem with this is that this function only takes arguments of type "a", so we have to define a different identity function for each type, even though all identity function look exactly the same. Universal quantification to the rescue! Now we can define the identity function once and for all, introducing some new notation, as (\a:*.\x:a.x) which is read as "given a type called a and a term of type a, return that term". I don't have a good way of showing in text the difference between abstraction of types and abstraction of values, but the first argument's type is * which is the type of all types. I kind of like using "\" for both term and type abstractions as they follow mostly the same rules. This makes "*" a kind of second order type, and it is called a kind. We pronounce it "star". To use this term, we must first supply some type, then some term of that type, and will get back our term unchanged like so- (\a:*.\x:a.x)Integer 3 =beta 3. In logic this would look like "forall a, a -> a" meaning that all things imply themselves.
The nice thing about this situation is that we can define functions that are the same for all types. This gives what is called parametric polymorphism, similar to Java's Generics. In Haskell the type system is a series of extensions on the second order lambda calculus, so we don't have some system tacked on to the language but rather a built-in and well understood form of parametric polymorphism.
I want to mention that Haskell's type system isn't quite System F, but rather the Hindley-Milner system, which restricts the locations that the universal quantification can occur in order to allow type inference. This means that the compiler can determine types for you, which is hugely convenient and useful, while imposing a very small restriction to the set of valid programs.
Lets look at one more interesting thing about this system. For the term (\a:*.\x:a.x) we must supply a type. What if we supply the terms own type? Well, its type is written (in my own ascii art interpretation of the actual symbols) as (\a:*.\x:a.x) : (\a:*.a->a). Therefore we have that (\a:*.\x:a.x)(\a:*.\x:a.x) =beta (\b:(\a:*.a->a).\x:b.b) : (\b:*->*.\x:b.b) : (* -> *) -> (* -> *). This is pretty hard to see just looking at the terms, especially as I don't have all the symbols I would like (like both lower and upper case lambdas, product types as the big pi symbol, and the box called "sort" which is the type of all kinds (which brings us to the fourth layer of the type system)). The important thing to see here is that the kind of the argument is not *, but rather (* -> *), and the kind of the resulting term is (* -> *) -> (* -> *). The kind * -> * is something that needs a type and returns a type. This is what I was talking about in the beginning of this post as something we see in programming. The array type in most languages (such as c, c++, Java, Haskell) is not itself a type. There is no such thing as an array, there are only arrays of some type of object. We can have arrays of ints, written int[], or of strings, written String[] (in Java), or of Objects, written Object[]. This means that arrays need a type, which we can call A, and return a type, an array of As. The term we just saw has a more complex kind, and it happens that supplying the identity function its own type give a kind of second order identity- the identity on type constructors.
In Haskell we can have kinds formed with * and ->, which may remind us of something. It is very similar to an untyped lambda calculus, as different occurrences of * may be different types.
I think that enough for now. Having mentioned the Calculus of Constructions, maybe I will post about it later on.
Before going over the proof (which is very easy), notice that there are many combinators besides S, K, and I. We have seen Y, but other cool ones are B = (\f.\g.\x.f(gx)), which composes two functions called f and g here (this is called "." in Haskell to mimic the notation in math of a small unfilled circle), and C = (\f.\x.\y.fyx) which swaps two arguments of a function (called flip in Haskell). These are cool because they give nice little transformations and show how combinators (and the lambda calculus in general) express control flow. Concatenative languages can be considered the composition of combinators in a cool way. Also, combinators appear in the compilers for functional languages. Very cool things, them.
So, the proof. The lambda calculus is a system of universal computation, so it can compute anything that can be computed (by definition). If we can turn any term of the LC into a term of the SKI combinatory calculus that is equivalent. There is some difficulty with the notion of equality here- the translation is not a simple bijection as a lambda term translated into SKI can be translated back, but it will not always be the same term. We may take an intensional notion of equality (an intentional equality considers terms to be equal if they are exactly the same syntactically) but this will not work in general. Remember that not all reduction terminate in the lambda calculus- that is one of the reasons type systems exist. To test if two terms are exactly the same syntactically we could want to reduce then to their normal form (as all normal forms are unique and therefore are a sort if "identity" for a term). This computation of the normal form may not terminate, and therefore we can't use this notion of equality. On the other hand, we can use an extensional notion of equality- terms are equal if they work the same in all possible uses. While intensional equality is concerned with the "internal" representation of the term, extensional equality is concerned with the "external" behavior of a term. The translation that we will be looking at may not get us back where we started, but it will get us somewhere equal to where we started if we consider terms equal if they behave the same way.
The actual translation is by cases. This is very easy to express in Haskell, so I've just now written a translator from SKI to lambda calculus and back, as well as a function to reduce an SKI and a function to reduce a lambda term, both by only one reduction (again, if we keep reducing until we are done we may never terminate as in the case of the term (\x.xx)(\x.xx)).
In code we have:
data SKI = S | K | I | App SKI SKI | Var Id deriving (Show, Eq)
data Lambda = LVar Id | LApp Lambda Lambda | Abs Id Lambda deriving (Show, Eq)
As data, and for the translation:
fv (Var id) = [id]
fv (App e1 e2) = fv e1 ++ fv e2
fv _ = []
freeIn id term = id `elem` fv term
lambda2ski :: Lambda -> SKI
lambda2ski (LVar id) = Var id
lambda2ski (LApp e1 e2) = App (lambda2ski e1) (lambda2ski e2)
lambda2ski (Abs id term) = lamb id $ lambda2ski term
lamb id term | not (id `freeIn` term) = App K term
lamb id (Var id') | id == id' = I
lamb id (App e1 e2) = App (App S (lamb id e1)) (lamb id e2)
This is the code only to translate one way, the other way is even easier. The function fv gets the list of free variables in a term, and the function freeIn tests if an identifier (a String) is a free variable in a term. Of course, lambda2ski does the translation, and lamb is a helper function to take care of lambda abstractions.
For those who do not know Haskell, the translation from Wikipedia is this:
1. T[x] => x
2. T[(E₁ E₂)] => (T[E₁] T[E₂])
3. T[λx.E] => (K T[E]) (if x does not occur free in E)
4. T[λx.x] => I
5. T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E)
6. T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])
Where T[term] is the translation function applied to the term "term". Having embedded the lambda calculus in SKI we have proven it as a system of universal computation, assuming the extensional equality of the translated term with the original.
It is interesting that the reverse translation, also given on the wikipedia page for combinatory logic, will make the resulting lambda term longer than the original. For the terms I have played with, it seems like translating from the LC into SKI and back always makes the term larger, although I'm not making an attempt to do reductions at the moment.
Well, that was fun. Hopefully this works out nicely in Coq as well, and I can make the project a computer verified proof of this translation.
One problem we might want to use a GA to solve is the "best" series of choices. For example, we may have many compiler flags, purchase choices, forks in the road, or any other type of yes/no decision to make. We can certainly do more then just yes and no, but for simplicity lets consider the situation where we must make 6 choices. To make it even simpler, it will turn out in our example that to get the best answer, we should always choose yes. The maximum fitness is 6 and the perfect individual will get this fitness by choosing "yes" for each choice.
So how do we write down random symbols that encode a series of 6 choices? Like so- 001010, 111000, 101010, 001011. This will be our population- each individual will chose "yes" for the indices that it has a 1 in, and "no" in the indices that it has a 0 in. Since we want the individuals to always choose yes, the fitness function will just count the number of 1s in the individual.
Remember the first step is determining fitness- f(001010)=2, f(111000)=3, f(101010)=3, f(001011)=3. Now lets let selection choose a new population- 111000, 111000, 111000, 001011. The way this is actually done is by creating something like a pie chart, where each individual gets a slice proportional to how high its fitness is. A little spinner is spun 4 times, in this case, and the individual that it lands on gets copied into our new population. This is called Roulette Wheel selection.
I want to mention that there are other selection methods. One, called Tournament Selection, just holds a series of tournaments to determine who gets copied into the new population. Each tournament consists of a random selection of individuals from the population (normally 2) and the competition is just selecting the individual with the higher fitness most of the time, and randomly choosing a less fit individual as the winner some of the time (normally 75% of the time the better individual wins). An individual might participate in many tournaments, or it might not be chosen for any tournaments at all.
Now lets do some mutation- 111000, 111000, 111000, 001011 becomes 111000, 111000, 111100, 001011.
And Crossover, pairing individuals up randomly- (111000, 111100), (111000, 001011). Lets say both pairs are chosen for crossover, as the rate of crossover is normally set pretty high (70% or so). The first pair gets the space between the third and fourth index as the cut point, and the second the space between the fifth and sixth. (111|000, 111|100), (11100|0, 00101|1), where the "|" is the cut point, becomes 111100, 111000, 111001, 001010.
We are going to go for more than one generation in this example, so lets start from the beginning- f(111100)=4, f(111000)=3, f(111001)=4, f(001010)=2. Notice that not all that much progress has been made and we certainly don't have a perfect solution (which would be 111111). Well, lets keep going- selection gets us 111001, 111001, 111001, 111001. It looks like one individual has taken over the population- we say the population has converged.
This population has no diversity, which is a very bad thing. Diversity is vital in a GA to get good solutions and partial solutions to create good results. Now we have to let mutation randomly mutate the 4th and 5th digits from 0s to 1s in order to discover the best individual. This is one of the contributions of mutation to a GA- it will introduce new genetic material into a population that no longer has the diversity to find good solutions through crossover.
I won't go through the details of the rest of the run- imagine that mutation takes several more generations to mutation those last couple of indices to 1s, and we find that the resulting population is all individuals that look like 111111. Maybe a 011111 is thrown in there too- mutation can decrease fitness just as easily as increase it.
This problem- finding an individuals of all ones- is called the MAX problem for GAs. There are many standard problems for different techniques that try to isolate properties of the problem solver (GA in this case) so that variations of the basic methods can show is they do better than others in the aspects that these problems try to showcase.
I sneakily introduced the "yes or no" encoding as 1s and 0s to introduce the most common encoding for individuals in a GA- a binary string aka bit vector aka {0, 1}* aka base two numeral.
I think next time we will move on to Genetic Programming on our long road to RGEP. Good times ahead!
The sample problem will be trying to find a value, x, for the function f(x) = x^2- the function that takes a single input number, lets say a positive whole number, and returns its square. We want to know what input number between 0 and 1000 (exclusive, so 0-999 inclusive) will get us the highest number as a result. The solution space is the numbers from 0 to 999. It will be convenient to write all numbers with 3 digits, so 0 is written as 000 and 23 as 023, etc.
The answer is obviously 999. If this partially random search of the solution space is to be "intelligent" it should arrive at the same conclusion that we have come to.
Now that we have a problem to solve (the max output of f(x)=x^2), a solution space (the numbers 0-999), and a way of writing down possible solutions as a list of symbols (000-999, which is all possible three symbol words using the numbers 0-9), we are ready for the biological metaphor. The story is that the list of symbols is sort of like the genetic material for an organism. The number that it corresponds could be considered its phenotype- so 023 is the genetic material that gives rise to the number 23 as the phenotype. The fitness of the individual is the result of putting its phenotype (its "body") into the fitness function (here its our squaring function). The result of squaring its phenotype tells us how well it solved our problem because we are looking for the highest output of the function f.
This is a nice little relation between the components of the problem and the situation in nature, but there are still parts missing. In nature we may expect there to be many individuals- in a GA we have many lists of symbols, not just one. Also we expect that fitness isn't just a number- fitness should affect the survival of the individual. It is not enough for fitness to affect survival, as there must also be some sort of variation between generations (which implies some way of creating children). This situation gives us the inspiration for the rest of the system.
Lets outline the situation using these new facts- there is a population of lists of symbols which will be random, our example population will be 900, 002, 299, and 432; there is some selection of good solutions that kills off some bad solutions, there is some random variation corresponding to mutation in natural genetics, and there is some mechanism for creating child, a crossover similar to crossover in natural genetics. We hope that good solutions will be copied many times during selection, that mutation will improve solutions and not make them worse, and the crossover will take two goodish solutions and create really good ones by combining the parts of the solutions that made them good into an individual with the traits to be great.
Starting with the population of randomly generated individuals 900, 002, 219, and 432 we should turn them into their phenotype-900 becomes 900, 002 becomes 2, 219 becomes 219, and 432 becomes 432. Now we can put them into our fitness function so f(900)=81000, f(2)=4, f(219)=47961, f(432)=186624. Clearly 900 is a good (but not perfect solution), and 432 is pretty good too. Now lets select some of the good ones, allowing them to be selected many times so the new population may have several individuals that look exactly the same. I won't go into example how to do this in this post, but lets say we end up selecting a new population from the old (think of the individuals as reproducing) and we get 900, 900, 219, and 432. The 219 wasn't as good as 900 or 432, but the "best" individual doesn't always live in nature and the "worst" doesn't always fail to reproduce.
Now lets do some mutation. This means that we take our new population (900, 900, 219, 432) and just randomly change some digits to random numbers. After mutation the population may look like this: (900, 900, 299, 132) which changed exactly two digits in different numbers. It looks like the 432 that got mutated into 132 got much worse, but that happens sometimes. The 219 that was mutated into 299 certainly got better, which is nice.
We are almost to the end of the first generation! Now we just to crossover. This means that we pair up each individual, and sometimes the "happy couple" crosses their genetic material, and sometimes (again, randomly) they don't. Lets say they are paired like this: (900, 299) and (132, 900). Lets assume only the first pair (900, 299) chose, or was chosen, to be crossed. Now we must chose a (random) place in the genetic material to do the cross, so lets chose between the first and second digit. This splits the individuals into the pieces (9, 00) and (2, 99). We take the first part of the first individual (9) and the second part of the second individual (99) and put them together getting 999, and the first part of the second individual (2) and the second part of the first individual (00) which combine to 200. The new population is 999, 200, 132, and 900.
This might have all seemed pretty random and not very intelligent at all- the only thing that wasn't *completely* random was selection. Mutation and crossover could create terrible mutants that perform nowhere near as well as the originals just as it could possibly create good solutions. So why did we do this at all? Well, for one thing, in practice we would repeat the selection, mutation, and crossover many times on a much larger population so there would certainly be some chance or getting a perfect solution.
The other thing to notice is the first individual in the new population- its the perfect solution 999! It looks like we started with a small random population that didn't contain a perfect individual and randomly ended up with the correct solution! Its almost as if I had this in mind from the very beginning!
The most vital thing to notice here- really the point of this whole post- is that the original population didn't contain a perfect individual, and none of selection, mutation, or crossover by itself created the perfect solution. Selection ensured that the individual 900, which is a pretty good solution, appeared in the population more than once. Mutation introduced a pattern that was not in the original population (the 99 in 299, which we would write as #99 with # as a "don't care" symbol, which says that we are interested in the last two digits being 9s, and we don't care what the first digit is in this pattern). Crossover took two patterns that helped the fitness of the individuals they were in (#99 and 9## are the patterns that combined) and this produced the individual 999, which has both useful patterns.
This is the basic Genetic Algorithm. The three operations performed many times is the canonical example of an Evolutionary Algorithm and is considered the primal form of Genetic Algorithms. The problems can be much more complicated and useful, the genetic material can have many different symbols and different digits may be constrained to different values. The genetic material may be many numbers, like 934202 could be two inputs to a function f(x, y) = x*y where x=932 and y=202 in the example individual.
Hopefully Genetic Algorithms aren't so mysterious now, and we can move on to more interesting material. The basic Genetic Algorithm is surprisingly similar to my own work- Robust Gene Expression Programming- but we will have to introduce many new concepts to get there from here.
