Anonymous user
Talk:Proof: Difference between revisions
no edit summary
No edit summary |
|||
Line 133:
: 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)
== Huh? ==
| |||