Fibred Semantics for

Feature-Based Grammar Logic^{∗}

Jochen Dörre^{1}  Dov Gabbay^{2}  Esther König^{1}

1 Institute for Computational Linguistics

University of Stuttgart

Azenbergstr. 12, 70174 Stuttgart, Germany

Fax: +49-711-121-1366 {jochen,esther}@ims.uni-stuttgart.de 2Department of Computing, Imperial College of Science, Technology and Medicine 180 Queen’s Gate, London SW7 2BZ dg@doc.ic.ac.uk

August 31, 1994

Abstract

We apply the paradigm of fibred semantics (or layered logics) to a combination of two modal logics, Lambek categorial grammar and Kasper/Rounds-style feature logic. These are combined by replacing (or annotating) atomic formulas of the first logic, i.e. the basic categories, by formulas of the second. Our investigation of the combined logic is lead by the aim to give a simple model-theoretic semantics to categorial brands of feature-based unification grammars. We show that a direct application of the fibred semantics method results in a logic which doesn’t match this aim. Essentially this says that the proof theory based on the straightforward generalization of Lambek’s calculus where types are matched using unification is not appropriate when we want to apply the most direct interpretation to these generalized types where a formula like np(num:sg & pers:3rd), which replaces some basic category, denotes those strings which have the indicated property, and the categorial operators denote the usual left- and right-residuals of these string sets.

However, if we reinterpret the (embedded) feature terms as global feature constraints while maintaining the same kind of fibred structures we can show that the anticipated proof system is sound and complete for this combined logic.

∗We are grateful to Hans Leiss who read a draft of the paper and pointed out gaps in our argumentation.

Contents

1 Introduction 131 1.1 More linguistic motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 1.2 The idea of fibred logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 1.3 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 1.4 Outline of the paper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136

2 A concatenation logic 136 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 2.3 Proof theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137

2.3.1 A labeled deductive system . . . . . . . . . . . . . . . . . . . . . . . . . 137 2.3.2 Soundness and Completeness . . . . . . . . . . . . . . . . . . . . . . . . 138

3 Feature Logic 141 3.1 Feature Constraint Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 3.2 EPF Constraints and Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . 143

3.2.1 Determining satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . 144 3.3 Feature Term Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144

3.3.1 Feature vs. first-order terms . . . . . . . . . . . . . . . . . . . . . . . . . 146

4 Excursion: Lambek Predicate Logic 147

5 The Combination 147

5.1 Embedded Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 5.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 5.1.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149

5.2 Global Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151 5.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151 5.2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 5.2.3 Proof Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 5.2.4 Soundness and Completeness . . . . . . . . . . . . . . . . . . . . . . . . 154 5.2.5 Computational Considerations . . . . . . . . . . . . . . . . . . . . . . . . 155

6 Discussion 157

A Hilbert-system for the Lambek calculus 160

1 Introduction

Consider the Horn program

α_{j} ← α_{j_{1}} … α_{j_{n}} ; α_{1} ← ; ⋮ ; α_{i} ←  (1)

where we separated the facts from the real clauses. Such programs can be formalisations of diverse applications. Any particular application area may require special constraints on the derivation. For example formal Horn clauses may represent the rules of a deductive database, with no special resource constraints or they may represent the rules of a formal grammar, where the special constraints are needed. Consider a formal grammar. The grammar rules can be represented as Horn clauses in the form, for example

s ← np vp ; np ← john ; vp ← walks  (2)

or

\begin{matrix}expr ← expr op expr \\ expr ← a \\ expr ← b \\ op ← + \end{matrix}  (3)

Although these grammar rules look similar to (propositional) Horn clauses, a standard Horn logic interpretation of these rules without constraints does not account for the intended meaning: Parsing an expression of a computer language or parsing a natural language requires “resource-awareness”: all subexpressions must be accounted for exactly once in a parse. Obviously additional restrictions are required. There are basically two ways to set up a “grammar logic”:

1. use a linear logic instead of pure propositional Horn logic (i.e. regard the Horn clauses as a fragment of linear logic and therefore certain resource restrictions are implicitly assumed).

2. use first order Horn logic; encode the required control information as term arguments, and possibly add some additional clauses for control.

The usual implementation of Definite Clause Grammars (DCGs) [30] in Prolog systems is an example of the second. In this well-known encoding an n-place nonterminal is realized as an n+2-place predicate with the two additional arguments bearing the start and end string position of actual instances of that nonterminal in a parse tree. Now, even if we adapt the first solution, we quickly discover that the usual linguistic practice requires a first-order language to express more fine-grained constraints than just the simple linear logic resource restriction. We obviously need a general mechanism for Horn clauses with restrictions. If the restrictions are also expressed in a logical language, then we have a case of interaction (fibring) of two logics, the main logic and the restriction logic. Applied to our particular needs (of ‘grammar logic’) we must show how two logics, a logic of (string) concatenation and a logic of feature descriptions can be combined on the proof-theoretic level and on the semantic level.

Before we come to the principal theme of the paper — a general combination scheme of this sort —, let us give some more motivation on the actual logics we have chosen to illustrate the scheme with. The choice of these logics is not as arbitrary as it may seem in the first place, because these may be seen as paradigmatic exemplars of the classes of main logic, respectively restriction logic, which we admit in our scheme.

1.1 More linguistic motivation

Subsequently, the Lambek calculus will serve as our paradigmatic grammar logic. It is put into linguistic use by the definition of a lexicon which maps strings of natural language words on sets of syntactic types. Compared to phrase structure grammars, where syntactic types are atomic symbols (‘nonterminals’), the syntactic types in a categorial grammar may be complex formulas which contain connectives for ‘left’ and ‘right’ implication → and ←. (In Lambek’s original notation, the symbols / and \ are used instead). Parsing a sentence means to find a proof for a goal (the start symbol of the grammar) from a database consisting of a syntactic type for each word (chosen from its lexical assignment) in the input string. The Lambek categorial grammars, which use the Lambek calculus as their inference system, are weakly equivalent to the contextfree grammars [24]. They generate the same set of strings but a different set of derivation trees. A derivation in a contextfree grammar (phrase structure grammar) does not include conditionalization (implication introduction) or hypothetical reasoning. From a linguistic point of view, hypothetical reasoning is well suited to model so-called movement phenomena where subphrases have been “moved” away from their basic position to some “landing site”. This is modeled in the Lambek calculus by providing the landing site with a syntactic type which is complex enough to cause the introduction of a hypothesis, i.e. to cause the use of a conditionalization rule, see e.g. the type of the word whom in example (4). As an hypothesis which is discharged later in the proof this [np]_{1} corresponds to a gap, i.e. an empty string, in the initial input sentence.

   \begin{matrix}John \\ np \end{matrix}

\begin{matrix}whom \\ (np → np) ← (s ← np) \end{matrix}

\begin{matrix}Mary \\ np \end{matrix}  \begin{matrix}\begin{matrix}likes \\ (np → s) ← np \end{matrix} & \begin{matrix}ϵ \\ [np] & 1 \end{matrix} \\ np → s \end{matrix}
s
|
s ← np_{1}
np → np
np

                                                                     \begin{matrix}slept \\ np → s \end{matrix}

s

(4)

We have already pointed out that many desirable linguistic generalizations like e.g. agreement constraints can only be expressed (in a reasonable manner) in a first-order version of a grammar logic. From a practical point of view, in order to get this first-order version, we could simply follow basically the way that leads from context-free grammars to DCGs and which is expressed in the following two statements:

1. Replace each basic category b by a one-place predicate b(t), where t is some first-order term.

2. Use unification in proof rules for matching of categories.

A generalization like this is also inspired by a Horn logic program^{1} which encodes^{2} the Lambek proof system, like the one in Fig. 1. Note that in this formulation basic categories need not

        reduce([A],A).
        reduce(String,A) :-
            append(L,R,String),
            reduce(R,B-->A),
            reduce(L,B).
        reduce(String,B-->A) :-
            reduce([B|String],A).

                                            reduce(String,A) :-
                                                append(L,R,String),
                                                reduce(L,A<--B),
                                                reduce(R,B).
                                            reduce(String,A<--B) :-
                                                append(String,B,S1),
                                                reduce(S1,A).

Figure 1: Horn logic program realising Lambek proofs

be atomic. Arbitrary logic terms as basic categories are perfectly meaningful. For instance, we could allow a goal

                  reduce( [np(X,3rd), np(sg,3rd)-->s], s ) ?

which would yield the solution X=sg. Allowing arbitrary terms as “basic categories” results in a hierarchical fine-structuring of these categories. It is attractive to think of b(t) as the set of strings of type b which also have the property t, where more specific terms denote more specific properties. However, the point of having first-order terms is not only having such systematic relations between categories, but rather to really make use of non-ground terms to express underspecification. The example above of such a category, np(X,3rd), would for instance be appropriate for the noun phrase “the fish” which is unspecified for number. Now, instead of adding first-order terms, we will follow an approach which could be dubbed as “mainstream” in computational linguistics and employ feature structures as data structures for linguistic modelling and feature terms for their description. Hence, we will consider Lambek logic extended by feature terms and propose model-theoretic semantics for this language based on fibred structures. Actually it will turn out that the most direct interpretation of the combined language results in a logic for which the proof system sketched above — Lambek calculus augmented with unification — is not appropriate. However, if we reinterpret the (embedded) feature terms as global feature constraints while maintaining the same kind of fibred structures we get a logic for which this proof system is sound and complete. It should be noted that the formalism we are aiming at is just a straightforward extension (by Lambek’s conditionalization rules) of the formalism of unification-based categorial grammars over feature structures which has been proposed independently by [33] and [37] and which has been employed quite successfully in a number of implementations. So, even in the context of categorial grammar the idea of generalizing basic categories to feature terms and employing unification for matching them is not at all new. What is new here is that we regard this as a combination of two logics and investigate it from a model-theoretic point of view. We thus provide also a direct model-theoretic semantics for this latter formalism, which has up-to-now only been defined as an encoding in PATR-II. Employing feature terms is so popular because of their well-known virtues with regard to linguistic engineering: they allow for partial descriptions and for the access to subterms via explicit path names (versus access by argument positions in traditional first order terms). However, this additional flexibility has to be paid for by certain complications when it comes to the rigorous definition of combined semantics for the extended logic, as it will become clear later in this paper. We will show that when using the fibred-semantics approach the formal notions needed to get the semantics of this extended logic right come naturally. A typical example for the application of feature terms is the encoding of the requirement that verbs have to agree with their subject noun phrases with respect to the number and person features. In the following user-friendly notation for the fibred formulas, feature terms come as the (single) arguments of syntactic types. For instance, the type of third person singular verb forms, in which we want to express an agreement restriction for the respective subject, can simply be written as:

1We use standard Edinburgh Prolog notation for list structures, i.e., [X|Y] is syntactic sugar for the list-forming binary functor X.Y, [] is the empty list symbol, and [X_{1},X_{2},...,X_{n}] abbreviates [X_{1}|[X_{2}|...[X_{n}|[]]...]]. The predicate append(Front,Back,Whole) is true if Whole is the list concatenation of Front with Back.

2This should be taken as an abstract logic program in the sense that its logical semantics captures the problem correctly (and completely). However, to make sense out of it procedurally one would need to add (logically redundant) conditions to guide the search.

( np ( \begin{matrix}number: & sg \\ person : & 3rd \end{matrix} ) → s ) ← np  (5)

Note that, although the features number and person introduce a subclassification of all nps, we need not mention them for the second np type here, where any combination of their values shall be allowed. In a purely propositional framework we would have to explicitly state all these combinations and hereby introduce irrelevant ambiguity. In the same way, the realizations of the np-complements of the verb can to be restricted concerning their case information:

( np ( \begin{matrix}number: & sg \\ person : & 3rd \\ case : & subject \end{matrix} ) → s ) ← np ( case: object )  (6)

If, in addition, relative pronouns like whom provide case information to the hypotheses they trigger — the missing element of the relative clause must be an object —, inappropriate uses of the inflected forms of relative pronouns can be excluded.

( np ( \begin{matrix}number: & N \\ person : & P \\ case : & C \end{matrix} ) → np ( \begin{matrix}number: & N \\ person : & P \\ case : & C \end{matrix} ) ) ← ( s ← np ( case: object ) ) (7)

Observe that the resulting np inherits number, person, and case information from the modified np. This again would cause a multiplication in the category assignment in a propositional framework.

1.2 The idea of fibred logics

Let us now state the basic idea of fibring two logics in general. Let L_{1} and L_{2} be two languages or logics. We assume the following:

1. L_{1} and L_{2} are syntactically built up from ‘atomic units’.

2. Each L_{i} identifies a sublanguage of ‘manipulated units’ which are built up from the atomic units. The manipulated units of each language are compatible to being regarded as atomic units of the other language. This can be done in two ways

• the units of L_{1} are atoms of L_{2}, and vice versa (’embedded fibring’)

• the units of L_{1} are atoms of L_{2} but the embedding of units of L_{2} into those of L_{1} is prohibited (’simple fibring’)

Example 1. If L_{1}, L_{2} are two logics, the atomic units are the atomic formulas and the manipulated units are the formulas of the language. Of course, any formula A(x) of one language can be regarded as atomic formula α_{A}(x) of the other language.

Definition 1.

1. L_{1}, L_{2} are fibred as L if the atoms of L are the union of atoms of L_{1} and L_{2} and the connectives of L is the union of the connectives of L_{1} and L_{2} and the expressions of L are built according to the union of the formation rules of L_{1} and L_{2} for the respective connectives plus the rules which describe the combined formulas.

2. The set of proof rules of L is the union of the proof rules of L_{1} and L_{2}. When fibring two systems, interaction axioms (or rules) in the mixed language may be added.

Example 2. Take two K4 modalities □_{G} and □_{H}. Axioms for modality:

1. Gentzen rules for classical logic

2. □A ▷ □□A

3. \begin{aligned}& A_{i} ▷ B \\ (□) \\ & □A_{i} ▷ □B \end{aligned}

Fibring: Put □_{G}, □_{H} together in one language and add each of the above rules for □_{G} and for □_{H}. To turn □_{G}, □_{H} into a temporal logic, we need interaction axioms:

1. A ▷ □_{G}◇_{H}A

2. A ▷ □_{H}◇_{G}A

P is ∼ □_{H} ∼ (i.e. ◇_{H}) and F is ∼ □_{G} ∼ (i.e. ◇_{G}).

1.3 Related work

What comes closest to our approach of combining a grammar logic and feature logic is the work by Blackburn/Gardent/Meyer-Viol 1993 [6]. They present a semantics for a general description language for (syntactic derivation) trees and fibre it with a semantics of feature structures. They do not relate it to a proof theory, as we will do here. Other work which is known to us describes grammar formalisms as homogenous systems. Pereira/Shieber 1984 [29] present a Hoare powerdomain construction for string/featuredescription pairs. Smolka 1992 [32] gives a rigourously formal description of the feature logic part of feature-based grammars, but no (formal) details concerning the connection between the reasoning on strings, i.e. the phrase structure rules, and the feature logic. Höhfeld/Smolka 1988 [18] define the combination of Horn Logic and constraint languages, which could be used as a mold to accommodate a feature-based grammar logic. However the grammar logic itself would have to be expressed by Horn formula which are annotated with certain control information in order to implement the required resource restrictions. Due to this ‘internal encoding’ of a grammar logic in the more general Horn logic, on the one hand, implementations of theorem proving methods are immediately available, while on the other hand, these methods are not optimized with respect to the specific requirements of grammar logics. Vijay-Shanker 1992 [35] extends feature logic by constraints on well-formed tree structures in order to encode feature-based Tree Adjoining Grammars (FTAG’s). He defines a fixpoint semantics for the whole system.

1.4 Outline of the paper

In this paper, we will examine the idea of ‘simple fibring’ in order to extend a grammar logic by a logic of feature terms. As a basis, the main concepts of the Lambek logic (the grammar logic) and of the logic of feature terms will be introduced in the Sections 2 and 3 respectively. Since we assume that most of our readers won’t be familiar with both of the logics, we explain them in quite some detail. In Section 4 we take a little detour and first lay out a formal semantics of the types of Lambek’s calculus augmented by first-order terms, which will serve as a contrast later on. Section 5 contains the main part of the paper. We define the notion of a fibred structure for the two logics and investigate two modes of their combination: direct interpretation of embedded feature terms vs. interpretation of feature terms as global constraints. The first of these is motivated by a direct application of the paradigm of fibred logics, while the second has the unification-based proof theory laid out before. For the latter we show soundness and completeness of this proof theory and consider its computational complexity. In Section 6 we close with a discussion.

2 A concatenation logic

In this section, we give a rather detailed description of the productfree subsystem^{3} of the (bidirectional) Lambek calculus [26], which serves as the basis for the combination of a concatenation logic and feature logic. The Lambek calculus is an intuitionistic, non-commutative variant of Linear Logic. Since directionality counts, there are two kinds of implications B ← C and C → B with the corresponding subcases of Modus Ponens in order to check for right- resp. left-adjacency of the proposition which matches the antecedent C.

3The transformation of categorial grammars based on the full Lambek calculus with the product operator into those based on the productfree Lambek calculus has been defined in [24].

2.1 Syntax

Definition 2. Formula (“syntactic type”). Given a finite set B of constant symbols b_{1}, b_{2}, …, the set of syntactic types A, B, C, … is given by

1. A ⟶ b  (basic type)
2.  | C → B (leftward type)
3.  | B ← C (rightward type)

2.2 Semantics

Definition 3. (String) structure S. A (string) structure S is a pair (S, ·^{S}) with a non-empty domain S of atomic elements (“words”), and an interpretation function ·^{S} which assigns to each basic syntactic type b a non-empty set b^{S} ⊆ S^{+}. S^{+} is the set of all non-empty strings (concatenations) τ built from the domain S. Juxtaposition of two strings τ_{j} and τ_{i} means concatenation. The interpretation function has to guarantee the associativity of the concatenation operation:

∀τ_{1}, τ_{2}, τ_{3} (τ_{1} τ_{2}) τ_{3} ∈ b^{S} iff τ_{1} (τ_{2} τ_{3}) ∈ b^{S}  (8)

Definition 4. Denotation of syntactic types.

1. [[b]]^{S} = b^{S}

2. [[C → B]]^{S} = { τ_{i} | ∀τ_{j} ∈ [[C]]^{S} τ_{j} τ_{i} ∈ [[B]]^{S} }

3. [[B ← C]]^{S} = { τ_{i} | ∀τ_{j} ∈ [[C]]^{S} τ_{i} τ_{j} ∈ [[B]]^{S} }

A type A holds at a string τ (τ ⊧ A) in a structure S iff τ ∈ [[A]]^{S}. Note that with this denotation types are always “satisfiable”, meaning that they have nonempty denotations in at least one structure.

2.3 Proof theory

2.3.1 A labeled deductive system

Since the Lambek calculus is a ‘resource-minded’ logic, the traditional notation of natural deduction rules is not quite adequate:

\begin{aligned}& B & B → A \\ (→E) \\ & & A \end{aligned}  (9)

In order to take care of the proper use of resources (i.e. of the data base) from which a formula is to be deduced, the formula has to carry along some representation of its resources. This can either be done by labeling the formula A with the corresponding sequence of database formulas U, i.e. by creating a declarative unit or a sequent

U ▷ A  (10)

or by using a two-dimensional notation

\begin{matrix}U \\ A \end{matrix}  (11)

The dashed triangle^{4} represents the proof task of deriving a goal A from a database U. A proof is a fully accomplished proof task, i.e. a proof task which does not contain any empty triangles. In the following we use the notions of declarative unit, sequent or proof task in an interchangeable manner.

Definition 5. The productfree subsystem L of the Lambek calculus. (U_{1} U_{2} means concatenation of U_{1} and U_{2}; U_{1}, U_{2} and U must not be empty)

\begin{matrix}(ax) & A ▷ A \\ \begin{aligned}& U_{1} ▷ B & U_{2} ▷ (B → A) \\ (→E) \\ & & (U_{1} U_{2}) ▷ A \end{aligned} & \begin{aligned}& U_{2} ▷ (A ← B) & U_{1} ▷ B \\ (←E) \\ & (U_{2} U_{1}) ▷ A \end{aligned} \\ \begin{aligned}& (B U) ▷ A \\ (→I) \\ & U ▷ (B → A) \end{aligned} & \begin{aligned}& (U B) ▷ A \\ (←I) \\ & U ▷ (A ← B) \end{aligned} \end{matrix}

Fig. 2 visualizes the Lambek calculus in the two-dimensional representation. For a backward chaining application of the inference rules, the initial proof task, i.e. a database and a goal have to be matched on the configuration which is defined by the outermost dashed lines (the conclusion). The required subproofs are given by the inner, empty dashed triangles (the premises). The natural deduction skeleton of a derivation in the above system has been shown in (4) in section 1. Derivability of a sequent U ▷ b is defined as usual and written as ⊢_{L} U ▷ b.

2.3.2 Soundness and Completeness

Various completeness results for the Lambek calculus and its variants have been reported in the literature, see e.g. Buszkowski 1982 [8], Došen 1985 [14], Buszkowski 1986 [9], Došen 1990 [15], Versmissen 1993 [34]. In order to sketch a soundness and completeness argument for the Lambek calculus, first, we have to extend the semantic notions to declarative units.

Definition 6. The denotation of a sequence U_{1}U_{2} is the cross-product of the denotations of the subsequences U_{1} and U_{2}:

[[U_{1} U_{2}]]^{S} = { τ_{1}τ_{2} | τ_{1} ∈ [[U_{1}]]^{S}, τ_{2} ∈ [[U_{2}]]^{S} }

A declarative unit U ▷ A is valid (⊧ U ▷ A) iff for all structures (S, ·^{S}) [[U]]^{S} ⊆ [[A]]^{S}.

Proposition 1. Soundness. If ⊢_{L} U ▷ A then ⊧ U ▷ A.

4In Yetter, 1990 [36] circles are used to mark subproofs in a (classical) linear logic. For intuitionistic logics, circles can be replaced by triangles, in order to distinguish the database formulas, i.e. the base of the triangle, from the goal formula, its top.

\begin{aligned}& \begin{matrix}A \\ | \\ A \end{matrix} & (ax) \\ \begin{aligned}\begin{matrix}U_{1} \\ B \end{matrix} & & \begin{matrix}U_{2} \\ B → A \end{matrix} \\ & A \end{aligned}  (→E) & & \begin{aligned}\begin{matrix}U_{2} \\ A ← B \end{matrix} & & \begin{matrix}U_{1} \\ B \end{matrix} \\ & A \end{aligned}  (←E) \\ \begin{matrix}U \\ [B]  U \\ A \\ | \\ B → A \end{matrix}  (→I) & & \begin{matrix}U \\ U  [B] \\ A \\ | \\ A ← B \end{matrix} (←I) \end{aligned}

Figure 2: Two-dimensional representation of the Lambek calculus (outermost dashed lines are omitted from the rules (→E) and (←E))

Proof. Soundness can be shown by straightforward induction on the size of the proofs. An axiom A ▷ A is valid trivially since [[A]]^{S} ⊆ [[A]]^{S}. By applying the definition of [[B → A]]^{S}, one can show the validity of the nontrivial inference rules like (→E). E.g. if the declarative units U_{2} ▷ (B → A) and U_{1} ▷ B are valid then (U_{1} U_{2}) ▷ A is valid. □

In order to show completeness, we introduce a notion of canonical structure for the Lambek calculus.

Definition 7. Canonical structure (S_{0}, ·^{S_{0}}) for the Lambek logic. [8], [16]

domain S_{0}: the set of syntactic types

interpretation function ·^{S_{0}}: b^{S_{0}} = { U | ⊢_{L} U ▷ b }, b ∈ B

Lemma 1. A_{1} … A_{n} ∈ [[A]]^{S_{0}} iff ⊢_{L} A_{1} … A_{n} ▷ A

Proof. Induction on the complexity of A.

1. A ∈ B.

The hypothesis holds by definition.

2. A = (B → A) ∉ B.

(a) Assume A_{1} … A_{n} ∈ [[B → A]]^{S_{0}} By the induction hypothesis, it holds that B ∈ [[B]]^{S_{0}}. Then BA_{1} … A_{n} ∈ [[A]]^{S_{0}} by the definition of [[B → A]]^{S_{0}}. By the induction hypothesis ⊢_{L} BA_{1} … A_{n} ▷ A. But then also ⊢_{L} A_{1} … A_{n} ▷ (B → A) by rule (→I).

(b) Assume ⊢_{L} A_{1} … A_{n} ▷ (B → A).

In order to show that A_{1} … A_{n} ∈ [[B → A]]^{S_{0}}, assume some sequence of syntactic types A_{21} … A_{2m} ∈ S_{0}^{+}, such that A_{21} … A_{2m} ∈ [[B]]^{S_{0}}. From the induction hypothesis, we get ⊢_{L} A_{21} … A_{2m}▷B. By applying the rule (→E) to this and the assumption, we conclude ⊢_{L} A_{21} … A_{2m}A_{1} … A_{n} ▷ A. Again, from the induction hypothesis, A_{21} … A_{2m}A_{1} … A_{n} ∈ [[A]]^{S_{0}}. Hence, A_{1} … A_{n} ∈ [[B → A]]^{S_{0}}.

□

Theorem 1. Completeness. (Buszkowski [8]) If ⊧ U ▷ A then ⊢_{L} U ▷ A .

Proof. A non-derivable declarative unit is not valid in the canonical structure (S_{0}, ·^{S_{0}}). Hence, we get a contradiction to the assumption that there are valid declarative units which are not derivable. □

The fact that the associativity of the concatenation operation is obtained on the deduction side, as well, has been demonstrated by Buszkowski [10] independently from the completeness proof, on the basis of the Hilbert-style characterization of the Lambek calculus (see Appendix A). This means that for any given bracketing of the database sequence, a proof is available.

3 Feature Logic

The object of concern in feature logics are feature structures. Generally we assume two disjoint alphabets F and P, the sets of feature symbols and sort symbols, respectively.

Definition 8. Feature structure. A feature structure A is a triple of the form (D^{A}, {f^{A} | f ∈ F}, {p^{A} | p ∈ P}) where

• D^{A} is some nonempty set,

• for each f ∈ F, f^{A} is a partial function on D^{A}, and

• for each p ∈ P, p^{A} is a subset of D^{A}.

Hence, a feature structure is a simple relational structure consisting just of binary and unary relations, where the binary relations are partial functional. To put it another way a feature structure is a graph whose edges are labeled with features and whose nodes carry (sets of) sort symbols and which is deterministic, i.e., two edges leaving the same node have to have different labels due to the partial functionality of features. Notice that this definition generalises most notions of feature structures found in the literature including the finite automata structures of [22]. More traditionally feature structures had to obey restrictions like connectedness, rootedness, finiteness, and sometimes acyclicity. We do not impose these restrictions. However, we do consider restrictions which in the more traditional settings are imposed on sorts, namely that they correspond to unique ‘atomic structures’ which are mutually disjoint. For the discussion of these atomic structures it is convenient to assume a subset P_{sg} of P of so-called singleton sorts such that whenever p, q ∈ P_{sg}, f ∈ F then

1. card(p^{A}) ≤ 1 (singletons are true in at most one element),

2. p^{A} ∩ q^{A} = ∅ (singletons are disjoint), and

3. (p^{A} × D^{A}) ∩ f^{A} = ∅ (singletons are atomic).

The third line simply says that no feature is defined on an element of a singleton sort. Two different kinds of standard logical languages come naturally for the description of feature structures. Firstly, since feature structures are completely ordinary Tarskian structures, i.e., the ordinary interpretations of first-order logic, it is straightforward to use first-order logic over a signature containing the binary predicates F and the unary predicates P, maybe extended by some abbreviating notation specially suited for feature structures. Languages of this kind we will call feature constraint languages and prominent representatives of this class are the languages of f-descriptions of lfg [21] and path equations of patr[31]. On the other hand, the framework of modal logic offers a rather different, often much more concise way of talking about structures which contain some distinguished graph substructure. An important advantage here is that most of what we want to say about feature structures can be expressed in a modal propositional fragment. Here features are used as modal operators, i.e., sentential operators, and sorts are propositional variables. We call this type of languages feature term languages.

There are also well-known languages of this kind. Thus, for example, the logic of Kasper and Rounds [22] is just a modal logic of this style, as is the language of FUG [23]. Also the language of attribute-value matrices can be counted into this class. A ‘formula’ (a matrix) can be embedded into another one as the argument of a feature (attribute). We will come to this second kind of feature logic in Section 3.3 where also the systematic relation between both kinds is explained. Our presentation of feature logic draws upon the work of Gert Smolka [32]. An introduction to feature logics should, however, not leave unmentioned the enlightening papers on the modal logic perspective on feature logics by Blackburn [5, 4] and Blackburn and Spaan [7], which undoubtedly have left their impression on our understanding of these logics. Notation. We will use throughout f, f_{1}, … to denote features, letters p and q to denote sorts, and letters a and b to denote singleton sorts. Moreover, letters u, v will always denote sequences of features, also called paths. For a path u = f_{1} … f_{n}, we write u^{A} for the composition of the binary relations f_{1}^{A} … f_{n}^{A}. Note that this is also a unary partial function. For the empty path ϵ, we let ϵ^{A} denote the identity on D^{A}.

3.1 Feature Constraint Logic

We are now going to define the feature constraint logic FC. The language of FC is that of function-free first-order logic with equality over the binary predicate symbols F, the unary predicate symbols P, and an infinite set of variables V (x, y, z shall throughout denote variables). Hence, atomic formulas are of the forms x f y, p(x), and x ≐ y. We take the connectives ¬ and ∧, as well as the quantifier ∃ to be primitive and all others to be defined.^{5} The formulas of FC are interpreted as usual for classical logic. The satisfaction relation ⊧_{FC} is given in Fig. 3. This relation determines under which assignment of variables g : V ↦ D^{A} a feature structure A is a model of a formula ϕ. We write (A, g) ⊧_{FC} ϕ, if the pair (A, g) satisfies the formula ϕ. If that is the case we also call g a solution to ϕ in A. The set of all solutions of ϕ in a given A is denoted as ϕ^{A} (= {g | (A, g) ⊧_{FC} ϕ}). The notation g[x ← d] stands for the variable assignment which is identical to g with the exception of x being mapped to d instead of g(x).

(A, g) ⊧_{FC} x ≐ y iff g(x) = g(y);
(A, g) ⊧_{FC} x f y iff g(x) f^{A} g(y);
(A, g) ⊧_{FC} p(x) iff g(x) ∈ p^{A};
(A, g) ⊧_{FC} ϕ ∧ ψ iff (A, g) ⊧_{FC} ϕ and (A, g) ⊧_{FC} ψ;
(A, g) ⊧_{FC} ¬ϕ  iff (A, g) |̸=_{FC} ϕ;
(A, g) ⊧_{FC} ∃x(ϕ) iff ∃d ∈ D^{A} : (A, g[x ← d]) ⊧_{FC} ϕ.

Figure 3: Satisfaction relation for formulas of FC

Fig. 4 shows how the rest of the usual propositional connectives as well as some additional syntax for expressing path constraints, undefinedness, inequations and the propositional constant ⊥ (false) are defined.

5Note however, that under the classical interpretation that we assume this choice is arbitrary and has no implications.

ϕ → ψ :⇔ ¬(ϕ ∧ ¬ψ)
ϕ ↔ ψ :⇔ (ϕ → ψ) ∧ (ψ → ϕ)
ϕ ∨ ψ :⇔ ¬ϕ → ψ
∀x(ϕ) :⇔ ¬∃x(¬ϕ)
x f u y :⇔ ∃z(x f z ∧ z u y), where z ∉ {x, y}
x f ↑ :⇔ ¬∃y(x f y)
x f u ↑ :⇔ ∃z(x f z ∧ z u ↑), where z ≠ x
x ≐ y̸ :⇔ ¬(x ≐ y)
⊥ :⇔ ¬(x ≐ x)

Figure 4: Formulas, defined as abbreviations

The semantic notions of satisfaction, satisfiability, validity, logical consequence, equivalence, and so on, are defined as usual. Actually, we will regard the first-order logic FC as a lingua franca for talking about feature structures, which is especially handy to use in the proofs to come. However, for the description of grammars, i.e., in our application, only a limited, decidable fragment is made use of, as will become clear below.

3.2 EPF Constraints and Satisfiability

We will restrict our attention to formulas in so-called existential prenex form (EPF) which have the nice property that their satisfiability problem is decidable [32]. Actually, from the point of view of computational complexity this fragment is, since it is NP-complete, not worse than propositional logic.

Definition 9. EPF constraints. A formula ∃x_{1} … x_{n}(ϕ) is called a constraint in existential prenex form iff ϕ contains quantifiers only in the forms x u y and x u ↑.

Definition 10. Primitive constraint. A formula is called a primitive constraint if it is of one of the forms:

x ≐ y, x ≐ y̸, p(x), ¬p(x), x f y, x f ↑

Definition 11. Feature clause. A feature clause is a set of primitive constraints representing their conjunction.

Proposition 2. Smolka. For every EPF constraint ∃x_{1} … x_{n}(ϕ) there exists an equivalent formula of the form ∃y_{1} … y_{m}(ψ), where ψ is a disjunction of feature clauses.

Note that, even if the input constraint does not contain an explicit existential quantifier we may need existentials for auxiliary variables when decomposing the constraint.

3.2.1 Determining satisfiability

We are now going to describe an algorithm that checks satisfiability of feature clauses in more detail. Actually, this algorithm will be sufficient for dealing with feature constraints in the proof systems for the combined logics below. This is so, since we can assume that ‘input’ constraints come always in form of feature clauses and all that is required in the proofs is to check the satisfiability of conjunctions of such input constraints, hence unions of feature clauses. We do not describe here how to transform arbitrary EPF constraints into an equisatisfiable disjunction of feature clauses. This is rather straightforward and can be found elsewhere [32, 12]. The algorithm works by carrying out equivalence transformations which turn a feature clause into solved form (defined below) or the unsatisfiable formula ⊥. The procedure essentially does what is known from feature-graph based implementations as the feature-graph unification procedure. Our presentation of it is derived from the one given in [32]. We give first the conditions for solved feature clauses in Fig. 5.

A feature clause C is called solved iff it satisfies the following conditions.

(C1) If x ≐ y is in C, then x occurs exactly once in C.

(C2) If x f y and x f z are in C, then y = z.

(C3) If a(x) and b(x) are in C, then b ≠ a.

(C4) If a(x) is in C, then C does not contain a constraint x f y.

(C5) If x f ↑ is in C, then C does not contain a constraint x f y.

(C6) If x ≐ y̸ is in C, then x ≠ y.

(C7) If a(x) is in C, then C does not contain a constraint a(y).

Figure 5: Solved Form

The equivalences defining the algorithm are presented in Fig. 6 and are, as suggested by the arrow, to be applied from left to right. The notation ϕ & C denotes the feature clause {ϕ} ∪ C and requires ϕ ∉ C. It should be noted that the rules as well as the conditions for solved form are sensitive for orientation of equalities x ≐ y. Constraints x ≐ y and y ≐ x are not exchangeable here. The details of the algorithm are not really essential for this paper. It should just be kept in mind that we have an effective procedure for determining satisfiability of EPF constraints.

3.3 Feature Term Logic

Feature term logics take advantage of the fact that feature structures are (polymodal) Kripke structures, where the feature relations are taken to be accessibility relations between nodes (worlds), which happen to be partial functional, and sorts denote sets of nodes. By assuming a) a sort to be a description for a node of that sort, b) a term f : T to describe a node with an outgoing f-arc leading to a node which matches the description T, and c) by allowing arbitrary

Simplification Rules

(R1)  x ≐ y & C → x ≐ y & [x/y]C,

if x occurs in C and x≠y

(R2)  x ≐ x & C → C
(R3)  x f y & x f z & C → x f y & y ≐ z & C
(R4)  a(x) & a(y) & C → a(x) & y ≐ x & C, if x≠y

Clash Rules

(C1)  a(x) & b(x) & C → ⊥, if a≠b
(C2)  x f y & a(x) & C → ⊥
(C3)  x ≐ x̸ & C → ⊥
(C4)  x f y & x f ↑ & C → ⊥

Figure 6: Equivalence rules for transformation to solved form

boolean combinations with ∧, ∨, and ¬ of such descriptions we obtain a variant of propositional modal logic, where f : T acts like ⋄T over the f-relations. Hence, in feature terms features are used as sentential operators to build larger structures in a very direct and concise way. Compare for instance the following equivalent feature term and feature constraint.^{6}

head : ( \begin{matrix}case  : & ( acc ∨ nom ) \\ agreement: & ( \begin{matrix}pers : & 3 \\ num: & sg \end{matrix} ) \end{matrix} )  \begin{matrix}x head y ∧ \\ (y case acc ∨ y case nom) \\ y agreement z ∧ \\ z pers 3 ∧ \\ z num sg \end{matrix}

Besides features and sorts we also use variables from the set V for graph nodes in order to express reentrancy, i.e., the situation that two paths starting in the current node end in one and the same node x. More precisely, we define the language L_{FT} of the feature term logic FT as follows:^{7}

1. If p ∈ P, then p is a feature term.

2. If x ∈ V, then x is a feature term.

3. If T_{1} and T_{2} are feature terms, then f : T_{1}, T_{1} ∧ T_{2}, and ¬T_{1} are feature terms.

4. Nothing else is a feature term.

The satisfaction relation (A, g, d) ⊧_{FT} T (read: T is true in A under assignment g at node d ∈ D^{A}) is given in Fig. 7. For convenience we also assume a feature term true whose interpretation shall always be fixed to the entire interpretation domain D^{A}. This doesn’t extend the logic, since we may define true as an abbreviation for ¬(x ∧ ¬x).

6We write feature terms in a matrix notation where the lines of a matrix have to be read as an implicit conjunction.

7f : T is sometimes also written ⟨f⟩T reminding of the analogy to the possibility operator ⋄.

(A, g, d) ⊧_{FT} p  iff d ∈ p^{A};
(A, g, d) ⊧_{FT} x  iff d = g(x);
(A, g, d) ⊧_{FT} f : T iff ∃d′ : d f^{A} d′ ∧ (A, g, d′) ⊧_{FT} T;
(A, g, d) ⊧_{FT} T_{1} ∧ T_{2} iff (A, g, d) ⊧_{FT} T_{1} and (A, g, d) ⊧_{FT} T_{2};
(A, g, d) ⊧_{FT} ¬T  iff (A, g, d) |̸=_{FT} T.

Figure 7: Satisfaction relation for formulas of FT

Definition 12. Consequence. Term T′ is a logical consequence of term T (in symbols: T ⊧_{FT} T′) if for all A, g, and d ∈ D^{A} whenever (A, g, d) ⊧_{FT} T then (A, g, d) ⊧_{FT} T′.

Except for the use of variables this is just straightforward propositional polymodal logic. Feature terms denote sets of nodes (worlds) and hence, are ontologically the same as sorts. I.e., we can think of feature terms as complex sort expressions. Note that a variable is true at exactly one node of the structure and thus always denotes a singleton set. In order to make explicit the correspondence between FT and FC formulas we introduce, as new form of feature constraint, the application of an arbitrary feature term to a variable:

(A, g) ⊧_{FC} T (x) iff (A, g, g(x)) ⊧_{FT} T for all T ∈ L_{F T}

To put it differently we allow complex sort expressions in place of simple sorts, now. We immediately get the following equivalences, which show that these additional forms can be eliminated in FC.

y(x) ⇔ x ≐ y
(f : T)(x) ⇔ ∃y(x f y ∧ T (y)) if y does not occur in T
(T_{1} ∧ T_{2})(x) ⇔ T_{1}(x) ∧ T_{2}(x)
(¬T)(x) ⇔ ¬ T (x)

These elimination rules can also be viewed as a translation function from feature terms to feature constraints defining the standard correspondence as in modal correspondence theory.

3.3.1 Feature vs. first-order terms

We have introduced feature terms as logical formulas, but on the other hand they are in some sense comparable to first-order terms. They can be seen as descriptions of term structures and can play the same role as first-order terms play in logic programming, namely provide a general means for structuring data. The line of logic programming languages based on Aït-Kaci’s Psiterms [2, 1] witnesses this fact. From this point of view one likes to see feature terms (or at least the purely conjunctive ones) as generalized first-order terms whose arity is not fixed and in which arguments are accessed by keyword (feature) instead of position. Being descriptions they exhibit an inherent partiality, which has obvious advantages in the modelling of data structures where the data is only partially known. This has turned out to come to meet the needs of linguistic modelling as it is done in unification-based grammar formalisms.

4 Excursion: Lambek Predicate Logic

Although our aim is to formalize a feature-based “Lambek Unification Grammar”, it is instructive to consider first its simpler counterpart with first-order terms. This logic and its intended mode of inference has been compactly described in the introduction with the two instructions:

1. Replace each basic category b by a one-place “predicate” b(t), where t is some first-order term.

2. Use unification in proof rules for matching of categories.

To provide a model-theoretic semantics for this extended language is a simple logic exercise. We just assume an interpretation domain D which includes the set of all strings S^{+} built from a string domain S. The interpretation function ·^{D} maps function symbols to functions over D and basic types to two-place relations from S^{+} × D. Note that under a variable assignment g : V ↦ D (which we identify, as usual, with its homomorphic extension to terms) each term t denotes a unique object [[t]]_{g} = g(t)^{D}. As denotations of types under assignment g we can now simply take

1. [[b(t)]]_{g} = { τ | (τ, [[t]]_{g}) ∈ b^{D} }

2. [[C → B]]_{g} = { τ_{i} | ∀τ_{j} ∈ [[C]]_{g} τ_{j} τ_{i} ∈ [[B]]_{g} }

3. [[B ← C]]_{g} = { τ_{i} | ∀τ_{j} ∈ [[C]]_{g} τ_{i} τ_{j} ∈ [[B]]_{g} }

4. [[∀xB]]_{g} = { τ | ∀d ∈ D τ ∈ [[B]]_{g[x←d]} }

5. [[∃xB]]_{g} = { τ | ∃d ∈ D τ ∈ [[B]]_{g[x←d]} }

Here g[x ← d] denotes an assignment identical to g except that it assigns d to x. Notice that the meaning given to quantification over first-order variables is straightforward. For this logic we just want to point out that the unification-based proof system sketched before relates to it in just the same way as Robinson’s resolution scheme relates to Predicate Logic. As is well-known, the purpose of unifications in those systems is

1. to circumvent the guessing of instantiations of variables

2. to calculate variable substitutions which make a given goal a logical consequence of a given database (ordinarily of facts and rules)

In our case we let the goal be a whole (quantifier-free) sequent U ▷A and the database be empty, i.e., we want our proof system to determine exactly those substitutions σ for which ⊧_{L} (U ▷A)σ holds. So, what we in fact prove, when abstracting away from the resulting substitutions, is the “existential closure” of U ▷ A which can be defined as the declarative unit with the universal closure of the types of U to the left and the existential closure of A to the right.

5 The Combination

When combining Lambek and Feature Logic syntactically there are different options upon which we have to decide.

Combination by replacement vs. combination by augmentation

As the headline of the paragraph already indicates we may either replace basic types of the grammar logic completely by feature terms or let a basic type b carry a feature term T as annotation, written b(T). Clearly, feature terms are better suited here than would be feature constraints, since they are, like the basic types, modal propositions, i.e., denote sets of ‘worlds’. Thus, semantically we let in the first case the denotation of basic types be just the denotation of the feature terms that they are. But also, in the second combination mode, we can assume b(T) to denote elements of type b which also have the property T in some sense we will make precise later. Now, an argument for the replacement version to be preferable is that it results in a simpler logic. However, it is also less flexible. The grammar logic has lost the possibility to distinguish basic types and has to rely for that purpose completely on the feature logic. Computationally this can be a disadvantage, since specialized fast inference methods for the grammar logic may only carry a significant share of the whole task, if the type information on this side is discriminating enough. This is the first reason why we consider the augmentation option in the sequel. A second reason lies in the fact that the combined logic resulting from the replacement of atoms can be seen as a special case of the augmented logic, namely the one where only a single basic type is used. Hence, the points we make below for the augmented version bear for both modes of combination.

Embedded terms vs. global constraints

Since our considerations have been inspired by the analogy of a feature-based Lambek logic to one which is based on first-order terms, we will first look at the combined logic where the embedded feature terms are interpreted ordinarily as embedded formulas. It will, however, turn out that under this interpretation the syntactic analogy does not carry over to the logical consequence relation, thus preventing a proof system of the kind “Lambek calculus plus unification” to be appropriate here. We therefore propose another combination scheme in which the feature formulas are viewed as global constraints. We consider both approaches in turn below after having introduced the notion of fibred structure, which is common to both.

Definition 13. Fibred structure. A fibred structure for the feature-based Lambek logic is a quadruple M = (S, A, g, {F_{b}}_{b∈B}) consisting of a string structure S, a feature structure A, a variable assignment function g : V ↦ D^{A}, and a family of fibring relations F_{b} ⊆ b^{S} × D^{A}, b ∈ B, such that whenever τ ∈ b^{S} then for some d ∈ D^{A}, (τ, d) ∈ F_{b} (i.e., F_{b} is left-total in b^{S} × D^{A}).

Our linkage of the two parts of the combined structures using a family of fibring relations may look a bit complicated. It is really needed if we want to let feature-added basic types behave like refinements of the propositional basic types also for polymorphic strings. In contrast to a linkage with just one fibring relation this construction allows us to have a polymorphic string τ, which, for instance, is in b_{1}^{S} as well as in b_{2}^{S}, to satisfy b_{1}(T) without the implication that it also has to satisfy b_{2}(T). In the replacement version of the logic, clearly, the family reduces to one single left-total fibring relation. Note also that the sets b^{S} of the string structure S are really redundant in the combined models. They are just the first components of the respective fibring relations. They are retained for the sake of modularity of fibred models.

5.1 Embedded Terms

5.1.1 Syntax

As motivated above we consider the syntactic combination where each basic type of the Lambek calculus is associated with a feature term. We call the resulting logic L(FT ).

Definition 14. Feature-based syntactic type. Given a finite set B of constant symbols b_{1}, b_{2}, …, and the language L_{F T} of feature terms T, T_{1}, T_{2}, … over the given signature ⟨F, P⟩, as defined above, the set of feature-based syntactic types A, B, C, … of L(FC) is given by

1. A ⟶ b(T)  (feature-based basic type)
2.  | C → B (leftward type)
3.  | B ← C (rightward type)

5.1.2 Semantics

Definition 15. Denotation of feature-based syntactic types. Given a fibred structure M = (S, A, g, {F_{b}}_{b∈B}). The denotations of the feature-based syntactic types in L(FT ) are the following subsets of the string domain.

1. [[b(T)]]^{M} = { τ | ∃d(τF_{b}d ∧ A, g, d ⊧_{FT} T) }

2. [[C → B]]^{M} = { τ_{i} | ∀τ_{j} ∈ [[C]]^{M} τ_{j} τ_{i} ∈ [[B]]^{M} }

3. [[B ← C]]^{M} = { τ_{i} | ∀τ_{j} ∈ [[C]]^{M} τ_{i} τ_{j} ∈ [[B]]^{M} }

4. [[U_{1} U_{2}]]^{M} = { τ_{1}τ_{2} | τ_{1} ∈ [[U_{1}]]^{M}, τ_{2} ∈ [[U_{2}]]^{M} }

A declarative unit U ▷ A is valid (⊧_{L(FT )} U ▷ A) iff for all fibred structures M, [[U]]^{M} ⊆ [[A]]^{M}.

Note that only the clause for basic types, which clearly needed alteration, has been changed. This logic is really a conservative extension to the productfree Lambek calculus, since a featurebased syntactic type in which all contained feature terms are just the term true expresses exactly the same as the “pure” syntactic type where all these (true)-annotations are omitted. According to the definition an extended basic type b(T) denotes all those strings of type b which also stand in relation to an object of the feature model satisfying T. Since the sequent operator ▷ simply represents the subset relation we can state that for the basic feature-added types the denotation is the smaller the more specific its feature term is.

Example 3.

(a) ⊧_{L(FT )} np ( \begin{matrix}num: & sg \\ pers : & 3rd \end{matrix} ) ▷ np ( pers: 3rd )

but

(b) |̸=_{L(FT )} np ( pers: 3rd ) ▷ np ( \begin{matrix}num: & sg \\ pers : & 3rd \end{matrix} )

The following proposition states this fact for the general case.

Proposition 3. If b ∈ B then

⊧_{L(FT )} b(T) ▷ b(T′) iff T ⊧_{FT} T′.

On the other hand, in antecedents of a complex type this relation is the other way round. The following examples show how validity behaves with respect to subsumption of feature terms.

Example 4.

(a) ⊧_{L(FT )} np ( \begin{matrix}num: & sg \\ pers : & 3rd \end{matrix} ) , np ( pers: 3rd ) → s(true) ▷ s(true)

but

(b) |̸=_{L(FT )} np ( pers: 3rd ) , np ( \begin{matrix}num: & sg \\ pers : & 3rd \end{matrix} ) → s(true) ▷ s(true)

Let us take these examples to illustrate that an intuitive meaning of these types is simply that they are partial classifications. To say a string is of type np(pers : 3rd) classifies it as an np which also satisfies pers : 3rd, however, it is left open how it relates to any subclassifications of this type. It may or may not be in a subclass like num : sg. Hence, obviously a string of type np(pers : 3rd) need not be in np(num : sg ∧ pers : 3rd). The same argument also explains the second pair of examples. Now, this proof-theoretical behaviour is unfortunate when we want to make use of underspecification as it is done in unification-based grammars where often one wants to let types be underspecified and let the context determine more and more their precise extensions. In contrast to the first-order version of L (cf. Section 4) a unification-based proof procedure is not adequate here and we will try to explain this now. Notice that in the first-order version we would also not be able to prove a goal corresponding to the one in Example 3b (nor the one in 4b), which would be np(X, 3rd) ▷ np(sg, 3rd), but rather the refinement of that goal with the substitution X = sg. This indicates that we should carefully distinguish between the notion of provability itself and its use in the task of proving a goal. We could, in order to accommodate the view of underspecified types, simply define that task as finding a “global refinement” of the goal that is valid. But then, we would still have to explain how such a task relates to the meaning of the formulas. Unfortunately we cannot rely on substitutions or existential closures like in the first-order case, since refinement on feature terms is not a case of variable instantiation, but is a semantical notion. Another case of interest, where this logic behaves different than the first-order version, is when inconsistent feature terms are involved. As shown in the next proposition there are certain constellations where a Lambek core proof would be bypassed altogether.

Proposition 4. If b ∈ B and T is unsatisfiable then

⊧_{L(FT )} (U_{1} b(T) U_{2}) ▷ A.

Note that the denotation of the antecedent must be empty here. Obviously, such an example is not directly comparable to the version involving first-order terms, since first-order terms cannot be inconsistent. Nevertheless, a proof procedure as the one laid out in the introduction would, if we replace first-order term unification by feature term unification, reject such a goal, since any unification failure would lead to a global failure there. On the other hand, with this example we scratch only the surface of how inconsistent terms have to be dealt with in a proof theory of L(FT ). For instance, we also have to account for the fact that for a functor category [[C → B]]^{M} is empty if [[B]]^{M} is empty and [[C]]^{M} is nonempty, however it denotes the full domain S^{+} if [[C]]^{M} is empty. We now leave the logic L(FT ), for which, admittedly, a lot of questions remain. We do not want to claim though that this logic is uninteresting. Rather we hope to have made clear that it is not accompagnied with a proof theory that is compatible with the unification-based processing of formulas that we aim at.

5.2 Global Constraints

Two circumstances, not completely independent of each other, are responsible for the logical behaviour of the last approach being different as compared to the first-order variant. The first is the fact that feature terms are formulas with propositional content. Embedding these into type formulas makes them sensitive to the place where they appear, e.g., whether they appear in an antecedent or in a consequent. In a way we want only the ‘described terms’ to restrict the type formulas, but not to let the descriptions of the terms be sensitive to the location of their appearance. This could be remedied by an interpretation which views these descriptions as global constraints, such that a type with an embedded feature term … b(T) … would be seen as an abbreviation of something like (… b(x) …) ∧ T (x), where T (x) is the feature constraint which is the application of T to the (new) variable x. The second reason for the mismatch is a more profound one, which has already been touched. When in the first-order variant we are looking for substitutions σ that make a given goal a valid formula in the logic, the notion to be used for feature terms to relate them to more and more specific ones is the notion of logical consequence for feature terms. I.e., we want as solutions for a given goal G those consistent feature constraints ϕ for which it holds that all fibred models M of ϕ are also models of G. Notice that this combines a satisfiability problem for the feature constraint part of G (some model has to exist for those constraints) with a validity problem which essentially involves only the type part of G (the feature constraints which can’t be ‘shown’ can always be ‘assumed’, i.e., get part of a solution constraint, as long as they are consistent). Now, the modularity inherent in our fibred structures makes it conceptually much simpler to define such a mixed satisfiability/validity problem in which we have to refer to parts of the model under universal quantification whereas to other parts under existential quantification. We show below that in our setup of fibred semantics, where a structure is built-up from clearly separated parts which can serve as models in the component logics, it is straightforward to define this enriched notion of consequence, which is required here. We can define it simply as a combination of consequence for the string-structural part and satisfiability for the feature part.

5.2.1 Syntax

Let us call the logical system to be presented now L(FC). Each basic type of the Lambek calculus is associated just by a variable on which feature constraints can then be imposed. Feature constraints are not embedded in syntactic types, but are kept separately on the toplevel of the formulas.

Definition 16. Feature-based syntactic type. A feature-based syntactic type of L(FC) (FeaST for short) has the form ϕ:: A where ϕ is a feature constraint and A is an indexed syntactic type of the form

1. A ⟶ b(x)  (indexed basic type)
2.  | C → B (leftward type)
3.  | B ← C (rightward type)

Note that indexed basic types are a special case of the feature-based syntactic types of L(FT ). The reason for the naming is that we use the variables on the basic types essentially like indices just to distinguish b(x) from b(y) as being different types.

5.2.2 Semantics

The denotation for indexed types is simply a special case of the denotation of the feature-based syntactic types of the previous setup. We take over these definitions simplifying the clause for indexed basic categories to become

1. [[b(x)]]^{M} = { τ | τF_{b}g(x) }

We will interpret feature constraints even in declarative units globally, i.e., insensitive to whether they appear to the left or to the right. For FeaSTs we are not interested in global validity, but rather in a mixture of validity and satisfiability. To ease the presentation we define the projections of units to their constraint and type parts, called the global constraint and type skeleton of the unit as follows.

Definition 17. Global constraint. The global constraint of a declarative unit ϕ_{1} :: A_{1} … ϕ_{n}:: A_{n} ▷ϕ_{0} :: A_{0} is ⋀_{i=0}^{n} ϕ_{i}. We write Φ(U ▷ A) for the global constraint of U ▷ A.

Definition 18. Type skeleton. The type skeleton of a feature-based syntactic type (sequence of those) [declarative unit] is just the indexed syntactic type (sequence of those) [declarative unit] that results when all feature constraints are omitted. We write Π(U ▷ A) for the type skeleton of U ▷ A.

Definition 19. Satisfaction in L(FC). U ▷ A is satisfied in M = (S, A, g, {F_{b}}_{b∈B}) (written M ⊧_{L(FC)} U ▷ A) iff

A, g ⊧_{FC} Φ(U ▷ A) and [[Π(U)]]^{M} ⊆ [[Π(A)]]^{M}).

Indexed basic types are of special interest, since they mediate the communication between the type structure and the feature structure parts. On the one hand they provide the hooks for the feature constraints, but on the other hand they can also be seen simply as (an enlarged set of) basic types. Actually, given a fibred model M we can carve out the parts necessary for the interpretation of indexed types and build a (pure) string structure in which we get the same interpretation for these types when interpreted as pure Lambek types where basic types are now all indexed basic types.

Definition 20. String structure of indexed types. Let M = (S, A, g, {F_{b}}_{b∈B}) be a fibred model with S = (S, ·^{S}). The corresponding string structure of indexed types S′ has domain S and interpretation function ·^{S′} which is defined for basic types BV = {b(x) | b ∈ B, x ∈ V} (the indexed basic types), such that b(x)^{S′} = {τ | τF_{b}g(x)}.

Proposition 5. Let M = (S, A, g, {F_{b}}_{b∈B}) be a fibred model and S′ be the corresponding string structure of the indexed types. Then for all sequences of indexed types U

[[U]]^{S′} = [[U]]^{M}.

Proof. This is shown by a straightforward induction on the structure of types, the only interesting case being the base case: τ ∈ [[b(x)]]^{M} iff τF_{b}g(x) iff τ ∈ [[b(x)]]^{S′}. □

Now, the semantic notion which we are primarily interested in and which embodies the mentioned satisfiability/validity mixture is the notion of a solution constraint. We define the set of solution constraints to a declarative unit as those satisfiable constraints which imply the global constraint and in whose fibred models the type skeleton is valid.

Definition 21. Solution set. The solution set Sol(U ▷ A) of a declarative unit is the set of feature constraints satisfying ϕ ∈ Sol(U ▷ A) iff ϕ is satisfiable and for all M = (S, A, g, {F_{b}}_{b∈B})

A, g ⊧_{FC} ϕ → M ⊧_{L(FC)} U ▷ A

Observe that if U ▷ A has any solutions, then for at least one variant (U ▷ A)σ, in which some of the variables may be identified, the type skeleton π((U ▷ A)σ) is valid in L (over indexed basic types). This implies that the “pure” type skeleton, where even the indices are omitted, is already valid in L (over B), if there are some solutions. We now turn to the question how to derive the solutions for a given sequent. The proof system below answers this question.

5.2.3 Proof Theory

We need some more concepts and notation. We use variable substitutions which substitute variables only with other variables or with constants, since there are no complex (first-order) terms in FC.

Definition 22. Substitution. A variable substitution is a mapping V ↦ V ∪ C which is equal to the identity function except for finitely many variables.

We represent a substitution σ as the set of those pairs (x, σ(x)) for which x ≠ σ(x). The set of first [second] components of these pairs is denoted by Dom(σ) [Ran(σ)]. Application of substitutions is usually written in postfix notation.

Definition 23. Substitution constraint. Let σ = {(x_{1}, y_{1}), …, (x_{n}, y_{n})} be a substitution. The substitution constraint of σ is the feature clause Φ_{σ} = {x_{1}≐y_{1}, …, x_{n}≐y_{n}}.

Idempotent substitutions, i.e. substitutions σ for which σσ = σ, play a special role.

Proposition 6. A substitution σ is idempotent iff Dom(σ) ∩ Ran(σ) = ∅.

Definition 24. Calculus for the feature-based Lambek logic. The inference system of L(FC) consists of the rules of the ordinary Lambek calculus ((→E), (←E), (→I), (←I), and (ax)) where declarative units shall be over indexed types, i.e., symbols with different indices are taken to be different, as well as the following rule:

\begin{aligned}& Π(U ▷ A)σ \\ (link) \\ & U ▷ A \end{aligned}  if Φ(U ▷ A)σ is consistent and Ran(σ) ⊆ V(Π(U ▷ A)).

Here σ is an idempotent variable substitution obeying the indicated restriction. We write ⊢_{L(FC)} U ▷ A if there exists a proof of U ▷ A in L(FC).

The last rule is spelled out more fully as

\begin{aligned}& (A_{1} … A_{n} ▷ A_{0})σ \\ (link) \\ & ϕ_{1} :: A_{1} … ϕ_{n}:: A_{n} ▷ ϕ_{0} :: A_{0} \end{aligned} if (ϕ_{0} ∧ … ∧ ϕ_{n})σ is consistent

and Ran(σ) ⊆ V(A_{1} … A_{n} ▷ A_{0})).

The proofs in this system always consist of a pure Lambek part, a pure FC part (as a side condition) and one application of (link). If applied in a backward-chaining manner the rule (link) requires the guessing of the substitution σ so that the rest of the proof goes through. It is thus comparable to instantiation rules for quantifiers in Gentzen calculi. Note that here we are not generating valid formulas in the ordinary sense of validity, i.e., “holds in all structures”. Instead our proof system constitutes a way of generating solutions. We call the constraint Φ(U ▷ A) ∧ Φ_{σ} the answer constraint of the proof. Note that, if Φ(U ▷ A)σ is consistent for an idempotent σ, so is Φ(U ▷ A) ∧ Φ_{σ}.

Definition 25. Answer set. The answer set Ans(U ▷A) of a declarative unit is the set of answer constraints of proofs of U ▷A, i.e., Ans(U▷A) = {ϕ = Φ(U▷A)∧Φ_{σ} | ϕ consistent, ⊢_{L} Π(U▷A)σ, and Ran(σ) ⊆ V(Π(U▷A))}

Observe that Ans(U ▷A) is a finite set. In formulas we use Ans(U ▷A) to denote the disjunction of its elements.

5.2.4 Soundness and Completeness

We show now that all answers are solutions and that all solutions are subsumed by the set of answers.

Theorem 2. Soundness of answer generation. For any declarative unit U ▷ A:

Ans(U ▷ A) ⊆ Sol(U ▷ A).

Proof. Let ϕ ∈ Ans(U ▷ A). Then ϕ is consistent and there is a σ such that ϕ is of the form Φ(U ▷ A) ∧ Φ_{σ}. Moreover, Π(U ▷ A)σ has a proof in L. But then, due to soundness of FC and L, ϕ is satisfiable and ϕ ⊧_{FC} Φ(U ▷ A) and for all M = (S, A, g, {F_{b}}_{b∈B}),

A, g ⊧_{FC} ϕ → [[Π(U)]]^{M} ⊆ [[Π(A)]]^{M}.

□

In a way the answer set contains a set of generators for the solution set. We get all solution constraints by taking all consistent feature clauses which are at least as constrained (instantiated) as some answer constraint. Before proving completeness we establish the following important property which links the notion of solution constraint to consequence and validity in the combined logics.

Lemma 2. If ϕ ∈ Sol(U ▷ A) then there exists an idempotent substitution σ such that

ϕ ⊧_{FC} Φ(U ▷ A) ∧ Φ_{σ} and ⊧_{L} Π(U ▷ A)σ

Proof. According to the definition of Sol(U ▷A) there exists A_{0} and g_{0} such that A_{0}, g_{0} ⊧_{FC} ϕ. Furthermore, we know from that definition that for all M = (S, A, g, {F_{b}}_{b∈B})

A, g ⊧_{FC} ϕ → (A, g ⊧_{FC} Φ(U ▷ A) ∧ [[Π(U)]]^{M} ⊆ [[Π(A)]]^{M}).

Let E_{ϕ} = {x≐y | x, y ∈ V(Π(U ▷ A)), ϕ ⊧_{FC} x≐y} be the (finite) set of equational constraints over variables from Π(U ▷ A) that are implied by ϕ. W.l.o.g. we assume a total order < on the variables and define the wanted substitution σ as follows:

σ = {(x, y) | x≐y ∈ E_{ϕ} ∧ y<x ∧ ¬∃y′(y′<y ∧ x≐y′ ∈ E_{ϕ})}

Hence, this assigns to each x ∈ V(Π(U ▷ A)) the smallest E_{ϕ}-equivalent y. Note that Dom(σ) ∩ Ran(σ) = ∅, so that σ is idempotent. Now, since we already know from above that ϕ ⊧_{FC} Φ(U ▷ A) and in each model (A, g), g(x) = g(xσ), we also get ϕ ⊧_{FC} Φ(U ▷ A) ∧ Φ_{σ}. In order to show ⊧_{L} Π(U ▷ A)σ, i.e. ∀S([[Π(U)σ]]^{S} ⊆ [[Π(A)σ]]^{S}), assume some string structure S = (S, ·^{S}) over indexed basic types obeying the identifications made by g_{0}, i.e. whenever g_{0}(x) = g_{0}(y) also b(x)^{S} = b(y)^{S} for all b, and let τ_{0} ∈ [[Π(U)σ]]^{S}. From S and A_{0} and g_{0} we construct a fibred model M_{0} = (S_{0}, A_{0}, g_{0}, {F_{b}^{0}}_{b∈B}) with S_{0} being the string structure over basic types (sans indices) having the same string domain as S and the denotation of a basic type b is the union of the denotations of all its indexed versions in S, i.e. b^{S_{0}} = ⋃_{x∈V} b(x)^{S}. The fibring relations are defined as

τF_{b}^{0}d iff ∃x(d = g_{0}(x) ∧ τ ∈ b(x)^{S}.

Hence, S is just the string structure of the indexed types corresponding to M_{0}. Now, observe that for each indexed basic type b(x) occurring in U ▷ A, [[b(x)σ]]^{M_{0}} = [[b(x)]]^{M_{0}}, so that we can extend the inclusion above to [[Π(U)σ]]^{M_{0}} ⊆ [[Π(A)σ]]^{M_{0}}. Finally by Proposition 5, since τ_{0} ∈ [[Π(U)σ]]^{S}, we get τ_{0} ∈ [[Π(U)σ]]^{M_{0}} implying τ_{0} ∈ [[Π(A)σ]]^{M_{0}} and again by Proposition 5, τ_{0} ∈ [[Π(A)σ]]^{S}. □

Theorem 3. Answer-Completeness. If ϕ ∈ Sol(U ▷ A) then ϕ ⊧_{FC} Ans(U ▷ A).

Proof. Let σ be a substitution as in Lemma 2. We can construct directly a proof using the (link) rule and this substitution. From Lemma 2 and completeness of L it follows that there is a proof for Π(U ▷ A)σ using only rules of L. Since also, by completeness of FC, Φ(U ▷ A) ∧ Φ_{σ} is consistent, we can apply (link) completing the L(FC)-proof of U ▷ A. Hence, Φ(U ▷ A) ∧ Φ_{σ} is one of the disjuncts of Ans(U ▷ A), which then must be entailed by ϕ. □

5.2.5 Computational Considerations

Let us first give a comment on the practical implementation of the proof system, before we dive into the theoretical matter of computational complexity. The calculus given is oriented towards simplicity of the proof theory, but not towards computational efficiency of proving given goals.

However, it can easily be converted into a more resolution-like calculus by assuming that the substitution σ is built incrementally during the core Lambek proof. Whenever the rules would require a type b(x) to match a type b(y), we simply set xσ = y and continue the proof under this substitution. Also the consistency checking of feature constraints can be done in parallel, which means that each such identification of two variables essentially triggers a unification of the feature terms that constrain them. Proceeding this way we actually obtain the feature-based analogue of the system that we departed from in the introduction. Turning to complexity issues let us first consider the complexity of L itself. Unfortunately we are not aware of any complexity result for L in the literature.

Theorem 4. Derivability in L is N P-easy.

Proof. We can simply guess a proof and check it in linear time. This is so, because in the usual presentation of the Lambek calculus (see e.g. [26]) proofs are bounded linearly with the goal sequent. □

We do not know of a lower complexity bound, however. Now, let us call the problem of deciding whether a given declarative unit U ▷ A of L(FC) has some solution constraint the solution existence problem of L(FC). It is clear from the beginning that this problem can at best be N P-complete, having the N Pcomplete satisfiability problem for feature constraints as a subproblem. The following theorem states that our combined logic in fact exhibits this best-case situation.

Theorem 5. The solution existence problem of L(FC) is N P-complete.

Proof. We are only left to show that the problem is N P-easy, i.e., that it can be solved on a nondeterministic Turing machine in polynomial time. To see this, assume a declarative unit U ▷ A. We can nondeterministically choose a σ — we need only consider mappings between the input variables of U ▷ A —, guess a Lambek proof of Π(U ▷ A)σ, check the proof in polynomial time, and at last solve Φ(U ▷ A)σ. This last step may involve bringing the individual conjuncts of Φ(U ▷ A)σ into Negation Normal Form (where negation appears only at the atomic level) in linear time, then selecting in every disjunction one disjunct and finally verifying satisfiability of a purely conjunctive constraint in polynomial time with the algorithm from Section 3. □

This result should be contrasted with the undecidability of the parsing problem of DCGs. Although one wouldn’t talk of a combination of two logics w.r.t. this formalism, since it is just an augmentation of context-free grammars by first-order terms, this problem can still be thought of as the superimposition of the unification problem for first-order terms onto the parsing problem for CFGs, both of which have polynomial time solution algorithms. In this light one might call our result on the complexity of the feature-based Lambek calculus at least “somewhat unexpected”. The fact that the lower bound complexity of the solution existence problem is already limited by the N P-complete satisfiability problem for feature constraints raises a follow-up question. Are we still facing N P-completeness, if we restrict the two logics we are combining to subsets for which the relevant problems can be solved in polynomial time ? More precisely, we consider now as constraint logic just purely conjunctive feature clauses (disallowing negation and therefore disjunction) and as grammar logic basic categorial grammar, which amounts to disallowing (←I) and (→I). This question is answered affirmatively in the next theorem uncovering that our junction of the two logics itself is a source of complexity leading to N P-completeness.

Theorem 6. The solution existence problem of L(FC) where feature constraints are restricted to feature clauses and where (←I) and (→I) are disallowed is still N P-complete.

Proof. We only need to show N P-hardness this time. To this end we give a reduction of 3SAT^{8} to our problem. Let us assume the 3SAT instance

γ = C_{1} ∧ C_{2} ∧ … ∧ C_{n}
= (l_{1,1} ∨ l_{1,2} ∨ l_{1,3}) ∧ (l_{2,1} ∨ …) ∧ … ∧ (l_{n,1} ∨ …)

and let us write var_{i,j} for the variable of literal l_{i,j} and val_{i,j} for the truth value which var(l_{i,j}) needs to take in order to make l_{i,j} true. We are constructing a declarative unit over basic types {s, c}, features as shown, and the truth values {T, F } as singleton sorts (i.e. T^{A} and F^{A} are always disjoint singleton sets).^{9} For each C_{i} we will use the following sequence of four types.^{10}

U_{i} = c ( \begin{matrix}vars: & var_{i,1} : val_{i,1} \\ aux : & X \end{matrix} ) ← c ( aux: l : X )

c ( aux: ( \begin{matrix}l : & r : var_{i,2} : val_{i,2} \\ r: & l : var_{i,3} : val_{i,3} \end{matrix} ) )

c ( aux: r : X ) → c ( aux: X )

c ( aux: X ) → c ( vars: X )

Observe that a sequence (c ← c) c (c → c) (c → c) has exactly three reductions to type c corresponding to the three bracketings (·((· ·)·)), (((· ·)·)·), and ((·(· ·))·). It is easy to verify that the attached variable of this resulting c must satisfy (vars : var_{i,j} : val_{i,j}) with j = 1 for the first, j = 2 for the second, and j = 3 for the third reading. Now we can give the full reduction. We define the declarative unit D(γ) as

A U_{1} A U_{2} … U_{n} s(true) ▷ s(true)

where A = (s ( vars: V ) ← s ( vars: V )) ← c ( vars: V ). Finally, we can state that D(γ) has a solution iff γ has a valuation making it true. Obviously, whenever γ is satisfiable, we can construct a proof with a satisfiable answer constraint for D(γ). But also, if D(γ) has a solution, there exists a proof of D(γ), the answer constraint of which must contain a valuation in form of var/val-pairs that makes at least one literal in every clause true. □

6 Discussion

We have presented a formal semantics for a system which consists of a combination of two logics. One alternative for such a formal semantics would have been to give a “monolithic semantics” for the combined logic. But by pursuing the idea of “fibred semantics” (and “combined proof systems”), we made use of a general scheme for combining two logic systems. In this way, we obtain immediately two positive effects. First, by leaving the individual proof systems intact, dedicated theorem provers can be developed, which promise to be more efficient than one, rather general theorem prover, which accounts for both logics simultaneously. Second, the combined logic, its semantics and proof system, can be taylored to new demands by extending the individual components, possibly without much change at their interface. Actually, an interesting aspect of our combination scheme involving global constraints is its generality. The proofs do not hinge in any way on special properties of Lambek nor of feature logic. Of the grammar logic part we only require to have a notion of basic type which is interpreted as a set of objects (not necessarily strings) and to have a complete proof system. On the other side feature logic can be replaced by any (constraint) logic with a decidable satisfiability problem. Whether a particular combination also leads to interesting semantic notions, which explain more than just reflecting a nice way of controlling proofs via constraints, is another question. The fibring method was demonstrated on the basis of the Lambek calculus and a decidable version of a feature logic. In this manner, we obtained a formal semantics for a grammar formalism which is paradigmatic for formalisms which are used for actual grammar implementation in computational linguistics. Practically, this was one of the motivations for writing this paper. One of us had implemented a theorem prover (a “parser”) for a feature-based Lambek calculus [25] by making use of the CUF-language [13] for the handling of the feature unification part. We wondered what the formal justification, the formal semantics, of this system would look like. The actual implementation combines two more expressive versions of logics than the ones described here. The feature logic part is a feature-based Horn logic with types. The Lambek logic part allows for “non-peripheral extraction”, i.e. it is semi-directional version of the Lambek logic whereas the original logic is strictly directional. The hypothetical reasoning of the Lambek calculus has been adapted to cover natural language sentences where the hypotheses should occur inside a phrase, not just at its very left or right corner:

83SAT is the satisfiability problem of boolean formulas in 3CNF, that is in conjunctive normal form where each conjunct is a disjunction of 3 boolean variables. 3SAT is a well-known N P-complete problem [17, 19].

9Instead of singleton sorts T and F we could also use T and ¬T for an arbitrary sort T.

10A type … b(T) … shall abbreviate (T (x) ∧ …) :: … b(x) … as explained above.

\begin{matrix}whom \\ (np → np) ← (s ← np) \end{matrix}

                          \begin{matrix}Mary \\ np \end{matrix}

\begin{matrix}\begin{matrix}gave \\ ((np → s) ← np) ← np \end{matrix} & \begin{matrix}ϵ \\ [np]_{1} \end{matrix} \\ (np → s) ← np \end{matrix}  \begin{matrix}\begin{matrix}the \\ np ← n \end{matrix} & \begin{matrix}book \\ n \end{matrix} \\ np \end{matrix}
np → s
s
|
s ← np_{1}
np → np

(12)

This is accounted for by integrating a permutation mechanism into the conditionalization rules:

\begin{matrix}\begin{matrix}U_{1} U_{2} \\ U_{1} [B] U_{2} \\ A \\ | \\ B → A \end{matrix}  (→I) & \begin{aligned}& (U_{1}, B, U_{2}) ▷ A \\ (→I) \\ & (U_{1}U_{2}) ▷ (B → A) \end{aligned} \\ \begin{matrix}U_{1} U_{2} \\ U_{1} [B] U_{2} \\ A \\ | \\ A ← B \end{matrix}  (←I) & \begin{aligned}& (U_{1}, B, U_{2}) ▷ A \\ (←I) \\ & (U_{1}U_{2}) ▷ (A ← B) \end{aligned} \end{matrix}  (13)

This version of a semi-directional Lambek calculus where the directionality of the implication connectives is ignored at even levels of embedding, could be obtained also by marking subtypes which qualify as hypotheses, e.g. (np → np) ← (s ← (▷◁ np)), and by defining a permutation rule and an elimination rule (but no introduction rule) for types which are marked with the ▷◁-operator. In the literature, various other extensions and variants of the Lambek calculus have been proposed, cf. [27], [28], and it is obvious from what has been said above, that they fit into our combination scheme. For example, a way to describe “barriers” for the movement of phrases.

\begin{matrix}tell \\ ((np → s) ← s) ← np \end{matrix} \begin{matrix}Mary \\ np \end{matrix}
(np → s) ← s

\begin{matrix}that \\ s/ (□nps) \end{matrix}  \begin{aligned}\begin{matrix}ϵ \\ np_{1} \end{matrix} & \begin{matrix}failed \\ np → s \end{matrix} \\ & s \end{aligned} ; ♯ ; □nps
s
np → s
\begin{matrix}did \\ (s ← (np → s)) ← np \end{matrix} \begin{matrix}Peter \\ np \end{matrix}
s ← (np → s)
s
|
s ← np_{1}

\begin{matrix}Who \\ s ← (s ← np) \end{matrix}

s (14)

The above derivation is blocked^{11} if we assume the following rule for a modal □-operator^{12}

11The blocked transition is marked by a ♯-sign.

12See Morrill 1992 [28] and literature cited therein for other definitions and uses of modal operators for

\begin{aligned}& U ▷ (□_{B}A) \\ (□ I) \\ & U ▷ A \end{aligned}  \begin{matrix}U \\ A \\ | \\ □BA \end{matrix}  if there is no undischarged hypothesis B ∈ U (□ I) (15)

Apart from syntactically motivated extensions, one could think to incorporate a system to handle the semantics of natural language. For example, the feature-based grammar logic could be combined with the logic of Discourse Representation Structures (DRS’s) [20]) in order to allow for a concurrent processing of the syntactic rules and the inferences on the DRS’s.

A Hilbert-system for the Lambek calculus

The Hilbert-style axiomatization of the Lambek calculus is due to Cohen [11] and Zielonka [38]^{13}.

(identity) A ⊢ A
(→trans) B → A ⊢ (C → B) → (C → A) (←trans) A ← B ⊢ (A ← C) ← (B ← C)
(→raise) B ⊢ (A ← B) → A  (←raise) B ⊢ A ← (B → A)
B′ ⊢ B  A ⊢ A′ (→rec-trans) (B → A) ⊢ (B′ → A′) B′ ⊢ B  A ⊢ A′ (←rec-trans) (A ← B) ⊢ (A′ ← B′)
(→MP) B(B → A) ⊢ A  (←MP) (A ← B)B ⊢ A
U_{2} ⊢ B U_{1}BU_{3} ⊢ A (cut) U_{1}U_{2}U_{3} ⊢ A

syntactic and semantic descriptions.

13For an overview of Hilbert-style axiomatizations of various versions of Linear logic see Avron 1987 [3].

References

[1] Hassan Aït-Kaci and Roger Nasr. LOGIN: A logic programming language with built-in inheritance. The Journal of Logic Programming, 3:185–215, 1986.

[2] Hassan Aït-Kaci and Andreas Podelski. Towards a meaning of LIFE. PRL Research Report 11, Digital Equipment Corporation, Paris Research Laboratory, Rueil-Malmaison, France, 1991.

[3] Arnon Avron. The semantics and proof theory of Linear Logic. Theoretical Computer Science, 57:161–184, 1987.

[4] Patrick Blackburn. Modal logic and attribute value structures. In M. de Rijke, editor, Diamonds and Defaults, number Vol 229 in Synthese Language Library, pages 19–65. Kluwer, Dordrecht, 1993.

[5] Patrick Blackburn. The structural approach to feature logic. In C. J. Rupp, M. A. Rosner, and R. L. Johnson, editors, Constraints, Language and Computation, pages 1–27. Academic Press, London, 1994.

[6] Patrick Blackburn, Claire Gardent, and Wilfried Meyer-Viol. Talking about trees. In Proceedings of the 6th Conference of the European Chapter of the Association for Computational Linguistics, pages 21–29, Utrecht, 1993.

[7] Patrick Blackburn and Edith Spaan. A modal perspective on the computational complexity of attribute value grammar. Journal of Logic, Language and Information, (2):129–169, 1993.

[8] Wojciech Buszkowski. Compatibility of a categorial grammar with an associated category system. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 28:229–237, 1982.

[9] Wojciech Buszkowski. Completeness results for Lambek syntactic calculus. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 32:13–28, 1986.

[10] Wojciech Buszkowski. Generative power of categorial grammars. In Emmon Bach, Richard Oehrle, and Deirdre Wheeler, editors, Categorial Grammars and Natural Languages Structures, pages 69–94. Reidel, Dordrecht, 1988. Proceedings of the Conference on Categorial Grammar, Tucson 1985.

[11] J.M. Cohen. The equivalence of two concepts of categorial grammar. Information and Control, 10:475–483, 1967.

[12] Jochen Dörre. Feature-Logik und Semiunifikation. Dissertation, Institut für maschinelle Sprachverarbeitung, Azenbergstr. 12, D-70174 Stuttgart, Germany, 1993. In German. Prepublished as Technical Report 48, Sonderforschungsbereich 340.

[13] Jochen Dörre and Michael Dorna. CUF - a formalism for linguistic knowledge representation. Deliverable R.1.2A, DYANA 2, August 1993.

[14] Kosta Došen. A completeness theorem for the Lambek calculus of syntactic categories. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 31:235–241, 1985.

[15] Kosta Došen. A brief survey of frames for the Lambek calculus. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, to appear. Preprint: Konstanzer Berichte, Logik und Wissenschaftstheorie, May 1990.

[16] Dov Gabbay. Labelled deductive systems, part I. CIS-Bericht 90-22, Centrum für Informations- und Sprachverarbeitung, Universiät München, München, Bavaria, 1990.

[17] Michael R. Garey and David S. Johnson. Computers and Intractability—A Guide to the Theory of NP-Completeness. Freeman, San Francisco, Cal., 1979.

[18] Markus Höhfeld and Gert Smolka. Definite relations over constraint languages. LILOG-Report 53, IBM Deutschland, Stuttgart, Baden-Württemberg, October 1988.

[19] John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, Mass., 1979.

[20] Hans Kamp and Uwe Reyle. From Discourse to Logic. Introduction to Modeltheoretic Semantics of Natural Language, Formal Logic and Discourse Representation Theory. Studies in Linguistics and Philosophy 42. Kluwer Academic Publishers, Dordrecht, The Netherlands, 1993.

[21] Ronald M. Kaplan and Joan Bresnan. Lexical-Functional Grammar: A formal system for grammatical representation. In Joan Bresnan, editor, The Mental Representation of Grammatical Relations, pages 173–281. MIT Press, Cambridge, Mass., 1982.

[22] Robert T. Kasper and William C. Rounds. A logical semantics for feature structures. In Proceedings of the 24th Annual Meeting of the ACL, Columbia University, pages 257–265, New York, N.Y., 1986.

[23] Martin Kay. Unification in grammar. In V. Dahl and P. Saint-Dizier, editors, Natural Language Understanding and Logic Programming, pages 233–241. Elsevier Science Publishers B.V. (North Holland), 1985.

[24] Esther König. Lambek categorial grammars are contextfree. Manuscript, Institut für Maschinelle Sprachverarbeitung, Universität Stuttgart, September 1992.

[25] Esther König. A study in grammar design. Arbeitspapier des Sonderforschungsbereich 340 54, Institut für Maschinelle Sprachverarbeitung, Universität Stuttgart, 1994.

[26] Joachim Lambek. The mathematics of sentence structure. American Mathematical Monthly, 65:154–170, 1958. Reprinted in: Buszkowski, W., W. Marciszewski, and J. van Benthem (eds): Categorial Grammar. John Benjamins, Amsterdam 1988.

[27] Michael Moortgat. Generalized quantifiers and discontinuous type constructors. In W. Sijtsma and A. van Horck, editors, Proceedings of the Tilburg Symposium on Discontinuous Constituency, The Hague, 1992. Mouton de Gruyter.

[28] Glyn Morrill. Type-logical grammar. Technical Report OTS-WP-CL-92-002, Utrecht University, Research Institute for Language and Speech, Utrecht, Netherlands, January 1992.

[29] Fernando C.N. Pereira and Stuart M. Shieber. The semantics of grammar formalisms seen as computer languages. In Proceedings. of the 22nd Annual Meeting of the Association for Computational Linguistics, pages 123–129, Stanford, Ca., 1984.

[30] Fernando C.N. Pereira and David H.D. Warren. Definite clause grammars for language analysis—a survey of the formalism and a comparison with augmented transition networks. Artificial Intelligence, 13:231–278, 1980.

[31] Stuart Shieber, Hans Uszkoreit, Fernando Pereira, Jane Robinson, and M. Tyson. The formalism and implementation of PATR-II. In B. Grosz and M. E. Stickel, editors, Research on Interactive Acquisition and Use of Knowledge. Stanford Research Institute International, Menlo Park, Ca., 1983.

[32] Gert Smolka. Feature constraint logics for unification grammars. The Journal of Logic Programming, 12:51–87, 1992.

[33] Hans Uszkoreit. Categorical Unification Grammar. In Proceedings of the 11th International Conference on Computational Linguistics, pages 187–194, Bonn, Germany, 1986.

[34] Koen Versmissen. Categorial grammar, modalities and algebraic semantics. In Proceedings of the 6th Conference of the European Association of Computational Linguistics, pages 377–383, Utrecht, The Netherlands, 1993.

[35] K. Vijay-Shanker. Using descriptions of trees in a tree adjoining grammar. Computational Linguistics, 18(4):481–517, 1992.

[36] D.N. Yetter. Quantales and (noncommutative) linear logic. Journal of Symbolic Logic, 55(1):41–64, March 1990.

[37] Henk Zeevat, Ewan Klein, and Jo Calder. An introduction to unification categorial grammar. In N. J. Haddock, E. Klein, and G. Morrill, editors, Categorial Grammar, Unification Grammar, and Parsing, pages 195–222. Edinburgh Working Papers in Cognitive Science 1, Centre for Cognitive Science, University of Edinburgh, January 1987.

[38] Wojczech Zielonka. Axiomatizability of Ajdukiewicz-Lambek calculus by means of cancellation schemes. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 27:215–224, 1981.