search

vikraman / 2DTypes

Collaborative work on reversible computing
17 stars 1 forks source link

Prove quote-eval^₁ #20

Closed inexxt closed 3 years ago

JacquesCarette commented 3 years ago

Just to 'ack' that I've seen this, and ramping up to be able to work on it.

JacquesCarette commented 3 years ago

Ok, I've been thinking about this.

  1. Pi -> transpositions seems doable. Seems the simplest route is to go through Fin n, i.e. normalize first.
  2. tranpositions -> Pi, is naturally already over Fin n, also seems doable
  3. transp -> Pi -> transp being equivalent to 'the identity' is probably ok
  4. Pi -> transp -> Pi being 2-equivalent to id seems... extremely difficult.

The road to this seems to be best done via having a normal form for Pi combinators (i.e. exactly what @sabry is currently working on).

I still don't see why transpositions would be any easier/harder than Lehmer codes (say). The hard part will still be the equivalent to item 4 above.

inexxt commented 3 years ago

As far as I understand, @sabry is trying to express a combinator in terms of transpositions, not to calculate its normal form - this is exactly what the Coxter/ part of the proof is supposed to do.

JacquesCarette commented 3 years ago

The code that I've seen being checked-in says otherwise!

inexxt commented 3 years ago

Almost solved, the remaining case is going from Pi to Pi^ and back. A separate issue has been created for that #77