Talk:Proof: Difference between revisions
Content added Content deleted
No edit summary |
(→Draft status: Task update/clarification needed?) |
||
| Line 141: | Line 141: | ||
: 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 typechecker ''performs'' that proof (so that this is compile-time verification). — [[User:Ht|Ht]] 02:44, 12 May 2012 (UTC) |
: 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 typechecker ''performs'' that proof (so that this is compile-time verification). — [[User:Ht|Ht]] 02:44, 12 May 2012 (UTC) |
||
::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) |
|||
== Haskell == |
== Haskell == |
||