Anonymous user
Talk:Proof: Difference between revisions
m
changed the name of the 1st section header.
m (changed the name of the 1st section header.) |
|||
| (16 intermediate revisions by 3 users not shown) | |||
Line 1:
== subtype pre-definitions ==
The subtype Natural is pre-defined for all Ada implementations. Arithmetic upon that subtype is also pre-defined. This does not appear to be a very interesting problem in Ada. Any suggestions? --[[User:Waldorf|Waldorf]] 14:42, 21 December 2007 (MST)
:This seems like less of a computing problem, and more of a discrete math problem. I'm not sure if it's a good task. --[[User:Mwn3d|Mwn3d]] 14:45, 21 December 2007 (MST)
Line 13 ⟶ 15:
::: The issue is not about the use of metatheory but is about the use of programming. Currently, we have the Salmon implementation for the task, which does not correspond to code that I can run. More generally, the task requires no machine output. In my experience, the educational value of this site is significantly improved when short bits of machine output are included to illustrate the behavior of the code. --[[User:Rdm|Rdm]] 13:04, 31 May 2012 (UTC)
:::: But all the languages which are suitable for this task are based on some metatheories. Twelf is based on the [[wp:Logical_framework|LF]], Agda and Omega are based on the [[wp:Intuitionistic_type_theory|MLTT]], Coq is based on the [[wp:Calculus_of_constructions|CIC]] (which is variation of the MLTT), MLes and Haskell
:::: About the output, if the proof is correct, then there is nothing to report (or just report "proven"), but if it is not correct and contains errors then it does make sense to tell why the proof is not admissible. Once the proof is (silently) verified you can start deduce types and evaluate normal forms for terms, e.g. for agda <code>+-associative 1 2 3</code> deduced <code>6 ≡ 6</code> and evaluates to <code>refl</code> (witness of the equality).
Line 70 ⟶ 72:
::::::: And, yes, this is a weak system of axioms. But no cases where this approach is insufficient are a part of this task as it is currently defined. And proofs always assume that their axioms are correct (which is how we can get away with denoting an infinite sequence in the first place.) --[[User:Rdm|Rdm]] 15:38, 5 June 2012 (UTC)
:::::::: With current version this holds:
::::::::
:::::::: <lang j>'A B' induction '(A addition A) equals (B addition B)'
'A B' induction '(A addition B) equals (B addition B)'
'A B' induction '(A addition A) equals (A addition B)'
</lang>
::::::::
:::::::: — [[User:Ht|Ht]] 19:06, 5 June 2012 (UTC)
:::::::: And even <lang j>'A B' induction 'A equals B'</lang> — [[User:Ht|Ht]] 19:19, 5 June 2012 (UTC)
:::::::: With bug fixed version commutativity is broken: <lang j>'A B' induction '(A addition B) equals (B addition A)'
|assertion failure: assert
| assert 0!:3 y</lang>
:::::::: — [[User:Ht|Ht]] 20:15, 5 June 2012 (UTC)
:::::::: Yes -- should be fixed now though. Free variables are now distinct in the context of arithmetic (and relations) but are associated with a canonical (but arbitrary) ordering when generating results. --[[User:Rdm|Rdm]] 21:17, 5 June 2012 (UTC)
== Scope of Task ==
Now, there is a problem with large expressions:
<lang j> 'A B C D' induction '(A addition (B addition (C addition D))) equals ((B addition (C addition D)) addition A)'
|assertion failure: assert
| assert(#all)>#;._1 LF,y</lang>
I changed the code like this:
<lang j>add=: +/ dyadic
mul=: */ dyadic
even=: [: context kernel@add~"0@,@kernel :[:
odd=: successor@even
defined=: '(zero -. exists_in odd successor equals is_member_of add mul even)'</lang>
so that
<lang j>'A B C D' induction '(A add (B add (C add D))) equals ((B add (C add D)) add A)'</lang>
now holds (but it slow!), however:
<lang j> 'A B C D E' induction '(A add ((B add E) add (C add D))) equals ((B add (C add D)) add (A add E))'
|assertion failure: assert
| assert 0!:3 y
'A B C' induction '(A mul (B mul C)) equals ((A mul B) mul C))'
|assertion failure: assert
| assert 0!:3 y</lang>
Also, why is <code># all = 82</code>? Or it is context-dependent? — [[User:Ht|Ht]] 23:06, 5 June 2012 (UTC)
: These are out of scope for this task, so I did not bother implementing support for them. As you have seen, it is possible to support them without introducing any new concepts, but it gets inefficient.
: The sorts of examples you are presenting here could be addressed by tuning the hard constraints. That 82 -: #all thing is one example of a hard constraint. It exists in the current implementation because I think it's "cute". But an explanations of my reasons is going to get verbose...
: First, J implements recursion using the C stack. So it's limited to a size which is determined before the program starts running. In this context, that limitation winds up being equivalent to about 6665 recursive instances. It's just an arbitrary machine limitation (worth talking about, but that gets into the design intent of J, the character of mathematics and maybe a paragraph about peano arithmetic). However, it's too big for my purposes here. Using three free variables, I would need to perform 6665^3 tests to treat all possibilities represented in my kernel. So I decided to use its square root (or rather, the next larger integer). The problem with shrinking the kernel is that it's hypothetically possible to introduce expressions which are not adequately represented by the kernel. Rather than thinking this through to try and find some sort of minimal valid kernel size, I imposed a flat limitation on the expressions I am supporting: they can have no more characters than the length of my kernel. This limits the scope of the expressions I can treat, but -- in combination with my enumeration of supported operations -- it guarantees that I am not claiming provably false expressions are true. And that is good enough for the current task.
: (As an aside: note that J supports alternatives to recursion (for example, it has an induction primitive -- which, ironically, I am not using here) which are not limited by the C stack.)
: So, anyways, this system has some flexibility in its tuning, but its cost is exponential in the number of free variables considered together. I can reduce the base of that exponent by shrinking my kernel but at some point I would have to introduce syntactic manipulation. The strategy I have been using in this task is explicit enumeration, so if I needed syntactic manipulation I would explicitly enumerate the syntactic transformations used (and quite probably I would also explicitly impose the order in which they are performed).
: But adding support for syntactic manipulation could double or triple the size of the program, and it's not relevant for the current task. (And if you want me to discuss philosophical reasons behind this, I can, but that's probably best done in a separate subtopic.) --[[User:Rdm|Rdm]] 14:08, 6 June 2012 (UTC)
:: For me it looks like the <code>printf</code> function which can print only the "Hello World" message, but nothing else. Of course, it can satisfy the "Hello World" task, but it is not right since the "Hello World" task not really intended for only that output, it covers all sorts of such tasks, i.e. printing text. This task is similar, although it asks something special, it assumes that one can prove many other theorems using the same methods as for theorems in the task.
:: For example, one can prove that the natural numbers with addition and multiplication forms a semiring; that there are infinitely many natural, even and odd numbers; that there are infinitely many prime numbers ([[wp:Euclid's_theorem|Euclid theorem]]); that linked lists with append operation forms a monoid; that the compiler produce a program which execution gives the same value as the value obtained in the interpretation of the same program; and so on (in fact, almost any constructive math proof). What is really required is possibility of forming sets, the way of defining operations on that sets and the way of proving logical/algebraic properties (including higher-order ones) about sets and its operations. CAS and proof systems allow to do all that (and they are not small pieces of software).
:: To make it clear, I look at this J code from the sideline, I don't really understand it, but when I see such inconsistencies I just started to doubt about the whole approach. Can you give some references? What is the "kernel" that you are implementing? It is consistent? — [[User:Ht|Ht]] 17:44, 6 June 2012 (UTC)
::: I disagree (obviously). Most languages include a variety of techniques for displaying strings, and we do not expect to see all of them illustrated in a "Hello World" task. We only expect to see one of them illustrated. Strings are not a good analogy here, though, because most languages include extensive support for strings, and most languages do not include extensive support for proofs. Also, historically, a proof has always been specific to a single theorem. We do not expect that a proof for associativity of addition for peano numbers will be valid for complex numbers or quaternions -- we demand a separate proof.
::: You did find a bug in my earlier implementation, where it was inconsistent -- it was treating different free variables as identical, but I have fixed that bug.
::: Anyways, there's a reason that Knuth once warned: "Beware of bugs in the above code; I have only proved it correct, not tried it." It's trivial to find cases where systems proven correct via denotational semantics will fail in practice. The axioms are not a valid reflection of the machine implementation, and a proof necessarily is only valid when its axioms are valid. --[[User:Rdm|Rdm]] 18:50, 6 June 2012 (UTC)
:::: > Most languages include a variety of techniques for displaying strings, and we do not expect to see all of them illustrated in a "Hello World" task. We only expect to see one of them illustrated.
:::: Yes, we know that anything can be printed in conventional languages just as anything (what is truth) can be proved in theorem proving systems.
:::: > Strings are not a good analogy here, though, because most languages include extensive support for strings, and most languages do not include extensive support for proofs.
:::: It's a good analogy because I do not consider conventional languages at all. I am only talking about proof systems, in them we can show a simple proof and expect that one can prove any theorem the same way (e.g. [https://gist.github.com/1286093/8ff1afbc8b8f8aef051349eda19ccaec193c902d here] is a proof of Euclid's theorem in Agda). In weak conventional language, on the other hand, nothing can be proved, only proof system can be written.
:::: > Also, historically, a proof has always been specific to a single theorem.
:::: Historically has been almost a hundred years since the advent of formal logic (Boole, Peano, Dedekind, Hilbert, Frege, Russell, Whitehead, Quine, Cantor, Zermelo, Fraenkel, Löwenheim, Skolem, Gödel, Gentzen, Tarski works) in which theorems is just sequences of symbols derivable by rules of inference from axioms and a proof is an algorithm of deriving. And more than fifty years since the advent of сomputability theory and formulation of the Church-Turing thesis and the Curry-Howard correspondence (Church, Kleene, Turing, Gödel, Post, Rosser, Curry works). Type Theory is a further development. [http://video.ias.edu/voevodsky-80th Quoting] Voevodsky mathematical logic is just a combinatorial game, which, of course, can be implemented as software, as proof system suitable for proving any theorems.
:::: I remind that you have not explained [[wp:Proof_theory|what]] is the kernel that you are implementing. — [[User:Ht|Ht]] 15:44, 7 June 2012 (UTC)
:::: History goes back much further than 100 years. But the basis of proof has not changed. A proof is based on its axioms. Meanwhile, the implementation of a theorem solver must be considered to be a part of the axioms.
:::: But there is no literature on the "kernel" concept, unless I get around to writing it (or perhaps unless you do so). However it is, as you said, "just a combinatorial game".
:::: That said, here's a quick overview: the kernel is a permutation of a prefix of the non-negative integers which is significantly longer than any representable feature of the mini-language. It's paired with a second copy of the permutation which represents the symbol. We guarantee that each free variable gets represented by a permutation different from any other free variable. Any single-valued functions are applied uniformly to the kernel and the symbol. Any two-valued operations enumerate the symbols and find the cartesian product using that operation based on the argument kernels (and then we sort the symbols and transpose the dimensions of the cartesian product to match that sort). When testing set membership we ignore any generated members (on either side of the set) which were not part of the original kernel. Equality is an exact match test on the entire data structure. Existence checks for any member of one generated kernel existing in the other generated kernel. This works because we are dealing with a limited vocabulary -- our starting kernel is larger than any of the artifacts (non-uniformly treated prefix of the numbers) we can express using our language, which makes it infinite in the context of this limited language. --[[User:Rdm|Rdm]] 20:56, 7 June 2012 (UTC)
:::: Note, by the way, that I have not thought through the issues involved in using more than one combining operation with this system. It has not mattered for the current version of this task. --[[User:Rdm|Rdm]] 21:14, 7 June 2012 (UTC)
== Huh? ==
Line 88 ⟶ 187:
The first line of the description reads: <cite>"Define a type for a sub-set of natural numbers (0, 1, 2, 3, ...) representable by a computer, and addition on them."</cite> Can somebody please clarify that last phrase, <cite>"addition on them"</cite>? I ''think'' I know what it's supposed to mean (and I'm ''fairly'' sure I understand the task as a whole) but just in case... -- [[User:Eriksiers|Eriksiers]] 22:24, 5 November 2009 (UTC)
:In mathematics, when we speak of "a binary operation on S", we mean a function whose domain is S × S and whose
::Hmmm... I slept through most of my calculus classes, due to having '''THE MOST BORING TEACHER IN THE UNIVERSE''' (really) and as a result, most math above simple algebra I just don't get. I think I'll give this task a pass. -- [[User:Eriksiers|Eriksiers]] 15:05, 6 November 2009 (UTC)
::: But this is not much more than elemental type theory. Hardly as complex as the infinitesimal calculus... –[[User:Dkf|Donal Fellows]] 16:38, 6 November 2009 (UTC)
Line 116 ⟶ 215:
: I'll add that while I had fun with this task, I don't consider it much of a proof. There's way too much hand waving for me. —[[User:Sonia|Sonia]] 23:29, 21 June 2011 (UTC)
:: I'm sure it was a fun thing to write, but "not much of a proof" is the problem here. I can write any kind of code to prove odd + odd = odd, and I can make it compile, but that proves nothing; only when I run the code, and do a test like "is 1 + 3 odd?" The code will go 1 + 3 = 4-> pred 2 ->pred 0 (BOOM, hopefully, because first element is 1), so that's a
: The task might be poorly worded and poorly named, but I think the examples posted by the task author and every example except Haskell show the same thing, which is using the language type system enforcement of closure over a type as an analog of mathematical closure over a set of numbers. The code to demonstrate isn't the code that you write, but the code that is in the language translator. —[[User:Sonia|Sonia]] 01:09, 22 June 2011 (UTC)
Line 134 ⟶ 233:
I suggest the task should be draft status. The varied solutions posted and the resulting discussions here show disagreement on what the current wording requires. —[[User:Sonia|Sonia]] 20:33, 11 May 2012 (UTC)
: I think the task is quite clear: "prove that the addition of any two even numbers is even". ''Any''. It is not possible with
: Putting something that looks like "2" in the CPU register, the same "2" in another, performing ADD, and getting something that looks like "4" doesn't help - that is not a proof! :) You need to ''define'' numbers, rules for arithmetic, induction, etc ''in'' the language based on a suitable [http://ncatlab.org/nlab/show/type+theory metatheory] such as [[wp:Intuitionistic_type_theory|MLTT]] or [[wp:Calculus_of_constructions|CoC]]/[[wp:Calculus_of_inductive_constructions|CoIC]], then prove. E.g., in the Agda version <code>even+even=even</code> takes ''any'' two even numbers and returns their sum as an even number, this is a ''type'', i.e. logical ''proposition'', ''algorithm'' itself is a ''proof'' by induction which ''builds'' a required term of a given (inhabited) type, and the
::It seems a wothwhile task in the way you describe it here on the talk page. Maybe the task description needs similar expansion to remove J-like entries and require "induction solving capabilities" or people to create such in a language without it, then apply it to the problem at hand. --[[User:Paddy3118|Paddy3118]] 07:22, 12 May 2012 (UTC)
Line 186 ⟶ 285:
::: Might I suggest you read a good book about the foundations of mathematics? Perhaps my terminology will seem less ambiguous to you after this. —''[[User:Ruud Koot|Ruud]]'' 21:33, 13 May 2012 (UTC)
:::: You have overgeneralized my statement.
:::: The issue I raised was not "computers are incapable of working with 'infinities'". The issue I raised was "computers can only represent finitely many distinct values. By leaving out that "distinct" part, you ignored my entire point.
Line 228 ⟶ 327:
::: > natural numbers are not countable
::: Finite sets is countable too (well, depending on the terminology, see the
::: > My current inclination is to believe that you treat some "failures" as "valid for purposes of proof" in your implementation of types
Line 266 ⟶ 365:
::: The section about natural numbers is on page 71. That is, the Peano axioms is embeddable into MLTT (even constructive ZF set theory is embeddable), so that the questions should be asked about MLTT itself. There is some free books - [http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/], [http://www.cse.chalmers.se/research/group/logic/book/] (see indexes for examples, e.g. the associativity of the append operation on lists from [2]). — [[User:Ht|Ht]] 14:06, 14 May 2012 (UTC)
:: By extension [[User:Rdm|Rdm]] believes that because
::: This is trivially false, in the sense that I have stated nothing about a relationship between sheets of paper and proofs. Please refrain from making up stuff about me. --[[User:Rdm|Rdm]] 13:17, 14 May 2012 (UTC)
| |||