Bug in issue code: Transitive `isa` Inference Fails with `BadType` Error Due to Restrictive Default Signature

[sivaji1012]

pip show hyperon
Name: hyperon
Version: 0.2.8+ga696c359
Summary: Hyperon API in Python
Home-page: https://github.com/trueagi-io/hyperon-experimental
Author:
Author-email:
License: MIT License
Location: /home/shivaji1012/AGI_Seed_Knowledge/.venv-agi/lib/python3.12/site-packages
Editable project location: /home/shivaji1012/hyperon-experimental/python
Requires:
Required-by:

Description:

When using a transitive inference rule for the isa predicate, a BadType error occurs. This happens because the interpreter appears to use a default, restrictive type signature for isa (-> Entity ...) that conflicts with the logic of the transitive rule, which needs to operate on untyped symbols.

The issue is reproducible in a clean environment (like the MeTTa dev playground) using the minimal example below.

---

Minimal Reproducible Example:

This self-contained script demonstrates the bug. It defines a minimal ontology with a transitive isa rule and then attempts to infer that a LivingAgent is an Entity.

;; Minimal script to reproduce the 'isa' inference bug.

;; --- Core Ontology ---
(: Type Type)
(: Entity Type)
(: Object Type)
(: Agent Type)
(: LivingAgent Type)
(: Pair Type)
(: TruthValue Type)
(subtype TruthValue Pair)

;; Using the restrictive signature that causes the error.
(: isa (-> Entity Type TruthValue Type))
(: subtype (-> Type Type TruthValue Type))

;; Transitive subtype and isa rules.
(subtype LivingAgent Agent (Pair 1.0 1.0))
(subtype Agent Object (Pair 1.0 1.0))
(subtype Object Entity (Pair 1.0 1.0))

(= (isa $x $B (Pair $s3 $c3))
    (and (isa $x $A (Pair $s1 $c1))
         (subtype $A $B (Pair $s2 $c2))
         (Pair (* $s1 $s2) (* $c1 $c2))))

;; --- Example Fact ---
(isa human-02 LivingAgent (Pair 0.9 0.8))

;; --- The Query That Fails ---
!(isa human-02 Entity (Pair $s $c))

---

Observed Behavior:

The query fails with a BadType error that originates from inside the transitive rule, indicating a conflict with the isa predicate's signature.

[(Error (isa human-02 $A#101 (Pair $s1#102 $c1#103)) BadType)]

---

Expected Behavior:

The query should successfully execute the chain of reasoning (human-02 -> LivingAgent -> Agent -> Object -> Entity) and return the calculated truth value. For example:

[(Pair 0.9 0.8)] 

---

Analysis & The Fix:

The error is resolved by making the isa predicate's signature more general. The inference rule needs to be able to work with an untyped Atom as its subject.

When the following line in the script:
(: isa (-> Entity Type TruthValue Type))

Is changed to:
(: isa (-> Atom Type TruthValue Type))

The query succeeds. This suggests the interpreter's default type checking for isa is too restrictive for the inference rule to function correctly.

[vsbogd]

I would rather expect that issue is type of `and` is incompatible with `TruthValue`. I am almost sure there is no `isa` definition in the standard library. But I am sure `and` expects `Bool` not `TruthValue`. There is PR with `BadType` improvement under review. Will try it to see whether error is more descriptive.

[vsbogd]

Please find the corrected program with comments below:

;; Minimal script to reproduce the 'isa' inference bug.

;; --- Core Ontology ---
(: Type Type)
(: Entity Type)
(: Object Type)
(: Agent Type)
(: LivingAgent Type)
; NB correct type for Pair, if pair is more generic then it is better to
; introduce a separate type constructor for TruthValue
(: Pair (-> Number Number TruthValue))
(: TruthValue Type)
; NB not critical but seems to be incorrect fact
(subtype TruthValue Pair)

;; Using the restrictive signature that causes the error.
(: isa (-> Entity Type TruthValue Type))
(: subtype (-> Type Type TruthValue Type))

;; Transitive subtype and isa rules.
(subtype LivingAgent Agent (Pair 1.0 1.0))
(subtype Agent Object (Pair 1.0 1.0))
(subtype Object Entity (Pair 1.0 1.0))

; NB function which either returns the immediate subtype or calculates truth
; value transitively
(= (subtype $A $C (Pair $s $c))
   ; NB unify allows handling both found and not found branches (match cannot
   ; do this)
   (unify &self (subtype $A $C (Pair $s $c))
     ; NB immediate fact, noeval prevents recursive evaluation
     (noeval (subtype $A $C (Pair $s $c)))
     ; NB transitive fact
     (unify &self (subtype $A $B (Pair $s1 $c1))
       (let $next (subtype $B $C (Pair $s2 $c2))
         ; NB return truth value via parameters
         (let $s (* $s1 $s2)
           (let $c (* $c1 $c2)
             ; NB calculated fact, noeval prevents recursive evaluation
             (noeval (subtype $A $C (Pair $s $c))) )))
       (empty) )))

; NB same structure as for a subtype
(= (isa $x $B (Pair $s3 $c3))
   (unify &self (isa $x $B (Pair $s3 $c3))
     (noeval (isa $x $B (Pair $s3 $c3)))
     (let $_ (isa $x $A (Pair $s1 $c1))
       (let $__ (subtype $A $B (Pair $s2 $c2))
         (let $s3 (* $s1 $s2)
           (let $c3 (* $c1 $c2)
             (noeval (isa $x $B (Pair $s3 $c3))) ))))))

;; --- Example Fact ---
(isa human-02 LivingAgent (Pair 0.9 0.8))

;; --- The Query That Fails ---
!(subtype LivingAgent Agent (Pair $s $c))
!(subtype LivingAgent Object (Pair $s $c))
!(subtype LivingAgent Entity (Pair $s $c))

!(isa human-02 LivingAgent (Pair $s $c))
!(isa human-02 Entity (Pair $s $c))

!(let $_ (isa human-02 Entity (Pair $s $c)) (Pair $s $c))

[vsbogd]

My understanding that the purpose of the code is to allow either match existing facts from atomspace or produce them using transitive rules. Using and doesn't work in this way. and is a standard library function on boolean values and applying it to other types of values doesn't work.

I would recommend using union instead. union is a function which matches two atoms and allows processing both matched and not matched scenarios. If one of the atoms is space then union works similarly to match but with two templates: first for the case when query is found in space and second for the case when query brings no results.

Thus isa could be rewritten using union to find the fact in the &self atomspace or (if fact not found) check whether there is a fact for some more general sub-type of Object. As isa is a type constructor I would return (isa ...) fact instead of Pair. To prevent infinite loop (when isa is evaluated further again and again) one can use noeval to return the fact without evaluating it further. Also one can use (let $s (* $s1 $s2) ...) to additionally return final truth value via isa parameters.

The final code looks like this:

(= (isa $x $B (Pair $s3 $c3))
   (unify &self (isa $x $B (Pair $s3 $c3))
     (noeval (isa $x $B (Pair $s3 $c3)))
     (let $_ (isa $x $A (Pair $s1 $c1))
       (let $__ (subtype $A $B (Pair $s2 $c2))
         (let $s3 (* $s1 $s2)
           (let $c3 (* $c1 $c2)
             (noeval (isa $x $B (Pair $s3 $c3))) ))))))

Please note that subtype should be written is the similar way if it should take into account transitive type relations. This is the case in the example because LivingAgent is a subtype of Agent which in turn as subtype of Entity. See previous comment for the full source code.

Finally one can see that code works correctly using simpler calls:

!(subtype LivingAgent Agent (Pair $s $c)) ; returns fact from the atomspace
!(subtype LivingAgent Object (Pair $s $c)) ; handles one step transitive relation
!(subtype LivingAgent Entity (Pair $s $c)) ; handles two steps transitive relation

!(isa human-02 LivingAgent (Pair $s $c)) ; returns fact from the atomspace
!(isa human-02 Entity (Pair $s $c)) ; generates fact using transitive type relation

!(let $_ (isa human-02 Entity (Pair $s $c)) (Pair $s $c)) ; gets truth value via parameters of `isa` and returns it

[vsbogd]

You can find more about MeTTa syntax and library functions at Learn MeTTa page

[vsbogd]

Transferring issue into https://github.com/trueagi-io/metta-examples as it is more relevant.