|
Post by sumedhghaisas on Jun 1, 2014 15:19:46 GMT -8
One more thing I wanted to discuss... I am really confused about adding Definition 15... I am unable to understand what purpose it serves??
"Essentially, this restriction ensures that functional terms cannot \grow" to unbounded size by use of recursive rules, since terms can only be passed along a recursive cycle without adding function symbols, and new terms introduced into recursive cycles must be grounded by a finite set of base relation sentences."
By using minimal model rule these cases can be taken care of at query stage. I tried a recursion in StaticValitor And it did not produce any errors. Is there a reason behind this??
|
|
|
Post by sumedhghaisas on Jun 3, 2014 19:18:14 GMT -8
The primary version of the parser is complete. I have uploaded the code on GitHub. Link to the repository is github.com/sumedhghaisas/gdlparserIncluded command line interface. Supports multiple files and can also generate DOT(GraphViz) representation of the dependency graph generated. Includes all primary errors and warnings I have mentioned earlier. Ready for development
|
|
|
Post by alandau on Jun 3, 2014 22:02:44 GMT -8
Definition 15 protects against rules like this:
(<= (foo (fn ?x)) (foo ?x))
This can cause an infinite number of sentences to be true in one turn:
(foo 0) (foo (fn 0)) (foo (fn (fn 0))) etc.
With the recursion restriction, only a finite number of sentences can be true in a given turn. This is very important for forward-chaining reasoning approaches in particular.
|
|
|
Post by sumedhghaisas on Jun 4, 2014 5:19:32 GMT -8
Couple of questions about definition 15 - 1) (<= (test (fun ?x)) (test ?x) (not (test2 ?x)) ) is this valid under definition 15... Or is it boundedness is necessary?? As negation as failure can have infinite domain this should be incorrect....
2) (<= (test ?x) (not (not (test2 ?x))) ) is this valid???
3) (<= (test ?x) (not (not (test ?x))) (test3 ?x) ) (<= (test2 ?x) (test ?x) (test3 ?x) ) is this recursion stratified???
Sent from my Nexus 5 using Tapatalk
|
|
|
Post by Stephan Schiffel on Jun 4, 2014 8:26:00 GMT -8
1) (<= (test (fun ?x)) (test ?x) (not (test2 ?x)) ) is this valid under definition 15... Or is it boundedness is necessary?? As negation as failure can have infinite domain this should be incorrect.... Definition 15 is a little vague regarding negative literals such as (not ...) or (distinct ...). But your example should not be allowed. 2) (<= (test ?x) (not (not (test2 ?x))) ) is this valid??? No, because of Definition 6 (Safety). Also it is not a syntactically correct rule (see below). 3) (<= (test ?x) (not (not (test ?x))) (test3 ?x) ) (<= (test2 ?x) (test ?x) (test3 ?x) ) is this recursion stratified??? The rules are not stratified according to Definition 8, because there is a cycle in the dependency graph (namely the edge from test to test) that is labelled with not. Technically, the first rule is not even syntactically correct, because (not (not (test ?x))) is not a literal according to Definition 4 and thus the rule is not a Datalog rule according to Definition 6.
|
|
|
Post by sumedhghaisas on Jun 5, 2014 4:15:52 GMT -8
Is it necessaary to apply definition 15 to all the rules involved in any recursion cycle??? For example.. (<= (rel1 (fun ?x)) (rel2 ?x) ) (<= (rel2 ?x) (rel1 ?x) (rel3 ?x) )
Assuming rel3 is bounded, will this recursion generate infinite functional terms??? I think applying this rule to any one rule involved in the recursion will break the chain and the recursion will be stratified...
Another point is... Recursion like these... (<= (rel1 ?x) (rel2 ?x)) (<= (rel2 ?x) (rel1 ?x)) Should be stratified as functional terms will be bounded...
For this can definition 15 be modified like this?? We define an index for a variable, a value associated with every variable. If variable appears directly as an argument to a relation its index is zero. If appears directly as an argument to function where that function appears as an argument to a relation, its index will be one. Similarly.... If a variable appearing in head has higher index than the same variable appearing in body then we can add a strong edge of dependency between body and head. If there is a cycle with strong dependency edge then the recursion is not stratified.
Will this solve the problem of infinite functional terms???
|
|
|
Post by Stephan Schiffel on Jun 5, 2014 5:12:06 GMT -8
Is it necessaary to apply definition 15 to all the rules involved in any recursion cycle??? For example.. (<= (rel1 (fun ?x)) (rel2 ?x) ) (<= (rel2 ?x) (rel1 ?x) (rel3 ?x) ) Not sure what you are getting at, but the definition requires you to look at all the rules. In this case the first rule does not obey the recursion restriction. However, the second one does. Anyway, since there is a rule that violates the restriction, the rules are not correct GDL. No and it could be trivially rewritten to be correct GDL without changing its semantics, just add (rel3 ?x) to the first rule. You are probably right. These rules are perfectly fine with regards to Definition 15. Why do you want to modify the definition? What problem is solved by your definition that is not already solved by the original one?
|
|
|
Post by sumedhghaisas on Jun 5, 2014 10:37:45 GMT -8
So (<= (rel1 (fun ?x)) (rel2 ?x)) (<= (rel2 ?x) (rel1?x) (rel3 ?x)) Can be considered valid right?? I was confused cause when I checked with static validator... (<= (rel1 (fun ?x)) (rel2 ?x) (rel3 ?x)) (<= (rel2 ?x) (rel1 ?x)) Caused no errors... But then first one caused error...
|
|
|
Post by alandau on Jun 5, 2014 20:41:38 GMT -8
The first set of rules is not valid, simply because it breaks the restriction.
Consider adding the rule (<= (rel2 ?x) (rel1 ?x)) to either set of rules. The rule itself is valid. In the first case it causes infinite recursion. In the second case it doesn't (and happens to be redundant).
There are multiple ways the restriction could have been defined. This is the one that was chosen. It doesn't require much in the way of computation to validate that it's correct, lets you identify individual rules as invalid, and doesn't really get in the way of writing games in practice.
|
|
|
Post by sumedhghaisas on Jun 6, 2014 17:17:21 GMT -8
Yes when (<= (rel2 ?x) (rel1 ?x)) is added the first set of rules will produce infinite recursion. Thats why addition (rel3 ?x) is necessary. But its not necessary to add anything to the first rule if (rel3 ?x) is added to the second rule. My point being is that if definition 15 can be applied to one rule in infite recursive cycle, the infinite recursive will break. Like in rules... (<= (rel2 (fun ?x)) (rel2 ?x)) (<= (rel2 ?x) (rel1 ?x) (rel3 ?x)) The second rule obeys definition 15 and hence there is no infinite recursion. Adding rule (<= (rel2 ?x) (rel1 ?x)) will generate another cycle and there is no rule in that cycle which satisfies definition 15 hence there will be infinite recursion. I dont know if this will give advantage while writing games, but most probably no. But still its any interesting thing which can cut down some restrictions. If it is true I mean. Cause I cant construct a formal proof for this. Just some logical sentenses and case study.
|
|
|
Post by alandau on Jun 7, 2014 12:15:25 GMT -8
As a counterexample, (<= (rel2 ?x) (rel1 ?x)) satisfies definition 15 just fine, and it can be part of a problematic cycle.
|
|
|
Post by sumedhghaisas on Jun 7, 2014 14:38:33 GMT -8
Yeah... You are right. It does satisfy definition 15 and still can be part of problematic cycle. Sorry, I misinterpreted definition 15 a little.
Sent from my Nexus 5 using Tapatalk
|
|
|
Post by sumedhghaisas on Jun 7, 2014 21:53:12 GMT -8
Okay I have added Stratified Recursion checking in GDLParser in the last commit. As of the last commit GDLParser tests everything StaticValidator checks. Have added tests in GDLParser to test it for all things. GDLParser github.com/sumedhghaisas/gdlparserSome things which are not fully implemented in StaticValidator * - Legal's first argument must be a player; ditto does, goal * - Goal values are integers between 0 and 100 I am trying to accomodate them in GDLParser. If legal or goal appears in fact it is very easy to check these things. The problem arises when legal or goal appears as head of the rule. Any ideas on how can these restrictions be checked in this case? My solution is to use Flattened GDL for this checking. Flattening will help detect many more errors such as * if legal is defined for every role * goal is defined for every role * deep warnings such as base defined but never used and things like that
|
|
|
Post by sumedhghaisas on Jun 7, 2014 22:15:09 GMT -8
Some comparisons I ran in GDLParser and StaticValidator(I didn't compile the JAVA.. Compiled JAVA may run faster... I don't know. ) Game Time by StaticValidator Time by GDLParser(g++ -O3) 3 Puzzle avg 168 ms avg. 7 ms 8 Puzzle avg 181 ms avg. 12 ms Nine Board Tic Tac Toe avg 190 ms avg. 18 ms You can post issues about GDLParser on this forum or on GIT. I am almost free these days, so I will try to solve it as soon as I can.
|
|
|
Post by sumedhghaisas on Jun 26, 2014 12:41:02 GMT -8
I have added gdl reasoner and KIF flattener to GDlParser now. I have changed repo name to libGDL. Have added command line kif flattener too. github.com/sumedhghaisas/libgdlUsing the dependency graph generated from the paring, flattener flattens the description in just one pass. time output f or flattening nine board tic tac toe game real 0.443 user 0.432 sys 0.008 Also flattener will remove all the occurrences of data relations from the flattened description as they are no longer needed. For example.. (<= (base (step ?x)) (successor ?x ?y)) (successor 1 2) (successor 2 3) flattener will produce output - (base (step 1)) (base (step 2)) Had fun implementing reasoner and flattener my reasoner work without actually substituting values at any stage except the last printing stage. That certainly boots performance. I just love c++ pointers and the cool things you can do with it. Next thing will be to add deep checking of GDL through flattened description. For that, first I have to add debugging symbol support so that verbose errors can be shown for flattened description checking. Lately I have been thinking, what all can be checked with flattened description.. 1) first argument to legal and goal must be a role 2) there should be atleast one legal and one goal for each role 3) some deep warnings such as unused base function or undefined function etc etc. basically defined undefined warnings any more??
|
|