# Posts

### Computer Program as Proof

“All your proof 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$.

### Minimal models for Propositional Formulas

We look at metaprogramming in Julia. We illustrate parse and eval using the problem of determining a minimal model for a given propositional formula. The computation of minimal models is of interest in answer set programming, as they are used to define stable models 1. The problem of finding a minimal model is NP-complete, whereas the problem of finding a stable model for a given set of propositional statements is $\Sigma_{2}^{P}$ complete.

### Binary Search Trees

Let us implement in julia 0.6.0 a binary search tree to store integers. Each node is either of type Nil or of type bst, as declared below. Type Nil is used a null pointer. We use type union MayBe to hold either a Nil() or a bst. At the start the tree is empty so it is initialized to Nil(). Removing the type declaration from the data element should be sufficient to store datatypes for which a comparator is implemented.

Numbers are all In this post, we examine two examples set out in the classic paper by Turing. The first problem is to report the $n^{th}$ binary digit of 1⁄3. The second problem is to report the $n^{th}$ binary digit of $\sqrt{2}$. The 1936 paper On computable numbers, with an application to the Entscheidungsproble describes two machines to perform the tasks. In this post, we give in Haskell two programs for the same.

In this post, we implement in Haskell, the augmenting path method to find a maximum matching in a bipartite graph. We use function composition and recursion mostly. We obtain a simple implementation of an algorithm to compute maximum matching in a bipartite graph. As a side affect of this exercise, you should know about algorithms to compute terminal objects, and fix points in a category. Only a basic familiarity with Haskell is assumed here.

AVL Trees are binary search trees with a balance condition. The balance condition ensures that the height of the tree is bounded. The two conditions satisfied by an AVL tree are: order property: the value stored at every node, is larger than any value stored in the left subtree, and is smaller than any value stored in the right subtree. balance property: at every node the difference in the height of the right and the left subtrees is at most 1.

### Splay Trees in Julia Lang

Let us implement Splay Trees in Julia which is, relatively new and popular, dynamically typed language with multiple dispatch. We model a node in the splay tree as an abstract data type. Each node contains a single integer data value and two references to the left and the right subtrees. The subtrees can be empty, as in the case of leaf nodes, and we model this by using the Nil type.

### Register Machines

An emulator for Register Machine Our goal is to implement an emulator for a register machine using flex and bison. In the process we will illustrate a function that assigns numbers to programs, the von Neumann machine, and explain how to write self modifying code. Recall that a register machine has an unlimited number of registers and the following three instructions. HALT, stops the machine INC r j, increments the contents of register r, and moves to instruction number j.

### Conference on Algorithms and Discrete Applied Mathematics CALDAM 2017

The third conference on algorithms and discrete applied mathematics [CALDAM 2017] is being organized by the Department of Mathematics, BITS Pilani K.K. Birla Goa Campus from February 16 to 18, 2017. Invited Speakers at CALDAM 2017 are Sumit Ganguly, IIT Kanpur Martin C. Golumbic, University of Haifa Günter Rote, Freie Universitaet, Berlin Ola Svensson, EPFL Lausanne The Program Committee Co-Chairs are N. S. Narayanaswamy, IIT Madras and Daya Gaur.