How to understand it? How it may be best used to model a problem?

--- Edward's comments ---

It is true that "top(X)" is not recognized as a constant. Currently we only support ground constants. I can fix this, but the fix is going to be complicated. I would need to start grounding the rules with all possible constant substitutions in these occurrences. It would take me about 8+ hours of work to do this and I suspect that a more generalized theory and handling of non-ground constants is necessary.

I think this brings back the question, how valuable are constants in modeling? Philosophically, if we can model without the use of constants, should we use constants? The use of constants should not be a gate-way to introducing structure elements into the theory.

In formal Algebra, groups and fields have special elements and operations. Each group has a unique operator and an identity element under the operator. + and 0 for addition, * and 1 for multiplication, etc. I can understand that if we were modeling a finite group theory that using constants for the operator and identity element would be appropriate and allow substitution when mapping through group theory onto a specific instance of a group in the structure.

The monkey-banana problem use of constants seems to be more about avoiding the work of creating a more generalized modeling of the scenario. The top of anything that is flat can be a target for standing on (elevation). What if there are more boxes in the room?

I think we need to have a more theoretical discussion about the purpose of constants in theories. It usually denotes significance of a singleton entity. The monotheistic God would be a constant in a theory, but polytheistic gods would be instances in structures. If there can be more than 1, then why is it not being instantiated in the structure instead of the theory? And if there can only be one, why is it not just a flat name, a string literal?

I think the answer to these questions is that between two different string literals "box" and "top(box)" there is no relationship between them except the relationships that we painfully detail out through axioms. But a constant "top(X)" where X is a thing, and "box" is a thing that can substitute for "X" has the relationships tied together through sub-structure. It becomes possible to extract "box" out of "top(box)". So I see the utility. But I don't see why we are not modeling the scenario a different way.

boxes :: things attributes topOf : elevations

Structure

top(X) in elevations where instance(X, box).

box in boxes topOf = top(box)

I am not saying I have the right modeling of top and boxes here. I don't even know if the above structure will become instantiated as there may be a circular dependency between the definitions of the instantiations.

What I am saying is that we should have the attitude as modelers of scenarios that we should avoid modeling with constants unless absolutely necessary. Constants seem more about singleton entities in generalized theories and that perhaps a flat string literal is sufficient in these cases.

thoughts?

For top(X), named as constant in ALM paper, we should really take top as a "function" (in the sense in logic program with Herbrand interpretation). So, top(X) is not a constant, but only top is. SPARC solution is handy here. In SPARC, we understand top as a record (e.g., in C) builder. We can introduce a new construct in ALM. Using monkey banana as an example below. (I feel the meaning should be clear although futher thoughts may be needed. However, for now, I don't have an idea on how implementation may be done.)

theory ... climbing module ... sort declarations elevations :: things top(elevations) :: points % a new anonymous sort defined as {top(x): x \in elevations} axioms dest(A) = top(E) if elevation(A) = E. % top could be function name or
% a (Herbrand) term, i.e., a record name to construct an object ... structure box: elevations % once elevations defined, sort top(elevations) is defined automatically

The design of treating record sort seems to be not as complex as I felt.
It seems to be simple and elegant. (Implementation could still take significant time.)

Here is an outline: --- type checking --- when come across f(...), have two cases: f: is a function name: do type checking on the parameters of f. the range of f is the type of f(...) f: is a record name: do type checking on parameters of f, the most immediately parent sort is the type of f(...). One issue: should we introduce an anonymous record sort, e.g., declare f: top(elevations) -> integer.

--- translation ---

Sort def. we seems to need an anonymous sort. in alm one can declare g: top(elevations) -> integer. or top(elevations) :: points in sparc we might need

a_top = top(elevations);

then we have g(#a_top, integer) for subsort "top(elevations) :: points" we only need to make sure the elements in top(elevations) are includes in the parent sorts.
statements e.g., dest(A) = top(E) when top is a record name, we don't introduce a new relation. assume dest(A) represented in SPARC by dest(A, Location, Time) then the above can be translated as dest(A, Location, Time), Location = top(E).

I also include earlier communications among Ed, YL and MG below.

(My intuition is not to allow.)

WHY? I do not mind prohibiting this. As I mentioned before renaming constants in the structure is not something I believe to be very important. But, as a general principle, a restriction should be justified.

Best, M

From: Zhang, Y Sent: Thursday, July 5, 2018 2:36:31 PM To: Gelfond, Michael; Edward Wertz Subject: Re: The use of constants in ALM.

Thanks. To clarify, consider some example. === In theory, assume we have object constants box : carriables, elevations top(elevations) : points

In structure, object definition box = table. === In the example, constant box is interpreted by table in the structure. Should we allow programmer to interpret record (name) top(...) by a different name in a structure? (My intuition is not to allow.)

Thanks, YL

From: Gelfond, Michael Sent: Wednesday, July 4, 2018 11:32 PM To: Zhang, Y; Edward Wertz Subject: Re: The use of constants in ALM.

Sorry, I missed this yesterday.

About your question. I am not sure I know what you are asking. We do not need to define top in structure because it is already defined in the theory. But in general, structure can contain new records, e.g. given a sort "names" we can write, say: name(michael,gelfond) in names

If I am not answering your question perhaps we can talk tomorrow on Skype. Best, M

I think I mean record. So, programmers are not expected to define "top" in structure, right? (however, they can define a simple constant in structure.)

From: Zhang, Y Sent: Monday, July 2, 2018 11:16:43 PM To: Gelfond, Michael; Edward Wertz Subject: Re: The use of constants in ALM.

I do not know what object constructor mean. top(box) is simply a record, like in Sparc. Top is not a function symbol. Look at our definitions of sorts there.

I think I mean record. So, programmers are not expected to define "top" in structure, right? (however, they can define a simple constant in structure.)

From: Gelfond, Michael Sent: Monday, July 2, 2018 10:54:29 PM To: Zhang, Y; Edward Wertz Subject: Re: The use of constants in ALM.

"In o = y do we require y to be an instance occurring in instance statements? " I did not think about it. Logically, it should be, but do we want to force a programmer to mention y twice? So, I am inclined not to require it, but really, whatever you decide is fine. These types of statement were not actually used in our programs. They are included in the language just to be faithful to the definition of structure (or, synonymously, interpretation) which allow interpretation of constants.
I do not know what object constructor mean. top(box) is simply a record, like in Sparc. Top is not a function symbol. Look at our definitions of sorts there.

Best, M

From: Zhang, Y Sent: Monday, July 2, 2018 10:27:53 PM To: Gelfond, Michael; Edward Wertz Subject: Re: The use of constants in ALM.

Thanks, Michael, for your quick response.

In o = y do we require y to be an instance occurring in instance statements?

In terms of modeling, I'd like to have an intuitive understanding an "object constant". By the intended meaning of top(elevations), an object constant declaration seems to be an object constructor.

For object constructor, it seems that normally, we want to understand the "function symbol" as it is. Should we allow to map the "function symbol" in an object constructor to a different one in the structure? If so, what may be the syntax?

Thanks.

From: Gelfond, Michael Sent: Monday, July 2, 2018 8:45:34 PM To: Edward Wertz; Zhang, Y Subject: Re: The use of constants in ALM.

Hi Edward, it is great to hear from you. I am happy to learn that you apparently is healthy enough to keep you industry job and even work on the dissertation. My sincere respect and best wishes.

You are asking good questions. I did not look at ALM for a while and do not remember all the details. But,..

First, the comment on page 23 look mysterious to me now. The footnote is clearly in the wrong place. I think we just wanted to allow a structure to contain statements of the form o = y where o : type is a constant definition in the theory.

For instance, in one structure box may denote a particular chair, in another, a particular ladder, etc. So, in the structure we say, e.g. Box = chair and in another structure Box = ladder.

In the first structure sort elevations will contain "chair", in the second - "ladder". If a structure contains no definition of Box then "elevations" will contain "box". Similarly, for the sort "carriables".

You write: If there had been a definition "box = box1" in the structure, would it still be proper to use the term "box" or should it be a semantic error?

I think it should be a semantic error. Any objections to it?

Question about top(elevation). The intended meaning was 2 . If in a particular structure "elevations" has two instances, "chair" and "ladder" then sort "points" contains "top(ladder)" and "top(chair)".

We could not figure out how to model it as an attribute function. Suppose monkey wants to climb to the ladder. To make it a special case of move, its destination must be a point. So top(ladder) must be a point. But maybe you can come up with an alternative representation.

Hope this helps. Please do not hesitate to ask questions. I can use Skype if it is more convenient.

Again, happy to hear that you seem to be converging. I'd like to be able to call you doctor (as well as being able to use ALM). Very best, Michael

From: Edward Wertz edward.o.wertz@gmail.com Sent: Monday, July 2, 2018 8:36:17 AM To: Gelfond, Michael; Zhang, Y Subject: The use of constants in ALM.

Dr. Gelfond,

I hope this email finds you doing well. I've been working in industry for over a year now and slowly picking away at my dissertation. I'm polishing up the capabilities of the ALM Compiler I've been working on and I have a few questions about the understanding of constants in ALM.

In the footnote on page 23 in the attached ALM paper with Dr. Inclezan it indicates that any constant that is not defined in the structure is to be interpreted as itself and belongs to the universe.

For undefined constants It is my intended implementation of the footnote to create a new instance element of the same name. It is not stated in the footnote, but it would seem appropriate and necessary to infer that the instance must also belong to every sort that the constant is declared to belong to in the theory. Is this correct? This decision impacts the behavior of type checking and the ability to use the constants in the sorted positions of axioms.

At the bottom of page 34 and top of page 35 the structure of the monkey banana alm program is provided. The element "box" is defined as a constant in the theory, belonging to the sorts carriables and elevations, but does not have a definition to an explicit instance. The term "box" is used in multiple instance definitions in the structure: "carry(box,P)" and "climb(box)" and is used as a value assigned to the attributes of these instances.

From the absence of the explicit definition of the interpretation of "box", I have a question about the intended understanding of the term "box" in the structure. Is this term the constant "box" from the theory, or is it the instance "box", which is implied by the footnote on 23? If there had been a definition "box = box1" in the structure, would it still be proper to use the term "box" or should it be a semantic error and instead the program writer should have used "box1" where box occurs?

The decision here may not matter if the use of the constant is treated as syntactic sugar and substitution of constants by their definitions occurs for the structure as well. I would presume that a canonical or well formed structure would not use constants from the theory. Is this correct?

My next question also comes from the monkey banana program. At the bottom of page 32 there is a use of a parameterized constant "top(elevations) : points" where the parameters can be sorts previously declared in the hierarchy. My question is related to the intended set of ground constants that this term would instantiate. It is clear that top(box) is an intended ground constant. There are two general interpretations that seem possible. (1) The sorts within parameterized constants are substituted by only the declared constants of those sorts within the theory. (2) The sorts within the parameterized constants are substituted by any instance of the sort declared within the structure.

The decision between (1) and (2) has an impact on what constants are created and how axioms are translated. Since top(elevations) is a constant, does every elevation have a top or only the declared constants of the sort elevations? At the top of page 33 there is a state constraint "false if loc_in(E) = top(E)".

If (2) holds, then it would seem that there would not need to be any change to the way the axiom would be translated. The constraint would apply to every elevation E and every elevation has a top(E).

If (1) holds, then it would seem that in the translation, any use of parameterized constants would need to be ground. The term "top(E)" would need to be replaced by "top(x) where x is a constant declared for the sort of element E". In this case top(E) would be replaced by top(box). This grounding would duplicate the rules across all possible groundings of the constant.

My intuition is that (1) is the correct understanding despite its added complexity in translation. It seems odd to have an unknown number of constants until after the structure has been provided. If the intent was (2), I wonder if it would be better modeled as an attribute function than a constant declaration.

Thank you for your time in considering my questions. This is one of the few remaining open issues with the compiler I've written.

Edward Wertz (806) 786-1782 edward.o.wertz@gmail.com

I agree that there is some need for the ability to instantiate related instances of things. Every person has left hand, right hand, left foot, right foot, head, etc. (unless they don't). It would be far simpler for the manual programmer to populate records based on the instance definition of a person than to define it all as values of attribute functions.

System Description 1

Theory

leftHands :: universe rightHands :: universe leftFoots :: universe rightFoots :: universe heads :: universe persons :: universe

Structure

lefthand(joe) in leftHands righthand(joe) in rightHands leftfoot(joe) in leftFoots rightfoot(joe) in rightFoots head(joe) in heads joe in Person leftHand = lefthand(joe) rightHand = righthand(joe) leftFoot = leftfoot(joe) rightFoot = rightfoot(joe) head = head(joe)

VS

System Description 2

Theory

leftHands :: universe rightHands :: universe leftFoots :: universe rightFoots :: universe heads :: universe persons :: universe

Records/Functors? leftHand(person) :: leftHands rightHand(person) :: rightHands leftFoot(person) :: leftFoots rightFoot(person) :: rightFoots heads(person) :: heads

Structure

joe, jane, henry, sue in person

Would it be fair to say that Functors/Records are equivalent to attribute functions whose values are pre-determined? (System Description 2 is short-hand for System Description 1)?

I agree, these do not feel like constants.

For system description 1, a. since lefthand/1 is in structure we are not able to use it in theory, which is a big restriction. b. as a result of a), we are not able to connect parts to "person".

System description 2 could be further simplified by not introducing sorts leftHands etc. it is more than a shorthand of description 1. In the theory part we can refer to functor leftHand and use it to connect to person. e.g., use(rightHand(X)) if hurt(leftHand(X)), hasNoAssistant(X).

As for idea using attribute functions, let us make it more specific. One way is person :: universe attributes leftHand: XXX rightHand: YYY we can write the axiom above use(rightHand(X)) if hurt(leftHand(X)), hasNoAssistant(X). Then we define instances of person joe, jane in person leftHand(X) = leftHand(X) % leftHand(X) is a term which is allowed in instance. % in fact we can use any name such as lf(X) that we would like % to occur in our final answer (e.g., for planning problem) rightHand(Y) = rightHand(Y) % We still need to define sorts XXX and YYY in structure. leftHand(X) in leftHand where instance(X, person) ... It seems that we don't need anything new. Maybe attribute function is a workaround. (However, it is a bit awkward/unecessary to introduce sorts XXX and YYY and define them in structure. On the other hand, attribute itself seems to fit well. A compromise maybe to introduce a keyword Herbrand. When declare leftHand(X): Herbrand, we know lefthand(X) is mapped to iteself (as a term). More thoughts are needed).

I'll check if the attribute function is a workaround of top(Elevation) in current CALM.

Test result: syntax seems to be ok. But there maybe a CALM bug

ErrorID: CND002
Message: Object Constant parameter [elevations at (166:16)] is not a source sort in the 
hierarchy since it has sub-sort [[NO TEXT] at (0,0)]

The program is basicmotion_yn.tp as follows


%ErrorID: TYP003 (this complaint is gone)
%Message: Sort mismatch in expression [box at (204:20)].  Sort [carriables] was expected but a term of sort [[elevations]] occurred.
system description monkeyBanana
    theory basic_motion
        module moving
        sort declarations
            points, things :: universe
            agents :: things
            move :: actions
                attributes
                    actor : agents
                    origin : points
                    dest : points
        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
                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.
            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 carrying_things depends on moving
        sort declarations
            carriables :: things
            % carry <actor, origin, dest, carried_obj>
            %   actor carries carried_obj from origin to dest.
            carry :: move
                attributes
                    carried_object : carriables
            % grasp <grasper, grasped_thing> - rasper grasps grasped_thing
            grasp :: actions
                attributes
                    grasper : agents
                    grasped_thing : things
            % release <releaser, released_thing> -
            %   releaser releases released_thing
            release :: actions
                attributes
                    releaser : agents
                    released_thing : things
        function declarations
            fluents
                basic
                    % holding(A, T) - agent A holds thing T.
                    total holding : agents * things -> booleans
                defined
                    % is_held(T) - thign T is held (by some agent)
                    is_held : things -> booleans
                    % can_reach(A, T) - agent A can reach thing T
                    can_reach : agents * things -> booleans
        axioms
            dynamic causal laws
                % grasp causes its grasper to hold its grasped_thing
                occurs(A) causes holding(X,Y) if
                    instance(A,grasp), grasper(A) = X, grasped_thing(A) = Y.
                % release causes its releaser not to hold its grasped_thing.
                occurs(A) causes -holding(X,Y) if
                    instance(A,release), releaser(A) = X, released_thing(A) = Y.
            state constraints
                % If A holds T, then they have the same location.
                loc_in(T) = P if holding(A,T), loc_in(A) = P.
                loc_in(A) = P if holding(A,T), loc_in(T) = P.
                -holding(X,Y2) if holding(X,Y1), Y1 != Y2.

                % NEW on default values of carry:
                %   its origin is where the agent is
                % general question - principles of where to
                % "set" values of attributes structure or state constraits?
                origin(C) = P if
                    instance(C, carry),
                    loc_in(actor(C)) = P.

            function definitions
                is_held(X) if holding(T,X).
                % Agent M can reach O if they are in the same location
                can_reach(M,O) if loc_in(M) = loc_in(O).
            executability conditions
                % grasp is not possible if its grasper already holds its grasped
                impossible occurs(A) if instance(A,grasp), grasper(A) = X, grasped_thing(A) = Y, holding(X,Y).
                % grasp is not possible if its grasper cannot reach its grasped
                impossible occurs(A) if
                    instance(A,grasp), grasper(A) = X,
                    grasped_thing(A) = Y, -can_reach(X,Y).
                % release is not possible if its releaser does not hold its grasped
                impossible occurs(A) if
                    instance(A,release), releaser(A) = X,
                    released_thing(A) = Y, -holding(X,Y).
                % move is not possible if its actor is held.
                impossible occurs(X) if
                    instance(X,move), actor(X) = A, is_held(A).
                % carry is not possible if its actor does not hold its carried
                impossible occurs(X) if
                    instance(X,carry), actor(X) = A,
                    carried_object(X) = C, -holding(A,C).

    module climbing depends on moving
        sort declarations
            elevations :: things
              attributes
                top: points
            % climb <actor, origin, destination, elevation>
            %    -- actor climbs the elevation (to its top)
            %       (from its origin)
            climb :: move
                attributes
                    elevation : elevations
        % constant declarations
            % top(elevations) : points
        axioms
            state constraints
                % ?? how do we know elevation below is an attribute function??
                % top(E) is the destination of climbing an elevation E
            dest(A) = C if elevation(A) = E, C = top(E).
                % Any thing T cannot locate on top of T
                false if loc_in(T) = top(T).
            executability conditions
                % climb is not possible if its elevation is not in the same
                % location of its actor. 
                impossible occurs(X) if
                    instance(X,climb), actor(X) = A,
                    elevation(X) = O, loc_in(O) != loc_in(A).

    module main depends on carrying_things, climbing
        sort declarations
            floor_points, ceiling_points, movable_points :: points
        constant declarations
            monkey : agents
            box :  elevations
            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
                        % The location of the box is connected to the top of the box
                        connected(top(box),P) if
                            loc_in(box) = P, 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
                % NEW climb a box is not possible if it is held by some agent
                    impossible occurs(X) if
                      instance(X,climb),
                      elevation(X) = box,
                      is_held(box).

    structure monkey_and_banana
    instances
        under_banana, initial_monkey, initial_box in floor_points
        initial_banana in ceiling_points
        top(X) in movable_points where instance(X, elevations)

        carry(box, P) in carry where instance(P, floor_points)
            actor = monkey
            carried_object = box
            dest = P
        grasp(C) in grasp where instance(C, carriables)
            grasper = monkey
            grasped_thing = C
        release(C) in release where instance(C, carriables)
            releaser = monkey
            released_thing = C

        climb(box) in climb
            actor = monkey
            elevation = box 
            %NEW destination of climb is top of the box
            %dest(monkey) = 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(grasp(box), 1).
    happened(carry(box, under_banana), 2).
    happened(release(box), 3).
    happened(climb(box), 4).
    happened(grasp(banana), 5).

Proposal: Modify Grammar of Sort Declarations

A Sort Declaration has both Attributes and "Functors"?

The difference being that an attribute has to be defined in the structure and it must select one of the elements of the range sort of the functions.

A a functor creates its own sort and specifies an instance in the sort based on instances of the original sort.

Example: ` person :: universe Attributes nameOf : names Functors (parts?) lefthand : hands righthand : hands

creates functions

lefthand: person -> hands righthand: person -> hands

creates function definitions lefthand(X) = Y :- instance(Y, hands), Y = lefthand(X).

Sparc Translation:

lefthand(X, Y) :- instance(Y, hands), Y = lefthand(X). `

This has significant syntactic ambiguity between the instance and the function denoting the instance. The functor function should be prefixed with the sort the way attributes would be prefixed.

person_lefthand(X,Y) :- instance(Y, hands), Y = lefthand(X).

If we proceed down this avenue of thought, it opens up a related topic: Parameterized Sorts.

Instead of a general "Hands" sort, we really want a narrower sub-sort that contains the hands of that person.

Sort Declaration

hands :: universe person :: universe Functor lefthand : hands righthand : hands

Structure

john, sue in person

Automatic Sort Declaration

hands(person) :: hands

Automatic Function Declarations:

lefthand: person(X) -> hands(X) % where X is an instance of a person. righthand: person(X) -> hands(X)

Automatic Instance/Constant Definitions

lefthand(X) in hands(X) where instance(X, person). righthand(X) in hands(X) where instance(X, person).

Automatic Function Definitions

lefthand(X) = Y if instance(X, person), instance(Y, hands(X)), Y=lefthand(X). righthand(X) = Y if instance(X, person), instance(Y, hands(X)), Y=righthand(X).

Translated Sort hierarchy

person = {john, sue}

hands_john = {lefthand(john), righthand(john)}

hands_sue = {lefthand(sue), righthand(sue)}

hands = #hands_john + #hands_sue

perhaps we can introduce a "dot" notation for functors.

person.lefthand(X)

person(X).lefthand

translated to

person_lefthand(X, Y)

I take attribute as a workaround, i.e., if it works, nothing is needed to be done with CALM. I will continue to test this workaround.

Just check if you note my proposal above. I copied it here:


Here is an outline:
--- type checking ---
when come across f(...), have two cases:
f: is a function name: do type checking on the parameters of f. the range of f is the type of f(...)
f: is a record name: do type checking on parameters of f, the most immediately parent sort is the type of f(...). One issue: should we introduce an anonymous record sort, e.g., declare f: top(elevations) -> integer.

--- translation ---

Sort def. we seems to need an anonymous sort. in alm one can declare g: top(elevations) -> integer. or top(elevations) :: points in sparc we might need

a_top = top(elevations);

then we have g(#a_top, integer) for subsort "top(elevations) :: points" we only need to make sure the elements in top(elevations) are includes in the parent sorts.

statements e.g., dest(A) = top(E) when top is a record name, we don't introduce a new relation. assume dest(A) represented in SPARC by dest(A, Location, Time) then the above can be translated as dest(A, Location, Time), Location = top(E).

I was testing if we can use herbrand term in constant declaration.

        constant declarations
            p(1,9) : points
              x = 1
              y = 9

I got an error message

ErrorID: CND004
Message: Object Constant parameter [1 at (/Users/yuazhang/Desktop/CALM/examples/attribute-constantWithParameter.txt:17:14)] has not been declared as a source sort in the sort hierarchy.
Explanation: Only names of source sorts in the sort hierarchy can be parameters of object constants.
Recommendation: Either change the name of the parameter to an existing source sort or create the declaration for the sort in the sort hierarchy.

ErrorID: CND004
Message: Object Constant parameter [9 at (/Users/yuazhang/Desktop/CALM/examples/attribute-constantWithParameter.txt:17:16)] has not been declared as a source sort in the sort hierarchy.
Explanation: Only names of source sorts in the sort hierarchy can be parameters of object constants.
Recommendation: Either change the name of the parameter to an existing source sort or create the declaration for the sort in the sort hierarchy.

ErrorID: CND008
Message: Term  [1 at (/Users/yuazhang/Desktop/CALM/examples/attribute-constantWithParameter.txt:35:53)] has not been declared as a function term or a constant for any sort.
Explanation: Non pre-defined and non-variable terms must be declared before they are used.
Recommendation: Either add a function definition or a constant definition for the term, or replace it with a declared term.

ErrorID: CND008
Message: Term  [9 at (/Users/yuazhang/Desktop/CALM/examples/attribute-constantWithParameter.txt:35:55)] has not been declared as a function term or a constant for any sort.
Explanation: Non pre-defined and non-variable terms must be declared before they are used.
Recommendation: Either add a function definition or a constant definition for the term, or replace it with a declared term.

I think the intended constant "p(1, 9)" is not allowed by CALM and ALM paper (where we can apply herbrand function to a sort. My intuition is that we should be able to user a herbrand term as a constant.

Here is the full program


system description test
    theory test
      module test
        sort declarations
            coordinates :: universe
            points :: universe
               attributes
                  x : 1..10
                  y : 1..10

            locations :: universe
            elevations :: universe
               attributes
                  top: locations

        constant declarations
            p(1,9) : points
              x = 1
              y = 9

            topSth : locations

            box: elevations
              top = topSth % we allow term here

        function declarations
            statics
             basic
                number : 0..10
              defined
                intersect: booleans

        axioms
            function definitions
            intersect if instance(X, 0..30), X = x(p(1,9)).

  structure attribute_test
    instances
        b1, b2, b3 in locations

        p(X, Y) in points
            x = X
            y = Y

        e(X) in elevations
           top = X

Right now the calm compiler only supports sort names as arguments to constants because if we allow full Herbrand terms as arguments then we have to deal with all the nested structure and partial grounding.

foo(bar(sort1, baz), sort2) : sort 3

for a constant declaration like that, the following items have to be done:

verify that bar is a previously declared constant that takes two arguments
verify that the first argument of bar is of sort sort1
get the expected sort of the second argument of bar
verify that baz is a previously declared constant that is a subsort of the expected sort.
verify all sorts uses are previously declared.

And this nesting can go arbitrarily deep.

I don't want keep making incremental changes to the treatment of constants until we have a unified theory and treatment of Herbrand terms throughout alm programs.

These are the requirements that I am feeling are appropriate.

Constants are single name Herbrand terms, no sub-structure, and can be substituted for in the structure with a constant definition.
Herbrand terms can appear in both the theory and structure by replacing the concept of "sort instances" in the structure and "parameterized constants" in the theory.
Herbrand terms can have arguments from {Herbrand Term, Variable, Sort Name} where Variables are given a sort through use of instance().
Herbrand terms created in the theory can be used in axioms.
Herbrand terms are allowed to have arbitrary finite nesting and we will implement a robust term walking capability for proper semantic error and type checking detection.

Thoughts?

I feel like the formal modeling constraints in the ALM paper are barriers that the lay-modelers will not want to wrestle with. When we sit down to write a program, we don't think about the distinction between structure and theory and performing formal interpretations of the symbols.

As a problem solver, if I wrote a large planning program, I would want to dynamically add state constraints and executability conditions after specifying the planning problem.

By expanding the expressive capability of constants, allowing sub-structure and specification of attributes, we've effectively allowed full "sort -instances" in the theory.

We've already eliminated the concept of a source sort as a leaf sort.

There seems to be significant utility to blurring the distinction between structure and module. Why not allow modules to specify values of statics? Why not allow modules to define constants of prior modules?

ALM 2.0

There are only modules.
Modules can optionally do everything a structure does.
Module dependency defines a tree structure.
The final SPARC program is rendered from the "root" module of the dependency tree. (The structure is effectively this root level module.)

For constant with parameters, agree to make minimal "patching." We can keep its current status of CALM (on constants) .

As for theory/structure, under the future introduction of a more precise/careful treatment of constants, it is worth of more thinking.

Topology / ALM-Compiler

Constant with parameters in ALM #3

a_top = top(elevations);

VS

person = {john, sue}

hands_john = {lefthand(john), righthand(john)}

hands_sue = {lefthand(sue), righthand(sue)}

hands = #hands_john + #hands_sue

a_top = top(elevations);