monoids, again? or a better bigger, if bigger is better

i've been invited to speak at G'fest08 and was going over my notes to prepare my talk when i spotted something i hadn't before. Here's a presentation of a free monoid on n generators, g1,...,gN.

m,n ::= e | g1 | ... | gN | m*n

the term language must be quotiented by the structural equivalence generated by

m*e=m=e*m, m1*(m2*m3)=(m1*m2)*m3

Now, we could consider the functor category from sets and bi-jections to the category of monoids to arrive at a nifty presentation of a monoid of infinitely many generators, but we can eschew all that machinery in favor of something that's already been worked out and looks cool.

m,n ::= e | x | (new x)m | m*n

Now, for this term language we have a little work to do. Firstly, we have to enrich our equivalence.

(new x)m = (new y)m{y/x} (provided y not in FN(m))
(new x)(new y)m = (new y)(new x)m
(new x)(new x)m = (new x)m
m*(new x)n = (new x)(m*n) (provided x not in FN(m))

where

FN(e) = {}
FN(x) = x
FN((new x)m) = FN(m)\{x}
FN(m*n) = FN(m) U FN(n)

e{y/x} = e
x{y/x} = y
u{y/x} = u
((new u)m){y/x} = (new v)(m{v/u,y/x}), v fresh
(m*n){y/x} = m{y/x}*n{y/x}

Once we get over the charm of repurposing the π-calculus's new operator for this task, there are some flies in the ointment. Of course, we also have to exclude terms with unbound occurrences of variables. What's more troubling about this scheme, however, is that -- if you're like me -- you don't like theories with infinite numbers of atoms, i.e. infinite number of things with no internal structure you can poke an prod. This is like taking on infinitary risk. So... we've got a trick that can help you out.

m,n ::= x | 'x'

x ::= e | m*n

The structural equivalence of this term language is generated by the equations of the finitely presented monoid enriched with on the following rule

m=n => 'm'='n'

Now we have an interesting interpretation we can give to our expressions. We'll warm up to this with a small step. Given the usual arithmetic operations denoted by + and *, let's define two operators

u(+) = 0, u(*) = 1
$(+) = *, $(*) = +

Now, we can define a function [| - |](-) : L(m) x {+,*} -> N as follows

[| e |](a) = u(a)
[| 'm' |](a) = [| m |]($a)
[| m*n |](a) = [| m |](a) a [| n |](a)

It is easy to see that

[| 'e' * ... * 'e' |](+) = n (where n is the number of occurrences of 'e' in the expression)
[| ''e' * ... * 'e'' * ... * ''e' * ... * 'e'' |](*) = n1 * ... * nK (where ni is the number of occurrences of 'e' in the ith term of the expression)

Ok, that's the warm up. For the first act of the main show, we need one more helper function.

#(e) = 0
#('m') = 1 + #(m)
#(m*n) = max(#(m), #(n))

Now, we'll rely on Knuth's up arrow notation; but, we'll write it this way

<| 0 |> = +
<| 1 |> = *
<| 2 |> = (-)^(-)
<| 3 |> = (-)^^(-)
...

allowing us to extend our $ function by

$(<| i |>) = <| i + 1 |>
@(<| i |>) = <| i - 1 |>

and then re-orient our interpretation of quotation inside out

[| 'm' |](a) = [| m |](@a)

[| m |] = [| m |](#(m) + 1 )

Now, like Conway and Knuth, we have a notation for very large numbers. Note, however, that there is a problem with this interpretation because the up arrow notation is notoriously not associative. There is a solution to this. Before i post it, let me see if anyone can crack it.

For the second act, notice that the solution to the following recursive equation is not reachable by the grammar.

u0 = ''e'*u0'

So, let's adjoin it.

m,n ::= x | 'x'

x ::= e | j*k

j,k ::= m | u0

Next, notice that the solution to the following recursive equation is not reachable by this grammar

u1 = '''e'*u0'*u1'

So, let's adjoin it.

m,n ::= x | 'x'

x ::= e | j*k

j,k ::= m | u0 | u1

As you can guess, the process doesn't really have an end. However, we can get a finite presentation of the limit of the process.

m,n ::= x | 'x'

x ::= e | j*k

j,k ::= m | u | rec u.m

This gives us a way to write REALLY large numbers.