Anonymous user
Talk:Proof: Difference between revisions
no edit summary
No edit summary |
|||
Line 12:
::: 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), ML/Haskell usualy based on polymorphic lambda calculus ([[wp:Hindley%E2%80%93Milner|HM]] or [[wp:System_F|SystemF]], however, they are ''not'' suitable) and so on. There is also other systems such as Mizar, MetaMath or ACL2 which are based on the set theory rather than on the Type Theory.
:::: About the output, if the proof is correct, then there is nothing to report (or just report "proved"), 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).
:::: I don't know about Salmon, but all you can do in C, J, Tcl or whatever is [http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf implement] dependently typed language or proof system, i.e. define syntax for terms and types (or terms, formulas and deduction rules) and write an unification algorithm on types and terms. — [[User:Ht|Ht]] 03:23, 1 June 2012 (UTC)
== Huh? ==
| |||