The OEIS mourns the passing of Jim Simons and is grateful to the Simons Foundation for its support of research in many branches of science, including the OEIS.
login
The OEIS is supported by the many generous donors to the OEIS Foundation.

 

Logo
Hints
(Greetings from The On-Line Encyclopedia of Integer Sequences!)
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
Sean A. Irvine, Java program (github)
A. Matos, On the number of lines of theorems in the formal system MIU, Universidade do Porto, 2000, 1-10.
Wikipedia, MU Puzzle
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.*)
(* Brian Tenneson, Sep 21 2023 *)
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
alst(maxd=10, v=True) # Michael S. Branicky, Dec 29 2020
CROSSREFS
Cf. A368946, A368953, A369148, A369173 (all MIU strings).
Sequence in context: A001867 A369691 A000998 * A365294 A221182 A109781
KEYWORD
nonn,more
AUTHOR
Brian Tenneson, Jan 19 2020
EXTENSIONS
a(11) from Rémy Sigrist, Feb 26 2020
a(12) from Sean A. Irvine, Mar 20 2020
Name edited by Brian Tenneson, Aug 19 2023
STATUS
approved

Lookup | Welcome | Wiki | Register | Music | Plot 2 | Demos | Index | Browse | More | WebCam
Contribute new seq. or comment | Format | Style Sheet | Transforms | Superseeker | Recents
The OEIS Community | Maintained by The OEIS Foundation Inc.

License Agreements, Terms of Use, Privacy Policy. .

Last modified May 13 11:34 EDT 2024. Contains 372504 sequences. (Running on oeis4.)