Zulip Chat Archive

Stream: maths

Topic: Conway addition thing


view this post on Zulip Kevin Buzzard (Jan 30 2020 at 19:04):

Someone at Xena just asked me how to define addition on the following data structure:

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 19:05):

IMG_20200130_190334916.jpg

view this post on Zulip Scott Morrison (Jan 30 2020 at 19:22):

In some sense, this is already in mathlib, as (particular terms in)pgame.

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 19:32):

Yes, but to actually define addition on the data structure one needs some kind of reduction algorithm to turn the non-standard form of the number back into a number :-/

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 19:32):

In some sense, this is already in mathlib, because mathlib has localisations and so it has Z[1/2]\mathbb{Z}[1/2] :P

view this post on Zulip Mario Carneiro (Jan 30 2020 at 19:35):

first things first, can you define the map from trees to real?

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 19:35):

ha yeah, that took us a while :-)

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 19:36):

You have to rewrite the tree as the integers with a tree hanging off each integer

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 19:36):

and the moment you step off the integers then you're just adding or subtracting 2^{-n}

view this post on Zulip Mario Carneiro (Jan 30 2020 at 20:04):

import data.real.basic

inductive treenum
| leaf
| left (_: treenum)
| right (_: treenum)

inductive treepos
| start : treepos
| left : treepos
| right : treepos
| inner (n : ) : treepos

noncomputable def to_real_aux : treenum  treepos    
| treenum.leaf      _                 r := r
| (treenum.left i)  treepos.start     r := to_real_aux i treepos.left (r - 1)
| (treenum.left i)  treepos.left      r := to_real_aux i treepos.left (r - 1)
| (treenum.left i)  treepos.right     r := to_real_aux i (treepos.inner 2) (r - 1 / 2)
| (treenum.left i)  (treepos.inner n) r := to_real_aux i (treepos.inner (n+1)) (r - 1 / 2 ^ n)
| (treenum.right i) treepos.start     r := to_real_aux i treepos.right (r + 1)
| (treenum.right i) treepos.left      r := to_real_aux i (treepos.inner 2) (r + 1 / 2)
| (treenum.right i) treepos.right     r := to_real_aux i treepos.right (r + 1)
| (treenum.right i) (treepos.inner n) r := to_real_aux i (treepos.inner (n+1)) (r + 1 / 2 ^ n)

noncomputable def treenum.to_real (t : treenum) :  := to_real_aux t treepos.start 0

instance : inhabited treenum := treenum.leaf

noncomputable def treenum.add (t₁ t₂ : treenum) : treenum :=
classical.epsilon $ λ t', t'.to_real = t₁.to_real + t₂.to_real

view this post on Zulip Mario Carneiro (Jan 30 2020 at 20:05):

it's a cheat, of course


Last updated: May 09 2021 at 10:11 UTC