adding in benchmarks

logicmoo · Feb 8, 2024 · 400e709 · 400e709
1 parent ab8ef80
commit 400e709
Show file tree

Hide file tree

Showing 118 changed files with 91,286 additions and 152 deletions.
diff --git a/MeTTa b/MeTTa
@@ -574,7 +574,8 @@ else
 
     [[ "$wants_print_help" == "1" ]] && { print_help; [[ "$IS_SOURCED" == "1" ]] && return "$EXIT_SCRIPT" || exit "$EXIT_SCRIPT"; }
     [[ -n "${EXIT_SCRIPT+x}" ]] && { [[ "$IS_SOURCED" == "1" ]] && return "$EXIT_SCRIPT" || exit "$EXIT_SCRIPT"; }
-    (DEBUG echo "$METTA_CMD"
+    #DEBUG echo "$METTA_CMD"
+    (
      eval "$METTA_CMD"
     echo $? > "$TEMP_EXIT_CODE_FILE" )
     #rm -f "$TEE_FILE"

diff --git a/examples/performance/comparisons/README.md b/examples/performance/comparisons/README.md
@@ -0,0 +1,108 @@
+| Test                          | Rust MeTTa  | MeTTaLog |
+|-------------------------------|-----------------------------|------------------------|
+| nils_if_control_test_3.metta  | 0m11.563s                    | 0m11.563s              |
+| fibo_hang_10.metta            | 0m3.911s                    | 0m0.412s               |
+| fibo_hang_20.metta            | 0m1.564s                    | 0m1.427s               |
+| fibo_hang_80.metta            | 0m1.549s                    | 0m21.317s              |
+| fibo_hang_900.metta           | 0m1.600s                    | <Still Running>        |
+
+```
+
+# time metta nils_if_control_test_3.metta 2>&1  > /dev/null
+real    0m49.559s
+user    0m49.468s
+sys     0m0.088s
+
+
+# time MeTTa nils_if_control_test_3.metta 2>&1  > /dev/null
+real    0m11.563s
+user    0m11.511s
+sys     0m0.070s
+
+
+# time MeTTa --v_old nils_if_control_test_3.metta 2>&1  > /dev/null
+real    0m8.552s
+user    0m8.609s
+sys     0m0.091s
+
+```
+
+
+
+
+```
+# time metta  fibo_hang_10.metta
+55
+[()]
+
+real    0m0.412s
+user    0m0.388s
+sys     0m0.024s
+
+
+
+# time MeTTa fibo_hang_10.metta
+[55]
+
+real    0m3.911s
+user    0m3.874s
+sys     0m0.056s
+
+```
+
+```
+# time metta fibo_hang_20.metta
+6765
+[()]
+[()]
+
+real    0m1.427s
+user    0m1.411s
+sys     0m0.016s
+
+
+# time MeTTa fibo_hang_20.metta
+[]
+[6765]
+
+real    0m1.564s
+user    0m1.523s
+sys     0m0.059s
+```
+
+
+```
+# time metta fibo_hang_80.metta
+23416728348467685
+[()]
+[()]
+
+real    0m21.317s
+user    0m21.265s
+sys     0m0.052s
+
+
+
+# time MeTTa fibo_hang_80.metta
+[]
+[23416728348467685]
+real    0m1.549s
+user    0m1.500s
+sys     0m0.066s
+```
+
+
+
+```
+# time MeTTa fibo_hang_900.metta
+[]
+[54877108839480000051413673948383714443800519309123592724494953427039811201064341234954387521525390615504949092187441218246679104731442473022013980160407007017175697317900483275246652938800]
+
+real    0m1.600s
+user    0m1.582s
+sys     0m0.036s
+
+
+# time metta fibo_hang_900.metta
+ Unknowm
+```
diff --git a/...ding_performance/add-atom-naive-fib.metta → ...ance/comparisons/add-atom-naive-fib.metta b/...ding_performance/add-atom-naive-fib.metta → ...ance/comparisons/add-atom-naive-fib.metta
diff --git a/examples/performance/comparisons/fibo_hang_10.metta b/examples/performance/comparisons/fibo_hang_10.metta
@@ -0,0 +1,13 @@
+
+(= (fib $n)
+    (if (== $n 0)
+        0
+        (if (== $n 1)
+            1
+            (+ (fib (- $n 1)) (fib (- $n 2))))))
+
+!(println! (fib 10))
+
+
+
+
diff --git a/examples/performance/comparisons/fibo_hang_20.metta b/examples/performance/comparisons/fibo_hang_20.metta
@@ -0,0 +1,15 @@
+
+;; makes this file be treated as if the command line --compile=full  was supplied
+!(pragma! compile full)
+
+(= (fib $n)
+    (if (== $n 0)
+        0
+        (if (== $n 1)
+            1
+            (+ (fib (- $n 1)) (fib (- $n 2))))))
+
+!(println! (fib 20))
+
+
+
diff --git a/examples/performance/comparisons/fibo_hang_80.metta b/examples/performance/comparisons/fibo_hang_80.metta
@@ -0,0 +1,15 @@
+
+;; makes this file be treated as if the command line --compile=full  was supplied
+!(pragma! compile full)
+
+(= (fib $n)
+    (if (== $n 0)
+        0
+        (if (== $n 1)
+            1
+            (+ (fib (- $n 1)) (fib (- $n 2))))))
+
+!(println! (fib 80))
+
+
+
diff --git a/examples/performance/comparisons/fibo_hang_900.metta b/examples/performance/comparisons/fibo_hang_900.metta
@@ -0,0 +1,23 @@
+
+;; makes this file be treated as if the command line --compile=full  was supplied
+!(pragma! compile full)
+
+(= (fib $n)
+    (if (== $n 0)
+        0
+        (if (== $n 1)
+            1
+            (+ (fib (- $n 1)) (fib (- $n 2))))))
+
+(= (fib1 $a $b $n $i)
+   (if (< $n 3)
+        (fib $n)
+        (if (== $i (- $n 2))
+             (+ $a $b)
+            (fib1 $b (+ $a $b) $n (+ $i 1)))))
+
+
+!(println! (fib1 0 1 900 0))
+
+
+
diff --git a/...g_performance/inf-ctl-month-xp-long.metta → ...e/comparisons/inf-ctl-month-xp-long.metta b/...g_performance/inf-ctl-month-xp-long.metta → ...e/comparisons/inf-ctl-month-xp-long.metta
diff --git a/..._performance/inf-ctl-month-xp-short.metta → .../comparisons/inf-ctl-month-xp-short.metta b/..._performance/inf-ctl-month-xp-short.metta → .../comparisons/inf-ctl-month-xp-short.metta
@@ -47,39 +47,7 @@
 ;; Backward Controlled Chainer ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; Backward Chainer.  The arguments of the backward chainer are:
-;;
-;; * Context abstraction updater.  Given the current query and
-;;   context, update the context before recursively calling the
-;;   backward chainer on the proof abstraction.
-;;
-;; * Context argument updater.  Given the current query and context,
-;;   update the context before recursively calling the backward
-;;   chainer on the proof argument.
-;;
-;; * Termination predicate.  Given the current query and context,
-;;   provide the condition of a conditional wrapping the base case and
-;;   recursive step functions (pre-application), as well its results
-;;   (post-application).  Terminating amounts to pruning the reduction
-;;   (as in evaluation) branches.  For now there is only one
-;;   termination predicate for both pre and post application, in the
-;;   future we may want to separate it in two.
-;;
-;; * Query: a metta term of the form (: <PROOF> <THEOREM>) where
-;;   <PROOF> and <THEOREM> may contain free variables that may be
-;;   filled by the backward chainer.
-;;
-;; * Context: a context to be updated and passed to the recursive
-;;   calls of the backward chainer.
-;;
-;; The choice of the arguments of the context updaters and the
-;; termination predicate is justified as follows.  Context updaters
-;; take first the query, which can be viewed an updater modulator,
-;; which then takes the actual context to the return updated one.  An
-;; alternative would have been to construct a contextualized query,
-;; and update that contextualized query instead.  However, we do not
-;; do that to guaranty that the user-programmed inference control does
-;; not interfere with the correctness of the chainer.
+
 (: bc (-> (-> $a $ct $ct)      ; Context abstraction updater
           (-> $a $ct $ct)      ; Context argument updater
           (-> $a $ct Bool)     ; Termination predicate
@@ -183,72 +151,6 @@
 (: depth-terminator (-> $a Nat Bool))
 (= (depth-terminator $query $depth) (is-zero $depth))
 
-;; Prove that Jan non-strictly precedes Jan
-!(assertEqualToResult
-  (bc depth-updater depth-updater depth-terminator
-      (fromNumber 2)
-      (: $prf (≼ Jan Jan)))
-  ((: JPA (≼ Jan Jan))
-   (: Refl (≼ Jan Jan))))
-
-;; Prove that Feb non-strictly precedes Feb
-!(assertEqual
-  (bc depth-updater depth-updater depth-terminator
-      (fromNumber 2)
-      (: $prf (≼ Feb Feb)))
-  (: Refl (≼ Feb Feb)))
-
-;; Prove that Jan precedes Feb
-!(assertEqualToResult
-  (bc depth-updater depth-updater depth-terminator
-      (fromNumber 2)
-      (: $prf (≼ Jan Feb)))
-  ((: JF (≼ Jan Feb))
-   (: JPA (≼ Jan Feb))))
-
-;; Prove that Jan precedes Mar
-!(assertEqualToResult
-  (bc depth-updater depth-updater depth-terminator
-      (fromNumber 3)
-      (: $prf (≼ Jan Mar)))
-  ((: ((Trans Refl) JPA) (≼ Jan Mar))
-   (: ((Trans JPA) FM) (≼ Jan Mar))
-   (: ((Trans JPA) Refl) (≼ Jan Mar))
-   (: ((Trans JPA) JPA) (≼ Jan Mar))
-   (: ((Trans JF) FM) (≼ Jan Mar))
-   (: JPA (≼ Jan Mar))))
-
-;; Prove that Feb precedes May
-!(assertEqual
-  (bc depth-updater depth-updater depth-terminator
-      (fromNumber 4)
-      (: $prf (≼ Feb May)))
-  (: ((Trans FM) ((Trans MA) AM)) (≼ Feb May)))
-
-;; Prove that Feb precedes Jun
-;; return seven values?
-;; !(assertEqualToResult
-  !(bc depth-updater depth-updater depth-terminator
-      (fromNumber 5)
-      (: $prf (≼ Feb Jun)))
-;; (: ((Trans ((Trans FM) MA)) ((Trans AM) MJ)) (≼ Feb Jun)))
-
-;; Prove that Feb precedes Jul
-;; !(assertEqual
-;  !(collapse (bc depth-updater depth-updater depth-terminator
-;      (fromNumber 6)
-;      (: $prf (≼ Feb Jul))))
-;  ;; (: ((Trans FM) ((Trans MA) ((Trans AM) ((Trans MJ) JJ)))) (≼ Feb Jul)))
-
-;; Disabled because it takes 3h.
-;;
-;; ;; Prove that Feb precedes Aug
-;; ;; !(assertEqual
-;;   !(bc depth-updater depth-updater depth-terminator
-;;       (fromNumber 7)
-;;       (: $prf (≼ Feb Aug)))
-;;   ;; (: ((Trans FM) ((Trans MA) ((Trans AM) ((Trans MJ) JJ)))) (≼ Feb Jul)))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Context is depth and target theorem ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -290,54 +192,11 @@
                ;; [3th observation] Otherwise, Trans is enough.
                (or (== $prf JPA) (== $prf Refl))))))
 
-;; Prove that Jan non-strictly precedes Jan
-!(assertEqual
-  (bc td-updater td-updater td-terminator
-      (MkTD (≼ Jan Jan) (fromNumber 2))
-      (: $prf (≼ Jan Jan)))
-  (: Refl (≼ Jan Jan)))
-
-;; Prove that Feb non-strictly precedes Feb
-!(assertEqual
-  (bc td-updater td-updater td-terminator
-      (MkTD (≼ Feb Feb) (fromNumber 2))
-      (: $prf (≼ Feb Feb)))
-  (: Refl (≼ Feb Feb)))
-
-;; Prove that Jan precedes Feb
-!(assertEqualToResult
-  (bc td-updater td-updater td-terminator
-      (MkTD (≼ Jan Feb) (fromNumber 2))
-      (: $prf (≼ Jan Feb)))
-  ((: JF (≼ Jan Feb))
-   (: JPA (≼ Jan Feb))))
-
-;; Prove that Jan precedes Mar
-!(assertEqual
-  (bc td-updater td-updater td-terminator
-      (MkTD (≼ Jan Mar) (fromNumber 4))
-      (: $prf (≼ Jan Mar)))
-  (: JPA (≼ Jan Mar)))
-
-;; Prove that Feb precedes May
-!(assertEqual
-  (bc td-updater td-updater td-terminator
-      (MkTD (≼ Feb May) (fromNumber 4))
-      (: $prf (≼ Feb May)))
-  (: ((Trans FM) ((Trans MA) AM)) (≼ Feb May)))
-
-;; Prove that Feb precedes Jun
-!(assertEqualToResult
-  (bc td-updater td-updater td-terminator
-      (MkTD (≼ Feb Jun) (fromNumber 5))
-      (: $prf (≼ Feb Jun)))
-  ((: ((Trans ((Trans FM) MA)) ((Trans AM) MJ)) (≼ Feb Jun))
-   (: ((Trans FM) ((Trans MA) ((Trans AM) MJ))) (≼ Feb Jun))))
 
 ;; Prove that Feb precedes Jul
 !(assertEqualToResult
   (bc td-updater td-updater td-terminator
-      (MkTD (≼ Feb Jul) (fromNumber 6))
+      (MkTD (≼ Feb Jul) (fromNumber 5))
       (: $prf (≼ Feb Jul)))
   ((: ((Trans ((Trans FM) ((Trans MA) AM))) ((Trans MJ) JJ)) (≼ Feb Jul))
    (: ((Trans ((Trans FM) MA)) ((Trans ((Trans AM) MJ)) JJ)) (≼ Feb Jul))