A program that derives strings in Hofstadter's MIU-system in a brainless (but idiomatic Go) manner.

miu.go

// Warning: eats memory quickly.
// Resource limiting recommended.
package main

import (
    "fmt"
    "os"
    "strings"
)

var rules map[int]func(string, chan<- string) = map[int]func(string, chan<- string){
    // Rule I: If you possess a string whose last letter is I,
    // you can add on a U at the end.
    1: func (s string, out chan<- string) {
            if s[len(s)-1] == 'I' {
                out <- s + "U"
            }
        },

    // Rule II: Suppose you have Mx.
    // Then you may add Mxx to your collection.
    2: func (s string, out chan<- string) {
            if s[0] == 'M' {    // originally omitted! ha!
                x := s[1:len(s)]
                out <- s + x
            }
        },

    // Rule III: If III occurs in one of the strings in your
    // collection, you may make a new string with U in place of III.
    3: func (s string, out chan<- string) {
            var head, tail string
            tail = s

            i := strings.Index(tail, "III")
            for ; i >= 0 ; i = strings.Index(tail, "III") {
                out <- head + tail[0:i] + "U" + tail[i+3:]
                head = head + tail[0:i+1]
                tail = tail[i+1:]
            }
        },

    // Rule IV: If UU occurs inside one of your strings,
    // you can drop it.
    4: func (s string, out chan<- string) {
            var head, tail string
            tail = s

            i := strings.Index(s, "UU")
            for ; i >= 0 ; i = strings.Index(tail, "UU") {
                out <- head + tail[0:i] + tail[i+2:]
                head = head + tail[0:i+1]
                tail = tail[i+1:]
            }
        },
}

func generate(in <-chan string, out chan<- string) {
    var s string
    for {
        s = <-in
        for _, f := range rules {
            go f(s, out)
        }
    }
}

func main() {
    theorems := make(chan string, 1024)
    input := make(chan string)

    go generate(input, theorems)
    fmt.Println("MI (axiom)")
    input <- "MI"

    var thm string
    for {
        thm = <-theorems
        fmt.Println(thm)
        if thm == "MU" { os.Exit(0) }
        input <- thm
    }
}

miu.overkill.go

package main

import (
    "container/list"
    "fmt"
    "os"
    "strings"
)

type Step struct {
    Value string
    Rule int
}

func (s Step) String() string { return s.Value }

type Theorem struct {
    Derivation *list.List
    Current *list.Element
    Step
}

func (t *Theorem) Derive(thm string, via int) *Theorem {
    step := Step{Value: thm, Rule: via}
    return &Theorem{
        Derivation: t.Derivation,
        Current: t.Derivation.PushBack(step),
        Step: step,
    }
}

func (t *Theorem) Trace() {
    fmt.Println(t)
    for el := t.Current.Prev(); el != nil; el = el.Prev() {
        step := el.Value.(Step)
        fmt.Printf("  by rule %d from %s\n", step.Rule, step.Value)
    }
}

var rules map[int]func(*Theorem, chan<- *Theorem) = map[int]func(*Theorem, chan<- *Theorem){
    // Rule I: If you possess a string whose last letter is I,
    // you can add on a U at the end.
    1: func (t *Theorem, out chan<- *Theorem) {
            s := t.String()
            if s[len(s)-1] == 'I' {
                out <- t.Derive(s + "U", 1)
            }
        },

    // Rule II: Suppose you have Mx.
    // Then you may add Mxx to your collection.
    2: func (t *Theorem, out chan<- *Theorem) {
            s := t.String()
            if s[0] == 'M' {
                x := s[1:len(s)]
                out <- t.Derive(s + x, 2)
            }
        },

    // Rule III: If III occurs in one of the strings in your
    // collection, you may make a new string with U in place of III.
    3: func (t *Theorem, out chan<- *Theorem) {
            var head, tail string
            tail = t.String()

            i := strings.Index(tail, "III")
            for ; i >= 0 ; i = strings.Index(tail, "III") {
                out <- t.Derive(head + tail[0:i] + "U" + tail[i+3:], 3)
                head = head + tail[0:i+1]
                tail = tail[i+1:]
            }
        },

    // Rule IV: If UU occurs inside one of your strings,
    // you can drop it.
    4: func (t *Theorem, out chan<- *Theorem) {
            var head, tail string
            tail = t.String()

            i := strings.Index(tail, "UU")
            for ; i >= 0 ; i = strings.Index(tail, "UU") {
                out <- t.Derive(head + tail[0:i] + tail[i+2:], 4)
                head = head + tail[0:i+1]
                tail = tail[i+1:]
            }
        },
}

func generate(in <-chan *Theorem, out chan<- *Theorem) {
    var t *Theorem
    for {
        t = <-in
        for _, f := range rules {
            go f(t, out)
        }
    }
}

func main() {
    theorems := make(chan *Theorem, 1024)
    input := make(chan *Theorem)

    go generate(input, theorems)
    fmt.Println("MI (axiom)")

    derivation := list.New()
    step := Step{Value: "MI", Rule: 0} // TODO this is a hack
    input <- &Theorem{
        Derivation: derivation,
        Current: derivation.PushBack(step),
        Step: step,
    }

    var thm *Theorem
    for {
        thm = <-theorems
        fmt.Println(thm)
        if thm.String() == "MU" {
            thm.Trace() // time to track down a bug...
            os.Exit(0)
        }
        input <- thm
    }
}