|
|
A331536
|
|
Number of theorems in the MIU formal system which can be proved in n steps or fewer starting with the axiom 'mi'.
|
|
7
|
|
|
1, 3, 6, 11, 25, 69, 282, 1730, 15885, 210105, 3986987, 106053474
(list;
graph;
refs;
listen;
history;
text;
internal format)
|
|
|
OFFSET
|
1,2
|
|
COMMENTS
|
The MIU system was invented by Douglas Hofstadter and is found in his book Gödel, Escher, Bach.
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.
1) Append a 'u' to a word ending in 'i'.
2) Append a word to itself, excluding the initial 'm'.
3) Replace an occurrence of 'iii' by 'u'.
4) Remove an occurrence of 'uu'.
|
|
LINKS
|
|
|
EXAMPLE
|
The a(2) = 3 words that can be reached in at most one step are mi, miu, mii.
The a(3) = 6 words that can be reached in at most two steps are mi, miu, mii, miiii, miiu, miuiu.
|
|
MATHEMATICA
|
MIURules = {StartOfString ~~ x : ___ ~~ "I" ~~ EndOfString :> x <> "IU", StartOfString ~~ "M" ~~ x : ___ ~~ EndOfString :> "M" <> x <> x, "III" :> "U", "UU" :> ""}; (*The rules of the MIU formal system*)
MIUNext[s_String, rule_Integer] :=StringReplaceList[s, MIURules[[rule]]]
g[x_]:=DeleteDuplicates[Flatten[Join[{x}, Table[Table[MIUNext[x[[j]], n], {n, 1, 4}], {j, 1, Length[x]}]]]]
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.*)
|
|
PROG
|
(Python)
def occurrence_swaps(w, s, t):
out, oi = [], w.find(s)
while oi != -1:
out.append(w[:oi] + t + w[oi+len(s):])
oi = w.find(s, oi+1)
return out
def moves(w): # moves for word w in miu system
nxt = [w + w] # Rule 2 ('m' not stored; else use nxt = [w + w[1:]])
if w[-1] == 'i': nxt.append(w + 'u') # Rule 1
nxt.extend(occurrence_swaps(w, 'iii', 'u')) # Rule 3
nxt.extend(occurrence_swaps(w, 'uu', '')) # Rule 4
return nxt
def alst(maxd=float('inf'), v=False):
alst, d = [], 0
reached, frontier = {'i'}, {'i'} # don't store 'm's (else use 'mi' twice)
alst.append(len(reached))
if v: print(len(reached), end=", ")
while len(frontier) > 0 and d < maxd:
reach1 = set(m for p in frontier for m in moves(p) if m not in reached)
if v: print(len(reached)+len(reach1), end=", ")
alst.append(len(reached)+len(reach1))
reached |= reach1
frontier = reach1
d += 1
return alst
|
|
CROSSREFS
|
|
|
KEYWORD
|
nonn,more
|
|
AUTHOR
|
|
|
EXTENSIONS
|
|
|
STATUS
|
approved
|
|
|
|