Linking Interaction Nets and Post Canonical Systems

And one more update due to a paper I wrote for the Models of Computation course. I'd like to attend you all to a very beautiful model of computation called interaction nets. One application this model is used for is to optimally implement lambda calculus in a certain theoretical sense.

The paper I wrote connects the Post correspondence problem (PCP) to interaction nets, by reducing PCP in a number of steps to an interaction net and giving some suggestions for the other way around. (Thereby proving interaction nets at least Turing complete, and leaving the suggestion for Turing equivalence.)

The reverse proof is much more involved, needing multiple reduction steps, possibly through the chemical abstract machine I referenced.

I hope some of you will be inspired by interaction nets.


You can find the paper here.

Slides Church-Turing Thesis and Gödels Incompleteness Theorems

A pair of slides this time. Again for Models of Computation I held a presentation, this time about the Church-Turing Thesis and some interesting variants of it. As a computer scientist one should really know the general ideas surrounding it.

And finally slides for a Philosophy of AI course about Gödel's Incompleteness Theorems (mostly the first theorem). In the slides I tackle some possible misconceptions when interpreting the theorem and try to convince you that Gödel's Incompleteness Theorems, although very interesting, are not very usable in a philosophical argument, but can be used as a starting point for devising new philosophical theories.


I hope you'll find it interesting and comments are always welcome.

The slides for the Church-Turing Thesis can be downloaded here.
The slides for Gödel's Incompleteness Theorems can be downloaded here.

Slides Church-Turing Thesis (MoC)


Slides Gödels Incompleteness Theorems


The slides for the Church-Turing Thesis can be downloaded here.
The slides for Gödel's Incompleteness Theorems can be downloaded here.

Post's Correspondence Problem

So I held a presentation for my course Models of Computation and I thought I'd share the slides with you.

The presentation is about the classic recursively unsolvable problem called Post's Correspondence Problem. I hope you find it interesting.


Slides MoC

Updated:
You can get the slides here.
I now completed the course and completed a paper related to this presentation. You can find that here.

A small handout on TTTAS (Typed Transformations of Typed Abstract Syntax)

This period I did the course Advanced Functional Programming and I had to choose a subject from a set list of subjects to present. I chose typed transformations of typed abstract syntax (TTTAS). (See this webpage for the technical report and associated library by Arthur Baars, Doaitse Swierstra and Marcos Viera.)

I already expected the subject to be one of the harder ones and I also had a restriction for the presentation due to practical issues, namely we could only use handouts (or your own laptop) and not a beamer because of multiple presenters.

Thus I made some handouts in a tutorial like fashion. It might save you some typing of the code found in the paper and hopefully get you interested in the subject. You might also find it useful to get some motivation for the use of GADTs and transformations of EDSLs in general.

The handouts:
The PDF file is here.
The lhs can be found here.

Using LaTeX for homework exercises

Last period I had a course about development of knowledge systems for which I had to do weekly (and quite large) assignments. The assignments were more suited for information science majors and therefore easier on the technical side. So I found this a good opportunity to invest some time in learning some more LaTeX by doing (most of) the exercises in LaTeX.

Anyway, one of the problems I had while working with LaTeX was the lack of larger examples. The documentation for LaTeX and the packages I used was pretty good most of the times, but larger examples still help a lot when you're just starting out. So hoping some people will get use out of it, I've uploaded the sources of my solutions to the exercises. (Of course these solutions are not 100% correct.)


Some of the packages I used were amsmath and amssymb. These really helped a lot to do the proofs. (Some documentation can be found here and here.)

For Assignment 2 I also learned to use graphviz to draw my graphs. So some example DOT files are included in the extras. (The guide I used was here.)


I split the assignments into the original problem description (the part I had to deliver was the hand-in part), the LaTeX source and other sources such as pictures, the final outputted PDF and possibly additional sources such as the solutions in the tools.


Assignment 1 (Logic):
Problem description | LaTeX + other source files | Outputted PDF | Extra files
(Extra files include the python files I used and edited to generate the truth tables in LaTeX, thanks to midorikid)


Assignment 2 (CLIPS):
Problem description | LaTeX + other source files | Outputted PDF | Extra files | CLIPS
(Extra files include the DOT files I used for graphviz, Microsoft Visio Drawing of the family tree and the CLIPS files I made.)

Assignment 3 (Protégé):
This was not done in LaTeX because I did not have access to my own computer. If you're interested, tell me, and I'll find the sources from Protégé and Microsoft Word anyway.

Assignment 4 (Hugin/Probability Theory):
Problem description | LaTeX + other source files | Outputted PDF | Extra files | Hugin
(Extra files include the multiple probabilistic networks.)

Assignment 5 (Fuzzy Logic/Systems):
Problem description | LaTeX + other source files | Outputted PDF | Extra files
(Extra files include the Maple 13 file to model the functions.)

Comparing Parser Construction Techniques

Already a few months ago I completed my Bachelor computer science by writing a small paper and attending and presenting at a student conference. Well anyway, the topic I wrote about is parser construction techniques. The paper talks about parser generators (ANTLR in specific), parser combinators (Parsec 2) and a nice novel combination of the two (Tinadic Parsing, still to published somewhere in the future).

Anyway I hope this paper might be interesting to some people reading my blog. The paper comes with quite some code examples and it's probably not a very hard read. So you might consider it a small tutorial on parser construction techniques (or even learn some Parsec while you're at it :) ).

My paper can be found here at the website of the University of Twente.

The accompanying code examples can be found here. If someone would really appreciate it, I might consider writing some more documentation.



As you might have noticed blog posts were a bit scarce the last weeks, because of my silly ambition of taking 3 instead of 2 courses :P. Anyway, I'm liking the pace but my side activities suffer a bit, so I'll probably switch back after next period.
(People waiting for the extended state monad implementation: I haven't given up yet!)

Breaking GHC and the monad laws

So the summer school Applied Functional Programming at the University of Utrecht ended a few weeks ago. I really had a lot of fun and learned even more than I had fun ;). Anyway during the summer school we received a lot of extra exercises you could do out of your own interests. So I picked up one of the exercises I didn't do during course. Namely an extension of the state monad.

In this exercise you should extend the state monad in such a way it keeps track of the number of binds, returns and some other capabilities. One can read the full exercise here. In short if you have a computation like this:

do return 3 >> return 4
   return 5
   diagnostics

After running this computation in the state monad one should have a result that somewhat looks like this:

 "[bind=3, diagnostics=1, return=3]"

That looks doable, but is a lot more tedious than you except at first. Anyway, a very important point you should catch is that after implementing this functionality we now do NOT abide to the monad laws anymore.

Remember the monad laws (stolen from here):

 
   1. "Left identity":  return a >>= f  ≡  f a
   2. "Right identity": m >>= return  ≡  m
   3. "Associativity": (m >>= f) >>= g  ≡  m >>= (\x -> f x >>= g) 

As you can see all three laws can transform an expression on the left side to an expression that contains one bind less. Therefore if we perform a computation in our state monad we would have a different number of binds after transforming and could therefore give a different result when getting out our number of binds and returns.


But let's first return to the implementation of this extension. I chose a Map with strings to int that can keep track of the number of binds and annotations. So we now have a State Monad with some extra functionality:

data StateMonadPlus s a = StateMonadPlus {runStateMonadPlus:: (s,Map String Int) -> (a, s, Map String Int)}

This is very similar to the original definition of the State Monad. (If you forgot some parts of it you can read a part of my State Monad tutorial here.

Anyway, before defining the Monad instance we define a useful helper function for updating the Map that keeps track of the number of binds and annotations and another function that puts the diagnostics as the result of the computation.
diagnostics :: StateMonadPlus s String
diagnostics = StateMonadPlus $ \(s,m) ->
let m2 = updateMap "diagnostics" m
in ((show m2 ), s, m2)

updateMap :: Ord k => k -> Map k Int -> Map k Int
updateMap k = M.insertWith (+) k 1

And now for the Monad instance:

test1 = do diagnostics
           return 4 
           return 5
           mget

diag = diagStateMonadPlus test1 undefined
eval =  evalStateMonadPlus test1 undefined
diageval = (diag, eval)

Anyway, halfway during the implementation I got stuck on something that seemed like a bug in my program, but before spoiling everything I will first show the functions I defined for running and evaluating our freshly made State Monad.

evalStateMonadPlus :: StateMonadPlus s a -> s -> a
evalStateMonadPlus (StateMonadPlus s) st = let (a,b,c) = s (st, M.empty) in a

execStateMonadPlus :: StateMonadPlus s a -> s -> s 
execStateMonadPlus (StateMonadPlus s) st = let (a,b,c) = s (st, M.empty) in b

diagStateMonadPlus :: StateMonadPlus s a -> s -> Map String Int
diagStateMonadPlus (StateMonadPlus s) st = let (a,b,c) = s (st, M.empty) in c

instance MonadState s (StateMonadPlus s) where
 get = StateMonadPlus $ \(s,m) -> (s, s, m)
 put a = StateMonadPlus $ \(_, m) -> ((),a, m)

mget:: StateMonadPlus s (Map String Int)
mget = StateMonadPlus $ \(s,m) -> (m, s, m)

Here the get and put functions are the familiar functions in the original state monad, and mget does something similar to diagnostics, by putting our map into the result.

Because I defined a multi parameter type class, and a flexible instance too, we will have to add some compiler pragma's to be able to use them. And we furthermore used some imports. So just add this to the start of the module:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
module StateMonadExercise where
import Control.Monad.State
import qualified Data.Map as M
import Data.Map(Map)

So the only part left to test this functionality is to define some tests:

test1 = do return 4 
           return 5
           mget

diag = diagStateMonadPlus test1 undefined
eval =  evalStateMonadPlus test1 undefined
diageval = (diag, eval)

So now we're ready to run these test right? (I've enclosed the full test module at the end of this blog post for your convenience, so you could just copy the whole code at once if you'd like.)

Anyway, after running these test, (and I think it's not a bug on my part but a (maybe) too enthusiastic optimization of GHC (6.10.4)). We get these results:

 
*StateMonadExercise> diag
fromList [("bind",2),("return",2)]
*StateMonadExercise> eval
fromList [("return",2)]
*StateMonadExercise> diageval
(fromList [("bind",2),("return",2)]
,fromList [("return",2)])

So here GHC just optimized away 2 binds for the result but not from the map. It serves me right though, since I'm breaking the monad laws anyway :-). So if anyone can confirm this is GHC's "fault" (or doing) and not mine I would be happy.
One final comment: I will probably post the full implementation later this month.


The full code:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
module StateMonadExercise where
import Control.Monad.State
import qualified Data.Map as M
import Data.Map(Map)

data StateMonadPlus s a = StateMonadPlus {runStateMonadPlus:: (s,Map String Int) -> (a, s, Map String Int)}

instance Monad (StateMonadPlus s) where 
 return a = StateMonadPlus $ (\ (s, m) -> (a, s, updateMap "return" m)) 
 (StateMonadPlus s) >>= f = StateMonadPlus $  \(state, m)  -> 
                             (let (a1, st1, m1) = s (state,m) in 
                               let (a2, st2, m2) = runStateMonadPlus (f a1) (st1,m1)
                                in (a2, st2, updateMap "bind" m2)
                             )

updateMap :: Ord k => k -> Map k Int -> Map k Int
updateMap k = M.insertWith (+) k 1

diagnostics :: StateMonadPlus s String
diagnostics = StateMonadPlus $ \(s,m) -> 
               let m2 = updateMap "diagnostics" m 
               in ((show m2 ), s, m2)

evalStateMonadPlus :: StateMonadPlus s a -> s -> a
evalStateMonadPlus (StateMonadPlus s) st = let (a,b,c) = s (st, M.empty) in a

execStateMonadPlus :: StateMonadPlus s a -> s -> s 
execStateMonadPlus (StateMonadPlus s) st = let (a,b,c) = s (st, M.empty) in b

diagStateMonadPlus :: StateMonadPlus s a -> s -> Map String Int
diagStateMonadPlus (StateMonadPlus s) st = let (a,b,c) = s (st, M.empty) in c

instance MonadState s (StateMonadPlus s) where
 get = StateMonadPlus $ \(s,m) -> (s, s, m)
 put a = StateMonadPlus $ \(_, m) -> ((),a, m)

mget:: StateMonadPlus s (Map String Int)
mget = StateMonadPlus $ \(s,m) -> (m, s, m)

test1 = do return 4 
           return 5
           mget

diag = diagStateMonadPlus test1 undefined
eval =  evalStateMonadPlus test1 undefined
diageval = (diag, eval)

{-
*StateMonadExercise> diag
fromList [("bind",2),("return",2)]
*StateMonadExercise> eval
fromList [("return",2)]
*StateMonadExercise> diageval
(fromList [("bind",2),("return",2)]
,fromList [("return",2)])
-}