P RO_{bj}LOG aka Prolog+Objects:

a well-founded proposal

Michele Bugliesi, Giorgio Delzanno, Luigi Liquori

Abstract. We present a linear logic programming language, called P RO_{bj}LOG , that gives a complete account of an object-based calculus with inheritance and override. The logical foundations of P RO_{bj}LOG lie in a fragment of intuitionistic higher-order Linear Logic. The higher-order nature of the syntax allows a direct encoding of objects as first-class values with attribute and method fields: the linear connectives, on the other hand, allow methods to be selected and applied according to the self-application semantics of method invocation.

1 Introduction

Object-oriented languages can be classified as either class-based or object-based according to the underlying object-oriented model. In class-based languages objects are created by instantiating their class. In object-based languages, instead, objects are derived dynamically by modifying or extending existing objects, used as prototypes. A derived object may then respond to messages directly, if it contains corresponding methods, or “pass them back”, i.e. delegate them, to the prototype.

Originated with the seminal work on Self [11], the object-based model has subsequently been studied in several papers, among which the record calculus of [3], and then in recent papers on functional object-oriented languages [1, 5]. These latter proposals are centered around two main design choices: (i) objects are first-class values consisting of the set of their methods (attributes are viewed as constant methods), and (ii) methods are functions with a distinguished parameter denoting the host object. The resulting languages are rather effective in that they encompass a very simple and elegant modeling of the object-oriented notion of self directly by lambda abstraction, and they provide a well-suited basis for studying a typed foundation for object-oriented languages and systems.

Drawing on these proposals, in this paper we present a linear logic programming language, called P RO_{bj}LOG , that gives a complete account of an object-based calculus with inheritance and override.

The logical foundations of P RO_{bj}LOG lie in a fragment of intuitionistic higher-order Linear Logic consisting of the connectives −∘, ⇒, & , and ∀. The higher-order nature of the syntax allows a direct encoding of objects as first-class values with attribute and method fields: the linear connectives, on the other hand, allow methods to be selected and applied according to the self-application semantics of method invocation. P RO_{bj}LOG also provides primitives for method addition and redefinition, peculiar to the companion functional calculi, and it encompasses the same mechanism of method and attribute inheritance by delegation. Method redefinition relies on a functional form of update whereby overriding a method (or attribute) is realized by computing a modified copy of the object containing that method.

The design of P RO_{bj}LOG shares ideas with previous proposals of linear object-oriented languages [2, 4, 9], but the resulting language exhibits several novel features. As in in these languages, computation in P RO_{bj}LOG is a process of logical deduction in which, however, objects are computed values rather than consumable resources. Accordingly, the result of a program is a set of answer substitutions as it is customary in logic programming. In fact, P RO_{bj}LOG can readily be extended to allow writing program clauses (actually metaprograms with respect to objects) in the usual logic programming style, using predicates which have objects as data.

A further important difference with respect to previous work, is in the choice of the underlying object-oriented model: to our knowledge, this is the first attempt to give a direct logical semantics to the object and record calculi that subscribe to the object-based view of object-orientation.

The rest of the paper is organized as follows. In Section 2 we introduce a front-end of the language by using a high-level syntax. In this section we consider only an object-based language in conformity with the above mentioned object-calculi. In Section 3 we describe the logic underlying the language definition. We will dwell here with the technical details encountered while dealing with a higher-order syntax. In Section 5 we describe how P RO_{bj}LOG can be expressed in this logic, and we exemplify it on a few programming examples. In Section 6 we describe an implementation given in Lolli [8] of P RO_{bj}LOG , adding facilities which make the language easier. Some programming examples are shown taken from interesting problems concering computational geometry. Further code is listed in A. We conclude in Section 7 discussing related research, and addressing issues relative to the design of a type system for our language.

2 P RO_{bj}LOG : An Introduction

P RO_{bj}LOG is an object-oriented logic language based on Linear Logic and objects. The goal of P RO_{bj}LOG is to show that equally elegant accounts of object-oriented concepts like self, inheritance, override and subsumption, can be given in logic.

Following the Smalltalk-80 [6] experience, P RO_{bj}LOG can easily codify classes, metaclasses via suitable objects. In contrast with Smalltalk-80, P RO_{bj}LOG can also build objects using other objects as “prototypes”. This approach is much more expressive, since it shares both the class- and the delegation-based object-oriented styles of programming, by allowing to build classes and instances and extending or overriding dynamically some object methods. The encoding of classes, metaclasses, and instances in P RO_{bj}LOG is given in Section 2.3.

P RO_{bj}LOG is an “untyped” language: this means that the programmer, during the development process of an application, does not need to declare the types of the (logical) variables: this is equivalent to say that the language have a single universal type that contains all values. Howewer, the design of P RO_{bj}LOG is motivated by a strict simililarity with some object-based functional formalism like [5, 1], where a static type system (i.e. a “compiletime” type-checker) can be defined and the soundness of that type system will enforce the good behaviour of programs. The design of O.O. type systems has been the subject of intensively study by many researchers in the past decade. The main further development of P RO_{bj}LOG is the design of a static and sound type system which prevents the occurrences of run-time errors such as message-not-found. This issue will be the subject of our next work (see Section 7).

2.1 Syntax of P RO_{bj}LOG

Anonymous Object Instances In P RO_{bj}LOG , objects are represented as particular terms: syntactically, an (anonymous) object instance agrees with the following syntax:

                   O ::= obj[ ] | obj[m_{1} = body_{1}, . . . , m_{k} = body_{k}],

where obj[] is the empty object and, for every i = 1, …, k, m_{i} is a method name acting as the label of the method definition body_{i}.

More precisely, objects can be results of message sending which can be assigned to (unbound) logical variables: as such, a complete definition of objects can be as follows:

                            object ::= X | O | self,

where X belongs to a set of denumerable set of variables Var, and self is a metavariable, (i.e. a logical constant) denoting the object itself.

Message Sending In any object-oriented language the computation is performed by a sequence of message send. Message send in P RO_{bj}LOG are atomic formulas of the following shape:

                       send ::= object_{1}.margs ↦ object_{2},

where

– object_{1} is the receiver of the message;

– args are the (possible empty) list of arguments that agrees with the following syntax:

                         args ::= ∅ | (object_{1}, . . . , object_{k});

– object_{2} is the result of send the message m to object_{1} with arguments args;

Sending a message to an object consists of two separate steps, namely (i) select the definition of the corresponding method on the receiver of the message, and (ii) apply the definition to the receiver itself and the input arguments specified in the message.

As example, a bidimensional diagonal point object instance with two “fields”, x, and y, can be expressed as follows:

                          obj[x = 1, y = self.x ↦ Y],

where 1 (shorthand for ↦ 1) is the constant object denoting the integer one; the result of send message y to the point instance will be unified with the unbound variable Y, which can be further used during the computation.

Operation on Objects The operations that modify objects in P RO_{bj}LOG are atomic formulas of the following shape:

                  modify ::= object_{1}.ext.m = body ↦ object_{2} |
                            object_{1}.over.m = body ↦ object_{2}.

Those forms requires some explication: the former extends object_{1} with a new method m, producing a new object object_{2}, while the latter rewrite the existing method m with a new body, producing object_{2}.

Method Definition So far, we have seen only trivial method bodies definition, such as the one for the y field. In order to write non trivial method bodies, we need to introduce, some constructs dealing with object extension and object override. Let the following compound object formulas be defined as follows:

                     comp ::= ∅ | send | modify | comp, comp,

where the “comma” means the logical conjunction connective. The complete definition of method bodies agree with the following syntax:

                         body ::= argscomp ↦ object_{2}.

Examples In this section, we put forward some examples that will give an intuition of the power of P RO_{bj}LOG .

Example 2.1 One-dimensional point with a move method. This object can be represented as follows:

          pt =^{def} obj[x = 3, mv = (Y)(self.x ↦ X, self.over.x = X+Y ↦ Z) ↦ Z].

Now, consider then the atomic formula:

                                pt.mv(2) ↦ P,

where P is is a free (i.e., existentially quantified) variable: evaluating this formula, leads to first bind Y with 2, Z with P (this is a “flound” binding), and then evaluating the conjoined formula:

                         pt.x ↦ X, pt.over.x = X+2 ↦ P,

which, in turn, binds X to the value 3 and then P to the new object:

         pt′ =^{def} obj[x = 5, mv = (Y)(self.x ↦ X, self.over.x = X+Y ↦ Z) ↦ Z].

Example 2.2 Inherit move from points to colored points. The next example illustrates how methods are inherited from prototypes to derived objects. Consider again the pt object of the previous example, and consider the following conjoined formula:

                   pt.ext.col = red ↦ P, P.mv(2) ↦ Q, Q.col ↦ C,

(where red is shorthand for ↦ red). In the left-most formula, pt is used as a “prototypical” point from which we derive a colored-point with a new constant method col. The query illustrates how the new object inherits the mv method (indeed, also the x method) from its prototype. In fact, evaluating the method extension on pt yields the following binding:

                    P with obj[x = 3, mv = body_{mv}, col = red].

Then, proceeding from left to right, p.mv(2) ↦ Q, yields the binding:

                    Q with obj[x = 3, mv = body_{mv}, col = red],

and, finally, the last message binds C with red, as expected.

Example 2.3 Object numerals. We show how natural numbers can be represented in P RO_{bj}LOG . Following [1], we define object-numerals as objects that respond to the methods zero? (test for zero), pred (predecessor) and succ (successor) and behave like natural numbers. In fact, we need only to define the numeral zero as the “prototypical” number, and let all other numerals be generated by repeated applications of the succ method. As such, let the zero numeral be defined as follows:

obj[zero? = true, (shorthand for ↦ true)
pred = self, (shorthand for ↦ self)

             succ = (self.over.zero? = false ↦ P, P.over.pred = self) ↦ Q].

One easily verifies, with a few tests, that the operational semantics of natural numbers is well represented. In particular, note that the body of succ consists of two cascaded updates for self: when invoked on any object-numeral, succ updates the zero? method to answer false, and updates the pred method to return the current value of self when succ is invoked. As example, other numerals be defined by the following composite queries:

               one =^{def} zero.succ ↦ M_{1}
               two =^{def} zero.succ ↦ M_{1}, M_{1}.succ ↦ M_{2}
             three =^{def} zero.succ ↦ M_{1}, M_{1}.succ ↦ M_{2}, M_{2}.succ ↦ M_{3}

. . . . . .

             n−th =^{def} zero.succ ↦ M_{1}, M_{1}.succ ↦ M_{2}, . . . , M_{i−1}.succ ↦ M_{i}.

2.2 Mixing O.O and L.P. in P RO_{bj}LOG

So far we have only presented the object-oriented features of P RO_{bj}LOG . However, it is also possible to write logic programs in P RO_{bj}LOG that use objects as data structures. We only need to be more liberal in the syntax, and allow atomic formulas to also have the conventional predicative structure p(a_{1}, …, a_{n}).

To exemplify, consider again the pt point-object of Example 2.1: we can now use the following simple program to create colored-points:

                     make cpt(P, C, CP) :− P.ext.col = C ↦ CP.

Similarly, the following clause creates bidimensional points from points:

           make 2dpt(P, Y, BP) :− P.ext.y = Y ↦ Q, Q.over.mv = body_{mv} ↦ BP,

where body_{mv} is:

           body_{mv} =^{def} (VW)(self.x ↦ X, self.y ↦ Y,

                       self.over.x = X+W ↦ H, H.over.y = Y+K ↦ K) ↦ K.

Now consider the following program to move a point in two-dimensions:

                      move pt(P, NP, X, Y) :− P.mv(XY) ↦ NP.

Then, it is possible to formulate queries as the following:

           make 2dpt(pt, 3, BP), make cpt(BP, blue, CP), move pt(CP, NP, 4, 5) ,

where, if pt is the one-dimensional point at position 3 on the line, the result is to bind NP to a two-dimensional colored point at position (7, 8) on the plane. It is worth noting that the move pt clause works well even if the CP logical variable unifies with a point without a color field: in other words, the clause is polymorphic in the input (i.e. the logical variable P). The capability to use a program that can receive as input both a longer or a shorter object is usually called subsumption, and (when a type system exists) is strictly related with a subtyping relation over object-types.

2.3 The SmallTalk-80 Hiearchy in P RO_{bj}LOG

In this section, we show how P RO_{bj}LOG can easily codify classes as objects; This encoding shares both the class- and the delegation-based object-oriented styles of programming, because it allows to build classes and instances and to extend and override dynamically some object methods. In the object-oriented jargon, creating an instance of a given class can be viewed as an activity that must be delegated to some object. Then the following question arises: which object should have the responsibility for this activity? One solution places a layer of management between the user, who desires the creation of a new object, and the code that performs the allocation of the memory. It follows that, for each class, say A, to be defined, we have a corresponding proper object, that has the responsibility of creating instances of A. We call that object (the metaclass) A Class; it must have all the information about the size of the class it represents, the methods to which instances of this class will respond and a method New, that performs the creation of the class A. As such, the class A is an instance of the (meta)class A Class. The class A, in turn contains a method, called new, that performs the creation of instances of the class A. Figure 1 depicts the class and subclass hierarchy.

In the next subsections, we present the encoding of the metaclasses, classes and instances of Figure 1. In particular, we present the encoding of the classes and metaclasses of points and colored points. It is worth noting that the only objects that need to be built are the objects representing metaclasses and the top level object Object: objects representing classes and instances are generated via message sending and successive reductions. To ease the presentation, we omit the symbol obj for anomymous object instances.

[figure: superclass; object; New; C Class; B Class; superclass; object; New; A Class; superclass; object; New; superclass; object; New; Object Class; instance relation; subclass relation; c; b; a; new; new; new; C; B; A; Object; new; New; Obj]

Fig. 1. The Class-Subclass Hierarchy

Metaclasses The metaclasses Obj Cl, P Cl, and CP Cl, together with the top level object of the hierarchy Object, are encoded as follows:

Object =^{def} [New = ↦ [ ]]

Obj Cl =^{def} [New = ↦ [new = (self.obj ↦ P) ↦ P],

super = ↦ Object,
obj = (self.super ↦ P, P.New ↦ Q) ↦ Q

]

P Cl =^{def} [New = ↦ [new = (self.obj ↦ P) ↦ P],

super = ↦ Obj Cl,
obj = (self.super ↦ P, P.obj ↦ Q, Q.ext.x = 1 ↦ R) ↦ R

]

CP Cl =^{def} [New = ↦ [new = (self.obj ↦ P) ↦ P],

super = ↦ P Cl,
obj = (self.super ↦ P, P.obj ↦ Q, Q.ext.col = red ↦ R) ↦ R

].

The meaning of the methods of the above metaclasses is as follows. When the method New is invoked on the metaclasses^{1} (i.e P Cl and CP Cl), it produces as result another object, which is the class representing all the objects instances (e.g. points and colored points, respectively). The super method contains a pointer of the direct super(meta)class of the class to be defined. Finally, the method obj contains a copy of the object instance of the class; that object will be cloned when an instance of the class is created (by sending the message new to the class).

Classes The classes Object, Point, and C Point, are encoded in P RO_{bj}LOG as follows

Object =^{def} [new = ↦ [ ]]
Point =^{def} [new = ↦ [x = 1]]

                     C Point =^{def} [new = ↦ [x = 1, col = red]],

and it holds that the queries

                               Obj Cl.New ↦ P

binds P with Object, and that

                                P Cl.New ↦ Q

binds Q with Point, and finally that

                                CP Cl.New ↦ R

binds Q with C Point.

Instances When the method new is invoked on the classes Point and C Point, it produces as results points and colored points objects instances, respectively, and it holds that the queries

                               Object.new ↦ P

binds P with [ ], and that

                                Point.new ↦ Q

binds Q with [x = 1], and finally that

                               C Point.new ↦ R

binds R with [x = 1, col = red].

3 Logical Foundations

We start with a presentation of a fragment of Intuitionistic Linear Logic that will serve as the logical language underlying the definition of P RO_{bj}LOG .

1 The New method should be “fired” automatically and only once on all defined metaclasses.

3.1 A Fragment of Higher-Order Intuitionistic Linear Logic

The language is defined over a denumerable set of variables V and a signature Σ partitioned into a set of typed nonlogical constants, and a set of typed logical constants, or connectives with the latter comprising the connectives &, ⇒, −∘, and the infinite list of quantifiers ∀_{τ} for every type τ (⇒ denotes intuitionistic implication, defined as A ⇒ B ≡ (!A) −∘ B).

Types, ranged over by τ, are defined by the following productions: τ ::= o | b | τ → τ with o denoting the type of formulas, b any primitive type and τ → τ function types. We assume that there are denumerably many variable and constants of each type, and that types for the logical constants are assigned as follows: &, −∘ and ⇒ have type o → o → o, whereas ∀_{τ} has type τ → o → o for every type τ.

Terms and Formulas We introduce higher-order features in the syntax of the language by (i) allowing atomic formulas to contain formulas as subterms, and (ii) allowing quantification over variables of the distinguished type o of formulas. The syntax of terms and formulas is given in terms of two mutually recursive definitions, introduced next.

Definition 3.1 D-Terms. The set of D-terms is the smallest set of λterms in normal form 2 built from a given signature with free variables, closed under the following formation rules:

1. every nonlogical constant h ∈ Σ is a D-term; every variable is a D-term;

2. if t:τ is a D-term and x is a variable, then λx.t is a D-term.

3. if h:τ_{1} → ⋯ → τ_{n} → τ is a constant from Σ, t_{1}:τ_{1}, …, t_{n}:τ_{n} are D-terms, then

(h t_{1} … t_{n}) is a D-term iff either one of the following two conditions hold: · h is a logical connective and (h t_{1} … t_{n}) is a D-formula (see the definition below); · h is a nonlogical constant and for every t_{i} such that τ_{i} = o, it is the case that t_{i} is a D-formula.

Let A be a meta-syntactic variable ranging over atomic formulas; the sets of D- and Gformulas are the collections of formulas generated by the nonterminals D and G according to the following productions:

\begin{aligned}D & ::= & A | G ⇒ A | D & D | ∀_{τ} v.D \\ G & ::= & A | D^{v} −∘ A | G & G | ∀_{τ} v.G. \\ D^{v} & ::= & D | v | D^{v} & D^{v} \end{aligned}

Intuitively, formulas generated by the non-terminal symbol D denote program formulas, whereas formulas generated by the non-terminal G denote goal formulas. Note that Dformulas are D-terms, whereas G-formulas are not. Existential quantification for goal formulas is omitted as it can be defined in terms of universal quantification within program formulas and replaced by the use of “logical” variables within top-level goal formulas.

A proof system for the language we just defined is shown in Figure 1. The intended interpretation of the sequent Γ; Δ →_{Σ} C is as follows: Γ and Δ (the unbounded and bounded

2 I.e., in α-β-η-normal form.

Γ; A →_{Σ} A (identity)  {Γ, B; Δ, B →_{Σ} C \atop Γ, B; Δ →_{Σ} C} (absorb)

{Γ; Δ, B_{i} →_{Σ} G \atop Γ; Δ, B_{1} & B_{2} →_{Σ} C} ( &_{l}) Γ; Δ →_{Σ} C_{1} Γ; Δ →_{Σ} C_{2} Γ; Δ →_{Σ} C_{1} & C_{2} ( &_{r})

{Γ; Δ, B [t/x] →_{Σ} C \atop Γ; Δ, ∀_{τ} x.B →_{Σ} C} (∀_{l})  {Γ ; Δ ⟶_{Σ′} C [c/x] \atop Γ ; Δ →_{Σ} ∀_{τ} x.C} (∀_{r})

Γ; ∅ →_{Σ} B Γ; Δ, C →_{Σ} D Γ; Δ, B ⇒ C →_{Σ} D (⇒_{l})  {Γ ; Δ, B →_{Σ} C \atop Γ ; Δ →_{Σ} B −∘ C} (−∘_{r})

Provisos. (∀_{l}): t : τ is a closed D-term of type τ. (∀_{r}): Σ′ = c:τ, Σ, with c fresh.

Figure 1. The proof system L.

contexts) are, respectively, a set and a multi-set of closed formulas, and C is closed formula all defined over the signature Σ. When the formulas in Γ and Δ are D-formulas, and C is a G-formula, we say that Γ; Δ →_{Σ} C is a (D, G)-sequent. The proof rules of system L are standard; given the proviso for the rule (∀_{l}), it is possible to prove that the language of (D, G)-formulas is an abstract programming language, in the sense of [10]. Let ⊢_{L} denote provability in system L.

Theorem 3.2. The language (D, G, ⊢_{L}) is an abstract programming language, i.e. every (D, G)-sequent Γ; Δ →_{Σ} C has an L-proof if and only if it has a uniform L-proof.

Proof. Given the proviso on (∀_{l}), it is easily verified that every sequent arising in L-proofs of a given (D, G)-sequent is itself a (D, G)-sequent. It then remains to show that L is complete with respect to uniform proofs. This follows from the more general result given in [8] for the first-order fragment of Intuitionistic Linear Logic consisting of & , −∘, ⇒, ∀, ⊥, and ⊤. ⊓ ⊔

In the light of the previous result, it is then possible to give the following specialized version of the proof system L. Sequents of the specialized proof system have two forms, namely Γ →_{Σ}^{D} G or Γ →_{Σ} G, where Γ is a set of D-formulas, D is a D-formula, and G is a G-formula. The sequent Γ →_{Σ}^{D} G denotes a standard intutionistic sequent with D as the unique formula in the bounded part of the context. All the formulas occurring in the sequents are assumed to be closed and defined over the signature Σ. The set of rules of the proof system is given below: The set [D] is the minimal set of formulas that satisfies the following conditions:

D ∈ [D];
if D_{1} & D_{2} ∈ [D], then D_{1} ∈ [D] and D_{2} ∈ [D];
if ∀x_{τ} .D ∈ [D], then D[t/x] ∈ [D] for every closed D-term t : τ.

We then have the following easy result

Theorem 3.3. Let Γ be a set of closed D-formulas and let G be a closed goal formula. The sequent Γ →_{Σ} G has an L_{−∘}-proof if and only if Γ ; ∅ →_{Σ} G has an L-proof.

{Γ, D →_{Σ}^{D} A \atop Γ, D →_{Σ} A} (absorb)  {Γ →_{Σ} G \atop Γ →_{Σ}^{D} A} (bc)  Γ →_{Σ}^{A′} A (identity)

{Γ →_{Σ}^{D} A \atop Γ →_{Σ} D −∘ A} (−∘_{r}) {Σ′ : Γ →_{Σ} G [c/x] \atop Γ →_{Σ} ∀_{τ} x.G} (∀_{r}) \begin{matrix}Γ →_{Σ} G_{1} & Γ →_{Σ} G_{2} \\ Γ →_{Σ} G_{1} & G_{2} \end{matrix} (&_{r})

Provisos. In the (bc) rule, A is an atomic formula, and G ⇒ A ∈ [D] in the (identity) rule, A is atomic and A ∈ [A′].

The proof system L_{−∘}.

4 Completeness wrt HO Intuitionistic Linear Logic

The syntax of Higher-Order Intuitionistic Linear Logic (henceforth hoill) consists of types and simply typed λ-terms. The set of types contains a collection of primitive types and is closed under formation of function types. Symply typed λ-terms are built in the usual fashion from typed constants and variables via abstraction and application. The logical constans include all of the linear connectives; a proof system for this logic can be formulated in the sequent calculus, and includes the standard rules for the linear connectives (with single-conclusion sequents) and the standard rules of substitution and λ-conversion for λ-terms.

What we wish to prove is a completeness result for L-provability of (D, G)-sequents with respect to provability in hoill In fact, in the light of Theorem 3.3, we will content ourselves with a proof of the following, less general, result.

Theorem 4.1. Let Γ be a set of closed D-formulas and let G be a closed goal formula. The sequent Γ ; ∅ →_{Σ} G has an L-proof if and only if it has a cut-free proof in hoill.

In first order case, (i.e. if we disallow quantification over variables of type o) and we restrict to first-order terms (as opposed to λ-terms), the theorem follows from the permutability of every right introduction rule with all of the left rules of L. In the higher-order setting, the “if” part of the theorem is still trivial (every L-proof is a proof in hoill). The “only if” part is not, for the substitution terms introduced by ∀_{l} as witnesses could be any λ-terms not necesarily D-terms. In particular, terms substituted for variables of type o could be formulas other than D-formulas and, as a result, it could be the case that the sequents arising in the proof of a (D, G)-sequent are not (D, G)-sequents. What we need to show, then, is that any such term may be systematically “normalized, i.e. replaced a D-term so that the resulting proof is, in fact, an L-proof. In that direction, we first introduce the following terminology and definitions.

Definition 4.2 Simple Sequents and Proofs. We say that a sequent (not necessarily a (D, G)-sequent) Γ; Δ →_{Σ} C is simple if and only if Δ is either empty or a singleton multiset. Then we say that an L-proof Ξ is simple if and only if all of the sequents occurring in Ξ are simple.

Definition 4.3 L-form. A formula F has L-form iff either one of the following conditions hold: (i) F is a closed D-formula; (ii) there exists a formula ∀_{τ} x.H that has L-form, and F is the formula that results from substituting any closed λ-normal term t for every free occurrence x in H; (iii) F is a conjunction of formulas that have L-form.

Definition 4.4 L-cut. Let Γ; ∅ →_{Σ} G be a (D, G)-sequent and let Ξ be a hoill proof of this sequent. We define the L-cut of Ξ, denoted by κ_{L}(Ξ), to be the partial proof-tree that results from dropping all the sequents of Ξ that occur above the lower sequent Γ; Δ →_{Σ} (F_{1} −∘ F_{2}) of an instance of −∘_{r} whenever the formula F_{1} does not have L-form. We then say that κ_{L}(Ξ) is simple if so is every sequent occurring in κ_{L}(Ξ).

Given a hoill proof of Γ; ∅ →_{Σ} G, it is easily seen that the formulas in the antecedents of the sequents in κ_{L}(Ξ) are in L-form; similarly, the formulas in the consequents of the sequents in κ_{L}(Ξ) are either atomic, or have one of & , −∘ of ∀_{τ} as their top-level logical connective.

The notion of L-form can be defined constructively in the following manner. Let then A_{L} denote any atomic formula and B denote arbitrary formulas. The set of formulas that have L-form is the set of closed formulas generated by the nonterminal D_{L} defined below:

\begin{aligned}D_{L} & ::= & A_{L} | G_{L} ⇒ A_{L} | D_{L} & D_{L} | ∀_{τ} v.D_{L} \\ G_{L} & ::= & A_{L} | B −∘ A_{L} | D_{v} −∘ A_{L} | G_{L} & G_{L} | ∀_{τ} v.G_{L}. \\ D^{v} & ::= & D_{L} | v | D^{v} & D^{v} \end{aligned}

In the following D_{L,x} will denote the set of formulas in L-form with free variables and we will say that F is in L, x-form if F ∈ D_{L,x}. Furthermore, T_{x} will denote the set of all simply typed λ-terms in λ-normal form

Given these observations, we then have the following result.

Lemma 4.5. Let Γ; ∅ →_{Σ} G be a (D, G)-sequent. If this sequent an hoill proof, then exists an hoill proof Ξ of the sequent in question such that κ_{L}(Ξ) is simple.

Proof. The proof follows from the property of permutability of the right introdution rules of L with the left introduction rules. Intuitively, in this process, every formula introduced in the bounded context of a sequent below an instance of the rule (−∘_{r}) are pushed up above that sequent (i.e., the L-cut moves down in the proof). ⊓ ⊔

It then follows, that the leaves of the L-cut are either initial sequents of the form Γ; A_{L} →_{Σ} A_{L}, or sequents of the form Γ; ∅ →_{Σ} B −∘ A_{L}.

4.1 Towards a Completeness Proof

Assume we are given a (D, G)-sequent Γ; ∅ →_{Σ} G, and a hoill proof Ξ for this sequent. If Ξ is a L-proof, we are done. Otherwise, we isolate, within Ξ, the L-cut κ_{L}(Ξ): Lemma 4.5 above ensures that we may assume that κ_{L}(Ξ) is a simple cut. Then, we give a way for transforming this simple L-cut into an L-proof for the normalization of the original sequent.

The argument for the proof is constructive: we use essentially the same technique as in the completeness proof for the language of Higher-Order Hereditary Harrop formulas (hohh) described in [10]. As we anticipated, the idea is to normalize every “wrong” terms arising in the proof with a corresponding D-term. In that direction, first observe that, since we don’t have λ-terms in our languages, any λ-abstraction arising in a proof is to be considered a “wrong” witness and, as such, should be normalized to a corresponding D-term. The remedy to this is, in fact, almost immediate: given the assumption that every type is inhabitated by denumerably many constans, we may safely replace every a λ-abstraction with a corresponding constant of the same type from the signature. It is then enough to identify a canonical constant at each type and use that constant to normalized every λ-term of the type in question.

As for the type o of formulas, we have are two cases to consider: the first is when the “wrong”witness occurs withing the scope of a nonlogical constant; the second is when a term t : o occurs within goal formulas of the form B −∘ A_{L}, with t occurring in the formula position within B. Given that we are restricting attention of simple L-cuts, there are no other cases to consider; furthermore, the second case may only arise in sequents of the form Γ; ∅ →_{Σ} B −∘ A_{L}.

In the first case the solution is again simple, for the wrong term may be noramlized to D-term of type o. In the second case, the formula B −∘ A_{L} may be normalized to ν((A_{L}) −∘ ν((A_{L}), where ν(A_{L}) is the normalization of A_{L}, yelding a derivable sequent. The only subtlety is that the same witness t may be used in different sequents along the L-cut, resulting in potentially different normalizing terms if we use the naive idea outlined above. Consider, to this regard, the following L-cut of a derivation, where ϕ : o does not have D-form, and where Γ contains the following D-formulas:

E = ∀v. \underbrace{[(v −∘ p(v)) & p(v)] ⇒ q}_{E′}; F = ∀w. \underbrace{[(w −∘ r(w))] ⇒ p(w)}_{F′} .

\begin{matrix}\begin{matrix}Γ; ∅ → (v −∘ p(v))[ϕ/v] ^{−∘^{r}} & {Ξ′ \atop Γ; ∅ → p(v)[ϕ/v]} \\ Γ; ∅ → (v −∘ p(v)) & p(v)[ϕ/v] \end{matrix} &_{r} & Γ; q → q (identity) \\ Γ; E′[ϕ/v] → q \end{matrix} ; ⇒_{l} ; Γ; ∅ → q ; (absorb + ∀_{l})

Here Ξ′ is the following sub-proof:

\begin{matrix}Γ; ∅ → (w −∘ r(w))[ϕ/w] ^{−∘^{r}} & Γ; p(w)[ϕ/w] → p(v)[ϕ/v] identity \\ Γ; F′[ϕ/w] → p(v)[ϕ/v] \end{matrix} ; ∀_{l} ; Γ; ∅ → p(v)[ϕ/v] ; absorb + ∀_{l}

and we assume that Γ; ϕ → p(ϕ) and Γ; ϕ → r(ϕ) have hoiil proofs. Now, if we used the naive normalization we outlined above, we would end up with two normalizing terms for ϕ, namely: p(ν(ϕ) and r(ν(ϕ)) where ν(ϕ) denotes any D-term of type o. Clearly, then, the result of normalization would not be a proof, for what we actually need is the D-term p(ν(ϕ)) & r(ν(ϕ)). In the next subsection we give a technique for systematically computing normalization terms for any given L-cut of a proof. The technique generalizes the idea we just illustrated yielding normalization terms in the form of (conjoined) universally quantified D-formulas.

4.2 Computing Normalization Terms

As illustrated by the previous example, normalization terms may not, generally, be determined by simply looking at the sequent where they are required: a global inspection of (the L-cut of) the proof is needed to find find the appropriate D-formula for every “wrong” witness of type o in the original proof. However, what we can do, locally to every sequent, is to collect the normalizing terms for every potentially “wrong” witness that might be introduced by a substitution over a variable of type o. This is the idea behind the following definition.

Definition 4.6 Local Normalization. Let F be a D_{L} or G_{L} formula, let B denote any formula, and let v be a variable. The the of local normalization terms for v in F, written N[v, F] is defined inductively as follows

- N[v, F_{1} & F_{2}] = N[v, F_{1}] ∪ N[v, F_{2}]

- N[v, ∀_{τ} x.F] = N[v, F]

- N[v, G_{L} ⇒ A_{L}] = N[v, G_{L}]

- N[v, B−∘A_{L}] = {A_{L}} ∪ N[v, B], if B = B_{1} & v & B_{2} for suitable (possibly empty) B_{1} and B_{2},

- N[v, B−∘A_{L}] = N[v, B], otherwise;

- N[v, B] = ∅ if none of the above applies.

As an example, in the formulas of the previous derivation we have: N[v, E′] = {p(v)} and N[w, F′] = {r(w)}.

Given a hoill proof, and a simple L-cut of Ξ, we may compute the normalization term of type o by “decorating” each sequent in the L-cut with a set N of local normaliziation terms. Where N : Γ; Δ →_{Σ} G denotes a decorated sequent, this process can be accomplished in teh following manner:

· the set N at the leaves of the cut is empty; · for every instance of a rule with two premises, the set N of the lower sequent is the union of the correspnding sets of the upper sequents; · for every instance of a rule with one premise, with the xception of (∀_{l}), the set N attached to the upper sequent is simply “copied” in the lower sequent; · for every instance of (∀_{l}) the set N is computed as follows:

{N : Γ; Δ, B[t/x] → C \atop N ∪ N[x, B] : Γ; Δ, (∀_{o}x.B) → C} ∀_{l}

Proceeding in this way at every sequent of the L-cut, the set N occurring at the root of the L-cut can be characterized as follows.

Lemma 4.7. Let Ξ be an hoill proof of a (D, G)-sequent Γ; ∅ →_{Σ} G, and let N be the decoration associated to the root of κ_{L}(Ξ) by the process we just described. Then, for every A_{L} such that Γ; ∅ →_{Σ} B −∘ A_{L} is a leaf sequent of κ_{L}(Ξ), it is the case that A_{L} ∈ N.

Proof. Easy.

Definition 4.8 Canonical Normalization Terms. Let Ξ be a simple L-cut of an hoill proof. Let N be set computed at the root of Ξ by augmenting each sequent in Ξ in the manner we just derscribed. For every type τ, the canonical normalization term of type τ, denote by ν_{τ}, is defined as follows:

· if τ ≠ o, choose a nonlogical constant h : τ from Σ of type τ, and define ν_{τ} = h; · If τ = o, define ν_{o} as the following D-term:

· if N ≡ {A_{1}, …, A_{n}}, and A_{i} = h_{i}(t_{1}, …, t_{n}), then ν_{o} = A_{1}^{∀} & ⋯ & A_{n}^{∀}, where

A_{i}^{∀} = ∀_{τ_{1}}x_{1}…. ∀_{τ_{n}}x_{n}.h_{i}(x_{1}, …, x_{n}).
· If N ≡ ∅, then ν_{o} = ∀_{τ} x.h(x) where h : τ ↦ o is any nonlogical symbol in Σ.

It only remains to define the normalization mapping that tranforms every λ-term to a corresponding nonlogical constant, and every formula to a corresponding D-formula (preserving D-terms and D-formulas).

Definition 4.9 Normalization. Let ν : T_{x} ⇝ T_{x}, the o-normalization of a term F, namely ν(F), be defined as follows:

· if F is a typed constant or a variable, then ν(F) = F;

· if F is the λ-abstraction λx.F′, and has type σ → τ, then ν(F) = λx.ν(F′); · if F is the term (t_{1} t_{2}), and it has type τ ≠ o then ν(F) = (ν(t_{1}) ν(t_{2})); · if F has type o, F ≠ x and F is not in L, x-form then ν(F) = ν_{o}; · if F has type o and F is in L, x-form, then ν(F) = ν^{−}(t) where ν^{−} is the mapping defined by the following mutual recursion:

\begin{aligned}ν^{−}(A_{L}) & = & ν(A_{L}) \\ ν^{−}(G_{L} ⇒ A_{L}) & = & ν^{+}(G_{L}) ⇒ ν(A_{L}) \\ ν^{−}(D_{L} & D_{L}) & = & ν^{−}(D_{L}) & ν^{−}(D_{L}) \\ ν^{−}(∀_{τ} v.D_{L}) & = & ∀_{τ} v.ν^{−}(D_{L}) \end{aligned}  \begin{aligned}ν^{+}(A_{L}) & = & ν(A_{L}) \\ ν^{+}(B −∘ A_{L}) & = & ν(B) −∘ ν(A_{L}) \\ ν^{+}(G_{L} & G_{L}) & = & ν^{+}(G_{L}) & ν^{+}(G_{L}) \\ ν^{+}(∀_{τ} v.G_{L}) & = & ∀_{τ} v.ν^{+}(G_{L}) \end{aligned}

Proposition 4.10. The mapping ν is well-defined.

Proof. Immediate, since ν is defined over terms in λ-normal form. ⊓ ⊔

Remark. Notice that the definition of ν^{−} and ν^{+} allows to keep intact the structure of a D_{L} formula as far as a goal B −∘ A is encountered. Here ν^{+} is recursively defined over ν to inspect the premise of the implication.

Lemma 4.11. Let t ∈ T_{x} then ν(t) is a D, x-term, s.t., F V (ν(t)) ⊆ F V (t).

Proof. By induction on the structure of t. If t is a variable or a constant, the thesis holds immediately. If t = λx.t_{1} or t = (t_{1} t_{2}) : τ ≠ o then the thesis follows by applying the inductive hypothesis. If t has type o, then:

– if t is not in L, x-form then, by definition, ν(t) = ν_{o} and F V (ν_{o}) = ∅, yielding the thesis.

– if t is in L, x-form then, ν(t) = ν^{−}(t). As remarked above, ν^{−} and ν^{+} do not modify the formula as far as a sub G-formula B −∘A is encountered: we can apply here the inductive hypothesis over ν(B) and ν(A) to conclude.

⊓ ⊔

As a consequence, we have the following result.

Corollary 4.12. Let F be in L-form (i.e., closed) then ν(F) is a closed D-formula.

Notice that, since we work on λ-terms in normal form ν is not compositional w.r.t. generic λ-terms and substitutions. For instance, let us consider the terms t = (x c) and s = λy.F/x, with F a D-formula. Then, t[s/x] = F, i.e., ν(t[s/x]) = F, whereas, ν(t)[ν(s)/x] = ν_{0}, since t is not a rigid atom and thus, it is not in L-form. However, it is possible to prove the following result.

Lemma 4.13. Let t : τ, τ ≠ o, be a D, x-term and s a closed term (in λ-normal form), then ν(t[s/x]) = t[ν(s)/x], which in turn is a D, x-term. Furthermore, under the same hypothesis, let t_{1} be a D, x-formula, and t_{2} be a G, x-formula, then ν(t_{1}[s/x]) = t_{1}[ν(s)/x], which, in turn, is a D, x-formula and ν^{+}(t_{2}[s/x]) = t_{2}[ν(s)/x], which, in turn, is a G, x-formula.

Proof. By induction on the structure of t. If t is a variable or a constant, the thesis immediately follows. If t = λx.t_{1}, ν(λx.t_{1}[s/x]) = λx.ν(t_{1}[s/x]), and then the thesis follows by applying the inductive hypothesis, similarly for t = (t_{1} t_{2}) : τ with τ ≠ o. If t has type o, then it must be either a D, x-formula or a G, x-formula. In the first case we must consider ν(t[s/x]), in the second, ν^{+}(t[s/x]).

– The base case for D and G formulas is the same: t = (h t_{1} … t_{n}). Here t[s/x] is equal to (h t_{1}[s/x] … t_{n}[s/x]) where by definition of D, x-term t_{i}, i : 1, …, n is a D, x-term. Thus, we can apply the inductive hypothesis to t_{i}[s/x], i : 1, …, n and then conclude.

– The interesting case of the inductive step occurs for t_{2} equal to D −∘ A. Here ν^{+}((D −∘ A)[t/x]) by definition is equal to ν(D[t/x]) −∘ ν(A[t/x]), and thus we can conclude by applying the inductive hypothesis.

⊓ ⊔

Corollary 4.14. Let F [x] (i.e., x is the unique free variable in F) be a D_{v}, x-formula and t any closed term, then ν(F [t/x]) = F [ν(t)/x], which in turn is a D_{v}-formula.

Based on the previous technical lemmas, we can prove the main result of this section.

Theorem 4.15. Let Γ; Δ →_{Σ} G be a (D, G)-sequent. This sequent has a hoill-proof if and only if it has an L-proof.

Proof. The if part is immediate. For the “only if” part, let Ξ be the hoill proof of the sequent. Take the simple L-cut of Ξ. As we noted sequents in the L-cut have the form Γ; Δ →_{Σ} G where Δ is either empty or contains a single D_{L}-formula, and G is a G_{L}-formula. Every such sequent is clearly derivable in hoill. In the following proof, we will consider D_{L}- and G_{L}-formulas having the form D[t_{1}/x_{1}] … [t_{n}/x_{n}], where D is a D_{v}, x-formula, and G[s_{1}/y_{1}] … [s_{m}/y_{m}], where ∀G is a G, x-formula, i.e., they are introduced by the ∀L rule. Here t_{i}, i : 1 … n and s_{i}, i : 1 … m are closed terms Furthermore, if F = F′[t_{1}/x_{1}] … [t_{n}/x_{n}] let F̂ be F′[ν(t_{1})/x_{1}] … [ν(t_{n})/x_{n}], and let Δ̂ be the pointwise application of ˆ to Δ.

Based on it, we will show that there exists an L-proof for the sequent Γ; Δ̂ →_{Σ} Ĝ_{L}. The theorem follows then easily from this claim: the proof of the claim is by induction on height of the subderivation of Ξ rooted at the sequent in question.

Base: If Γ; A[t_{1}/x_{1}] … [t_{n}/x_{n}] →_{Σ} B[s_{1}/y_{1}] … [s_{m}/y_{m}] is provable, then A[t_{1}/x_{1}] … [t_{n}/x_{n}] is equal to B[s_{1}/y_{1}] … [s_{m}/y_{m}]. By lemma 4.13, A[ν(t_{1})/x_{1}] … [ν(t_{n})/x_{n}] is equal to ν(A[t_{1}/x_{1}] … [t_{n}/x_{n}]) which, in turn, is equal to ν(B[s_{1}/y_{1}] … [s_{m}/y_{m}]), which, again by lemma 4.13, is equal to B[ν(s_{1})/y_{1}]…[ν(s_{m})/y_{m}].

Inductive step: By cases on the last rule.

Left rules: Let us consider ( & L): Γ; F [t_{1}/x_{1}] … [t_{n}/x_{n}] →_{Σ} G is provable and F [t_{1}/x_{1}]…[t_{n}/x_{n}] corresponds to D_{1} & D_{2}, i.e., Γ; D_{i} →_{Σ} G is provable for i : 1..2.

– If F has already the form F_{1} & F_{2} then D_{i} ≡ F_{i}[t_{1}/x_{1}] … [t_{n}/x_{n}], i : 1, 2, then the thesis follows by applying the inductive hypothesis.

– If F is a free variable x then there must exist a substitution term [t_{i}/x_{i}] s.t. x_{i} = x and t_{i} = D_{1} & D_{2} (since t_{i} is a closed term). Let us observe that x[t_{1}/x_{1}] … [t_{n}/x_{n}] can be written as z_{1} & z_{2}[D_{1}/z_{1}][D_{2}/z_{2}]. Now we can apply the inductive hypothesis to the premises, i.e., Γ; D_{i} →_{Σ} G which is equivalent to Γ; z_{i}[D_{i}/z_{i}] →_{Σ} G, i : 1, 2, and we obtain a proof for Γ; z_{i}[ν(D_{i})/z_{i}] →_{Σ} Ĝ, i : 1, 2 and for Γ; z_{1} & z_{2}[ν(D_{1})/z_{1}][ν(D_{2})/z_{2}] →_{Σ} Ĝ, i.e., for Γ; x[ν(t_{1})/x_{1}] … [ν(t_{n})/x_{n}] →_{Σ} Ĝ.

Similar arguments can be applied to the other left rules: For instance, for (∀ L) we have that Γ; ∀x.F [t_{1}/x_{1}] … [t_{n}/x_{n}] →_{Σ} G is provable, thus Γ; F [t_{1}/x_{1}] … [t_{n}/x_{n}][t/x] →_{Σ} G is provable. By lemma 4.14, we know that F [ν(t_{1})/x_{1}] … [ν(t_{n})/x_{n}] is a D, x-formula, thus, by inductive hypothesis, we know that Γ; F [ν(t_{1})/x_{1}] … [ν(t_{n})/x_{n}][ν(t)/x] →_{Σ} Ĝ is provable. Applying again the ∀ L rule we obtain a proof for Γ; ∀x.F [ν(t_{1})/x_{1}] … [ν(t_{n})/x_{n}] →_{Σ} Ĝ. Notice here that we have just normalized the substitution terms introduced by ∀ L in order to preserve well-formed (D, G)-sequents while constructing the proof.

Right-rules: Let us consider (−∘ R), i.e., Γ; ∅ →_{Σ} G[s_{1}/y_{1}] … [s_{m}/y_{m}] is provable with G[s_{1}/y_{1}] … [s_{m}/y_{m}] equal to D′ −∘ A′[s_{1}/y_{1}] … [s_{m}/y_{m}] (say D −∘ A), s.t. Γ; D →_{Σ} A is provable. Now, if D is in L-form we can conclude by applying the inductive hypothesis. If D ≡ D′[s_{1}/y_{1}] … [s_{m}/y_{m}] is not in L-form: since by hypothesis D′ is a D_{v}-formula it follows that there exists x a variable of type o occurring at the top level in D and a term s_{i} s.t. x_{i} = x and s_{i} is not a D-formula. By definition in D′[ν(s_{1})/y_{1}] … [ν(s_{m})/y_{m}] one of the conjuncts is x[ν(s_{i})/x] ≡ ν_{o}. Now since ν_{o} is defined over the initial proof, if A′ = (h t_{1} … t_{k}) then one of the conjuncts of ν_{o} is the formula ∀x_{1}…. ∀x_{n}.(h x_{1} … x_{k}). Thus it is easy to build a proof for the considered sequent:

\begin{matrix}Γ; (h x_{1} … x_{k})[t′_{1}/x_{1}] … [t′_{k}/x_{k}] →_{Σ} (h t′_{1} … t′_{k}) & (initial) \\ ⋮ . k (∀_{l}) steps \end{matrix} ; Γ; ∀x_{1}…. ∀x_{k}.(h x_{1} … x_{k}) →_{Σ} (h t′_{1} … t′_{k}) ; ⋮ . n (&_{l}) steps ; Γ; ν_{o} →_{Σ} (h t_{1} … t_{k})[s_{1}/y_{1}] … [s_{m}/y_{m}]

Here t′_{i} = t_{i}[s_{1}/y_{1}] … [s_{m}/y_{m}], i : 1, …, k. The other cases can be proved by simply applying the inductive hypothesis. ⊓ ⊔

5 Encoding P RO_{bj}LOG in L

The key idea in defining P RO_{bj}LOG is to distinguish, within the object calculus we have just outlined, the aspects relative to the representation of objects and methods, from those relative to the semantics of the primitive operations of extension, override and method invocation. Intuitively, this distinction is achieved by representing objects a complex terms, with method fields, occurring within G formulas, while encoding the ⟶^{eval} relation by means of D formulas placed in the unbounded context of a sequent. As in the language F &O of [4], the higher order nature of the syntax allows us to encode both these aspects uniformly in the language.

5.1 Encoding P RO_{bj}LOG into L.

In the following we will fix an encoding from the P RO_{bj}LOG -syntax into L the considered fragment of Linear Logic. As we will show objects will find an immediate counterpart into higher order terms, methods invocations into particular G-formulas, and methods definitions into D-formulas. Let us fix the followig set of primitive types: α (denoting the set of methods identifiers), ω (denoting object-terms).

The encoding [[ •]] x_{β}, where β is a type and x is a variable name, is defined as follows:

[[ x]] s_{ω} ≡ x, if x is a variable and x ≠ s .
[[ self]] s_{ω} ≡ s.
[[ obj[ ]]] s_{ω} ≡ ( )
[[ obj[m_{1} = D_{1}, …, m_{k} = D_{k}] ]] s_{ω} ≡ ((m_{1}, [[ D_{1} ]] _{μ}^{m_{1},s}) :: …:: ( m_{k}, [[ D_{k}]] _{μ}^{m_{k},s})).

Here [] is a term of type ω, (•, • :: …:: •, •) is a family of term constructors with type α → o → … α → o → ω. For every i = 1, …, k, m_{i} is a method name (i.e., a constant with type α) and D_{i} a formula which corresponds to a method definition. Methods invocations are represented by atomic formulas:

     [[ object_{1}.margs ↦ object_{2} ]] s_{γ} ≡ send [[ object_{1} ]] s_{ω} m [[ args]] s_{τ} [[ object_{2} ]] s_{ω}.

here the operator •. send • • • is a predicate name having type ω → α → τ → ω → o. The arguments of an invocation are encoded as follows:

[[ ∅]] s_{τ} ≡ nil.
[[ (object_{1}, …, object_{k}) ]] s_{τ} ≡ ( [[ object_{1} ]] s_{ω}, …, [[ object_{k} ]] s_{ω}).
[[ object]] s_{τ} ≡ [[ object]] s_{ω}.

Here (•, …, •) is a family of tuple constructors (each for any arbitrary combination of types). Primitive operations are encoded as follows:

[[ obj_{1}.ext.m = body ↦ obj_{2} ]] s_{γ} ≡ ext [[ obj_{1} ]] s_{ω} m [[ body]] s_{μ}) [[ obj_{2} ]] s_{ω}.

        [[ obj_{1}.over.m = body ↦ obj_{2} ]] s_{γ} ≡ over [[ obj_{1} ]] s_{ω} m [[ body]] s_{μ} [[ obj_{2} ]] s_{ω}.

The composition of invocation is mapped into conjunctions of atomic G-formulas:

[[ ∅]] s_{γ} ≡ ϵ .
[[ comp]] s_{γ} ≡ [[ comp]] s_{γ}.
[[ comp, comp ]] s_{γ} ≡ [[ comp]] s_{γ} & [[ comp]] s_{γ}.

here ϵ stands for the empty string. Finally, methods are represented as follows:

[[ argscomp ↦ object ]] _{μ}^{m,y} ≡ ∀s.∀\overline{x}. (m s [[ args]] s_{τ} [[ object]] s_{ω}) ⇐ [[ comp]] s_{γ}.

                              if comp ≠ ∅

[[ args ∅ ↦ object ]] _{μ}^{m,y} ≡ ∀s.∀\overline{x}. m s [[ args]] s_{τ} [[ object]] s_{ω}.

Here, m is a predicate symbol having type ω → τ → ω → o, \overline{x} is a sublist of all the variables occurring in the definition, (i.e. variables may occur free in a method definition) ands is a new variable representing the host object for the method.

Outside the scope of a method definition it is possible to forget the self superscript. This is true in particular for conjunctions of top-level object invocations msg_{1}, …, msg_{n}, which can be encoded as [[ msg_{1} ]]_{μ} & … & [[ msg_{n} ]]_{μ}.

The symbols send, ext and over are symbols corresponding to the three object-related primitives defined defined by means of the D-formulas that we discuss next. To ease the notation, in the rest of this section we adopt the following standard conventions: top-level typed quantifiers are omitted, and quantified variables are denoted by upper-case symbols; conjoined D formulas are written as separate clauses, whereas G-formulas are separated by commas; finally, square brackets are omitted from 1-component tuples.

Messages and Method Invocation. Sending a message to an object consists of two separate steps, namely (i) select the definition of the corresponding method on the receiver of the message, and (ii) apply the definition to the receiver itself and the input arguments specified in the message. To account for these operations, we introduce the following Ddefinition of the send and select primitives (the abuse of notation m ≠ n below is only apparent as this test could, in principle, be expressed as a message to an object with an eq method):

send o m t r ⇐ select o m d, (d −∘ m o t r).

select ((m, d) :: o) m d.

select ((n, ) :: o) m d ⇐ m ≠ n, select o m d.

The effect of evaluating a send primitive can be illustrated as follows. Let Γ be a set of D-formulas including the above D-definitions of send and select , and let O be an object containing an m method defined by D. Then, proving the goal formula send M O T R amounts to the following derivation in the system L:

⋮ . Σ : Γ →_{Σ}^{E} select O M D Σ : Γ →_{Σ} select O M D (absorb)  \begin{matrix}{… \atop Σ : Γ →_{Σ}^{D} m O T R} & (bc) \\ Σ : Γ →_{Σ} D −∘ m O T R \end{matrix} ; (−∘R)
Σ : Γ →_{Σ} select O M D, (D −∘ m O T R)

(&R)

Σ : Γ →_{Σ} send M T O R (absorb + bc)

The upper-right application of the (bc) rule in the right branch of the proof selects (nondeterministically) one formula in [D]_{Σ}, which is used to reduce the formula m O T R: matching the term that encodes the host object in the head of D with O captures desired effect of “self-applying” the m method to the receiver of the message. Note further that methods are made available as bounded resources for backchaining only when explicitly requested by a message. Since objects are non identified, this ability to activate methods selectively upon evaluating a message is crucial to avoid conflicts among methods of different objects.

Method Extension and Override The remaining primitive operations on objects are method addition and overriding defined by the following D-formulas, whose intended meaning should be self-explanatory.

( ). ext (m, d) ↦ ((m, d)).

ext ((n, ) :: o) m d ((n, ) :: o_{1}) ⇐ m ≠ n, ext o m d o_{1}.

over ((m, ) :: o) m d ((m, d) :: o).

over ((n, ) :: o) m d ((n, ) :: o_{1}) ⇐ m ≠ n, over o m d o_{1}.

Two examples. Let us consider the example 2.1 in section 2. The point object is defined by:

          pt =^{def} obj[x = 3, mv = (Y)(self.x ↦ X, self.over.x = X+Y ↦ Z) ↦ Z].

Its encoding in L is defined as:

[[ pt]]_{ω} =^{def} ((x, D_{x}) :: (move, D_{move})),

where D_{x} is ∀self. m self nil 3. and D_{move} is the following clause:

∀self, z, o, v, s.

m self z ↦ o ⇐ send self x () v, over self x (∀s. m s () v+z.) ) o.

Here we have simplified the notation for integers-objects and their corresponding methods (e.g., “+”).

Let us consider now the translation of the object definition in the example 2.3. Here numerals are defined by objects having the following form:

   num =^{def} obj[ zero? = ↦ true,
               pred = ↦ self
               succ = self.over.zero? = M_{zero} ↦ P, P.over.pred = M_{pred} ↦ Q ↦ Q].

where M_{zero} = ↦ false and M_{pred} = ↦ self.

Thus, [[ num]]_{ω} is the following term:

[[ num]]_{ω} =^{def} (
(zero? , ∀self. m self () true.) ::
(pred , ∀self. m self () self) ::
(succ , ∀self. m self () o ⇐

over self zero? [[ M_{zero} ]] self_{μ} p &

                                 over p pred [[ M_{pred} ]] self_{μ} o)

)

where [[ M_{zero} ]] self_{μ} = ∀s. m s zero? () false. [[ M_{pred} ]] self_{μ} = ∀s. m s pred () self.

6 Implementation using Lolli

Lolli [8] is a linear logic programming language based on intuitionistic linear logic. The set of its connectives includes those of L. Lolli enjoys some higher-order features suitable to encode P RO_{bj}LOG . In particular, Lolli allows universally quantified formulas to occur inside terms, thus allowing to represent self-referencing objects accordingly to the ideas shown in the previous sections.

MODULE point.
class point ((coord,(0,0))::nil) (prettyprint::nil).
meth  mv Self (Dx,Dy) NewS (
 get Self coord (X,Y),
 X1 is X + Dx,
 Y1 is Y + Dy,
 update Self coord (X1,Y1) NewS
).
pred prettyprint Self nil (
 write("Point Object with coordinates: "),
 get Self coord (X,Y),
 write(X),
 write(","),
 write(Y),
 nl
).

Fig. 2. A P RO_{bj}LOG class using Lolli syntax.

In Fig. 2 we show an example of an P RO_{bj}LOG -object representation in Lolli. Objects are created by means of a class declarator which allows to specify the list of attributes (i.e., constant methods) and of method-names of the objects belonging to the class. Methods are defined through separate facts having form meth MethName Self Parameters Result

(Body) and pred MethName Self Parameters (Body) for predicates. At the moment of

an object creation (see the clause defining new in the module obj of Fig. 3) this definitions are clustered together into one term having form (St,Mts), where St is a list of pairs

(Attribute-Name,Value) and Mts is a list of pairs (Method-Name,Def). Keeping separate

the definition of methods simplifies the syntax, as shown in the examples. In fact, they can be defined as clauses getting rid of universal quantifiers by simply using free-variables.

Based on this syntax it is possible to define the basic primitives of P RO_{bj}LOG , see Fig. 3 and Fig. 4: send to invoke a meth-method, call to invoke a pred-method, get, update, enrich respectively to retrieve, update and add a new value for a given attribute, override, extend to ovveride a method definition and to extend the set of methods of an object, and finally init to initialize a newly created object. Notice that it is possible to invoke get in

MODULE obj.
new Class (St,Mts):-
   (class Class St MtNs) -> true |
      (nl,write_sans ("Error: Class "),
          write(Class),
          write_sans(" is not defined"),
       nl,fail),
   buildMts Class (MtNs) Mts.
get Ob M V:-
 Ob = (St,Mts),
 select St M V.
get Ob M V:-
 Ob = (g Oo Mo),
 get Oo Mo Oi,
 get Oi M V.
send Ob M P V:-
 Ob = (St,Mts),
 select Mts M Def,
 generalize Def QDef,
 QDef -o (m Ob P V).
send Ob M P V:-
 Ob = (s Oo Mo Po),
 send Oo Mo Po Oi,
 send Oi M P V.
call Ob M P:-
 Ob = (St,Mts),
 select Mts M Def,
 generalize Def QDef,
 QDef -o (p Ob P).

Fig. 3. An interpreter in Lolli for P RO_{bj}LOG .

cascade; for instance, a goal get (g (g O m1) m2) m3 V corresponds to get O m1 W,get W m2 Z,get Z m3 V. In the send and call definition of Fig. 3 we have also used the built-in predicate generalize F QF which transforms a formula with free variables X_{1}, … X_{n} into a close formula universally quantified over X_{1}, … X_{n}, in order to avoid name-clashing.

Also, in Fig. 4 we have included the definition of the pre-defined methods swrite, init and write associated with each class.

A Case-study: a computational geometry application In this section we will present an application of P RO_{bj}LOG to a computational geometry problem inspired by [7]. In computer graphics problem concerning surfaces representation and analisys it comes naturally to resort to logic programming techniques to handle queries on a large search-space. Here we are interested in considering a particular representation of surfaces based on triangulated models. The idea is to consider various level of precision in the description of a terrain by defining a

update (St,Mts) M V (NewSt,Mts):-
  adjorn St M V NewSt.
enrich (St,Mts) M V (NewSt,Mts):-
  add St M V NewSt.
override (St,Mts) M Def (St,NewMts):-
  adjorn Mts M Def NewMts.
extend (St,Mts) M Def (St,NewMts):-
  add Mts M Def NewMts.
init (St,Mts) (NewSt,Mts):-
  initAs St NewSt.
pred write Self nil (
  writeObj Class Self n
).
pred swrite Self nil (
  writeObj Class Self s
).
meth init Self nil InitSelf (
  init Self InitSelf
).

Fig. 4. Definition of P RO_{bj}LOG -built-in predicates.

hierarchy of triangles (called HTTM: hierarchical triangulation terrain model), i.e., triangles can be subdivided in more precise ones.

Our problem is a simplification of the more general of solving interference queries: given a HTTM T, a geometrical object O, and a fixed precision ϵ, it is to find the minimal triangle Tr interfering with O and such that its precision is less or equal to ϵ. In our case we will consider points as geometrical objects with the interference relation given as follows: a point belongs to a triangle of the hierarchy.

Let us formulate the data-scheme in our P RO_{bj}LOG prototype. We will reconsider the class point definition in Fig. 3 in addition to the class triangle defined in Fig. 5, whose attributes are its vertices p, q, r, considered in anticlockwise order, its precision eps, and the list of subtriangles lx. The most important method of this class is in which takes Self and InP (a point object) as input arguments and checks whether InP belongs to Self. The other ones are used to pretty-print its objects.

The main program is based on a visit of the HTTM in order to search for the minimal triangle this simple program is shown in Fig. 6, where start is the goal that must be invoked to start the search process.

The flexibility of P RO_{bj}LOG which mixes OO and LP, allows to write a very clear scheme of the solution demanding to the methods definitions the details of the algorithm. In this case it should be possible to consider global methods, i.e., defined over all objects of a same class,

MODULE trgclass.
class triangle St Mts:-
  St=((p,nil)::(q,nil)::(r,nil)::(eps,0)::(lx,nil)::nil),
  Mts=(in::writeTrg::writeLx::nil).
pred in Self InP (
 get Self p P,
 get P coord (X1,Y1),
 get Self q Q,
 get Q coord (X2,Y2),
 get Self r R,
 get R coord (X3,Y3),
 get InP coord (X,Y),
 isin X Y X1 Y1 X2 Y2 X3 Y3
).
pred writeTrg Self nil (
 get Self p P,
 get P coord C1,
 get Self q Q,
 get Q coord C2,
 get Self r R,
 get R coord C3,
 get Self eps Eps,
 writeTrg C1 C2 C3 Eps
).
pred  writeLx Self nil (
 get Self lx Lx,
 writeTrgList Lx
).

Fig. 5. A definition of HTTM’s.

since it is not necessary to modify them (modulo the attributes (constant methods) which are considered apart). For sake of completeness, in appendix A we include the definition of the other predicates useful to fully implement this example.

Dynamic behaviour of objects. The possibility of dynamically modifying the set of methods of a P RO_{bj}LOG -objects can be useful in order to deal with exceptions, without the need of inserting a new class and thus to re-design the data scheme. For instance, consider the definitions in Fig. 7. The class employee inherits the attributes and methods of the class person (the methods are the built-in ones specified in Fig. 4) adding the method check which checks whether the salary of an employee is less then the salary of his/her superior.

Now, if we assume that a given employee enjoys extra earnings and we want to specify this by adding a further attribute extras to its set of methods, than we must re-arrange the definition of method check in order not to burden the scheme by adding a further method, as shown in figure Fig. 8. Here a query like modify 1000 creates a new employee E (the built-in method init reads the data from standard input), and assuming a new definition of check,

MODULE triangle.
findTrg T P Eps Tr:-
 get  T eps E,
 call T in P,
 checkEps T P E Eps Tr.
checkEps T P E Eps T:-
 E =< Eps.
checkEps T P E Eps Tr:-
 E > Eps,
 get  T lx Lx,
 member ST Lx,
 call ST writeTrg nil,
 findTrg ST P Eps Tr.
checkEps T P E Eps T:-
 write_sans("Warning: it is not possible to have better precison than "),
 write(E),nl.
start :-
build_triangulation T,
call T writeTrg nil,
new_point P,
write_sans("Insert Precision:"),
read(Eps),
findTrg T P Eps Tr,
write_sans("Minimal Triangle:"),
call Tr writeTrg nil.

Fig. 6. Solution for the interference query locate a point in a HTTM.

MODULE over.
class person St Mts:-
St=((name,nil)::(salary,nil)::nil),
Mts=(swrite::write::init::nil).
class employee ((superior,nil)::St) (check::Mts):-
class person St Mts.
pred check Self nil (
get (g Self superior) salary S,
get Self salary MS,
nl,write_sans("Comparing "),
write(S),
write_sans(" to "),
write(MS),nl,
S > MS
).

Fig. 7. Typical examples: person and employee.

def ((p Self nil) <= Body):-
 Body =
 (
  get (g Self supervisor) salary S,
  get Self salary MSo,
  get Self extras MSi,
  MS is MSo + MSi,
  write_sans("Comparing "),
  write(S),
  write_sans(" to "),
  write(MS),nl,
  S > MS -> write_sans(" Ok!") | write_sans(" Anomaly!"),
  nl
 ).
modify Ex:-
  new employee E,
  call E init nil,  % we assume to specify here E's superior
  def D,
  enrich   E  extras Ex E1,
  override E1 check  D  E2,
  call E2 write nil,
  call E2 check nil.

Fig. 8. A query over an employee object.

enriches the set of attributes of E with the pair (extras,1000) and overrides the definition of check with the new one D.

As final remark, it is interesting to notice that during the develpment of the Lolli prototype for P RO_{bj}LOG , many interesting features have been added to the core language. As mentioned before, we have considered a simplified form of object definition based on a class template, which also allows to enjoy class-based inheritance, as shown by the definition of the class employee in Fig. 8, and overriding (not shown in the examples above but easy to figure out). On the other hand, object-based inheritance and overriding are ensured by the object primitives override and extend, thus, allowing many levels of data-refinement.

7 Conclusions

We have presented a linear logic programming language that gives a complete logical account of an object calculus with overriding and inheritance by delegation. We have defined a proofsystem for the language, as well as an interpreter based on unification.

7.1 Related Work

As we already mentioned, the use of Linear Logic as a tool for modeling object-oriented programming in logic has already been addressed in the literature: among others, notable examples are the LO language of [2], the Linear Logic Language F &O [4] and the the HACL language of [9].

In LO, objects are represented as ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} –disjunctions of atomic formulas playing the role of attributes, while methods are specified as linear clauses that are used to rewrite (possibly modifying them) the attributes of objects. In P RO_{bj}LOG , instead, objects are encoded as terms that encapsulate their methods as subterms. With this encoding, while retaining the form of method inheritance peculiar to [2], we also obtain a natural modeling of dynamic method redefinition, a functionality that could hardly be accounted for in [2].

The encoding of objects in P RO_{bj}LOG is inspired to the language F &O of [4], from which, however, our approach differs for the choice of both the computational model and the object model. F &O subscribes to the proofs-as-computations principle of Linear Logic which interprets sequents as encodings of the state of the computation and proofs as descriptions of the state evolution. Furthermore, F &O takes, essentially, a class-based approach where objects are created by instantiating a class and referenced to by means of the identifiers they are associated with at creation time. A similar approach is taken in the HACL language of [9]. HACL is a concurrent linear logic calculus which also adheres to the proofs-as-computations and formulas-as-processes principles of Linear Logic. Again, the object model is, essentially, a class-based model where objects are encoded as (λ-abstraction of) records that result as the fixed points of their associated class definitions.

On the other hand, P RO_{bj}LOG is a standard logic programming language, that uses unification to compute values returned as results in answer substitutions, and shared variables to capture the semantics of cascaded method invocations peculiar to the companion functional calculi. Furthermore, the underlying data model is an object-based model, where the recursive nature of objects is captured relying on the self-application semantics of method invocation rather than on the on the explicit use of fixed-point operators. Using this encoding, objects in P RO_{bj}LOG could be construed as elements of recursive types in a way similar to that described in [5]. The rest of this section briefly describes how this can be done.

7.2 An Object-Type System for P RO_{bj}LOG

In the type system of [5], the types that are assigned to objects have the form objectt.⟨⟨m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩, describing the methods (and corresponding types) available from objects with this type. Given an expression e : objectt.⟨⟨…, m : τ⟩⟩, the result of the method invocation e ⇐m is a value of type [objectt.⟨⟨…, m : τ⟩⟩/t]τ, with the substitution of the object-type for t in τ reflecting the recursive nature of object-types.

Object representation in P RO_{bj}LOG was designed precisely to allow types of objects to be encoded exactly in this manner. For instance, assuming to replace the generic type o in the current encoding with the mode expressive class of object-types, we could, for instance, assign the point object pt of section ?? the following type: objectt.⟨⟨x : int, move : int→t⟩⟩.

Allowing object-types in the set of legal types would thus be a smooth extension that does not break the type structure we have devised, provided that unification be instrumented to deal with the new types. This, and the other related problems relative to the extension with object-types represent subject of our future work.

Acknowledgements. The authors wish to thank the anonymous referees for their comments and suggestions.

References

1. M. Abadi and L. Cardelli. A Theory of Primitive Objects. In Proceedings of Theoretical Aspect of Computer Software, volume 789 of LNCS, pages 296–320. Springer-Verlag, 1994.

2. J. M. Andreoli and R. Pareschi. Linear Objects: Logical Processes with Built-In Inheritance. New Generation Computing, 9:445–473, 1991.

3. L. Cardelli and J.C. Mitchell. Operations on Records. Mathematical Structures in Computer Sciences, 1(1):3–48, 1991.

4. G. Delzanno and M. Martelli. Objects in Forum. In Proceedins of the International Logic Programming Symposium, Portland, Oregon, pages 115–129. The MIT Press, 1995.

5. K. Fisher, F. Honsell, and J. C. Mitchell. A Lambda Calculus of Objects and Method Specialization. Nordic Journal of Computing, 1(1):3–37, 1994.

6. A. Goldberg and D. Robson. Smalltalk-80, The Language and its Implementation. Addison Wesley, 1983.

7. G. Guerrini and P. Marzano. Interference Queries on Hierarchical Terrain Models in a Deductive Object-Oriented Database Language, DISI-TR-95-14. Technical report, Dept. of Computer and Information Science, University of Genova, Genova, 1995.

8. J. Hodas and D. Miller. Logic Programming in a Fragment of Intuitionistic Linear Logic. Information and Computation, pages 110(2):327–365, 1994.

9. N. Kobayashi and A. Yonezawa. Type-Theoretic Foundations for Concurrent Object-Oriented Programming. In Proceedings of ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA ’94), 1994.

10. D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

11. D. Ungar and R. B. Smith. Self: the Power of Simplicity. In Proceedings of ACM Symp. on Object-Oriented Programming Systems, Languages, and Applications, pages 227–241. ACM Press, 1987.

A Auxiliary predicates

MODULE aux.
not G   :- G       -> fail | true.
neq N M :- (N = M) -> fail | true.
select ((M,V)::R) M V.
(select ((N,V)::R) M W) <=
neq N M,
select R M W.

adjorn ((M,V)::St) M W ((M,W)::St).
(adjorn ((N,V)::St) M W ((N,V)::St1) )<=
(neq N M),
(adjorn St M W St1).
adjorn nil M V ((M,V)::nil).
add ((M,V)::St) M W ((M,V)::St).
(add ((N,V)::St) M W ((N,V)::NewSt) ) <=
(neq M N),
(add St M W NewSt).
add nil M V ((M,V)::nil).
initAs ((N,V)::St) ((N,W)::NewSt):-
write(N),
write_sans(": Value[y] or Object[class_name]?"),
read(I),
(I = y) -> read(W) |
 (nl,write("> sub-object"),nl,
  new I Ob,
  send Ob init nil W,nl,
  write("> back-to-super-object"),nl),
initAs St NewSt.
initAs nil nil.
writeObj Class (St,Mts) F:-
write_sans("Object of Class: "),
write_sans(Class),nl,
write_sans("attributes: "),nl,
writeAts St,
F = n -> (nl,write_sans("methods: "),nl,(writeMts Mts)) | true.
writeAts nil.
writeAts ((N,Ob)::Rest):-
(Ob = (St,Mts)),
write(N),write_sans(": "),
nl,write_sans("-----"),nl,
writeObj " " Ob s,
nl,write_sans("-----"),nl,
writeAts Rest.
writeAts ((N,V)::Rest):-
write(N),write_sans(": "),write(V),nl,
writeAts Rest.
writeMts nil.
writeMts ((N,D)::Rest):-
nl,
write(N),write_sans(" "),writeMt D,nl,
writeMts Rest.
writeMt (Body => (m X P R)):-
write(X),write_sans(" "),write(P),
write_sans(" --> "),write(R),write_sans(" :-"),nl,
writeBody(Body).

writeMt (Body => (p X P)):-
 write(X),write_sans(" "),write(P),
 write_sans(":-"),nl,
 writeBody(Body).
writeBody Bo:-
 write_sans("  "),
 (Bo = (A,B)) ->
   (write(A),nl, writeBody(B)) |
   (write(Bo)).
buildMts Class (Name::R) ((Name,QDef)::Mts):-
meth Name X Ps V Body ,
QDef = ((m X Ps V) <= Body),
buildMts Class R Mts.

buildMts Class (Name::R) ((Name,QDef)::Mts):-
pred  Name X Ps Body,
QDef = ((p X Ps) <= Body),
buildMts Class R Mts.
buildMts Class nil nil.

MODULE geo.
det X Y X1 Y1 X2 Y2 R:-
R is (((X1 * Y2) - (X2 * Y1)) - ((X * Y2) - (X2 * Y))) +
     ((X * Y1) - (X1 * Y)).
dist X Y X1 Y1 R :-
R is ((X - X1) * (X - X1)) + ((Y - Y1) * (Y - Y1)).
between X Y X1 Y1 X2 Y2:-
dist X  Y  X1 Y1 D1,
dist X  Y  X2 Y2 D2,
dist X1 Y1 X2 Y2 D3,
D1 =< D3,
D2 =< D3.
isinP    X Y X1 Y1 X2 Y2:-
det     X Y X1 Y1 X2 Y2 0,
between X Y X1 Y1 X2 Y2.
isin   X Y X1 Y1 X2 Y2 X3 Y3 :-
isinP X Y X1 Y1 X3 Y3.
isin   X Y X1 Y1 X2 Y2 X3 Y3 :-
isinP X Y X1 Y1 X2 Y2.
isin   X Y X1 Y1 X2 Y2 X3 Y3 :-
isinP X Y X3 Y3 X2 Y2.
isin   X Y X1 Y1 X2 Y2 X3 Y3:-
 det  X Y X1 Y1 X2 Y2 R1,
 R1 > 0,
 det  X Y X2 Y2 X3 Y3 R2,
 R2 > 0,
 det  X Y X3 Y3 X1 Y1 R3,
 R3 > 0.
member X (X::L).
member X (Y::L):-
 member X L.

MODULE triangleAUX.
writeTrg (X1,Y1) (X2,Y2) (X3,Y3) Eps:-
nl,write_sans("Precision: "),write(Eps),nl,
write_sans("     "),
write(X3),write_sans(","),write(Y3),nl,
write_sans("    /    \"),nl,
write(X1),write_sans(","),write(Y1),
write_sans(" ----- "),
write(X2),write_sans(","),write(Y2),nl,nl.
writeTrgList nil.
writeTrgList (T::Ts):-
call T writeTrg nil,
writeTrgList Ts.
new_point Q:-
write_sans("Insert X:"),
read(X),
write_sans("Insert Y:"),
read(Y),
new point P ,
initPt (X,Y) P Q.
readVertex P Q R Eps:-
write_sans("Epsilon:"),
read(Eps),
new_point P,
new_point Q,
new_point R.
initTrg P Q R Eps Lx (St1,Mts) (St,Mts):-
St1 = ((p,P1)::(q,Q1)::(r,R1)::(eps,Eps1)::(lx,Lx1)::Stx),
St  = ((p,P) ::(q,Q) ::(r,R) ::(eps,Eps) ::(lx,Lx) ::Stx).
initPt C (St1,Mts) (St,Mts):-
St1 = ((coord,C1)::Stx),
St  = ((coord,C)::Stx).
build_triangulation NT:-
readVertex P Q R Eps,
write_sans("Quanti sotto triangoli?"),
read(N),
build_triangle_list N Lx,
new triangle T,
initTrg P Q R Eps Lx T NT.
build_triangle_list N (T::Ts):-
N>0,
build_triangulation T,
N1 is N-1,
build_triangle_list N1 Ts.
build_triangle_list 0 nil.