Generate similar but not equal type

Stream: Machine Learning for Theorem Proving

[Joachim Hauge]

Given a type A the task is to find a type B and maps f:A->B, g:B->A minimizing the sum of lengths of f and g. You are also not allowed to pick B=A.

So in logical terms the task is to find a statement different from a given statement but that is transparently logically equivalent to it.

Is there a program that can solve this task? Were similar things considered in the literature?

[Kevin Buzzard]

I choose B = id A

[Joachim Hauge]

Kevin Buzzard said:

I choose B = id A

Does id mean the identity on the universe? That's judgmentally equal to A. I meant you aren't allowed to pick judgmentally equal things.

[Kevin Buzzard]

Ok I choose the subtype of option A corresponding to A

[Joachim Hauge]

OK I don't know all the details of Lean's pattern matching. Let's say you are only allowed to use Pi-types, Sigma-types, the natural numbers, axiom choice and law of excluded middle. Can you still trivialize this game?

[Shing Tak Lam]

Doesn't B = unit -> A work?

[Joachim Hauge]

Shing Tak Lam said:

Doesn't B = unit -> A work?

It does. OK as stated this game is nonsense. I think there maybe a fix via homotopy type theory (have two players where one player can shoot down the proposals (B, f, g) of the other if they can exhibit an equivalence h:A->B of similar length).

[Kevin Buzzard]

In homotopy type theory if f and g are inverses then I'm afraid B = A by the univalence axiom!

[Joachim Hauge]

Kevin Buzzard said:

In homotopy type theory if f and g are inverses then I'm afraid B = A by the univalence axiom!

No in the homotopy version we would allow A=B but we would impose an upper limit on the lengths of the definitions of the equivalences (e.g. any provable proposition is equal to 1 but the length of the minimum equivalence can be large).

[Jason Rute]

@Joachim Hauge what is the motivation for this game?

[Joachim Hauge]

Jason Rute said:

Joachim Hauge what is the motivation for this game?

No particular motivation. I am just trying to think of ways to make reinforcement learning algorithms think non-trivial thoughts other than "here is a statement, prove or disprove it".