CALM bug? – translation attribute (Herbrand term related)

[anuradha252]

here is a small portion of the entity_event_and_action module

module entity_event_and_action sort declarations thing :: universe entity :: thing event :: thing attributes agent : entity -> booleans object : entity -> booleans

function declarations statics defined defined_agent : event -> booleans defined_object : event -> booleans

axioms defined_agent(X) if agent(X, Y). defined_object(X) if object(X, Y).

the exact error message Exception in thread "main" java.lang.RuntimeException: SPARC V2.54 : predicate agent of arity 2 at line 588, column 21 was not declared

line number 588 is % Definition for function [defined_agent]. defined_agent(X) :- agent(X, Y).

Please find generated SPARC program attached along with this wrestling_SPARC.txt. In that, I actually don’t see agent in the sort section. We have an event_agent % Attribute Function [agent] for sort [event]. event_agent(#event, #entity).

So I wonder if this line

% Definition for function [defined_agent]. defined_agent(X) :- agent(X, Y).

should have been

% Definition for function [defined_agent]. defined_agent(X) :- event_agent (X, Y).

[zhangyuanlin]

Good job, Anu. Here is my quick summary of the possible bug.

event :: thing
      attributes
        agent : entity -> booleans
……
  function declarations
    statics 
      defined
        defined_agent : event -> booleans
……
axioms
    defined_agent(X) if agent(X, Y).
……

The axiom above is translated into

% Definition for function [defined_agent].
defined_agent(X) :- agent(X, Y).

But agent(X,Y) should be event_agent(X, Y)?

[Topology]

This bug is now fixed and committed to the master branch. I am now looking up the fully qualified function name from the symbol table when writing the sparc programs.

This issue is the same as #15. I'd prefer we didn't create new issues for redundant things, just provide more detail on the original issue.

[zhangyuanlin]

It is different from #15. We distinguish an issue (#15 for discussion) and a bug report (#16). So, in the subject title of this issue we have word "bug".

[anuradha252]

does this bug fix reflect in the latest calm.jar available on google drive? because I received the same error on testing again.

[Topology]

It is now updated in the calm.jar.

[anuradha252]

On running the module with the new jar, I do not see an error however i do not see an output sparc file either. Would there be any specific reason for it?

[Topology]

Please post the ALM program you are currently testing with that has no output sparc file.

[zhangyuanlin]

I opened a separate bug for this no output file in #21. I posted a file there.

[Topology]

Does my explanation in 21 cover why there is no output here? Or is there a structure in the system description and there is still no output?

[zhangyuanlin]

I think so. That's not a bug then.

[zhangyuanlin]

This directly plays into the Herbrand term on the right hand side. I will need to work on that. However we need to discuss how complex of a solution. Are we going to require a ground Herbrand term? (from #20)

Just recalled that you the righ hand side Herbrand decision. I think we can add as much simplification as needed to make implementation easy. Igore other things for now. E.g., we don't require the term ground, unless it makes implementation easier.

1. Edward, can add "Herbrand Term in Structure" at the end of the title of this issue? 2.Future: We need a clear understanding/theory of Herbrand term in both Theory and Structure 2.1 For theory, we have an initial understanding in discussion #3. 2.2 For structure, it is new. The question is where do we allow Herbrand term? Currently we allow in instantiation such as t(1) in tSorts. Another place is the attribute assignment, seems that we should allow Herbrand term (but not sure if we should allow a normal function). Current CALM allows normal function but not Herbrand function. If we allow both Herbrand and normal function in a term, they could be nested. As for Herbrand function, we don't have a declaration mechanism for it. Type checking may be used to keep consistent use of Herbrand function symbols.