by decide implies Computable

Stream: Is there code for X?

[Bjørn Kjos-Hanssen]

[The suggestion below is wrong as pointed out downthread by Daniel Weber, however a modified version is still open, see below...]

Would this be a suitable additional axiom for Lean in the context where we do not open Classical?
By "suitable" I mean, nobody is likely to be able to prove it or disprove it, but it is presumably true in the intended model of Lean.

import Mathlib.Computability.Partrec

axiom church_turing (f : ℕ → ℕ) [DecidablePred (fun x : Fin 2 → ℕ => f (x 0) = (x 1))] :
  Computable f

For example, this is how one then proves that x => 2*x is computable:

Try this: exact church_turing fun k ↦ 2 * k

[Edward van de Meent]

I think the fact that Classical exists causes this to not be true?

[Daniel Weber]

You mean if we don't have Classical.choice as an axiom?

[Bjørn Kjos-Hanssen]

Yes... or is there a way to express "Decidable in a such a way that by decide will actually decide it"?

[Daniel Weber]

Note that equality on ℕ is always decidable, so your axiom is just that every function is computable

[Daniel Weber]

I don't know much constructive logic, but that should still be false there

[Bjørn Kjos-Hanssen]

Daniel Weber said:

Note that equality on ℕ is always decidable, so your axiom is just that every function is computable

Not true since you also need to find the value of f. There are uncountably many f and only countably many algorithms...

[Daniel Weber]

What do you mean?

import Mathlib.Computability.Partrec

axiom church_turing (f : ℕ → ℕ) [DecidablePred (fun x : Fin 2 → ℕ => f (x 0) = (x 1))] :
  Computable f

lemma all_computable (f : ℕ → ℕ) : Computable f := church_turing f
-- or equivalently
-- lemma all_computable (f : ℕ → ℕ) : Computable f := @church_turing f (fun x ↦ instDecidableEqNat (f (x 0)) (x 1))

-- 'all_computable' depends on axioms: [church_turing, propext, Quot.sound]
#print axioms all_computable

[Bjørn Kjos-Hanssen]

Daniel Weber said:

What do you mean?

import Mathlib.Computability.Partrec

axiom church_turing (f : ℕ → ℕ) [DecidablePred (fun x : Fin 2 → ℕ => f (x 0) = (x 1))] :
  Computable f

lemma all_computable (f : ℕ → ℕ) : Computable f := church_turing f
-- or equivalently
-- lemma all_computable (f : ℕ → ℕ) : Computable f := @church_turing f (fun x ↦ instDecidableEqNat (f (x 0)) (x 1))

-- 'all_computable' depends on axioms: [church_turing, propext, Quot.sound]
#print axioms all_computable

Thanks, that's surprising! Okay but my question remains about predicates for which by decide or #eval can be used ... do they have a name?

[Daniel Weber]

You mean functions which are/aren't marked noncomputable? Note that you can't talk about that in Lean itself, because that's a property of the implementation, not the function.

[Bjørn Kjos-Hanssen]

Well we do talk about it in some sense when we write by decide...

[Daniel Weber]

by decide is equivalent to exact of_decide_eq_true rfl, it just takes a docs#Decidable and checks if it's defeq to true. However, defeq-ness is not a mathematical property, it just a property of Lean's implementation.

[Bjørn Kjos-Hanssen]

Ah but then isn't it a subclass of the computable functions, even if exactly which subclass it is depends on implementation? If so, it could make sense to postulate that these functions are in fact Computable

[Daniel Weber]

It's also not just a property of the function, it's also a property of the implementation:

import Mathlib

def obviously_true : Prop := ∀ n : ℕ, ∃ m > n, Prime m ∧ Prime (m + 2)

section

noncomputable instance inst1 : Decidable obviously_true := Classical.propDecidable _

example : obviously_true := by
  /-
  tactic 'decide' failed for proposition
  obviously_true
  -/
  decide

end

section

theorem obvious : obviously_true := sorry

instance inst2 : Decidable obviously_true := .isTrue obvious

example : obviously_true := by
  decide

end

example : inst1 = inst2 := Subsingleton.elim _ _

[Johan Commelin]

@Yannick Forster can probably give some advice here. He gave a talk in Bonn about (amongst other things) a synthetic approach to (un)decidability. But I don't feel confident commenting about details.

[Benedikt Peterseim]

Similar comment: I’ve heard people talk about how “all functions are computable” holds in the internal language of the so-called effective topos. I’m not quite sure how Lean’s type theory precisely relates to the internal language of toposes (with universes perhaps?), but people seem to treat them as if they were essentially the same. Cf. Johan’s “condensed type theory”. So by that intuition your axiom should be consistent to add.

[Bjørn Kjos-Hanssen]

@Benedikt Peterseim Here's a sense in which not "all functions are computable":

import Mathlib.Computability.Partrec
import Mathlib.Computability.Halting

example : ¬ (∀ f : Nat.Partrec.Code → Bool, Computable f) := by
  have Q :=  @ComputablePred.halting_problem 2
  contrapose Q; simp_all
  unfold ComputablePred
  use (by apply Classical.decPred)
  apply Q

[Johan Commelin]

That proof relies on classical axioms.

[Bjørn Kjos-Hanssen]

OK... well, the question is whether there is a way to have
"not all functions are Computable"
and at the same time postulate
"all functions decided by of_decide_eq_true rfl are Computable."

[Johan Commelin]

I think that might be possible with a tactic.

[Johan Commelin]

But I'm not capable of writing it.

[Bjørn Kjos-Hanssen]

I don't mean to prove
"all functions decided by of_decide_eq_true rfl are Computable"
just to be able to state it in Lean?

[Mario Carneiro]

no you can't state that, this is a quantified definitional equality hypothesis, which doesn't exist in lean

[Mario Carneiro]

what you could prove by a tactic is "all functions expressible as closed terms are Computable"

[Bjørn Kjos-Hanssen]

How do you state
"all functions expressible as closed terms are Computable"?

[Mario Carneiro]

you can't

[Mario Carneiro]

you can state "Function f is Computable" where f is a concrete function given to the tactic as an Expr

[Bjørn Kjos-Hanssen]

If such a tactic were available, would it give a way to automatically prove e.g.

Computable fun k ↦ k * k + 1

(without having to mess with the specifics of how Computable is defined)?

[Mario Carneiro]

yes

[Mario Carneiro]

writing such a tactic would be very challenging though

[Mario Carneiro]

because you basically have to compile all of lean down to turing machines or partial recursive functions or something

[Bjørn Kjos-Hanssen]

#goals

[Violeta Hernández]

A simpler approach is just to show that certain large classes of functions are computable, and that computability is closed under certain wide ranges of operations. "Every primitive recursive function is computable" should already get you a lot of the way.

[Bjørn Kjos-Hanssen]

True although when proving e.g. that if f is Computable then `fun k : ℕ => f k + 1 is Computable we are already beyond primitive recursive functions in a way.

[Bjørn Kjos-Hanssen]

Would the fact that there are only countably many computable functions be worth adding to Mathlib? Here's my proof of it:

import Mathlib.Computability.PartrecCode

instance : Countable {f : ℕ →. ℕ | Nat.Partrec f} := by
  rw [Set.ext <| fun f => @Nat.Partrec.Code.exists_code f]
  apply @Function.Injective.countable
    ({f | ∃ c, Nat.Partrec.Code.eval c = f}) Nat.Partrec.Code _ (fun f => Classical.choose f.2)
  intro f g h
  apply SetCoe.ext
  rw [← Classical.choose_spec f.2,← Classical.choose_spec g.2]
  tauto

instance : Countable {f : ℕ → ℕ | Computable f} :=
  @Function.Injective.countable {f : ℕ → ℕ | Computable f} {f : ℕ →. ℕ | Nat.Partrec f} _
    (fun f => ⟨f.val, Partrec.nat_iff.mp f.2⟩)
    fun _ _ h => SetCoe.ext <| PFun.lift_injective <| (Subtype.mk.injEq _ _ _ _) ▸ h

[Violeta Hernández]

Yes! If we have some way to state there's only countably many computable numbers, that would be great too.

[Bjørn Kjos-Hanssen]

Would need to define "computable real number" first, it seems... :thinking:

[Yannick Forster]

Johan Commelin said:

Yannick Forster can probably give some advice here. He gave a talk in Bonn about (amongst other things) a synthetic approach to (un)decidability. But I don't feel confident commenting about details.

I'm a bit late to the party. In Lean without classical axioms, "all functions are computable" is a fine axiom. In Coq, we at some point worked towards a tactic doing computability proofs automatically. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.17 it worked well-ish. In principle, it should be possible to do something similar if not better for Lean, if somebody wants to chat about that I'd be happy to -- but it would be a major project

[Kevin Buzzard]

Related: Martin Hairer once pointed out to me that without AC it's consistent that all functions are measurable, so there could in theory be a measurability tactic which just checks that the function was defined constructively and then says yes :-) However I would imagine that fun_prop deals with this situation more effectively.

[Floris van Doorn]

I'm not sure how useful that observation is, given that almost anything involving the real numbers is not constructive in Mathlib.

[Yannick Forster]

Kevin Buzzard said:

Related: Martin Hairer once pointed out to me that without AC it's consistent that all functions are measurable, so there could in theory be a measurability tactic which just checks that the function was defined constructively and then says yes :-) However I would imagine that fun_prop deals with this situation more effectively.

Probably one could even write a tactic which given any constructively defined function constructs a proof of measurability -- for the same reason why one can write one that gives computability proofs

[Kevin Buzzard]

His actual observation was that you could also assume countable dependent choice and still have a model with all functions measurable

[Daniel Weber]

This just implies that you can't construct a function which is provably immeasurable, I don't see why it implies that all functions you can construct are provably measurable

[Kevin Buzzard]

Yes I guess you're right. I'll tell Hairer that his papers have holes in.

[Bjørn Kjos-Hanssen]

Violeta Hernández said:

Yes! If we have some way to state there's only countably many computable numbers, that would be great too.

https://github.com/leanprover-community/mathlib4/pull/16935

[Daniel Weber]

Talking about computable numbers, I guess there's a negative to the division by zero convention—it means that the field structure on the computable numbers isn't computable

[Daniel Weber]

What can be done computability for them? NormedCommRing and StrictOrderedCommRing?

[Bjørn Kjos-Hanssen]

Would you define a computable real number as the equivalence class of a computable Cauchy sequence with a computable modulus of convergence?

[Daniel Weber]

That sounds reasonable, yes

[Daniel Weber]

Another option is to define an Real.IsComputable predicate

[Violeta Hernández]

Daniel Weber said:

Talking about computable numbers, I guess there's a negative to the division by zero convention—it means that the field structure on the computable numbers isn't computable

But the set of computable reals is still a field!

[Mario Carneiro]

that depends on what you mean by "field"

[Mario Carneiro]

it's only closed under division by values apart from 0

[Mario Carneiro]

Given a turing machine M, define a real number as 2^-n if M halts in n steps, and 0 if it does not halt. This is a computable real number because you can get an n-digit approximation of it by running M for n steps. But the inverse of this real number is not computable unless you can decide the halting problem for M.

[Daniel Weber]

Assuming em either M halts (and then you can compute this number), or it doesn't, and then the number is 0 which is computable, so the inverse is always computable

[Mario Carneiro]

in this example you don't actually know whether it is even legal to take the inverse unless you solve the halting problem for M. If I tell you it is not equal to 0, then classically we can say that the inverse is well defined and there exists a turing machine outputting the integral value but we don't know what it is

[Daniel Weber]

The inverse is computable if you're promised that the input number is non-zero, i.e. the function inv : (x : Computable) -> x ≠ 0 -> Computable is computable, but there's no computable function inv0 : Computable -> Computable which agrees with it

[Daniel Weber]

Just compute the number with increasing accuracy until you separate it from zero and then it's fairly simple

[Mario Carneiro]

you still need em for that argument

[Mario Carneiro]

the proper intuitionistic version uses "apart from 0" instead of "not equal to 0"

[Mario Carneiro]

i.e. there exists an n such that |x| >= 2^-n

[Mario Carneiro]

but assuming em, there is a lean-computable function Computable -> x != 0 -> Computable

[Daniel Weber]

Mario Carneiro said:

you still need em for that argument

Only for the termination proof, not the computation

[Bjørn Kjos-Hanssen]

By the way, I noticed that Computable.ite is missing in Partrec.lean, maybe worth adding?

theorem ite {c : ℕ → Bool} {f : ℕ → ℕ} {g : ℕ → ℕ}
    (hc : Computable c) (hf : Computable f)
    (hg : Computable g) : Computable fun a => if (c a) then (f a) else (g a)
     := Computable.of_eq (Computable.cond hc hf hg)
      (fun n => by rw [Bool.cond_eq_ite_iff])

[Mario Carneiro]

it's basically the same as cond though with that spelling

[Mario Carneiro]

which btw can be written as bif a then b else c

[Bjørn Kjos-Hanssen]

Right. I just noticed there's Primrec.ite so then I expected to find Computable.ite as well... but had to prove it instead

[Mario Carneiro]

I mean that you are not taking a propositional argument so there is no advantage to using if there, you can just use bif instead

[Bjørn Kjos-Hanssen]

Ah, I see. How about this one instead: #17039

[Violeta Hernández]

Mario Carneiro said:

that depends on what you mean by "field"

Well, the set is closed under all the operations, isn't it? It's just that you can't necessarily decide what they evaluate as

[Daniel Weber]

I think Mario's point is that constructively it's only closed to division by values apart from zero, not by values not equal to it

[Violeta Hernández]

That makes sense. But "the computable numbers are a field" is a claim I've definitely seen before.

[Violeta Hernández]

Like, the function ℕ → ℝ where f n = 0 if the nth turing machine (under some enumeration) halts and f n = 1 otherwise, only takes on computable values, even if it's not itself computable.

[Violeta Hernández]

Something similar should happen for division of computable numbers

[Violeta Hernández]

And that's a result I think would be worth having in Mathlib.

[Daniel Weber]

Violeta Hernández said:

Like, the function ℕ → ℝ where f n = 0 if the nth turing machine (under some enumeration) halts and f n = 1 otherwise, only takes on computable values, even if it's not itself computable.

In this analogy I think what happens is that constructively you can't prove that

[Luigi Massacci]

Violeta Hernández said:

That makes sense. But "the computable numbers are a field" is a claim I've definitely seen before.

Because paper math Field allows to leave division by zero undefined, unlike lean

[Mario Carneiro]

I think the result of the discussion above is that the computable reals are a field, but the computable reals are not a computable field unless you make some subtle tweaks to the definition

[Bjørn Kjos-Hanssen]

You also run into the problem that given a program/code c it is quite hard to tell whether it represents a Cauchy sequence with computable modulus of convergence (something like second iteration of the halting problem, 0'').
Apparently the characterization is that you need a high Turing degree,

$$a'\ge_T 0''$$

(By the way I wrote a whole file about many-one reducibility only to finally discover @Mario Carneiro 's reduce.lean...
looking forward to checking that out though.)

[Mario Carneiro]

did I write something on reducibility?

[Mario Carneiro]

file#Computability/Reduce seems that way

[Bjørn Kjos-Hanssen]

I guess you're the second author. File

[Mario Carneiro]

I think I reviewed this but did not write most of it

[Mario Carneiro]

Bjørn Kjos-Hanssen ☀️ said:

You also run into the problem that given a program/code c it is quite hard to tell whether it represents a Cauchy sequence with computable modulus of convergence

But generally you won't be asked to determine this in the first place. Obviously determining whether a given real is computable is also hard

[Mario Carneiro]

I think you would just bake into the definition that a computable real is one for which there is a turing machine which spits out approximations with a fixed modulus of convergence (e.g. 2^-n)

[Bjørn Kjos-Hanssen]

Usually in computability theory we say a structure A is computable if it has domain Nat and all functions and relations on A are computable.

[Bjørn Kjos-Hanssen]

There's no computable structure with operations +, * (of course, not the usual such operations on Nat) that's isomorphic to the computable reals (by the paper I linked to)

[Mario Carneiro]

isomorphic to the computable reals sounds like it is asking for too much, in particular it will be a surjection onto the computable reals and not a bijection because equality is not decidable

[Mario Carneiro]

but also having domain Nat sounds like too much to ask for, this is a total function between subtypes of Nat

[Mario Carneiro]

i.e. it is only required to have sensible behavior on inputs satisfying a condition, not necessarily decidable, but all such inputs have to produce elements in the target satisfying the condition

[Mario Carneiro]

This is the natural notion you get out of the type theoretic reading of computability

[Mario Carneiro]

I think I basically disagree with the definition in that presentation, or at least, it's not sufficiently considering what it means to have computable functions on types that are not Nat

[Bjørn Kjos-Hanssen]

Maybe we can call your notion "computable relative to the domain" or "given the domain"

[Mario Carneiro]

what would it mean for a function to be computable not relative to its own domain?

[Mario Carneiro]

This is just like the observation that $x\in\mathbb{R}\setminus\{0\}\mapsto 1/x : \mathbb{R}\setminus\{0\}$ is a continuous function

[Bjørn Kjos-Hanssen]

I mean, the indicator function for the halting set, restricted to the halting set, is computable given its domain, i.e., it is the constant function 1 on its domain. But its graph is not computable in the ambient space.

[Mario Carneiro]

relative to a larger domain, it is a partial function and therefore not computable but partial recursive, but that's a different function we're talking about

[Mario Carneiro]

Bjørn Kjos-Hanssen ☀️ said:

I mean, the indicator function for the halting set, restricted to the halting set, is computable given its domain, i.e., it is the constant function 1 on its domain. But its graph is not computable in the ambient space.

I think it is fair to say that the halting problem is decidable when restricted to turing machines that halt

[Bjørn Kjos-Hanssen]

For a computable field we should (acc. to common definition) be able to write down multiplication and addition tables showing how the elements interact... but for the computable reals you don't know what the elements are and you can't.

[Mario Carneiro]

For addition and multiplication I fail to see the issue?

[Mario Carneiro]

You can calculate approximations within any given precision given TMs for the inputs which provide approximations within any given precision

[Mario Carneiro]

I mean it's not really a table so much as a functional program but you can write it down

[Mario Carneiro]

this is how exact real arithmetic libraries work

[Bjørn Kjos-Hanssen]

Suppose I wanted to know if there's a square root of 2 in a given field. In a computable field I can fix my 1 and then 2=1+1 and then check all the x's one at a time. If there's an x with x^2=2 I eventually find it.
In a field where I don't know the domain, I can't do that [of course in the computable reals we know sqrt(2) exists but I think you see my point]

[Mario Carneiro]

no I don't think I do see your point. Enumeration is not the way to construct computable reals

[Mario Carneiro]

because it implies that "checking" is even a thing you can do

[Mario Carneiro]

What you are showing is that a particular bad algorithm doesn't work, that doesn't show that no algorithm exists

[Mario Carneiro]

and indeed one does exist, you can implement square root on computable reals too

[Bjørn Kjos-Hanssen]

Okay how about this.... the structure $Q := (\mathbb Q,+,\cdot)$ is computable in the sense that there exist computable functions $f$ and $g$ on $\mathbb N$ such that $Q$ is isomorphic to $(\mathbb N,f,g)$. In that same sense, the structure $(\text{ComputableReals},+,\cdot)$ is not computable. That's an interesting difference (to some people, part of the time...) but what you want to call it is of course a sociological question.

[Bjørn Kjos-Hanssen]

($\mathbb N$ could be replaced by $\{0,1\}^*$ (finite strings) or your favorite nice discrete type here)

[Mario Carneiro]

that definition explicitly excludes any type Q which is not bijective with Nat, and even for those that are denumerable it doesn't allow for types that have complex well formedness conditions and/or have no natural bijection to Nat

[Mario Carneiro]

There are plenty of examples like "the strings accepted by regular language $L$" which, even if they are denumerable, would result in a bijection so complex that the asymptotic complexity of basic operations is thrown completely off

[Mario Carneiro]

which is why I argue that this is the wrong definition

[Bjørn Kjos-Hanssen]

How hard would it currently be to prove this kind of thing, i.e., basic computability facts in non-Nat types?

import Mathlib.Computability.PartrecCode
import Mathlib.Computability.Halting
import Mathlib.Computability.Primrec

def get_part (σ : List Bool) (k : ℕ) : Part Bool := σ.get? k

example : Partrec₂ get_part := sorry

[Mario Carneiro]

There are plenty of such proofs in Computability.Partrec

[Mario Carneiro]

Note that your function is actually the composition of a primitive recursive function yielding Option Bool and the coercion from Option A to Part A, which is probably proved in there although I forget

[Mario Carneiro]

I'm pretty sure get? is proved primrec

[Mario Carneiro]

oh yes this is the composition of docs#Computable.ofOption and docs#Primrec.list_get?

[Bjørn Kjos-Hanssen]

Thanks! Sometimes, I search but I don't read...

example : Partrec₂ get_part := by
  apply Computable.ofOption
  apply Computable.list_get?