:shift-occurrence-forward/backward first attempt

src/nal/core.clj

@@ -13,9 +13,6 @@
 (def revision t/revision)
 
 (comment
-  :seq-interval-from-premises                               ;post
   :shift-occurrence-forward                                 ;pre
   :shift-occurrence-backward                                 ;pre
-  :measure-time                                             ;pre
-  :concurrent
   :linkage-temporal)

src/nal/deriver/matching.clj

@@ -8,8 +8,8 @@
     [nal.deriver
      [set-functions :refer [f-map not-empty-diff? not-empty-inter?]]
      [substitution :refer [munification-map substitute]]
-     [preconditions :refer [sets compound-precondition get-terms
-                            implications-and-equivalences abs
+     [preconditions :refer [sets compound-precondition shift-transformation
+                            implications-and-equivalences get-terms abs
                             preconditions-transformations]]
      [normalization :refer [commutative-ops sort-commutative reducible-ops]
       :as n]
@@ -42,13 +42,18 @@
 (defn form-conclusion
   "Formation of cocnlusion in terms of task and truth/desire functions"
   [{:keys [t1 t2 task-type]}
-   {c :statement tf :t-function pj :p/judgement df :d-function}]
+   {c  :statement tf :t-function pj :p/judgement df :d-function
+    sc :shift-conditions}]
   (let [conclusion-type (if pj :judgement task-type)
-        conclusion {:statement c
-                    :task-type conclusion-type}]
-    (case conclusion-type
-      :judgement (assoc conclusion :truth (list tf t1 t2))
-      :goal (assoc conclusion :desire (list df t1 t2))
+        conclusion {:statement  c
+                    :task-type  conclusion-type
+                    :occurrence :t-occurrence}
+        conclusion (case conclusion-type
+                     :judgement (assoc conclusion :truth (list tf t1 t2))
+                     :goal (assoc conclusion :desire (list df t1 t2))
+                     conclusion)]
+    (if sc
+      (shift-transformation sc conclusion)
       conclusion)))
 
 (defn traverse-node
@@ -69,13 +74,13 @@
        ~(traverse-node vars results tree)
        @~results)))
 
-(defn replace-occurences
+(defn replace-occurrences
   "Reblaces occurrences keywords from matcher's code by generated symbols."
   [code]
-  (let [t-occurence (gensym) b-occurence (gensym)]
+  (let [t-occurrence (gensym) b-occurrence (gensym)]
     (walk code
-      (= :el :t-occurence) t-occurence
-      (= :el :b-occurence) b-occurence)))
+      (= :el :t-occurrence) t-occurrence
+      (= :el :b-occurrence) b-occurrence)))
 
 (defn match-rules
   "Generates code of function that will match premises. Generated function
@@ -84,9 +89,9 @@
   (let [t1 (gensym) t2 (gensym)
         task (gensym) belief (gensym)
         truth-kw (if (= :goal task-type) :desire :truth)]
-    (replace-occurences
-      `(fn [{p1# :statement ~t1 ~truth-kw :t-occurence :occurence :as ~task}
-            {p2# :statement ~t2 :truth :b-occurence :occurence :as ~belief}]
+    (replace-occurrences
+      `(fn [{p1# :statement ~t1 ~truth-kw :t-occurrence :occurrence :as ~task}
+            {p2# :statement ~t2 :truth :b-occurrence :occurrence :as ~belief}]
          (match [p1# p2#] ~(quote-operators pattern)
            ~(traversal {:t1        t1
                         :t2        t2
@@ -195,6 +200,15 @@
     (and (coll? :el) (reducible-ops (first :el)) (<= 3 (count :el)))
     `(~(reducible-ops (first :el)) ~:el)))
 
+(defn find-shift-precondition
+  [preconditions]
+  (first
+    (filter
+      #(and (coll? %)
+            (#{:shift-occurrence-backward
+               :shift-occurrence-forward}
+              (first %))) preconditions)))
+
 (defn premises-pattern
   "Creates map with preconditions and conclusions regarding to the main pattern
    of rules branch.
@@ -230,20 +244,24 @@
                 (if-not (#{`munification-map `not-empty-diff?} f)
                   (concat (list f) (sort-placeholders tail))
                   el)))]
-    {:conclusion {:statement   (-> conclusion
-                                   (preconditions-transformations preconditions)
-                                   (replace-symbols sym-map)
-                                   check-commutative
-                                   check-reduction)
-                  :t-function  (t/tvtypes (get-truth-fn post))
-                  :d-function  (t/dvtypes (get-desire-fn post))
-                  :p/judgement (some #{:p/judgement} post)}
-     :conditions (walk (concat (check-conditions sym-map) pre)
-                   (and (coll? el) (= \a (first (str (first el)))))
-                   (concat '() el)
-                   (and (coll? el) (not ((conj reserved-operators 'quote)
-                                          (first el))))
-                   (vec el))}))
+    {:conclusion {:statement        (-> conclusion
+                                        (preconditions-transformations preconditions)
+                                        (replace-symbols sym-map)
+                                        check-commutative
+                                        check-reduction)
+                  :shift-conditions (replace-symbols
+                                      (find-shift-precondition preconditions)
+                                      sym-map)
+                  :t-function       (t/tvtypes (get-truth-fn post))
+                  :d-function       (t/dvtypes (get-desire-fn post))
+                  :p/judgement      (some #{:p/judgement} post)}
+     :conditions (remove nil?
+                         (walk (concat (check-conditions sym-map) pre)
+                           (and (coll? el) (= \a (first (str (first el)))))
+                           (concat '() el)
+                           (and (coll? el) (not ((conj reserved-operators 'quote)
+                                                  (first el))))
+                           (vec el)))}))
 
 (defn conditions->conclusions-map
   "Creates map from conditions to conclusions."

src/nal/deriver/preconditions.clj

@@ -85,13 +85,13 @@
 
 (defmethod compound-precondition :measure-time
   [_]
-  [`(not= :eternal :t-occurence)
-   `(not= :eternal :b-occurence)
-   `(<= ~duration (abs (- :t-occurence :b-occurence)))])
+  [`(not= :eternal :t-occurrence)
+   `(not= :eternal :b-occurrence)
+   `(<= ~duration (abs (- :t-occurrence :b-occurrence)))])
 
 (defmethod compound-precondition :concurrent
   [_]
-  [`(> ~duration (abs (- :t-occurence :b-occurence)))])
+  [`(> ~duration (abs (- :t-occurrence :b-occurrence)))])
 
 ;-------------------------------------------------------------------------------
 (defmulti precondition-transformation (fn [arg1 _] (first arg1)))
@@ -128,7 +128,7 @@
 (defmethod precondition-transformation :measure-time
   [[_ arg] conclusion]
   (let [mt (gensym)]
-    (walk `(let [~arg (abs (- :t-occurence :b-occurence))]
+    (walk `(let [~arg (abs (- :t-occurrence :b-occurrence))]
              ~(walk conclusion
                 (= :el arg) [:interval arg]))
       (= :el arg) mt)))
@@ -143,3 +143,23 @@
   "Some transformations of conclusion may be required by precondition."
   [conclusion preconditions]
   (reduce check-precondition conclusion preconditions))
+
+(defn shift-transformation
+  [[type arg1 [_ arg2]] conclusion]
+  (let [dur (if (= :shift-occurrence-forward type)
+              duration
+              (- duration))]
+    (cond
+      (and (= :unused arg1) ('#{=|> ==>} arg2)) conclusion
+      (and (= :unused arg1) (not ('#{=|> ==>} arg2)))
+      `(let [:t-occurrence (~(if (= arg2 'pred-impl) `+ `-)
+                            :t-occurrence ~dur)]
+         ~conclusion)
+      ('#{=|> ==>} arg2)
+      `(let [:t-occurrence (+ :t-occurrence ~arg1)]
+         ~conclusion)
+      :default
+      `(let [:t-occurrence (+ (~(if (= arg2 'pred-impl) `+ `-)
+                               :t-occurrence ~dur)
+                              ~arg1)]
+         ~conclusion))))

src/nal/reader.clj

@@ -42,9 +42,7 @@
       (s/replace #"\(\\" "(int-image")
       (s/replace #"\(/" "(ext-image")
       (s/replace #"\$([A-Z])" "(ind-var $1)")
-      (s/replace #"#([A-Z])" "(dep-var $1)")
-      ;todo what does /0 mean?
-      (s/replace #"\/([0-9]+)" "(op $1)")))
+      (s/replace #"#([A-Z])" "(dep-var $1)")))
 
 (defn read-rule [s]
   (-> s replacements add-brackets read-string))

src/nal/rules.clj

@@ -261,10 +261,10 @@
 
   ; conditional syllogism
   ; If after M P usually happens and M happens it means P is expected to happen
-  #R[M (M ==> P) |- P :post (:t/deduction :d/induction :order-for-all-same) :pre ((:shift-occurrence-forward unused ==>))]
-  #R[M (P ==> M) |- P :post (:t/abduction :d/deduction :order-for-all-same) :pre ((:shift-occurrence-backward unused ==>))]
-  #R[M (S <=> M) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-backward unused <=>))]
-  #R[M (M <=> S) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-forward unused ==>))]
+  #R[M (M ==> P) |- P :post (:t/deduction :d/induction :order-for-all-same) :pre ((:shift-occurrence-forward :unused ==>))]
+  #R[M (P ==> M) |- P :post (:t/abduction :d/deduction :order-for-all-same) :pre ((:shift-occurrence-backward :unused ==>))]
+  #R[M (S <=> M) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-backward :unused <=>))]
+  #R[M (M <=> S) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-forward :unused ==>))]
 
   ; conjunction decompose
   #R[(&& :list/A) Ai |- Ai :pre (:contains? (:list/A) Ai) :post (:t/structural-deduction :d/structural-strong)]
@@ -308,7 +308,7 @@
                               (&& (S --> #Y) (P --> #Y)) :post (:t/intersection))
                                   :pre ((:!= S P))]
 
- #R[(S --> M) (P --> M) |- (((&/ (P --> $X) I) =/> (S --> $X)) :post (:t/induction :linkage-temporal)
+  #R[(S --> M) (P --> M) |- (((&/ (P --> $X) I) =/> (S --> $X)) :post (:t/induction :linkage-temporal)
                               ((S --> $X) =\> (&/ (P --> $X) I)) :post (:t/abduction :linkage-temporal)
                               ((&/ (P --> $X) I) </> (S --> $X)) :post (:t/comparison :linkage-temporal)
                               (&/ (P --> #Y) I (S --> #Y)) :post (:t/intersection :linkage-temporal))
@@ -371,11 +371,11 @@
 
 
   ; independent variable elimination
-  #_#R[B (A ==> C) |- C (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward unused ==>))]
-  #_#R[B (C ==> A) |- C (:t/abduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward unused ==>))]
+  #R[B (A ==> C) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward :unused ==>))]
+  #R[B (C ==> A) |- C :post (:t/abduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward :unused ==>))]
 
-  #_#R[B (A <=> C) |- C (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward unused <=>))]
-  #_#R[B (C <=> A) |- C (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward unused <=>))]
+  #R[B (A <=> C) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward :unused <=>))]
+  #R[B (C <=> A) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward :unused <=>))]
 
   ; second level variable handling rules
   ; second level variable elimination (termlink level2 growth needed in order for these rules to work)
@@ -390,7 +390,8 @@
 
   ; NAL7 specific inference
   ; Reasoning about temporal statements. those are using the ==> relation because relation in time is a relation of the truth between statements.
-  #_#R[X (XI ==> B) |- B  :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" XI (&/ X /0)) (:shift-occurrence-forward XI ==>))]
+#R[X ((&/ K (:interval I)) ==> B) |- B  :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" K X) (:shift-occurrence-forward I ==>))]
+  #_#R[X (XI ==> B) |- B  :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" XI (&/ X :interval)) (:shift-occurrence-forward XI ==>))]
   #_#R[X (BI ==> Y) |- BI :post (:t/abduction :d/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" Y X) (:shift-occurrence-backward BI ==>))]
 
   ; Temporal induction:

test/nal/test/core.clj

@@ -9,97 +9,110 @@
                    [&| [--> [ext-set tim] [int-set driving]]]
                    [--> [ext-set tim] [int-set dead]]]
        :truth     [1.0 0.81]
-       :task-type :judgement})
+       :task-type :judgement
+       :occurrence 1})
 
     '[{:statement [--> [ext-set tim] [int-set drunk]]
        :truth     [1 0.9]
        :task-type :judgement
-       :occurence 1}
+       :occurrence 1}
 
       {:statement [==> [&| [--> [ind-var X] [int-set drunk]] [--> [ind-var X] [int-set driving]]]
                    [--> [ind-var X] [int-set dead]]]
        :truth     [1 0.9]
-       :occurence 0}]
-
+       :occurrence 0}]
 
     '({:statement [--> a1 [ext-image m _ a2 a3]]
        :truth     [1 0.9]
-       :task-type :judgement})
+       :task-type :judgement
+       :occurrence 1})
     '[{:statement [--> [* a1 a2 a3] m]
        :truth     [1 0.9]
        :task-type :judgement
-       :occurence 1}
+       :occurrence 1}
 
       {:statement a1
        :truth     [1 0.9]
-       :occurence 0}]
+       :occurrence 0}]
 
-    '[{:statement [&| [--> [* a1 a2 a3] m] a1]
-       :task-type :judgement
-       :truth     [1.0 0.81]}
-      {:statement [<|> a1 [--> [* a1 a2 a3] m]]
-       :task-type :judgement
-       :truth     [1.0 0.44751381215469616]}
-      {:statement [=|> [--> [* a1 a2 a3] m] a1]
-       :task-type :judgement
-       :truth     [1 0.44751381215469616]}
-      {:statement [=|> a1 [--> [* a1 a2 a3] m]]
-       :task-type :judgement
-       :truth     [1 0.44751381215469616]}]
+    '[{:statement [=|> [--> [* a1 a2 a3] m] a1],
+       :task-type :judgement,
+       :occurrence 1,
+       :truth [1 0.44751381215469616]}
+      {:statement [<|> a1 [--> [* a1 a2 a3] m]],
+       :task-type :judgement,
+       :occurrence 1,
+       :truth [1.0 0.44751381215469616]}
+      {:statement [&| [--> [* a1 a2 a3] m] a1],
+       :task-type :judgement,
+       :occurrence 1,
+       :truth [1.0 0.81]}
+      {:statement [=|> a1 [--> [* a1 a2 a3] m]],
+       :task-type :judgement,
+       :occurrence 1,
+       :truth [1 0.44751381215469616]}]
     '[{:statement a1
        :truth     [1 0.9]
        :task-type :judgement
-       :occurence 1}
+       :occurrence 1}
 
       {:statement [--> [* a1 a2 a3] m]
        :truth     [1 0.9]
-       :occurence 0}]
+       :occurrence 0}]
 
-    '({:statement a1 :truth [1 0.44751381215469616] :task-type :judgement})
+    '({:statement a1 :truth [1 0.44751381215469616]
+       :task-type :judgement
+       :occurrence 1})
     '[{:statement [conj a1 a2 a3]
        :truth     [1 0.9]
        :task-type :judgement
-       :occurence 1}
+       :occurrence 1}
 
       {:statement a1
        :truth     [1 0.9]
-       :occurence 0}]
+       :occurrence 0}]
 
-    '[{:statement [&| [--> M S] [[--> M S] [--> M P]]]
-       :task-type :judgement
-       :truth     [1.0 0.81]}
-      {:statement [<|> [--> M S] [[--> M S] [--> M P]]]
-       :task-type :judgement
-       :truth     [1.0 0.44751381215469616]}
-      {:statement [=|> [--> M S] [[--> M S] [--> M P]]]
-       :task-type :judgement
-       :truth     [1 0.44751381215469616]}
-      {:statement [=|> [[--> M S] [--> M P]] [--> M S]]
-       :task-type :judgement
-       :truth     [1 0.44751381215469616]}]
+    '[{:statement [=|> [--> M S] [[--> M S] [--> M P]]],
+       :task-type :judgement,
+       :occurrence 1,
+       :truth [1 0.44751381215469616]}
+      {:statement [<|> [--> M S] [[--> M S] [--> M P]]],
+       :task-type :judgement,
+       :occurrence 1,
+       :truth [1.0 0.44751381215469616]}
+      {:statement [&| [--> M S] [[--> M S] [--> M P]]],
+       :task-type :judgement,
+       :occurrence 1,
+       :truth [1.0 0.81]}
+      {:statement [=|> [[--> M S] [--> M P]] [--> M S]],
+       :task-type :judgement,
+       :occurrence 1,
+       :truth [1 0.44751381215469616]}]
     '[{:statement [[--> M S] [--> M P]]
        :truth     [1 0.9]
        :task-type :judgement
-       :occurence 1}
+       :occurrence 1}
 
       {:statement [--> M S]
        :truth     [1 0.9]
-       :occurence 0}]
+       :occurrence 0}]
 
     '({:statement [conj [--> [dep-var Y] [int-set B]]
                    [==> [--> [ext-set A] [int-set Y]] [--> [dep-var Y] P]]]
        :truth     [1.0 0.81]
-       :task-type :judgement}
+       :task-type :judgement
+       :occurrence 1}
        {:statement [==>
                     [conj [--> [ext-set A] [int-set Y]] [--> [ind-var X] [int-set B]]]
                     [--> [ind-var X] P]]
         :truth     [1 0.44751381215469616]
-        :task-type :judgement})
+        :task-type :judgement
+        :occurrence 1})
     '[{:statement [==> [--> [ext-set A] [int-set Y]] [--> [ext-set A] P]]
        :truth     [1 0.9]
        :task-type :judgement
-       :occurence 1}
+       :occurrence 1}
 
       {:statement [--> [ext-set A] [int-set B]]
        :truth     [1 0.9]
-       :occurence 1}]))
+       :occurrence 1}]))