non-computable non-non-computables?

Stream: Equational

[Cody Roux]

Silly lean question; can defs not marked with noncomputable actually be non-computable?

[Shreyas Srinivas]

noncomputable lean defs are ones that use an axiom (usually choice). So their meaning is "you are using a theorem that says you get a data object of your type, but doesn't really tell you how to pick this object". Non-noncomputable defs have to be total and provably terminating, so I don't see how you can encode a non-computable function in it.

[Joachim Breitner]

Fair point, so the last bullet may already be given.

[Alex Meiburg]

Shreyas Srinivas said:

noncomputable lean defs are ones that use an axiom (usually choice). So their meaning is "you are using a theorem that says you get a data object of your type, but doesn't really tell you how to pick this object". Non-noncomputable defs have to be total and provably terminating, so I don't see how you can encode a non-computable function in it.

Defs that aren't noncomputable don't actually have to be terminating, that's a common misconception. This is due to how partial functions work in Lean. They exist, and the guarantee is just that they don't violate the type safety, so I can't have a partial function that returns a {x:Nat // And (IsSquare x) (Prime x)}, since there's no data of that type. But I can have a define a partial function that returns how many steps an (arbitrary, possibly non-halting) Turing machine takes to halt, and prove that this is what it computes. This doesn't compromise any safety because the mere existence of this information doesn't let me prove False.

And, this data can then be used in a later definition that isn't partial, there wouldn't be any external indicator that this function doesn't terminate.

[Shreyas Srinivas]

I am completely ignoring partial since one can't prove anything about them

[Shreyas Srinivas]

In the context of the discussion, I think Joachim was trying to prove something about the implication graph

[Shreyas Srinivas]

But yeah it is new to me that you can plug in a partial def into a non-partial one

[Shreyas Srinivas]

And still prove anything with this def

[Joachim Breitner]

Once we have https://github.com/leanprover/lean4/issues/3119 we can even have (some) genuinely non-terminating functions and still do all the proofs we want about them.

[Mario Carneiro]

Cody Roux said:

Silly lean question; can defs not marked with noncomputable actually be non-computable?

Yes, it's actually trivial to do so:

partial def choice {α} : Nonempty α → α := choice

[Mario Carneiro]

We can even formally prove it using mathlib:

import Mathlib.Computability.Halting

partial def choice {α} : Nonempty α → α := choice

open Nat.Partrec
def haltingFunction (c : Code) : Bool :=
  @decide (Code.eval c 0).Dom <| choice <| Classical.instNonemptyDecidable _

theorem haltingFunction_not_computable : ¬Computable haltingFunction :=
  fun h => ComputablePred.halting_problem 0 ⟨_, h⟩

[Shreyas Srinivas]

What's the decision procedure for classical.instNonEmptyDecidable?

[Cody Roux]

it's a pattern match on the excluded middle, which itself is proven using choice

[Cody Roux]

I'm sad that noncomputable isn't as "sticky" as I thought, I'm not entirely sure why partial isn't.

[Mario Carneiro]

What non-noncomputable actually means is that the lean compiler can generate code for the definition. Because there is no assumption that the code be terminating, it is always possible to trivially implement any axiom via looping on every input; it's a "courtesy" that this is not done and instead you get a compilation error if you try to call Classical.choice in your program, because this is presumably more useful than just wasting CPU cycles.

[Mario Carneiro]

The reason partial is not a viral marker is because it's not really marking the partiality, it's marking the opaqueness. A partial definition is not provably equal to its unfolding

[Mario Carneiro]

You can of course implement a metaprogram to check for transitive usage of opaques or partial definitions; see link and the transitive links

[Cody Roux]

Ok, so either we need to do this check, or "promise" not to use partial in the "final end-to-end theorem" definition.

[Mario Carneiro]

sorry, I am missing the context here. In what way do you think this relates to the final theorem?

[Mario Carneiro]

I didn't think computability (in the mathematical sense) was on the agenda

[Alex Meiburg]

I'm not even sure what that would mean here. We're proving theorems, not providing a calculation. Surely we're not aiming to prove everything constructively (i.e. without using the law of excluded middle).

[Vlad Tsyrklevich]

The final calculation is trying to prove statements like A=>B OR NOT (A=>B) so LEM is somewhat of a hinderance there

[Cody Roux]

We're trying to say: here is a complete, concrete graph of all implications and non-implications. No need to stare at it, it's huge, but trust us it is both complete and concretely given.

[Cody Roux]

If we just say "there exists such a graph" then perhaps people might be less than impressed, since it's easy to prove it exists.

[Cody Roux]

This happens all the time in classification problems.

[Sébastien Gouëzel]

Using choice or LEM to prove things about whether some implications are true or false does not change anything to the concreteness of the graph, which is completely explicit here.

[Cody Roux]

I know that, but does the casual reader know this? How do they know it?

[Alex Meiburg]

I see. You'd like to see some final result that's something like

/-- The implication graph, as an adjacency matrix --/
def doesImply (eqA eqB : Fin 4695) : Bool := < ... something computable ... >

theorem doesImply_correct (eqA eqB : Fin 4695) : doesImply eqA eqB \iff ↔ (Equation eqA → eqB) := by
   < ... proof of correctness ... >

and that way, anyone who wants to see that the project is complete, would just have to verify that (1) doesImply_correct doesn't depend on sorryAx, and (2) that doesImply is a computable function.

And the concern is that doesImply could just be defined in terms of e.g. whether a particular Turing machine halts or not, without being marked noncomputable, and then we could have cheated and "skipped" the whole project.

[Mario Carneiro]

I think the right way to present this is something like "here is a concrete list of implications and non-implications, and here is a proof that the transitive closure of these generates the whole graph"

[Mario Carneiro]

"oh and here's a function if you want to query parts of it"

[Joachim Breitner]

Mario Carneiro said:

I think the right way to present this is something like "here is a concrete list of implications and non-implications, and here is a proof that the transitive closure of these generates the whole graph"

That list will be large and possibly generated by a tactic, so the user cannot just eyeball it to see that it really is concrete (and not produced with Classical.choose), hence the musing of whether there is a more declarative way of saying “this function or this data is concrete/computable/whatever”, besides #print.

[Mario Carneiro]

It should be specified by some actually explicit list together with some closure algorithm which may do more than just implication chaining but also duals and I don't know what else

[Eric Wieser]

Mario Carneiro said:

We can even formally prove it using mathlib:

This sounds like a nice result for the Counterexamples directory

[Eric Wieser]

regarding the completeness of the graph, could the statement be something like

def theRawData : Matrix (Fin _) (Fin _) Bool := read_matrix% "implications.txt"

theorem as_closure : theRawData = closureOf (someSmallerData) := sorry

theorem : theRawData i j \iff implies i j := by
  rw [as_closure]
  sorry

[Eric Wieser]

Then you just need to trust read_matrix%, which is hopefully very trivial

[Mario Carneiro]

the trouble is that this formulation is very likely to crash lean

[Mario Carneiro]

because theRawData is an object with 22 million entries

[Mario Carneiro]

maybe it would be okay if you encoded it as a bitvector in a string literal or bignum? but even then you'll be stuck trying to prove anything about it without an explosion in term size

[Eric Wieser]

22 million bits is only 2.76 megabytes, so storing it as a bitvector and proving facts about it via halving it 25 times could work

[Eric Wieser]

Maybe you need ofReduceBool for this to work

[Mario Carneiro]

never underestimate lean's ability to use more memory than a napkin calculation would suggest :skull:

[Amir Livne Bar-on]

Alex Meiburg said:

I can have a define a partial function that returns how many steps an (arbitrary, possibly non-halting) Turing machine takes to halt, and prove that this is what it computes. This doesn't compromise any safety because the mere existence of this information doesn't let me prove False.

Can't you define a proof sequence of False using this method? With functions conclusion : ProofSeq -> Prop and embed : (seq : ProofSeq) -> (term : conclusion seq)? Or even if such embedding is not possible in Lean, it would prove that first-order logic formalized in Lean is inconsistent?

[Joachim Breitner]

Eric Wieser said:

22 million bits is only 2.76 megabytes, so storing it as a bitvector and proving facts about it via halving it 25 times could work

That’s what I am experimenting in https://github.com/teorth/equational_theories/pull/636 with, zulip thread #Equational > A final end-to-end theorem in Lean

[Alex Meiburg]

Amir Livne Bar-on said:

Can't you define a proof sequence of False using this method? With functions `conclusion : ProofSeq -> Prop` and `embed : (seq : ProofSeq) -> (term : conclusion seq)`? Or even if such embedding is not possible in Lean, it would prove that first-order logic formalized in Lean is inconsistent?

Sorry, I should say, "it computes how many steps it takes to halt, if it halts; otherwise it returns -1". That was implied in my head (because Lean has a number of functions that do something similar of returning junk "if something never happens") but I should have been more explicit.

No, it's not something that implies it's inconsistent.

[Amir Livne Bar-on]

This presumably requires choice though? So we can detect such non-computable definitions by their axioms

[Amir Livne Bar-on]

Oh I see, there's also the partial loophole, so no need for choice

[Mario Carneiro]

Note that the partial loophole is secretly using choice

[Mario Carneiro]

I mean, that should be pretty obvious because it gives you a value with the same type as Classical.choice

[Mario Carneiro]

partial def foo : α → α := foo
#print axioms foo -- 'foo' does not depend on any axioms

partial def bar : Nonempty α → α := bar
#print axioms bar -- 'bar' depends on axioms: [Classical.choice]

[Mario Carneiro]

Here's the secret definition they don't want you to know:

partial def bar : Nonempty α → α := bar

open Lean
run_meta -- fun {α} a => Classical.ofNonempty
  let some (.opaqueInfo c) := (← getEnv).find? `bar | failure
  logInfo c.value

[Amir Livne Bar-on]

So here
https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/non-computable.20non-non-computables.3F/near/477706720
item (2) would be a statement that doesImply does not depend on AoC

[Amir Livne Bar-on]

That is, assuming that the DB constructed by equational_result doesn't depend on the axioms used by the theorems

[Amir Livne Bar-on]

I guess the greedy construction can be done without choice, so we don't actually need it in the proofs yet