A331536 Number of theorems in the MIU formal system which can be proved in n steps or fewer starting with the axiom 'mi'.
1, 3, 6, 11, 25, 69, 282, 1730, 15885, 210105, 3986987, 106053474
Offset: 1
Examples
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.
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, Gödel, Escher, Bach
- Wikipedia, MU Puzzle
- Index entries for sequences from "Goedel, Escher, Bach"
Programs
-
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 *) -
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
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
Comments