Closed zhangyuanlin closed 5 years ago
Here is the whole testing program:
system description monkeyBanana
theory basic_motion
module moving
sort declarations
points, things :: universe
agents :: things
carriables :: things
elevations :: things
attributes
top: points
move :: actions
attributes
actor : agents
origin : points
dest : points
climb :: move
attributes
elevation : elevations
function declarations
statics
basic
symmetric_connectivity : booleans
transitive_connectivity : booleans
fluents
basic
% connnected(P1, P2) - true if P1 and P2 are connected
connected : points * points -> booleans
% loca_in(T) - the point where thing T is at
total loc_in : things -> points
axioms
dynamic causal laws
% move action causes its actor to be at its destination
occurs(X) causes loc_in(A) = D if
instance(X, move),
actor(X) = A,
dest(X) = D.
state constraints
% top(E) is the destination of climbing an elevation E
dest(A) = C if elevation(A) = E, C = top(E).
connected(X, X).
connected(X, Y) if connected(Y, X),symmetric_connectivity.
-connected(X, Y) if -connected(Y, X),symmetric_connectivity.
connected(X, Z) if
connected(X, Y),connected(Y, Z),transitive_connectivity.
% NEW bug?
executability conditions
% move is not possible if its actor is not at its origin.
% NEW - what if the origin of actor unknown?
impossible occurs(X) if
instance(X, move),actor(X) = A,loc_in(A) != origin(X).
% instance(X, move), loc_in(actor(X)) != origin(X).
% move is not possible if its actor is at its dest.
impossible occurs(X) if
instance(X, move),actor(X) = A,loc_in(A) = dest(X).
% instance(X, move), loc_in(actor(X)) = dest(X).
% move is not possible if the location of its actor is not
% connected to its dest.
impossible occurs(X) if
instance(X, move),
actor(X) = A,
loc_in(A) = O,
dest(X) = D,
-connected(O, D).
module main depends on moving
sort declarations
floor_points, ceiling_points, movable_points :: points
constant declarations
monkey : agents
box : elevations
% top = top(box)
% top(elevations): movable_points
box, banana : carriables
function declarations
statics
basic
% under(P, T) - point P is under thing T
under : floor_points * things -> booleans
axioms
function definitions
% monkey can reach the banana if it is on top of the box
% which under the banana
%?? can_reach(monkey, banana) if
% loc_in(box) = P, under(P,banana),loc_in(monkey) = top(box).
state constraints
% top(E) is the destination of climbing an elevation E
% NEW ??
%dest(A) = C if instance(A, climb), elevation(A) = E, C = top(E).
% The location of the box is connected to the top of the box
connected(T,P) if
loc_in(box) = P, T= top(box), instance(P, floor_points).
% top of box is not connected to
% any points other than the box's location.
-connected(top(box),P) if
loc_in(box) != P, instance(P,floor_points).
% any two points on floor are connected
connected(P1,P2) if
instance(P1,floor_points), instance(P2, floor_points).
% any ceiling point is not connected to any other point
-connected(P1, P2) if
instance(P1, ceiling_points),
instance(P2,points), P1 != P2.
executability conditions
structure monkey_and_banana
instances
under_banana, initial_monkey, initial_box in floor_points
initial_banana in ceiling_points
box in elevations
top = top(box)
% top = t(box)
top(X) in movable_points where instance(X, elevations)
move(P) in move where instance(P, points)
actor = monkey
dest = P
climb(box) in climb
actor = monkey
elevation = box
dest = top(box)
value of statics
under(under_banana, banana).
symmetric_connectivity.
-transitive_connectivity.
temporal projection
max steps 7
history
observed(loc_in(box), initial_box, 0).
observed(loc_in(monkey), initial_monkey, 0).
happened(move(initial_box), 0).
%happened(grasp(box), 1).
%happened(carry(box, under_banana), 2).
%happened(release(box), 3).
%happened(climb(box), 4).
%happened(grasp(banana), 5).
This is a compiler bug.
elevations_top(box, T_) :- instance(top(box), points), elevations_top(box, TO), T_=TO.
should be
elevations_top(box, T_) :- instance(top(box), points), T_= top(box).
The problem is name collision. What is happening is that the top(box) in the correct case is resolved with the attribute function instead of the functor/constant. This makes me think that the translation of attribute functions to be prefixed by their sort does not happen until late in the game and may need to happen immediately. But there would still be ambiguity in term relations as to whether the instance was intended or the function was intended.
foo(X) = top(box)
There is name ambiguity.
I will look and see if there is an easy way to disambiguate in the step going from ALM to ASP{f}. The translation from ASP{f} to SPARC has less context sensitivity. I may need to add annotations/markers to ALMTerms to force resolution with "functors" instead of functions.
Alternatively we bail out and generate semantic errors if a functor and function have the same name.
Thanks. I think here we need to decide if we want to allow people to use function to define an instance. For example, in
instances
box in elevations
top = top(box)
do we allow top(..) to be a function?
For now, one proposal is
1. all terms in right-hand side in an instantiation are understood as Herbrand terms.
1.1 current CALM allows to define an instance using Herbrand term, e.g., top(box) in points
2. in future, we can discuss if we allow function to be used in instantiation.
2.1. This issue may be also related if we want to introduce "record sort" (e.g., we can declare
top(elevations) :: points -- [you use a different syntax in the relevant discussion]
)
Conclusion: With this understanding, attribute functions can be used to achieve "constants with parameters" (see program I posted in earlier comment) and we don't need to do any change of CALM for now. However, "record sort" might be still a better idea.
From Discussion
box in elevations
top = top(box)
top(X) in movable_points where instance(X, elevations)
-------------- BROKEN---------
% Sort Instance [box] for sort [elevations].
is_a(box, elevations) :- instance(elevations_top(box), points).
% Sort Instance [elevations_top(X)] for sort [movable_points].
is_a(elevations_top(X), movable_points) :- instance(X, elevations).
% Definition of attribute [top] for instance [box] of sort [elevations].
elevations_top(box, T_) :- instance(elevations_top(box), points), elevations_top(box, TO), T_=TO.
------------------ Attempted fix, but circular ----------------------
% Sort Instance [box] for sort [elevations].
is_a(box, elevations) :- instance(top(box), points).
% Sort Instance [elevations_top(X)] for sort [movable_points].
is_a(top(X), movable_points) :- instance(X, elevations).
% Definition of attribute [top] for instance [box] of sort [elevations].
elevations_top(box, T_) :- instance(top(box), points), T_=top(box).
-----------------------
% Sort Instance [box] for sort [elevations].
is_a(box, elevations) :- (where clauses).
% Definition of attribute [top] for instance [box] of sort [elevations].
elevations_top(box, T_) :- instance(top(box), points), T_=top(box), (where clauses).
% Sort Instance [elevations_top(X)] for sort [movable_points].
is_a(top(X), movable_points) :- instance(X, elevations).
1. remove instance requirements on range of attribute functions for definition. (when herbrand)
2. RHS as herbrand, not function
Will likely need to add marker to herbrand terms in attribute function definition.
Skip type checking for now, do what needs to be done to get the string literal forward.
Latest calm.jar can now run these two programs that have herbrand terms assigned to attributes.
program 1:
system description monkeyBanana
theory basic_motion
module moving
sort declarations
points, things :: universe
movable_points :: points
% intended: the instances of movable_points
% are surface(X) where X is an elevation
% the instances of elevations are some objects
% whose attribute is an elment in points.
elevations :: things
attributes
top: points
structure monkey_and_banana
instances
box in elevations
top = surface(box)
surface(X) in movable_points where instance(X, elevations)
program 2:
system description test
theory test
module test
sort declarations
things :: universe
locations :: universe
elevations :: universe
attributes
top: locations
things_with_elevations :: things
structure attribute_test
instances
top2(X) in locations where instance(X, elevations)
X in elevations where instance(X, things_with_elevations)
top = top2(X)
box in things_with_elevations
I do not consider these permanent solutions. We need to formally model herbrand terms in the compiler. I disabled several aspects of type checking and translation error checking to put these through quickly.
Program 2 did not have circularity in instance definitions. I had to disable the instance(surface(box), points)
condition in program 1 to make it non-circular.
I just uploaded a distribution that I believe resolves this issue for now. Please verify. The program posted in this issues, however, has other issues. The compiler is now reporting name collisions. (See Below) I believe these name collision errors are correct for the posted program. I am closing this issue. If there are any further issues related to this, I believe the code base has migrated enough to warrant a new issue being created.
--------------------------
---- NO SYNTAX ERRORS ----
--------------------------
-------------------------
---- SEMANTIC ERRORS ----
-------------------------
ErrorID: NAM003
Message: Sort Instance [box at (test.alm:118:8)] cannot have the same name as element [box:elevations at (test.alm:79:3)].
Explanation: The names of sort instances must be new and not collide with functions, constants or previously defined sort instances.
Recommendation: Change the name of one of the elements to avoid name collision.
ErrorID: NAM003
Message: Sort Instance [top(X) at (test.alm:122:8)] cannot have the same name as element [top:points at (test.alm:12:16)].
Explanation: The names of sort instances must be new and not collide with functions, constants or previously defined sort instances.
Recommendation: Change the name of one of the elements to avoid name collision.
Given
The instance
is translated into
top(box) in the instance is understood by CALM as applying function top to box. Can it be understood as a Herbrand term? in fact, we do have the following instance in the same program.
In summary, what is the right understanding of a right-hand side term in instantiation? (If it is understood as an Herbrand term, then attributes seem (is conjectured) to be used to represent "constants with parameters as in ALM paper")