Computability

Stream: new members

[Kenny Lau]

def asdf : subtype (λ n : set ℕ, true) :=
⟨@classical.epsilon (set ℕ) ⟨∅⟩ (λ s, true), trivial⟩

noncomputable def ghjk : subtype (λ n : set ℕ, true) :=
@classical.epsilon (subtype (λ n : set ℕ, true)) ⟨⟨∅, trivial⟩⟩ (λ s, true)

Why is the first one computable but not the second one?

[Kenny Lau]

"why" as in the mechanism behind

[Chris Hughes]

Because Sorts are always computable. In the first one you defined a nat - > Prop using choice, and the second one you defined an element of some subtype with choice.

[Chris Hughes]

I think.

[Brandon B]

I have more questions about the computational interpretation of classical logic in type theory. I am making a new topic to separate from the rest. I am reposting my original question and some replies.

Original post:
"I was reading Kevin Buzzard's recent post "Proofs are not programs" < https://xenaproject.wordpress.com/2019/06/15/proofs-are-not-programs/ > which argues that only in constructive logic is the Curry-Howard correspondence held (proofs are programs) and that in general in ZFC with the axiom of choice and excluded middle etc that Curry-Howard does not apply; which is why is why in lean we label certain things as noncomputable. However, looking at https://en.wikipedia.org/wiki/Lambda-mu_calculus it seems to suggest that there are more sophisticated lambda calculi that can model "classical logic" with excluded middle etc and still maintain a form of the curry-howard correspondence. Is lean's type system CoC just not rich enough to model classical deductions with computational content?"

[Brandon B]

reply: "Andrew Ashworth5:05 PM
urgh, if you really want to go into gory detail, you could try chapter 8 of http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf "

[Brandon B]

reply: "Mario Carneiro6:06 PM
The basic idea behind computational semantics for EM (or more simply, double negation elimination) is that you put everything in continuation passing style, the logical equivalent being putting double negations on everything, and then all the classical theorems become intuitionistically provable, and the computational semantics are that of call/cc or exception handling.

If you wanted to do something similar with full choice, I think you could do it like so: Suppose you want to produce an element of type A satisfying p. Save the current continuation, and then start enumerating well formed terms of type A. Return the first one you find (whether or not it satisfies p). Later, the program may later discover that you lied to it and will prove that the element does not in fact satisfy p, deriving a contradiction. When you call false.elim on this proof of false, the eliminator goes back to the original continuation, "rewinding the universe" to the original state, whereupon it tries the next term it finds.

This should satisfy type correctness, but it is not strongly normalizing as you might be enumerating terms forever looking for one that satisfies p."

[Brandon B]

My sense so far is that a type theory that models constructive logic yields a programming language where all programs are guaranteed to terminate, which comes at the expense of certain classes programs not being definable at all (namely those that cannot be proven to terminate). Whereas, classical logic with LEM allows non-terminating programs, expanding the universe of definable programs at the expense of not being able to verify if a defined program will ever finish a computation. Is that on the right track?

[Nam]

on this note, is it possible to extract / compile Lean code into executable code that can be linked with, say, C/C++? the last i found on this subject was in 2018 and someone mentioned Lean 4 would have this feature. is that still on? is there any sample extraction?

[Mario Carneiro]

My sense so far is that a type theory that models constructive logic yields a programming language where all programs are guaranteed to terminate, which comes at the expense of certain classes programs not being definable at all (namely those that cannot be proven to terminate).

Well, any type theory models a constructive logic. The ones that have nonterminating programs just have an inconsistent constructive logic

[Mario Carneiro]

Whereas, classical logic with LEM allows non-terminating programs, expanding the universe of definable programs at the expense of not being able to verify if a defined program will ever finish a computation.

LEM doesn't give you nonterminating programs. The double negation elimination method mentioned in the books still yields a strongly normalizing system. The one I mentioned for full choice doesn't, but I'm also not 100% sure it even works in the first place, it's more of a sketch.

[Mario Carneiro]

on this note, is it possible to extract / compile Lean code into executable code that can be linked with, say, C/C++? the last i found on this subject was in 2018 and someone mentioned Lean 4 would have this feature. is that still on? is there any sample extraction?

Lean 3 doesn't have this feature, Lean 4 is basically built around it. Lean 4 itself is being mostly written in lean and compiled to C++

[Mario Carneiro]

I think there are some experiments with FFI in lean 3 though

[Jalex Stark]

is there a lean 4 paper or similar where one can learn more?

[Kevin Buzzard]

There's not even a Lean 4 release yet. Leo was due to give a talk about it a few weeks ago but it got cancelled

[Marc Huisinga]

@Jalex Stark
i don't think that there's a paper on the FFI.
papers on lean4 from https://leanprover.github.io/publications/:

• type class resolution: https://arxiv.org/pdf/2001.04301.pdf
• notation: https://arxiv.org/pdf/2001.10490.pdf
• garbage collection and IR: https://arxiv.org/pdf/1908.05647.pdf

[Marc Huisinga]

the more recent slides in the first link might also be of interest to you.