# Tag Info

23

I'm going to disagree with DW. I think that it is possible (although difficult) for a P vs. NP result to be stated in a proof assistant, and moreover, I wouldn't trust any supposed proofs unless they were formalized in this way, unless they came from very reputable sources. In particular, none of the resources DW states are based on type theory, which is a ...

15

There is a variety of systems for Interactive Theorem Proving (ITP) -- see also the conference of that name -- Coq, Isabelle, HOLs, ACL2, PVS etc. All of them are relatively challenging to learn, and each has its own specific culture. It is like learning a foreign language: lets say you know English already, and then have the choice of French, German, ...

12

The remark is about one specific usage of Coq, namely formalization of programming language theory. Let us first make clear the distinction between synthetic and analytic: In a synthetic approach to a subject we say that there are things whose basic properties and structure are postulated in one way or another. We then study these things by relying only on ...

11

This is a very active research topic, very promising, though full automation of program generation probably has intrinsic limitations (but are human beings any better?). But the idea is still be very useful in assisting considerably the creation of programs by mechanizing many steps, and by automatically checking the correctness of the program generation. ...

10

I think you're confusing two things: dependently typed languages are convenient for specifying properties and giving proofs about functional programs. The techniques you mention are possible decision procedures for certain properties of functional programs. The ability to specify program properties usually takes place within a logic. Dependent types are a ...

10

Long story short: no you can't. A foreign function is like a black box and the type you ascribe to it is a promise you make: in the Curry-Howard correspondence that would correspond to adding an axiom to your theory. That being said, there are ways. In Coq for instance, there are various formalisations of the C standard (e.g. Robbert Krebbers' work). ...

10

Using proof assistants for this purpose is certainly possible in principle, but I suspect it would take more effort than most folks who write such proofs would be interested in putting in. It would require a substantial amount of effort from the author of a purported P vs NP proof to formalize their proof. Translating a proof written for humans into a ...

9

At first approximation, there is a difference in "locality" of memory access, when a programm just runs forward on the heap in CPS style, instead of the traditional growing and shrinking of stack. Also note that CPS will always need GC to recover your seemingly local data placed on the heap. These observations alone would have been adequate 10 or 20 years ...

9

The wag answer: Yes, but at the time of writing, for most nontrivial programs the specifications seem to be just as hard to write and debug as the programs would be. More seriously, babou's answer is good, but I'm also going to suggest checking out the area of dependent types. There's a rather good book using Coq (full disclaimer: written by a friend of ...

8

Proving the correctness of a program in a form of a proof that's nothing but the program itself This is not quite how the Curry-Howard-Correspondence works. First one has to show that the language of choice actually corresponds to some consistent logic. Different languages correspond to different logics, and many languages correspond to inconsistent ...

8

In order with the explicit questions: Yes Yes No To answer the question I think you're attempting to ask, we can prove many things using type checking, but not everything. What does this have to do with programs? That's what the Curry-Howard correspondence tells us. The Curry-Howard correspondence is a relationship between logic and computational models. ...

8

Your reasoning is incorrect. It is true that your hypothetical "proof deriver" cannot derive all true statements. No proof derivation system can, and indeed, it is not even possible to express the set of true statements in arithmetic, which is a consequence of Tarski's theorem on truth, itself a consequence of Gödel's theorem. However, your algorithm does ...

8

The existential form of the axioms of set theory is convenient for the meta-theoretic explorations of set theory, such as forcing etc., where it is important to have a minimal language to worry about (only $\in$ relation). But even just stating the axioms of set theory without any constants and operation symbols is pretty haunting, see this gist of mine. If ...

7

Coq is a bit more cruel than paper proofs: when you write "and we are done" or "clearly" in a paper proof, there is often much more to do to convince Coq. Now I did a little clean up of your code, while trying to keep it in the same spirit. You can find it here. Several remarks: I used built in datatypes and definitions where I thought it wouldn't hurt ...

7

I would say that the classic distinction of "automated theorem proving" (ATP) vs. "interactive theorem proving" (ITP) needs to be reconsidered. If you take a well-known ITP system like Isabelle/HOL today (Isabelle2013 from February 2013), it integrates quite a lot of add-on tools from the ATP portfolio: On-board generic automated proof tools: old-school ...

7

There's nothing stopping you from defining binary numbers in type theory, and this should give greater efficiency in practice. For example: https://coq.inria.fr/library/Coq.Numbers.BinNums.html EDIT: Why not base 10? Comparison on binary numbers can be done in $O(\log_2 n))$ time. If you have base 10, you can do it in $O(\log_{10} n)$ time. But if we ...

7

I would expect a proof assistant to provide: a syntax to express some mathematical statements a syntax to express a proof of one of those statements a computational process to "check" that a proof of a statement is indeed valid (returns success or failure, or maybe does not return at all) Finally, for such a proof assistant to be trustworthy, it should ...

7

From the perspective of Homotopy Type Theory (HoTT), i.e. if we have the Univalence Axiom, there are definitely values of Bool ≡ Bool that are distinct from refl. Because Agda without Axiom K is compatible with univalence, it can't then assume that refl is the only value of type Bool ≡ Bool. ℕ, on the other hand, is an h-set in HoTT (see Section 2.13 of the ...

7

I can give a direct answer to (2): $P\ne NP$ has been stated in Lean (along with the other main results of Cook's paper, where the conjecture was first described), as part of the Formal Abstracts project.

6

Let me try to clarify a point that seems to be confusing you: you seem to be conflating 2 related, but different concepts. The first is the concept of a proof system, which allows you to specify and prove theorems about mathematics or computer science. Dependent types are one elegant way to do this, where the types are the specification language and the ...

6

looks entirely identity function to me, which can definitely be inhabited by a closed term A proof of $\forall C : Prop, C$ is a function from an arbitrary proposition to its proof. Since a proposition isn't a proof, an identity function is not a function from propositions to proofs. The identity function (or rather, a function returning the identity ...

6

The term you're applying ¬_ to is large: it quantifies over all M : Set and therefore has type Set 1. So instead of ¬_ : Set -> Set you need ¬_ : Set 1 -> Set 1. A more general solution it to make ¬_ level polymorphic as in the standard library: you will be able to use this definition of negation across the board no matter how large the thing you're ...

5

The idea is that two expressions which are α-equivalent are not meaningfully different. λx.λy.x and λz.λy.z are technically different expressions. They are α-equivalent, though, they intuitively represent the same thing. In most circumstances, differentiating between them is useless at best, counter-productive at most. The quotient set is a formal definition ...

5

It's a term coming from abstract algebra. When you quotient a set $S$ with respect to some equivalence relation $\sim$, you are replacing the set $S$ with its equivalence classes under $\sim$. Often the set $S$ has operations defined on it, and in that case we want these operations to be well defined for the quotient $S/\sim$, in the sense that if $x_i \sim ... 5 The fundamental restriction is human computer programmers' inability so far to create computers equipped with real intelligence. "Never" is a very long time, so it's hard to accept that something will "never" happen unless there is a very good argument. Human brains and computers are not fundamentally different. The practical difference is that some human ... 5 SAT solvers work in the propositional calculus, and usually accept as input a formula in conjunctive normal form. There are several different propositional variants of the pigeonhole principle; they are all contradictions, and the actual pigeonhole principle is their negation. One of them, which states that there is a one-to-one mapping from$\{1,\ldots,n\}$... 5 You understand incorrectly. That is not how logic programming works. The number of consequences typically grows exponentially, or is even infinite. For instance, some consequences of$\forall x \in \mathbb{N} \,.\, \phi(x)$are$\phi(0)$,$\phi(1)$,$\phi(2)$,$\phi(3)$,$\phi(3 + 2)$,$\phi(x \cdot 2)$, and so on. Generating all consequences is infeasable ... 5 At the end of each iteration you have $$\forall j: 0 \leq j < i \implies b[j] = a[j+1]$$ which you can prove by induction. Thus, when the algorithm terminates,$i$has reached$n-1$and you have $$\forall j: 0 \leq j < n-1 \implies b[j] = a[j+1]\,.$$ I figured this out by just asking myself what kind of statement I can make at the end of each ... 5 Every assumption that is introduced between brackets has to be discharged at some point for the proof to be complete. Otherwise, we could prove that$A$is true for any given$A$as follows. [A]¹ ─── A This proof is incorrect, we have not discharged the initial assumption. The following proof of$A\to A\$ would be correct, as it discharges the assumption (...

5

In the theory of computation "diverge" means "does not terminate" or "runs forever". This is a computational effect (of a peculiar kind).

Only top voted, non community-wiki answers of a minimum length are eligible