Talk:Proof: Difference between revisions
→Satisfaction
No edit summary |
|||
Line 90:
:::::::: 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>
mul=: */ dyadic
even=: [: context kernel@add~"0@,@kernel :[:
Line 105 ⟶ 107:
defined=: '(zero -. exists_in odd successor equals is_member_of add mul even)'</lang>
|assertion failure: assert
| assert 0!:3 y
Line 118 ⟶ 120:
| assert 0!:3 y</lang>
: 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)
== Huh? ==
| |||