Title: MIU in Curry
Author: Wolfgang Jeltsch
Date: 30 August 2015
Tags: breadth-first search, Curry, Denis Firsov, Douglas
Hofstadter, functional logic programming, functional
pattern, functional programming, Haskell, Institute of
Cybernetics, KiCS2, literate programming, logic
programming, MU puzzle, string rewriting, talk, Theory
Lunch
More than two years ago, my colleague Denis Firsov and I gave a
series of three [Theory Lunch][theory-lunch] talks about the
MIU string rewriting system from Douglas Hofstadterâ€™s [MU
puzzle][mu-puzzle]. The first talk was about a Haskell
implementation of MIU, the second talk was an introduction to
the functional logic programming language [Curry][curry], and
the third talk was about a Curry implementation of MIU. The
blog articles [*MIU in Haskell*][miu-in-haskell] and [*A taste
of Curry*][a-taste-of-curry] are write-ups of the first two
talks. However, a write-up of the third talk has never seen the
light of day so far. This is changed with this
article.
[denis-firsov]:
http://cs.ioc.ee/~denis/
"Denis Firsov"
[theory-lunch]:
http://theorylunch.wordpress.com/
"Theory Lunch"
[mu-puzzle]:
http://en.wikipedia.org/wiki/MU_puzzle
"MU puzzle"
[curry]:
http://www-ps.informatik.uni-kiel.de/currywiki/
"Curry"
[miu-in-haskell]:
https://jeltsch.wordpress.com/2013/04/18/miu-in-haskell/
"MIU in Haskell"
[a-taste-of-curry]:
https://jeltsch.wordpress.com/2013/04/27/a-taste-of-curry/
"A taste of Curry"
As usual, this article is written using literate programming.
The [article source][article-source] is a literate Curry file,
which you can load into [KiCS2][kics2] to play with the code.
[article-source]:
http://hub.darcs.net/jeltsch/blog/raw-file/2015/08/30/MIUInCurry.lcurry
"MIU in Curry"
[kics2]:
http://www-ps.informatik.uni-kiel.de/kics2/
"KiCS2"
I want to thank all the people from the Curry mailing list who
have helped me improving the code in this article.
Preliminaries
=============
We import the module `SearchTree`:
> import SearchTree
Basic things
============
We define the type `Sym` of symbols and the type `Str` of
symbol strings:
> data Sym = M | I | U
>
> showSym :: Sym -> String
> showSym M = "M"
> showSym I = "I"
> showSym U = "U"
>
> type Str = [Sym]
>
> showStr :: Str -> String
> showStr str = concatMap showSym str
Next, we define the type `Rule` of rules:
> data Rule = R1 | R2 | R3 | R4
>
> showRule :: Rule -> String
> showRule R1 = "R1"
> showRule R2 = "R2"
> showRule R3 = "R3"
> showRule R4 = "R4"
So far, the Curry code is basically the same as the [Haskell
code][miu-in-haskell]. However, this is going to change below.
Rule application
================
Rule application becomes a lot simpler in Curry. In fact, we
can code the rewriting rules almost directly to get a rule
application function:
> applyRule :: Rule -> Str -> Str
> applyRule R1 (init ++ [I]) = init ++ [I, U]
> applyRule R2 ([M] ++ tail) = [M] ++ tail ++ tail
> applyRule R3 (pre ++ [I, I, I] ++ post) = pre ++ [U] ++ post
> applyRule R4 (pre ++ [U, U] ++ post) = pre ++ post
Note that we do not return a list of derivable strings, as we
did in the Haskell solution. Instead, we use the fact that
functions in Curry are nondeterministic.
Furthermore, we do not need the helper functions `splits` and
`replace` that we used in the Haskell implementation. Instead,
we use the `++`-operator in conjunction with functional
patterns to achieve the same functionality.
Now we implement a utility function `applyRules` for repeated
rule application. Our implementation uses a similar trick as
the famous Haskell implementation of the Fibonacci sequence:
> applyRules :: [Rule] -> Str -> [Str]
> applyRules rules str = tail strs where
>
> strs = str : zipWith applyRule rules strs
The Haskell implementation does not need the `applyRules`
function, but it needs a lot of code about derivation trees
instead. In the Curry solution, derivation trees are implicit,
thanks to nondeterminism.
Derivations
===========
A derivation is a sequence of strings with rules between them
such that each rule takes the string before it to the string
after it. We define types for representing derivations:
> data Deriv = Deriv [DStep] Str
>
> data DStep = DStep Str Rule
>
> showDeriv :: Deriv -> String
> showDeriv (Deriv steps goal) = " " ++
> concatMap showDStep steps ++
> showStr goal ++
> "\n"
>
> showDerivs :: [Deriv] -> String
> showDerivs derivs = concatMap ((++ "\n") . showDeriv) derivs
>
> showDStep :: DStep -> String
> showDStep (DStep origin rule) = showStr origin ++
> "\n-> (" ++
> showRule rule ++
> ") "
Now we implement a function `derivation` that takes two strings
and returns the derivations that turn the first string into the
second:
> derivation :: Str -> Str -> Deriv
> derivation start end
> | start : applyRules rules start =:= init ++ [end]
> = Deriv (zipWith DStep init rules) end where
>
> rules :: [Rule]
> rules free
>
> init :: [Str]
> init free
Finally, we define a function `printDerivations` that
explicitly invokes a breadth-first search to compute and
ultimately print derivations:
> printDerivations :: Str -> Str -> IO ()
> printDerivations start end = do
> searchTree <- getSearchTree (derivation start end)
> putStr $ showDerivs (allValuesBFS searchTree)
You may want to enter
`printDerivations [M, I] [M, I, U]`

at the KiCS2 prompt to see the `derivations` function in action.