[WIP] Kanren2 #17

maxeeem · 2023-09-13T18:25:19Z

Expanding on the previous attempt at using miniKanren for rule matching.

Added initial versions of methods for converting between Narsese and miniKanren logic forms
Added helper functions for iterating through an array or rules and applying them to test terms
Added one possible way of handling conditional rules with a modified version of the rule {<(&&, C, S) ==> P>. S} |- <C ==> P> making the difference operation explicit (not production ready solution, just an example)

bowen-xu · 2023-09-13T21:26:12Z

pynars/NARS/InferenceEngine/Logic2.py

+                    l = components[0]
+                    r = components[1]
+                    l = set(l.terms.terms if type(l) is Terms else l.terms)
+                    r = set(r.terms.terms if type(r) is Terms else r.terms)
+                    diff = l.difference(r)
+                    if l == diff:
+                        difference = None
+                    else:
+                        terms = list(diff)
+                        if len(terms) == 0:
+                            difference = None # TODO: what is a better way to handle this?
+                        elif len(terms) == 1:
+                            difference = terms[0]
+                        else:
+                            difference = Compound(components[0].connector, *list(diff))


There is a built-in difference operation of Compound. You can simply write, for example,

difference = components[0] - components[1]

ok, that's good to know. I figured you already had something like that.

There is an edge case that i found though, (&&, A, B) - (&&, B, C) produces A but what we want for conditional rule is for it to return False I believe. If that's correct, is there another method that would allow us to know if the right part is fully contained in the left?

Oh i think i found it, there's contains method on the Compound which should do the trick!

bowen-xu · 2023-09-13T21:29:12Z

pynars/NARS/InferenceEngine/Logic2.py

+    difference = -1 # result of applying diff
+
+    if type(c) is Statement:
+        if type(c.subject) is Compound and c.copula is Copula.Implication:


There is a variable indicating the type of a term.
c.subject.is_compound is better than type(c.subject) is Compound.
The former one is more efficient (though we don't much care about runtime efficiency in python)

bowen-xu · 2023-09-13T21:30:07Z

pynars/NARS/InferenceEngine/Logic2.py

+
+prefix = '_rule_'
+
+def logic(term, rule=False):


It would be better to add a "type hint" when defining a function.
For example,

def logic(term: Term, rule=False):

bowen-xu · 2023-09-13T21:31:37Z

pynars/NARS/InferenceEngine/Logic2.py

+prefix = '_rule_'
+
+def logic(term, rule=False):
+    if term.type is TermType.ATOM:


term.is_atom is preferable. The same things in the following.

bowen-xu · 2023-09-13T21:33:26Z

pynars/NARS/InferenceEngine/Logic2.py

+            return Compound(con, *terms)
+    return logic # atom or cons
+
+def toList(pair) -> list:


Maybe we shall make a convention on the naming rule of function, class, and variable. I prefer to use the name to_list here, but that's ok.

Yeah... that's my Swift experience showing :) I'll keep it in mind that in Python underscore is more common.

pynars/NARS/InferenceEngine/Logic2.py

maxeeem · 2023-09-15T12:57:29Z

pynars/NARS/InferenceEngine/Logic2.py

+
+from unification import unify, reify
+
+def variable_elimination(t1: Term, t2: Term) -> list:


@bowen-xu I didn't do extensive testing but seems to work in the few test cases we looked at during our call

At least it works in these cases.

bowen-xu · 2023-09-15T15:06:33Z

pynars/NARS/InferenceEngine/Logic2.py

+
+from unification import unify, reify
+
+def variable_elimination(t1: Term, t2: Term) -> list:


At least it works in these cases.

bowen-xu · 2023-09-15T15:07:50Z

pynars/NARS/InferenceEngine/Logic2.py

+            substitution.append(d)
+    result = []
+    for s in substitution:
+        reified = reify(logic(t1), s)


This answers my question. reifycan be used for substitution.

bowen-xu · 2023-09-15T17:32:35Z

I can see a long way to go, but it's promising. The good news is that in the current structure of the project, the logic part and the control part are seperated, thus it's ok to explore the implementation of each of them. I believe we can get an elegant implementation of inference engine by uisng miniKanran.

bowen-xu · 2023-09-15T17:38:03Z

I think there are two steps to enhance the inference engine. The first is to implement all of the rules from NAL-1 to NAL-9. The second is to construct the rules only once when initializing the program (rather than construct them when used).

maxeeem · 2023-09-15T18:39:13Z

I think there are two steps to enhance the inference engine. The first is to implement all of the rules from NAL-1 to NAL-9. The second is to construct the rules only once when initializing the program (rather than construct them when used).

The good news is that there's no need to implement the rules, only add their Narsese signatures to the array ;)

bowen-xu · 2023-09-15T18:48:33Z

I think there are two steps to enhance the inference engine. The first is to implement all of the rules from NAL-1 to NAL-9. The second is to construct the rules only once when initializing the program (rather than construct them when used).

The good news is that there's no need to implement the rules, only add their Narsese signatures to the array ;)

Yeah, that's what I mean by "implement all the rules", sorry for my inaccuracy. We don't need to explicitly implement certain functions to do the transformation, but just describe them in the array.

maxeeem · 2023-09-16T20:45:19Z

Tests/utils_for_test.py

 nars = Reasoner(100, 100)
 engine: GeneralEngine = nars.inference
-
+kanren: KanrenEngine = KanrenEngine()


@bowen-xu please ignore my changes to the tests, it was just me temporarily changing the code just to see if KanrenEngine returns the same values as the GeneralEngine. When this branch is ready to merge I will delete all of this code plus it's probably going to be gone anyway when we rewrite the tests.

maxeeem · 2023-09-16T20:49:00Z

pynars/NARS/InferenceEngine/Logic2.py

+    return task.term if rule else task.sentence
+
+class KanrenEngine:
+    _all_rules = '''{<M --> P>. <S --> M>} |- <S --> P> .ded


@bowen-xu do you know of a convenient way to get a list of all rules grouped by NAL level? I just dumped all the rules I had in Swift and formatted them a bit but in order to accept a parameter similar to how GeneralEngine does it for NAL levels, it would be better to have the rules grouped, I just couldn't find a grouped list at the moment, in the book's appendix the rules aren't separated by NAL levels so if you know some document or resource I can use as a reference to build a complete list of rules separated by NAL level that would be great!

There is no such a document. However, the rules are grouped in PyNARS by NAL level. For example, you can see all the rules on NAL1 from pynars/NARS/InferenceEngine/GeneralEngine/Rules/NAL1.py

Some of the functions which implement corresponding rules have very clear comment, from which you could know clearly which rule(s) it implements. But not all comments are correct, some might be misleading. Before getting a chance to check and correct all those comments, one have to read the code of the rule functions to double-check. I know that would cost time, but there might be no better ways :(

bummer. i guess we can compile it and it'll be a good thing to have for the future

Yeah, and Patrick just said there's such a list in ONA, which I didn't know before. That would be a good reference.

maxeeem · 2023-09-16T20:51:05Z

pynars/NARS/InferenceEngine/Logic2.py

+        c = self.logic(c, True)
+        return ((p1, p2, c), r)
+
+    def inference(self, t1: Sentence, t2: Sentence) -> list:


The code here needs to handle more than judgements but this was just a quick test.

maxeeem · 2023-09-17T01:08:50Z

pynars/NARS/InferenceEngine/KanrenEngine/NAL_rules.txt

+- Theorems can be handled explicitly using miniKanren
+should they be applied at the same time as immediate rules?
+
+


@bowen-xu this is my best understanding of the breakdown of rules by level.
will need to find answers to the questions above.

When should we apply immediate rules?
When to apply decomposition rules?
Is any arbitrary S valid for this rule?
Should these be handled outside of normal flow?
should they be applied at the same time as immediate rules?

I thinks those questions refer to the same answer. Not all theorems or the rules you mentioned should be applied until there is a hint. For example, the rule {S, P} |- (S && P) is always valid. However, the rule is applied (for backward inference) only when there a goal (S && P)! or question appears. Otherwise, combinatorial explosion would happen.

Can these also be the variable introduction rules (substituting {M/#x})?

I don't quite understand this question. What to be the variable introduction rules?
But I'm sure that the rules on variable are not complete, even in NAL book. In NAL book, it just describes some overall principles and considerations on variable and gives some sample rules.

I guess what I mean is {S, P} |- (S && P) is not applied to arbitrary S and P, right? They have to be related so this rule in forward inference is mainly used for events using temporal relation as a hint or for variable introduction like in Table 10.3 or as you mentioned for backward inference when there is a corresponding goal.

Regarding theorems:
In the technical report (and maybe in the book) it says that immediate rules are applied when the task enters the system, which to me sounds like it is done once for each task, not repeatedly. So I wonder if theorems can have a similar treatment. I'm trying to understand if the many permutations of rules are necessary or if the same effect can be achieved in other ways.

Regarding variables:
It is exactly the principles I'm trying to capture instead of the actual rules. As far as I can tell the principles can be described at the meta-level as applying certain rules, for example, compositional intersection rule, and then performing the substitution on the conclusion. This is how one of the variable rules in Table 10.4 is described in the NAL book so I'm wondering if the variable introduction rule needs to be made explicit or if we can just have the procedure by applying the substitution to the result of inference. The question is then more about when to apply it? Every time such a conclusion is formed? Or should there be some limit?

I guess what I mean is {S, P} |- (S && P) is not applied to arbitrary S and P, right?

In forward reasoning, S and P can be arbitrary sentences, as long as they are no the same.

So I wonder if theorems can have a similar treatment. I'm trying to understand if the many permutations of rules are necessary or if the same effect can be achieved in other ways.

Well, I don't think there is a standard answer to this question. The issue is whether the system can afford the resources regarding the permutations. There might be plenty of useless conclusions by applying the theorems without hints, and that might harm the system achieving goals. I'm not sure.

Oh sorry, I meant the other rule, {P,S} |- S => P. This one isn’t applied to arbitrary S and P, right?

I'm wondering if the variable introduction rule needs to be made explicit or if we can just have the procedure by applying the substitution to the result of inference. The question is then more about when to apply it? Every time such a conclusion is formed? Or should there be some limit?

My solution is to make them explicit rules in PyNARS, though this might not be an optimal solution.
For example, there is a variable introduction rule in pynars:

{<S-->M>, <S-->P>} |- <<$x-->M> ==> <$x-->P>>

This rule is applied only when the pattern of the premises matches this form {<S-->M>, <S-->P>}.
The substitution happens when the rule is applied.

Oh sorry, I meant the other rule, {P,S} |- S => P. This one isn’t applied to arbitrary S and P, right?

No, not right. This rule is applied to arbitrary S and P in forward reasoning.

Are you sure? In the book when these rules are introduced it states:

“The rules in Table 9.5 are not syllogistic, but compositional, since the statements in the conclusions are compound terms composed by the terms in the premises. Because they are applicable only when the premises “can be seen as based on the same implicit condition”, NAL does not take two arbitrary judgments as premises and apply these rules on them.”

In NAL book, Table 9.5 is to provide justifications for the rule {S, P} |- <S==>P>. It supposes there is an implicit condition E, so that <E ==> P> and <E ==> S>, then syllogistic induction rule can be applied to derive <S ==> P>.

In logic, they are not arbitrary. However, in NARS, the reasoning system, what is the implicit condition E?
You can think all the statements have a common implicit condition E, so that arbitrary S and P are valid for that rule. Nevertheless, NARS doesn't do it even if the rule is applicable, because that will leads to combinatorial explosion.

Can we consider the case where the two premises have common evidential base? Maybe. But I don't think it's going to get any better regarding combinatorial explosion.

can discuss with Pei in the group meeting next week.

…ning up the code

…ness

This reverts commit 3ae6f6a.

maxeeem · 2024-01-25T17:16:11Z

@bowen-xu @ccrock4t regarding inference times

I ran some quick tests this morning, to measure just the run time of inference step using miniKanren. I modified the code to calculate the time it takes to run the function that iterates through all the rules (~100, excluding theorems) and applies matching ones. I also kept a running average because simpler statements like <a --> b>. take less time to process than <(&&,<$x --> flyer>,<$x --> [chirping]>, <(*, $x, worms) --> food>) ==> <$x --> bird>>. and I wanted to know a rough average estimate.

t0 = time()

results = self.inference(task.sentence, belief.sentence)

t1 = time() - t0

print("inf:", 1 // t1, "per second")

self._run_count += 1
self._inference_time_avg += (t1 - self._inference_time_avg) / self._run_count

print("avg:", 1 // self._inference_time_avg, "per second")

The results so far on a small sample indicate ~300-400 calls per second on my laptop.

inf: 320.0 per second
avg: 365.0 per second
inf: 528.0 per second
avg: 378.0 per second
inf: 1100.0 per second
avg: 404.0 per second
inf: 1438.0 per second
avg: 433.0 per second
inf: 1042.0 per second
avg: 455.0 per second
inf: 214.0 per second
avg: 419.0 per second
inf: 1172.0 per second
avg: 439.0 per second
inf: 131.0 per second
avg: 379.0 per second
inf: 1362.0 per second
avg: 397.0 per second
inf: 220.0 per second
avg: 379.0 per second

maxeeem requested a review from bowen-xu September 13, 2023 18:25

bowen-xu marked this pull request as ready for review September 13, 2023 19:05

bowen-xu reviewed Sep 13, 2023

View reviewed changes

pynars/NARS/InferenceEngine/Logic2.py Outdated Show resolved Hide resolved

bowen-xu added the enhancement New feature or request label Sep 13, 2023

maxeeem marked this pull request as draft September 15, 2023 12:55

maxeeem commented Sep 15, 2023

View reviewed changes

bowen-xu reviewed Sep 15, 2023

View reviewed changes

maxeeem force-pushed the kanren2 branch from 5b25581 to cd822c4 Compare September 16, 2023 20:42

maxeeem commented Sep 16, 2023

View reviewed changes

maxeeem commented Sep 17, 2023

View reviewed changes

maxeeem changed the title ~~Kanren2~~ [WIP] Kanren2 Sep 18, 2023

maxeeem added documentation Improvements or additions to documentation do-not-merge and removed documentation Improvements or additions to documentation labels Sep 18, 2023

maxeeem added 5 commits September 19, 2023 11:28

wip

9f8c254

expand logic rule application to handle multiple rules and begin clea…

d2ff838

…ning up the code

addressing pr comments

a607900

code cleanup

188e3aa

adding variable elimination

f4d3fd6

maxeeem added 3 commits September 19, 2023 11:28

wrap kanren code in a KanrenEngine class; parse rules on init

46c0bc3

begin compiling list of rules and meta-rules of NAL by level

565752c

clean up rule instantiation; add constraints ensuring variable unique…

1b1eeb8

…ness

maxeeem force-pushed the kanren2 branch from d27e6fe to 1b1eeb8 Compare September 20, 2023 00:07

maxeeem added 7 commits September 19, 2023 20:00

cleanup constraints implementation

2b0cd1b

allow _C and C to be the same for certain rules; code cleanup

ba880b4

fix syntax error

d0c35ef

improved performance 10x by applying all rules in one iteration

3ae6f6a

Revert "improved performance 10x by applying all rules in one iteration"

64af85a

This reverts commit 3ae6f6a.

better way to achieve performance improvement

3b964ed

add rule variants accounting for symmetric compounds

d4599eb

bowen-xu deleted the branch dev October 17, 2023 17:41

bowen-xu closed this Oct 17, 2023

bowen-xu reopened this Oct 17, 2023

maxeeem added 2 commits November 27, 2023 14:38

updating to latest dev branch

65717a9

merge changes from test branch

c55e482

maxeeem closed this Jan 30, 2024

maxeeem mentioned this pull request Jan 31, 2024

Working Cycle Metric #87

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[WIP] Kanren2 #17

[WIP] Kanren2 #17

maxeeem commented Sep 13, 2023

bowen-xu Sep 13, 2023

maxeeem Sep 13, 2023

maxeeem Sep 13, 2023

bowen-xu Sep 13, 2023

bowen-xu Sep 13, 2023

bowen-xu Sep 13, 2023

bowen-xu Sep 13, 2023

maxeeem Sep 13, 2023

maxeeem Sep 15, 2023

bowen-xu Sep 15, 2023

bowen-xu Sep 15, 2023

bowen-xu Sep 15, 2023

bowen-xu commented Sep 15, 2023

bowen-xu commented Sep 15, 2023 •

edited

Loading

maxeeem commented Sep 15, 2023

bowen-xu commented Sep 15, 2023

maxeeem Sep 16, 2023

bowen-xu Sep 16, 2023

maxeeem Sep 16, 2023

bowen-xu Sep 16, 2023

maxeeem Sep 16, 2023

bowen-xu Sep 16, 2023

maxeeem Sep 16, 2023

maxeeem Sep 17, 2023

bowen-xu Sep 17, 2023 •

edited

Loading

maxeeem Sep 17, 2023

bowen-xu Sep 17, 2023

bowen-xu Sep 17, 2023

maxeeem Sep 17, 2023

bowen-xu Sep 17, 2023

bowen-xu Sep 17, 2023

maxeeem Sep 17, 2023

bowen-xu Sep 17, 2023

maxeeem commented Jan 25, 2024


		from unification import unify, reify

		def variable_elimination(t1: Term, t2: Term) -> list:

		- Theorems can be handled explicitly using miniKanren
		should they be applied at the same time as immediate rules?

[WIP] Kanren2 #17

[WIP] Kanren2 #17

Conversation

maxeeem commented Sep 13, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bowen-xu commented Sep 15, 2023

bowen-xu commented Sep 15, 2023 • edited Loading

maxeeem commented Sep 15, 2023

bowen-xu commented Sep 15, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bowen-xu Sep 17, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

maxeeem commented Jan 25, 2024

bowen-xu commented Sep 15, 2023 •

edited

Loading

bowen-xu Sep 17, 2023 •

edited

Loading