Talk:Proof: Difference between revisions
→Satisfaction
No edit summary |
|||
Line 36:
:::::::: Currently I can't understand this J code, nor the idea behind it. Did it use some special features? Can it be simply translated to, say, Scheme? — [[User:Ht|Ht]] 06:26, 5 June 2012 (UTC)
:::::::: It could be translated to Scheme, but a literal translation would probably not complete because J has a limitation on recursion depth (which I exploit here) which Scheme does not. But the algorithm is trivially simple, so perhaps it would be better to translate it to english:
:::::::: <lang english>Define words:
zero: peano zero
successor: peano successor (defined on zero and on the result of successor)
equals: determines if two peano numbers are equal
all: represents all natural numbers, is implemented as a prefix of those numbers
is_member_of: determines whether members of a set which are members of all are members of another set which are also members of all.
exists_in: determines whether the intersection of two sets is non-empty
induction: given a list of names (which can represent any natural number) and a list of expressions, accepts or rejects the list of expressions based on these steps:
1) If an expression uses any name which has not been explicitly named here (including addition, odd and even), then the list of expressions is rejected.
2) If an expression is too long (longer than "all"), then the list of expressions is rejected.
3) If an expression is not a tautology then the list of expressions is rejected.
addition: given two lists of peano numbers, produces the cartesian product of the sums of all elements of those lists.
even: doubles each element of a list using addition to add (only) that number to (only) itself.
odd: finds the successor (to each member of the list resulting from) even</lang>
::::::: In other words, the constraints are: only the words defined for this task are allowed, and sentences using those words are limited in length, and any remaining sentences must be valid for all of the defined test cases.
::::::: 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)
== Huh? ==
| |||