login
Number of theorems in the MIU formal system which can be proved in n steps or fewer starting with the axiom 'mi'.
7

%I #57 Aug 06 2024 11:15:06

%S 1,3,6,11,25,69,282,1730,15885,210105,3986987,106053474

%N Number of theorems in the MIU formal system which can be proved in n steps or fewer starting with the axiom 'mi'.

%C The MIU system was invented by Douglas Hofstadter and is found in his book Gödel, Escher, Bach.

%C In the MIU system words begin with the letter 'm' with the remaining letters being either 'u' or 'i'. Essentially, words can be represented by binary strings. It is given that 'mi' is a word. Thereafter, at each step words may be transformed by one of the following rules.

%C 1) Append a 'u' to a word ending in 'i'.

%C 2) Append a word to itself, excluding the initial 'm'.

%C 3) Replace an occurrence of 'iii' by 'u'.

%C 4) Remove an occurrence of 'uu'.

%H Sean A. Irvine, <a href="https://github.com/archmageirvine/joeis/blob/master/src/irvine/oeis/a331/A331536.java">Java program</a> (github)

%H A. Matos, <a href="https://citeseerx.ist.psu.edu/pdf/2732f13f008cd209e9dee35b56c53415ab29398a">On the number of lines of theorems in the formal system MIU</a>, Universidade do Porto, 2000, 1-10.

%H Wikipedia, <a href="https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach">Gödel, Escher, Bach</a>

%H Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>

%H <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>

%e The a(2) = 3 words that can be reached in at most one step are mi, miu, mii.

%e The a(3) = 6 words that can be reached in at most two steps are mi, miu, mii, miiii, miiu, miuiu.

%t MIURules = {StartOfString ~~ x : ___ ~~ "I" ~~ EndOfString :> x <> "IU", StartOfString ~~ "M" ~~ x : ___ ~~ EndOfString :> "M" <> x <> x, "III" :> "U", "UU" :> ""}; (*The rules of the MIU formal system*)

%t MIUNext[s_String, rule_Integer] :=StringReplaceList[s, MIURules[[rule]]]

%t g[x_]:=DeleteDuplicates[Flatten[Join[{x},Table[Table[MIUNext[x[[j]],n], {n, 1, 4}],{j, 1,Length[x]}]]]]

%t a[n_Integer]:=Nest[g, "MI", n] // Length (*a[n] gives the number of theorems that can be proved in n steps or fewer. A331536[n]=a[n]. Remove //Length if you wish to see the theorems being counted.*)

%t (* _Brian Tenneson_, Sep 21 2023 *)

%o (Python)

%o def occurrence_swaps(w, s, t):

%o out, oi = [], w.find(s)

%o while oi != -1:

%o out.append(w[:oi] + t + w[oi+len(s):])

%o oi = w.find(s, oi+1)

%o return out

%o def moves(w): # moves for word w in miu system

%o nxt = [w + w] # Rule 2 ('m' not stored; else use nxt = [w + w[1:]])

%o if w[-1] == 'i': nxt.append(w + 'u') # Rule 1

%o nxt.extend(occurrence_swaps(w, 'iii', 'u')) # Rule 3

%o nxt.extend(occurrence_swaps(w, 'uu', '')) # Rule 4

%o return nxt

%o def alst(maxd=float('inf'), v=False):

%o alst, d = [], 0

%o reached, frontier = {'i'}, {'i'} # don't store 'm's (else use 'mi' twice)

%o alst.append(len(reached))

%o if v: print(len(reached), end=", ")

%o while len(frontier) > 0 and d < maxd:

%o reach1 = set(m for p in frontier for m in moves(p) if m not in reached)

%o if v: print(len(reached)+len(reach1), end=", ")

%o alst.append(len(reached)+len(reach1))

%o reached |= reach1

%o frontier = reach1

%o d += 1

%o return alst

%o alst(maxd=10, v=True) # _Michael S. Branicky_, Dec 29 2020

%Y Cf. A368946, A368953, A369148, A369173 (all MIU strings).

%K nonn,more

%O 1,2

%A _Brian Tenneson_, Jan 19 2020

%E a(11) from _Rémy Sigrist_, Feb 26 2020

%E a(12) from _Sean A. Irvine_, Mar 20 2020

%E Name edited by _Brian Tenneson_, Aug 19 2023