Addition categorically!

See “Computational Category Theory” by Rydeheard and Burstall for implementation, in ML, of the algorithms in elementary category theory. Following their lead, we present data types in Haskell that can be used to implement basic algorithms in category theory. We use a category in which addition (of integers) can be performed to ground the discussion. You will also need familiarity with types, type variables and classes in Haskell (see learnyouahaskell.com website) to proceed.

Cut & Negation in Prolog

! pronounced “cut” is a special goal in prolog which always succeeds. The purpose of cut, loosely speaking, is to freeze some of the choices made by the backtracking sytem so far. Cuts can therefore be used to increase the efficiency (time) of prolog programs. First we will see how the backtracking is affected by the use of cuts. Then we will give an example use of cuts to speed up prolog programs.

Non-Determinism in Prolog

We will look at terms (the basic data structure) in prolog. All prolog data and prolog programs are stored as terms. A widely used term type is a list. We will look at several non-deterministic predicates over lists. Using the predicates on lists and their non-deterministic capabilities, we develop a program to do breadth first search (BFS) and a program to solve the n-queens problem. BFS is the basis for many search algorithms in AI such as $A^*$, IDA, $\alpha-\beta.

An Introduction to Prolog

The starwars way Prolog stands for programming in logic. Prolog programs are specified as relations and rules around the relations defined by programming in logic. The programs can be queried to determine the veracity of facts or to infer new facts using the rules. The specification of the facts and rules will be illustrated using the STAR WARS family tree as per the end of episode 8 at the end of this post (obtained from google images).

Computer Program as Proof

“All your proof are belong to us“ The first way we learn to do proofs is by induction. Proofs by induction are done in three steps. First, we establish a base case. Next we assume a hypothesis, and finally, we prove the inductive step. As an example let us consider the fact that the sum $0+1+2+ \ldots+n$ is $n(n+1)/2$. The three steps are: Base case: consider the series $0+1$, the sum is $1$, and the formula is $1(2)/2$.