Abstract 1 Introduction 2 Preliminaries 3 Hypergraph First-Order Categorial Grammars 4 Expressive Power of String MILL1 Grammars 5 Hypergraph Language Semantics 6 Conclusion References

First-Order Intuitionistic Linear Logic and Hypergraph Languages

Tikhon Pshenitsyn ORCID Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russian Federation
Abstract

The Lambek calculus is a substructural logic known to be closely related to the formal language theory: on the one hand, it is used for generating formal languages by means of categorial grammars and, on the other hand, it has formal language semantics, with respect to which it is sound and complete. This paper studies a similar relation between first-order intuitionistic linear logic ILL1 along with its multiplicative fragment MILL1 on the one hand and the hypergraph grammar theory on the other. In the first part, we introduce a novel concept of hypergraph first-order logic categorial grammar, which is a generalisation of string MILL1 grammars introduced in Richard Moot’s works. We prove that hypergraph ILL1 grammars generate all recursively enumerable hypergraph languages and that hypergraph MILL1 grammars are as powerful as linear-time hypergraph transformation systems. In addition, we show that the class of languages generated by string MILL1 grammars is closed under intersection and that it includes a non-semilinear language as well as an NP-complete one. This shows how much more powerful string MILL1 grammars are as compared to Lambek categorial grammars.
In the second part, we develop hypergraph language models for MILL1. In such models, formulae of the logic are interpreted as hypergraph languages and multiplicative conjunction is interpreted using parallel composition, which is one of the operations of HR-algebras introduced by Courcelle. We prove completeness of the universal-implicative fragment of MILL1 with respect to these models and thus present a new kind of semantics for a fragment of first-order linear logic.

Keywords and phrases:
linear logic, categorial grammar, MILL1 grammar, first-order logic, hypergraph language, graph transformation, language semantics, HR-algebra
Category:
Track B: Automata, Logic, Semantics, and Theory of Programming
Copyright and License:
[Uncaptioned image] © Tikhon Pshenitsyn; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Theory of computation Linear logic
; Theory of computation Grammars and context-free languages ; Theory of computation Rewrite systems
Related Version:
Extended Version: https://arxiv.org/abs/2502.05816 [30]
Acknowledgements:
I thank Richard Moot and Sergei Slavnov for their attention to my work and for the productive discussions. I am also grateful to the anonymous reviewers for valuable remarks.
Funding:
This work was supported by the Russian Science Foundation under grant no. 23-11-00104, https://rscf.ru/en/project/23-11-00104/.
Editors:
Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, and Gabriele Puppis

1 Introduction

There is a strong connection between substructural logics, especially non-commutative ones, and the theory of formal languages and grammars [5, 23]. This connection is two-way. On the one hand, a logic can be used as a derivational mechanism for generating formal languages, which is the essence of categorial grammars. One prominent example is Lambek categorial grammars based on the Lambek calculus L [18]; formulae of the latter are built using multiplicative conjunction “” and two directed implications “\”, “/”. In a Lambek categorial grammar, one assigns a finite number of formulae of L to each symbol of an alphabet and chooses a distinguished formula S; then, the grammar accepts a string a1an if the sequent A1,,AnS is derivable in L where, for i=1,,n, Ai is one of the formulae assigned to ai. A famous result by Pentus [25] says that Lambek categorial grammars generate exactly context-free languages (without the empty word, to be precise).

On the other hand, algebras of formal languages can serve as models for substructural logics. For example, one can define language semantics for the Lambek calculus as follows: a language model is a function u mapping formulas of L to formal languages such that u(AB)={vwvu(A),wu(B)}, u(B\A)={wvu(B)vwu(A)}, and u(A/B)={vwu(B)vwu(A)}; a sequent AB is interpreted as inclusion u(A)u(B). Another famous result by Pentus [26] is that L is sound and complete w.r.t. language semantics; strong completeness for the fragment of L without “” had been proved earlier by Buszkowski in [4] using canonical models.

Numerous variants and extensions of the Lambek calculus have been studied, including its nonassociative version [23], commutative version [37] (i.e. multiplicative intuitionistic linear logic), the multimodal Lambek calculus [19], the displacement calculus [24] etc. These logics have many common properties, which motivates searching for a unifying logic. One such “umbrella” logic is the first-order multiplicative intuitionistic linear logic MILL1 [20, 22], which is the multiplicative fragment of first-order intuitionistic linear logic ILL1. The Lambek calculus can be embedded in MILL1 [22]: for example, the L sequent pp\qq is translated into the MILL1 sequent p(x0,x1)y(p(y,x1)q(y,x2))q(x0,x2). In such a translation, variables “fix” the order of formulae. Although MILL1 is a first-order generalisation of L, derivability problems in these logics have the same complexity, namely, they are NP-complete. One can define MILL1 categorial grammars in the same manner as Lambek categorial grammars [20, 34]. The former generalise the latter, hence generate all context-free languages (see the definition of the latter in [14]). Moot proved in [20] that MILL1 grammars generate all multiple context-free languages, hence some non-context-free ones, e.g. {wwwΣ}.

It turns out that the interplay between propositional substructural logics and formal grammars can be elevated fruitfully to that between first-order substructural logics and hypergraph grammars. This is the subject of this article. Hypergraph grammar approaches generate sets of hypergraphs; usually they are designed as generalisations of grammar formalisms for strings. For example, hyperedge replacement grammar [8] is a formalism that extends context-free grammar. A rule of a hyperedge replacement grammar allows one to replace a hyperedge in a hypergraph by another hypergraph; see an example below.

Figure 1: A hyperedge replacement rule (in a box) and an example of it being applied twice.

Note that, in this approach, hyperedges but not nodes are labeled. Some of the nodes, called external, are distinguished in a hypergraph; e.g., in the above example, these are the nodes marked by (i),(o),(i),(o). External nodes are needed to specify how hyperedge replacement is done. A more general approach, which corresponds to type-0 grammars in the Chomsky hierarchy, is hypergraph transformation systems (the term is taken from [17]), which allow one to replace a subhypergraph in a hypergraph by another hypergraph.

Naturally, a hypergraph can be represented by a linear logic formula. Namely, one can interpret hyperedges as predicates, nodes as variables, and external nodes as free variables. For example, the hypergraph in the box from Figure 1 can be converted into the formula x.y.a(i,x)b(i,y)A(x,o,y,o). This idea underlies the concept of hypergraph first-order categorial grammars, which we introduce in Section 3. Roughly speaking, given a first-order logic , say, MILL1, a hypergraph categorial grammar takes a hypergraph, assigns a formula of to each its hyperedge and node, converts the resulting hypergraph into a sequent and check whether it is derivable in . Using first-order linear logic for generating hypergraph languages is a novel idea which has not yet been explored in the literature. In Section 3, we study expressive power of grammars defined thusly and prove the following.

  1. 1.

    Hypergraph ILL1 grammars are equivalent to hypergraph transformation systems and thus they generate all recursively enumerable hypergraph languages (Theorem 23). This result relates hypergraph ILL1 grammars to the well studied approach in the field of hypergraph grammars based on the double pushout graph transformation procedure.

  2. 2.

    Hypergraph MILL1 grammars are at least as powerful as linear-time hypergraph transformation systems (Theorem 25). The latter are hypergraph transformation systems where the length of a derivation is bounded by a linear function w.r.t. the size of the resulting hypergraph. The linear-time bound has been studied for many grammar formalisms [2, 11, 29, 35], but, to our best knowledge, it is the first time it is used for graph grammars.

The proofs partially use the techniques from [29] where languages generated by grammars over the commutative Lambek calculus are studied. As compared to [29], the proofs in this paper are more technically involved because of complications arising when working with quantifiers and variables in the first-order setting.

In Section 4, using the methods developed for hypergraph MILL1 grammars, we discover the following properties of the class of languages generated by string MILL1 grammars.

  1. 1.

    Languages generated by string MILL1 grammars are closed under intersection (Theorem 26). Consequently, non-semilinear languages, e.g. the language {a2n2n}, can be generated by string MILL1 grammars.

  2. 2.

    String MILL1 grammars generate an NP-complete language (Theorem 30). Note that the Lambek calculus is NP-complete [27] but Lambek categorial grammars generate only context-free languages, which are in P. The logic MILL1 is NP-complete as well but string MILL1 grammars are able to generate non-polynomial languages (assuming PNP), hence they are much more powerful.

The question whether string MILL1 grammars generate only multiple context-free grammars was left open by Richard Moot in [20], and I considered Theorem 30 to be the first one answering it. Recently, however, Sergei Slavnov pointed out to an alternative answer to this question, using previously known techniques. Namely, in [21], it is shown that hybrid type-logical grammars can be translated into MILL1; hybrid type-logical grammars generalise abstract categorial grammars, and it is proved in [32] that the latter generate an NP-complete language. Our proof relies on a different technique, namely, on reducing linear-time hypergraph transformation systems, which are a rule-based approach unlike hybrid type-logical grammars. In general, finding a natural rule-based formalism equivalent to a MILL1 grammars is an interesting question to study, and Theorem 30 is a step towards the answer111We believe that linear-time hypergraph transformation systems are essentially equivalent to MILL1 grammars in terms of generative power because, as we conjecture, it is possible to simulate MILL1 axioms and rules by hypergraph transformation rules and hence to convert hypergraph MILL1 grammars into linear-time transformation systems. However, some subtleties arise related to the definition of hypergraph transformation rules when one tries to do so; we discuss them after the proof of Theorem 25..

The second part of the paper (Section 5), not related to the first one, is devoted to developing hypergraph language semantics for MILL1, thus establishing the other way round connection between first-order linear logic and hypergraph languages. Linear logic is considered as a logic for reasoning about resources [10], and language models for the Lambek calculus are one of formalisations of this statement with resources being words; this agrees with linguistic applications of L. In this paper, we shall show that hypergraphs can be treated as “first-order resources.” In a hypergraph language model (Definition 33), MILL1 formulas are interpreted by sets of hypergraphs, and the tensor operation AB is interpreted using the parallel composition operation. The latter one is “gluing” of hypergraphs; it is studied well in the hypergraph grammar theory, namely, it is one of the operations in the language of HR-algebras [7]. Hypergraph language models are a particular case of intuitionistic phase semantics (see the definition in [15]) with the trivial closure operator Cl(X)=X.

Our main result concerning hypergraph language models is soundness of MILL1 and completeness of its {,}-fragment w.r.t. them (Theorem 35). The proof is inspired by Buszkowski’s one [4] but it is more technically involved, again because of the first-order setting. This result’s importance amounts to the fact that hypergraph language models is one of few, to our best knowledge, examples of a specific semantics for a fragment of first-order intuitionistic linear logic, which, moreover, is grounded in the hypergraph language theory.

2 Preliminaries

In Section 2.1, we introduce notions from the field of graph grammars, and, in Section 2.2, we introduce first-order intuitionistic linear logic.

2.1 Hypergraphs & Hypergraph Transformation Systems

There are many paradigms in the field of graph grammars, including node replacement grammars, hyperedge replacement grammars, algebraic approaches (double pushout, single pushout) with a more categorical flavour, definability in monadic second-order logic etc. We shall work with the definition of a hypergraph from the field of hyperedge replacement grammars [8, 9, 12] because it fits first-order linear logic better than other ones. In hypergraphs we shall deal with, only hyperedges are labeled while nodes play an auxiliary role. Some of the nodes are marked as external; informally, they play the role of gluing points. Throughout the paper, we shall explore a natural correspondence between hypergraphs defined thusly and first-order linear logic formulae. In contrast, there would be no such correspondence if we sticked to the definition of a hypergraph where nodes are labeled and edges are not.

We fix a countable set Σ; its elements are called selectors. In the grammar-logic correspondence we shall develop, selectors will guide variable substitution.

Definition 1.

A Σ-typed alphabet is a set C along with a function type:C𝒫(Σ) such that type(c) is finite for cC.

Definition 2.

Let C be a finite Σ-typed alphabet of hyperedge labels. A hypergraph over C is a tuple H=VH,EH,𝑙𝑎𝑏H,𝑎𝑡𝑡H,𝑒𝑥𝑡H where VH is a finite set of nodes; EH is a finite set of hyperedges; for each eEH, 𝑙𝑎𝑏H:EHC is the labeling function and 𝑎𝑡𝑡H(e):type(𝑙𝑎𝑏H(e))VH is the attachment function; 𝑒𝑥𝑡H:type(H)VH is a function with the domain type(H)Σ. Elements of ran(𝑒𝑥𝑡H) are called external nodes. The set of hypergraphs over C is denoted by (C). Let typeH(e):=dom(𝑎𝑡𝑡H(e)) for each eEH.

In drawings of hypergraphs, nodes are depicted as black circles and hyperedges are depicted as labeled rectangles. When depicting a hypergraph H, we draw a line with a label σ from e to v if 𝑎𝑡𝑡H(e)(σ)=v. External nodes are represented by symbols in round brackets: if extH(σ)=v, then we mark v as (σ).

There is a standard issue with distinguishing between concrete and abstract hypergraphs, i.e. between hypergraphs and their isomorphism classes. When one considers a hypergraph language L, it is reasonable to assume that it consists of abstract hypergraphs (or, equivalently, that it is closed under isomorphism); however, when we write HL, we assume that H is a concrete hypergraph. Following tradition, we often do not distinguish between abstract and concrete hypergraphs to avoid excessive bureaucracy.

Let us fix two selectors, 𝐬 and 𝐭. If typeH(e)={𝐬,𝐭}, then the hyperedge e is called an edge and it is depicted by an arrow going from 𝑎𝑡𝑡H(e)(𝐬) to 𝑎𝑡𝑡H(e)(𝐭).

Definition 3.

A string graph sg(w) induced by a string w=a1an is defined as follows: Vsg(w)={v0,,vn}, Esg(w)={e1,,en}; type(ei)=type(sg(w))={𝐬,𝐭}, 𝑎𝑡𝑡sg(w)(ei)(𝐬)=vi1, 𝑎𝑡𝑡sg(w)(ei)(𝐭)=vi, 𝑙𝑎𝑏sg(w)(ei)=ai (for i=1,,n); 𝑒𝑥𝑡sg(w)(𝐬)=v0, 𝑒𝑥𝑡sg(w)(𝐭)=vn. For example, sg(ab)=.

Definition 4.

Given aC, a is a hypergraph such that Va=type(a); Ea={e} with typea(e)=type(a); 𝑎𝑡𝑡a(σ)=𝑒𝑥𝑡a(σ)=σ for σtype(a). For example, if type(a)={x,y,z}, then a=.

Definition 5.

If H1,H2 are hypergraphs with type(H1)type(H2)=, then their disjoint union is the hypergraph H1+H2:=VH1VH2,EH1EH2,𝑎𝑡𝑡,𝑙𝑎𝑏,𝑒𝑥𝑡 where 𝑎𝑡𝑡=𝑎𝑡𝑡Hi, 𝑙𝑎𝑏=𝑙𝑎𝑏Hi on Ei for i=1,2, and 𝑒𝑥𝑡 is the union of functions 𝑒𝑥𝑡H1 and 𝑒𝑥𝑡H2.

Now, let us define the hyperedge replacement operation.

Definition 6.

Let H be a hypergraph and let R be a binary relation on VH. Let R be the smallest equivalence relation on VH containing R. Then H/R=H is the following hypergraph: VH={[v]RvVH}; EH=EH; 𝑙𝑎𝑏H=𝑙𝑎𝑏H; 𝑎𝑡𝑡H(e)(s)=[𝑎𝑡𝑡H(e)(s)]R; 𝑒𝑥𝑡H(s)=[𝑒𝑥𝑡H(s)]R.

Definition 7.

Let H,K be two hypergraphs over C; let eEH be a hyperedge such that type(e)=type(K). Then the replacement of e by K in H (the result being denoted by H[e/K]) is defined as follows:

  1. 1.

    Remove e from H and add a disjoint copy of K. Formally, let L be the hypergraph such that VL=VHVK, EL=(EH{e})EK, 𝑙𝑎𝑏L is the restriction of 𝑙𝑎𝑏H𝑙𝑎𝑏K to EL, 𝑎𝑡𝑡L is the restriction of 𝑎𝑡𝑡H𝑎𝑡𝑡K to EL, and 𝑒𝑥𝑡L=𝑒𝑥𝑡H.

  2. 2.

    Glue the nodes that are incident to e in H with the external nodes of K. Namely, let H[e/K]:=L/R where R={(𝑎𝑡𝑡H(e)(s),𝑒𝑥𝑡K(s))stype(e)}.

Using hyperedge replacement, we define hypergraph transformation system, a formalism which shall be used to describe expressive power of hypergraph categorial grammars. It enables one to replace a subhypergraph in a hypergraph with another hypergraph.

Definition 8.

A hypergraph transformation rule (ht-rule) is of the form r=(HH) where H,H are hypergraphs such that type(H)=type(H) and 𝑒𝑥𝑡H,𝑒𝑥𝑡H are injective.
We say that G is transformed into G via r and denote this by GrG (also by GG) if G=K[e/H] and G=K[e/H] for some K and eEK such that 𝑎𝑡𝑡K(e) is injective.
A hypergraph transformation system (ht-system) is a tuple 𝒢=N,T,P,S where N,T are Σ-typed alphabets, P is a finite set of hypergraph transformation rules and S(NT) is a start hypergraph such that 𝑒𝑥𝑡S is injective. The language L(𝒢) generated by 𝒢 consists of hypergraphs H(T) such that SH.

Figure 2: An example of a hypergraph transformation rule (boxed) and of its application.

The definition of a hypergraph transformation rule, although given in a slightly unconventional way through hyperedge replacement, coincides with the standard notion of a graph transformation rule with injective morphisms of the double pushout approach formalism in the corresponding category of hypergraphs; compare it with [17]. Also, our definition is essentially the same as that from [36] (with the only difference that the cited paper deals with graphs rather than with hypergraphs). In that paper, the following proposition is proved.

Proposition 9.

Hypergraph transformation systems generate all recursively enumerable hypergraph languages.

This is a rather expected result related to string rewriting systems generating all recursively enumerable string languages. To prove Proposition 9, it suffices to show how to convert a string representation of a hypergraph into the hypergraph itself by means of ht-rules.

The injectivity requirements in Definition 8 are quite standard, ht-systems defined thusly correspond to the class of DPOi/i grammars investigated in [13] (“DPO” stands for “double-pushout approach”). In our paper, injectivity is crucial in the proof of Theorem 25.

2.2 First-Order Intuitionistic Linear Logic

We assume the reader’s familiarity with the basic principles and issues of first-order logic. Let us fix a countable set of variables Var and a countable set of predicate symbols with arities. Atomic formulae are of the form p(x1,,xn) where p is a predicate symbol of arity n and x1,,xn are variables. Following [16, 20, 22], we do not allow function symbols; note that complex terms would not fit in the variables are nodes, predicates are hyperedges paradigm. We also do not allow constants because they can easily be simulated by variables.

Formulae of intuitionistic linear logic ILL1 are built from atomic formulae and propositional constants 0,1, using the multiplicative connectives ,, the additive ones ,, and the exponential one ! along with the quantifiers ,. The multiplicative fragment of ILL1 denoted by MILL1 does not have constants and uses only , and ,. A sequent is a structure of the form ΓB where Γ is a multiset of formulae and B is a formula.

Note that we shall sometimes describe multisets using the notation {f(x)Φ(x)}. An element a belongs to this multiset n times if there are exactly n elements x1,,xn such that f(xi)=a and such that xi satisfies Φ.

The only axiom is AA. The rules for MILL1 are presented below.

Γ,A,BC(L)Γ,ABCΓAΔB(R)Γ,ΔAB
ΠBΓ,AC(L)Γ,Π,BACΓ,BA(R)ΓBA
Γ,A[z/x]B(L)Γ,xABΓA[y/x](R)ΓxA
Γ,A[y/x]B(L)Γ,xABΓA[z/x](R)ΓxA

Here y is any variable while z is a variable which is not free in Γ,A,B; A[y/x] denotes replacing all free occurrences of x in A by y. More generally, if h:FVar(A)Var is a function defining a correct substitution, then A[h] denotes the result of substituting h(x) for x for xFVar(A) (FVar(A) is the set of free variables in A). Rules for additive and exponential connectives of ILL1 can be found e.g. in [33, Appendix E].

The cut rule is admissible in ILL1:

ΓAA,ΔC(cut)Γ,ΔC

Using it, one can prove that the rules (L), (R), (L), and (R) are invertible, i.e. that, if a conclusion of any of these rules is provable in ILL1, then so is its premise.

3 Hypergraph First-Order Categorial Grammars

The idea of extending the Lambek calculus and categorial grammars to hypergraphs was explored recently in the work [28], where the hypergraph Lambek calculus was introduced. This is a propositional logic whose formulae are built using two operators, × and ÷ (similar to linear logic and ). Formulae of this calculus can be used as labels on hyperedges: e.g. if H is a hypergraph labeled by formulas, then ×(H) is a formula. Based on the hypergraph Lambek calculus, hypergraph Lambek grammars were defined and their properties were investigated. Although the definition of the hypergraph Lambek calculus is justified in [28], the syntax of this logic is somewhat cumbersome. We are going to show that one can use any first-order logic, such as MILL1, as the underlying logic for hypergraph categorial grammars. The definitions we propose below are much simpler than those from [28]; besides, they enable one to rely on the well studied apparatus of linear logic.

Let us start with the definition of a string categorial grammar over a first-order logic. This notion appears in [20, 34] for MILL1 but we would like to start with a more general exposition. Let be a first-order sequent calculus of interest and let Fm() denote the set of its formulas. Let 𝐬,𝐭 be two fixed variables (note that earlier we used them as selectors).

Definition 10.

A string grammar is a tuple 𝒢=T,S, where T is a finite alphabet, S is a formula of such that FVar(S){𝐬,𝐭}, and T×Fm() is a finite binary relation such that aA implies FVar(A){𝐬,𝐭}. The language L(𝒢) generated by 𝒢 is defined as follows: a1anL(𝒢) if and only if there are formulas A1,,An such that aiAi for i=1,,n and such that the sequent A1[x0/𝐬,x1/𝐭],,An[xn1/𝐬,xn/𝐭]S[x0/𝐬,xn/𝐭] is derivable in where x0,,xn are distinct variables.

Example 11.

Let T={a}, let S=q(𝐬,𝐭), and let consist of the pairs ap(𝐬,𝐭), ax.p(x,𝐬)q(x,𝐭). This grammar accepts the string aa, because the sequent

p(x0,x1),x.p(x,x1)q(x,x2)q(x0,x2)

is derivable in MILL1.

We see that, in Definition 10, the noncommutative structure of a string is simulated by variables. Informally, one could imagine a string graph with the nodes x0,,xn such that, for i=1,,n, there is an edge labeled by Ai connecting xi1 to xi. Based on this observation, let us introduce the central notion of hypergraph grammars. From now on, we consider nodes, selectors and logical variables as objects of the same kind. Besides, if T is a Σ-typed alphabet, then we treat aT as a predicate symbol.

Definition 12.

Let us fix a variable x and a symbol . A hypergraph grammar is a quadruple 𝒢=T,S,X, where T is a Σ-typed alphabet; (T{})×Fm() is a finite binary relation such that aA implies FVar(A)type(a) and A implies FVar(A){x}; finally, S is a formula of such that FVar(S)XΣ.

Definition 13.

The language L(𝒢) is defined as follows: HL(𝒢) if and only if type(H)=X and there are functions hV:VHFm(), hE:EHFm() such that

  1. 1.

    hV(v) for vVH, 𝑙𝑎𝑏H(e)hE(e) for eEH;

  2. 2.

    the sequent {hE(e)[𝑎𝑡𝑡H(e)]eEH},{hV(v)[v/x]vVH}S[𝑒𝑥𝑡H] is derivable in .

Example 14.

Let 𝒢 be a hypergraph MILL1 grammar with T:={a,b} (type(a)={𝐬,𝐭}, type(b)={1,2,3}), X:={𝐬,𝐭}, S:=p(𝐬,𝐭)rrr, and with consisting of the pairs

  • aq(𝐬,𝐭);   ax.q(x,𝐬)p(x,𝐭);

  • bq(2,3)p(1,1)p(2,3);

  • r;   y.p(x,y).

Consider the hypergraph H= with VH={v1,v2,v3,v4} (nodes are enumerated left to right, top to bottom). It belongs to L(𝒢), because the sequent

q(v3,v4),q(v3,v4)p(v1,v1)p(v3,v4),y.p(v1,y),r,r,rp(v3,v4)rrr

is derivable in MILL1. In this sequent, the first formula corresponds to the a-labeled hyperedge, the second one corresponds to the b-labeled hyperedge, the third formula corresponds to v1 and the remaining formulae correspond to v2,v3,v4.

The string graph sg(aa)= also belongs to L(𝒢), because the sequent

q(v0,v1),x.q(x,v1)p(x,v2),r,r,rp(v0,v2)rrr

is derivable in MILL1 (the nodes of sg(aa) from left to right are v0,v1,v2).

Finally, the hypergraph without hyperedges and with nodes w1,w2,w3,w4 is also accepted by 𝒢, because the following sequent is derivable in MILL1:

y.p(w1,y),r,r,rp(w1,w4)rrr.

Let us comment on Definitions 12 and 13. The relation assigns formulae of to hyperedge labels from T. Besides, it assigns formulae with the free variable x (or without free variables) to the distinguished “node symbol” . Since, in the theory of hyperedge replacement, it is traditional to consider hypergraphs where only hyperedges are labeled, one might ask why we assign formulas not only to hyperedges but to nodes as well. The answer is that we need to have some control over nodes. If we remove all the parts concerning nodes from Definitions 12 and 13, then hypergraph grammars would completely ignore isolated nodes; this is a minor yet annoying issue. Moreover, each hypergraph language generated by a hypergraph grammar (for, say, =MILL1) would be closed under node identification.

Example 15.

Assume that sg(aa)L(𝒢) for a hypergraph MILL1 grammar 𝒢=T,S,{𝐬,𝐭}, where nodes do not participate in the grammar formalism. This would mean that there are formulae A1,A2 with free variables in {𝐬,𝐭} such that aA1, aA2 and such that the sequent A1[v0/𝐬,v1/𝐭],A2[v1/𝐬,v2/𝐭]S[v0/𝐬,v2/𝐭] is derivable in MILL1. However, this necessarily implies that the sequent A1[v0/𝐬,v0/𝐭],A2[v0/𝐬,v1/𝐭]S[v0/𝐬,v1/𝐭] is derivable in MILL1 too, hence the hypergraph is also accepted by 𝒢. Consequently, hypergraph MILL1 grammars without node-formula assignment are not able to generate a language consisting only of string graphs, which is quite undesirable.

Another remark concerning Definition 12 is why we need the set X. This set makes the language generated by a grammar consistent in terms of external nodes: if H1,H2L(𝒢), then type(H1)=type(H2)=X. Note that ht-systems and hyperedge replacement grammars [8] are consistent in this sense.

Given a hypergraph grammar 𝒢, one can consider only string graphs generated by it and thus associate a string language with Γ.

Definition 16.

The string language L𝑠𝑡𝑟(𝒢) generated by a hypergraph grammar 𝒢 is the set {wsg(w)L(𝒢)}.

One expects that, normally, string languages generated by hypergraph grammars should be the same as languages generated by string grammars. For example, for =MILL1, the following proposition holds.

Proposition 17.

If a language L is generated by a string MILL1 grammar, then there is a hypergraph MILL1 grammar 𝒢 such that L𝑠𝑡𝑟(𝒢)=L. Conversely, if 𝒢 is a hypergraph MILL1 grammar, then L𝑠𝑡𝑟(𝒢){ε} is generated by some string MILL1 grammar.

This proposition is almost trivial; the only minor technicality is that hypergraph MILL1 grammars assign formulae to nodes while string MILL1 grammars are unable to do so. This technicality is the cause why we need to exclude the empty word in the second part of the proposition. See the proof of this proposition in [30, Appendix A.1].

3.1 Hypergraph Transformation Rules as MILL1 Formulae

Our main goal now is to describe a relation between hypergraph first-order linear logic grammars and hypergraph transformation systems. We start with showing how a ht-rule is encoded by a MILL1 formula. Let us fix a unary predicate ν(x); informally, it is understood as “x is a node”. Given a hypergraph H, let us treat its hyperedge labels as predicate symbols. Namely, if 𝑙𝑎𝑏H(e)=a, then let us assume that the elements of type(a) are enumerated, i.e. type(a)={σ1,,σn}; for any function h:type(A)Var, let 𝑙𝑎𝑏H(e)[h] stand for the formula a(h(σ1),,h(σn)). The arity of a is n=|type(a)|.

Definition 18.

The diagram of a hypergraph H is the multiset

𝒟(H):={𝑙𝑎𝑏H(e)[𝑎𝑡𝑡H(e)]eEH}{ν(v)vVH}.

Let D(H):=v𝒟(H) where v is the list of nodes in VHran(𝑒𝑥𝑡H).

Example 19.

Let H= be a hypergraph such that VH={v1,v2,v3,v4}. Then 𝒟(H)=C(v1,v3,v4),D(v3,v4),X(v4,v3),Y(v4),ν(v1),ν(v2),ν(v3),ν(v4).

Definition 20.

Given a ht-rule p=(HH), let
𝑓𝑚(p):=u(D(H)D(H)[χp]) where

  • u is the list of nodes in ran(𝑒𝑥𝑡H);

  • χp is a substitution function defined on ran(𝑒𝑥𝑡H) as follows: χp(𝑒𝑥𝑡H(σ))=𝑒𝑥𝑡H(σ).

The formula 𝑓𝑚(p) is closed. Note that χp is well defined because 𝑒𝑥𝑡H is injective.

Example 21.

Consider the ht-rule

p=

Let u1,u2,u3 be the nodes of the left-hand side hypergraph (from left to right) and let v1,v2,v3,v4 be the nodes of the right-hand side hypergraph. Then

𝑓𝑚(p)=v3.v4.((v1.v2.C(v1,v3,v4)D(v3,v4)ν(v1)ν(v2)ν(v3)ν(v4))(u2.A(u2,v3)B(u2,v4)ν(v3)ν(u2)ν(v4))).

The main lemma about 𝑓𝑚(p) is presented below.

Lemma 22.

Let P,P be multisets of ht-rules and let G,G be two hypergraphs with injective 𝑒𝑥𝑡G,𝑒𝑥𝑡G. The sequent

{!𝑓𝑚(r)rP},{𝑓𝑚(r)rP},𝒟(G)D(G)[χGG] (1)

is derivable in ILL1 if and only if there exists a derivation of a hypergraph isomorphic to G from G which uses each rule from P exactly once and that can use rules from P any number of times.

The proof of this lemma, placed in [30, Appendix A.2], is quite technical; its idea is to do a proof search using focusing [1]. Using Lemma 22 we can prove the following theorem.

Theorem 23.

Hypergraph ILL1 grammars generate the class of all recursively enumerable hypergraph languages.

Proof.

Clearly, all languages generated by hypergraph ILL1 grammars are recursively enumerable. To prove the converse, according to Proposition 9, it suffices to show that any ht-system 𝒢=N,T,P,S can be converted into a hypergraph ILL1 grammar generating the same language. Define the hypergraph ILL1 grammar 𝒢=T,S,type(S), such that

  1. 1.

    S:={!𝑓𝑚(r)rP}D(S)[hS] where hS(𝑒𝑥𝑡S(σ))=σ for σtype(S);

  2. 2.

    aa(σ1,,σn) for aT and type(a)={σ1,,σn};

  3. 3.

    ν(x).

A hypergraph H is accepted by 𝒢 if and only if the following sequent is derivable in ILL1:

{𝑙𝑎𝑏H(e)[𝑎𝑡𝑡H(e)]eEH},{ν(v)vVH}S[𝑒𝑥𝑡H].

Note that the antecedent of this sequent is the diagram of H and that the succedent equals {!𝑓𝑚(r)rP}D(S)[hS][𝑒𝑥𝑡H]={!𝑓𝑚(r)rP}D(S)[χSH]. By invertibility of the rules (R) and (L), the above sequent is equiderivable with the one

{!𝑓𝑚(r)rP},𝒟(H)D(S)[χSH]

By Lemma 22, derivability of the latter sequent is equivalent to the fact that H is derivable from S using rules from P, i.e. that HL(𝒢). Thus, L(𝒢)=L(𝒢).

This result justifies soundness of Definition 12: if hypergraph grammars based on ILL1, which includes the powerful exponential modality, were not Turing-complete, this would indicate that we do not have enough control in the grammar formalism. For example, if we did not include node-formula assignment in Definition 12, then Theorem 23 would be false.

3.2 Hypergraph MILL1 Grammars

We proceed to investigating expressive power of hypergraph MILL1 grammars. They are clearly less expressive than ht-systems because they generate only languages from NP. Nevertheless, it turns out that they as powerful as ht-systems in which the length of a derivation of a hypergraph is bounded by a linear function w.r.t. the size of the hypergraph.

Definition 24.

The size of a hypergraph H denoted by |H| is the number of nodes and hyperedges in H. A linear-time hypergraph transformation system is a ht-system 𝒢=N,T,P,S for which there is c (a time constant) such that, for each HL(𝒢), there is a derivation SH with at most c|H| steps.

Adding linear-time bound to formal grammars has a long history. Linear-time type-0 Chomsky grammars were studied in [2, 11]; linear-time one-tape Turing machines were studied in [35]; linear-time branching vector addition systems were studied in [29] in the context of commutative Lambek grammars. However, to our best knowledge, linear-time graph grammars have not appeared in the literature. Linear-time ht-systems may be considered as the hypergraph counterpart of linear-time type-0 grammars studied in [2, 11], so it is quite a natural formalism. The main result concerning them is presented below.

Theorem 25.

Each linear-time ht-system can be converted into an equivalent hypergraph MILL1 grammar.

Proof of Theorem 25.

Let 𝒢=N,T,P,S be a linear-time ht-system with the time constant c. Define the hypergraph MILL1 grammar 𝒢=T,S,type(S), such that

  1. 1.

    S:=D(S)[hS] where hS(𝑒𝑥𝑡S(σ))=σ for σtype(S);

  2. 2.

    aa(σ1,,σn)𝑓𝑚(p1)𝑓𝑚(pk) for aT, type(a)={σ1,,σn}, 0kc, and for p1,,pkP;

  3. 3.

    ν(x)𝑓𝑚(p1)𝑓𝑚(pk) for 0kc, and for p1,,pkP.

A hypergraph H is accepted by 𝒢 if and only if, for each eEH (and for each vVH), there exist at most c rules from P, which we denote by p1e,,pk(e)e (by q1v,,qk(v)v resp.), such that the sequent

{𝑙𝑎𝑏H(e)[𝑎𝑡𝑡H(e)]𝑓𝑚(p1e)𝑓𝑚(pk(e)e)eEH},{ν(v)𝑓𝑚(q1v)𝑓𝑚(qk(v)v)vVH}S[𝑒𝑥𝑡H]

is derivable in MILL1. By invertibility of (L), this is equivalent to the fact that there exists a multiset P of cardinality at most c|EH|+c|VH|=c|H| such that all its elements are from P and such that the following sequent is derivable in MILL1:

{𝑓𝑚(p)pP},𝒟(H)D(S)[χSH]

By Lemma 22, this is equivalent to the fact that there is a derivation of a hypergraph H isomorphic to H from S that uses each rule from P exactly once. Existence of P satisfying these properties is equivalent to the fact that there is a derivation of H from S of length at most c|H|, which is equivalent to HL(𝒢). Thus, L(𝒢)=L(𝒢). The question arises whether the converse holds as well. We are not going to address it in the article because of space-time limitations and also because we are mainly interested in lower bounds for the class of hypergraph MILL1 grammars. Still, we claim that it is possible to convert each hypergraph MILL1 grammar into a linear-time ht-system with non-injective rules, i.e. with rules HH where 𝑒𝑥𝑡H is allowed to be non-injective. This could be done by a straightforward (yet full of tiring technical details) encoding of MILL1 inference rules by hypergraph transformations. We leave proving that for the future work.

Speaking of upper bounds, we noted that all languages generated by hypergraph MILL1 grammars are in NP; besides, as we shall show in Theorem 30, there is an NP-complete language of string graphs generated by a hypergraph MILL1 grammars, so the NP upper bound is accurate.

Let us further explore properties of the class of languages generated by hypergraph MILL1 grammars. It turns out to be closed under intersection.

Theorem 26.

Languages generated by hypergraph MILL1 grammars are closed under intersection.

Proof.

Let 𝒢i=Ti,Si,Xi,i be two hypergraph MILL1 grammars; we aim to construct a hypergraph MILL1 grammar generating L(𝒢1)L(𝒢2). Let us assume without loss of generality that T1=T2=T; also, let us assume that predicate symbols used by 𝒢1 and 𝒢2 are disjoint. Let us denote the set of subformulas of formulas occuring in 𝒢i by Fmi (i=1,2). Note that, if X1X2, then L(𝒢1)L(𝒢2)= (hypergraphs in these languages would have different types); thus, we can assume that X1=X2 (let us denote this set by X).

Define the grammar 𝒢:=T,S,X, where S=S1S2 and is the smallest relation such that aA1A2 holds whenever aT{} and aiAi for i=1,2.

Lemma 27 (splitting lemma).
  1. 1.

    If the sequent A1,,AnB is derivable in MILL1 such that AiFm1Fm2 and BFmk for some k{1,2}, then all Ai are also from Fmk.

  2. 2.

    The sequent A1,,An,B1,,BmAB such that Ai and A are from Fm1 and Bi, B are from Fm2 is derivable in MILL1 if and only if the sequents A1,,AnA and B1,,BmB are derivable in MILL1.

Both statements are proved jointly by straightforward induction on the length of a derivation.

A hypergraph H is accepted by 𝒢 if and only if, for i=1,2, there exist functions hVi:VHFmi and hEi:EHFmi such that ihVi(v) for vVH, 𝑙𝑎𝑏H(e)ihEi(v) for eEH, and the following sequent is derivable in MILL1:

{(hE1(e)hE2(e))[𝑎𝑡𝑡H(e)]eEH},{(hV1(v)hV2(v))[v/x]vVH}(S1S2)[𝑒𝑥𝑡H].

By invertibility of (L) and splitting lemma, this is equivalent to derivability of the sequents {hEi(e)[𝑎𝑡𝑡H(e)]eEH},{hVi(v)[v/x]vVH}Si[𝑒𝑥𝑡H] for i=1,2, hence is equivalent to the fact that H belongs to L(𝒢1)L(𝒢2). An analogous technique cannot be used for Lambek categorial grammars because the Lambek calculus is non-commutative, and splitting lemma does not hold for it. In fact, since Lambek categorial grammars generate context-free languages [25], which are not closed under intersection, a similar result does not hold for Lambek categorial grammars.

4 Expressive Power of String MILL1 Grammars

Now, let us apply the results and techniques developed for hypergraph MILL1 grammars to describing the class of languages generated by string MILL1 grammars. First, Proposition 17 and Theorem 25 imply the following lower bound.

Corollary 28.

If 𝒢=N,T,P,S is a linear-time ht-system, then {wT+sg(w)L(𝒢)} is generated by a string MILL1 grammar.

Next, the following result can be proved in the same way as Theorem 26.

Theorem 29.

Languages generated by string MILL1 grammars are closed under intersection.

(Note that we cannot directly infer this theorem from Proposition 17 and Theorem 26 because of the empty string issue.) Since languages generated by string MILL1 grammars contain all context-free languages, they also contain their finite intersections, in particular, the language

{(anbn)nn>0}={an1bn1ankbnkn1,,nk}{akbn1an1bnk1ank1blk,l,n1,,nk1>0}.

It is simple to prove that languages generated by string MILL1 grammars are also closed under letter-to-letter homomorphisms, so the language {a2n2n} can be generated by a string MILL1 grammar as well. Thus, string MILL1 grammars generate languages with non-semilinear Parikh images.

Note that, for Lambek categorial grammars, there is imbalance between expressive power and algorithmic complexity. Namely, on the one hand, Lambek categorial grammars generate exactly context-free languages, all of which are polynomially parsable, but on the other hand, parsing in the Lambek calculus is an NP-complete problem [27]. This is not the case for MILL1 grammars, as the following theorem shows.

Theorem 30.

String MILL1 grammars generate an NP-complete language.

Proof.

In view of Corollary 28, it suffices to present a linear-time ht-system generating an NP-complete language of string graphs. Let P,Q1,Q2,S,T1,T2,U be nonterminal symbols such that type(Q1)=type(Q2)=, type(P)=type(S)=type(T1)=type(U)={𝐬,𝐭} and type(T2)={1,2,3,4}; let 0,1,a,b,c be terminal symbols with type {𝐬,𝐭}. Let the start hypergraph be S+Q1 (“+” is introduced in Definition 5). The rules are presented below.

  1. 1.

    S+Q1sg(SaT1aT1aT1)+Q1;

  2. 2.

    T1+Q1sg(kT1)+Q1,   T1+Q1sg(k)+Q1 for k=0,1;

  3. 3.

    S+Q1;

  4. 4.

    T2+Q1,   T2+Q1 for k=0,1;

  5. 5.

    S+Q1U+Q2;

  6. 6.

    ;

  7. 7.

    U+Q2c.

This ht-system is linear-time because each production, except for 5, which is applied at most once in any derivation, increases the number of terminal symbols. This ht-system generates hypergraphs of the form

sg(bw1bbw2bbwmbcax1ay1az1axnaynazn) (2)

such that wi,xi,yi,zi are nonempty strings over the alphabet {0,1} and such that {w1,,wm} coincides as a multiset with {xi1,yi1,zi1,,xil,yil,zil} for some 1i1<<iln. Consequently, one can reduce the exact cover problem by 3-sets to this language: if X={w1,,wm} is a set and C={{x1,y1,z1},,{xn,yn,zn}} is a collection of 3-element subsets of X, then checking whether X is the disjoint union of some sets from C is equivalent to checking whether the hypergraph (2) is generated by the ht-system.

Let us present another proof of Theorem 30 that relies on a result by Book [3]. Consider a string rewriting system 𝒮=N,T,P,S where P is a finite set of rules of the form αβ (α,β(NT) are arbitrary strings) and S(NT) is the start string. Recall that ηαθ𝒮ηβθ whenever (αβ)P (and no other pairs of strings are in the relation 𝒮); recall also that L(𝒮)={wTS𝒮w}. Let us convert 𝒮 into the ht-system 𝒢=N,T,P,sg(S) where the symbols from NT have the type {𝐬,𝐭} and P={sg(α)sg(β)(αβ)P}. (Let us assume that, in each rule αβ, α and β are nonempty.) It is straightforward to check that L(𝒢)={sg(w)wL(𝒮)}. Finally, [3, Theorem 1] says that there is a linear-time string rewriting system 𝒮 that generates an NP-complete language. Thus, if one constructs 𝒢 from it and then applies Corollary 28, then they obtain a string MILL1 grammar generating an NP-complete language.

One of the reviewers pointed out that string MILL1 grammars generating nonsemilinear languages is too much for linguistic applications, where it is widely assumed that natural languages are semilinear. The reviewer asked whether restricting MILL1 to the fragment where each (free or bound) variable occurs in each formula at most twice results in languages generated by the corresponding class of grammars being semilinear. I am afraid that, even with this restriction, string MILL1 grammars generate some non-semilinear and NP-complete languages. Let us consider the above construction involving string rewriting systems. If, for example, ABBCD is a string rewriting rule, then

𝑓𝑚(sg(AB)sg(BCD))=v1.v2.[(x.A(v1,x)B(x,v2)ν(v1)ν(x)ν(v2))(y.z.B(v1,y)C(y,z)D(z,v2)ν(v1)ν(y)ν(z)ν(v2))].

In a formula of the form 𝑓𝑚(sg(α)sg(β)), each variable occurs at most four times. However, we claim that one could remove ν predicates everywhere, which would result in each variable occurring in each formula at most twice. We also claim that Lemma 22 would remain true without ν predicates in formulas in case where we consider only string graphs. Thus, we can use Book’s result from [3] to generate an NP-complete and a non-semilinear language by a grammar over the restricted fragment of MILL1. We do not provide formal proofs but leave them for the future work.

5 Hypergraph Language Semantics

Now, let us proceed to model-theoretic investigations into MILL1. Our objective is to generalise language models for the Lambek calculus to MILL1 and to devise hypergraph language models. This will enable one to regard MILL1 as a logic for reasoning about hypergraph resources. The most important question is how the composition of such resources should be defined: if H1,H2 are two hypergraphs, then how should one understand “H1H2”?

Language semantics for the Lambek calculus, algebraically speaking, is a mapping of L formulae to a free semigroup of words which interprets product AB as elementwise product of interpretations of A and B. What is the hypergraph counterpart of free semigroups? In the field of hyperedge replacement, there are algebras of hypergraphs called HR-algebras [6, 7, 31]. They include the parallel composition operation and source manipulating operations. Parallel composition is a way of gluing hypergraphs defined as follows.

Definition 31.

Let H1 and H2 be hypergraphs. Let be the smallest equivalence relation on VH1VH2 such that 𝑒𝑥𝑡H1(σ)𝑒𝑥𝑡H2(σ) for σtype(H1)type(H2). Then, parallel composition H1//H2 is the hypergraph H such that type(H)=type(H1)type(H2); VH=(VH1VH2)/, EH=EH1EH2; 𝑎𝑡𝑡H(e)(σ)=[𝑎𝑡𝑡Hi(e)(σ)], 𝑙𝑎𝑏H(e)=𝑙𝑎𝑏Hi(e) for eEHi; 𝑒𝑥𝑡H(σ)=[𝑒𝑥𝑡Hi(σ)] for σtype(H1)type(H2).

Informally, H1//H2 is obtained by taking the disjoint union of H1 and H2 and fusing 𝑒𝑥𝑡H1(σ) with 𝑒𝑥𝑡H2(σ) for σtype(H1)type(H2). This operation is illustrated on Figure 3. Note that parallel composition is associative and commutative.

Figure 3: Scheme of parallel composition of H1 and H2 (left) and an example of substitution of a hypergraph according to h where h(x)=h(y)=σ, h(z)=τ, and h(t) is undefined (right).

Other operations used in HR-algebras allow one to reassign selectors to external nodes, to make an external node non-external, or to fuse some external nodes. We shall use an operation that unifies all the three manipulations; we shall call it substitution.

Definition 32.

Given a hypergraph H and a partial function hΣ×Σ, let be the smallest equivalence relation such that 𝑒𝑥𝑡H(σ1)𝑒𝑥𝑡H(σ2) whenever h(σ1)=h(σ2). Then 𝑠𝑢𝑏h(H) is the hypergraph H such that type(H)=h(type(H)); VH=VH/; EH=EH; 𝑎𝑡𝑡H(e)(σ)=[𝑎𝑡𝑡H(e)(σ)], 𝑙𝑎𝑏H(e)=𝑙𝑎𝑏H(e) for eE; 𝑒𝑥𝑡H(h(σ))=[𝑒𝑥𝑡H(σ)].

One can compare the substitution operation with the operations of source renaming and source fusion from [31] and verify that the former one is interdefinable with the latter ones (in presence of parallel composition). Hence, one can use // and 𝑠𝑢𝑏h as basic operations of HR-algebras. Nicely, exactly these operations can also be used for defining hypergraph language models, which we are going to do now. Let K0:=,,,, be the empty hypergraph. From now on, Σ=Var (i.e. selectors and variables are the same objects).

Definition 33.

A hypergraph language model is a pair T,u where T is a Σ-typed alphabet and u:Fm(MILL1)𝒫((T)) is a function mapping formulas of MILL1 to sets of abstract hypergraphs over T which satisfies the following conditions:

  1. 1.

    𝑠𝑢𝑏h(u(A))u(A[h]) for any total function h:ΣΣ;

  2. 2.

    u(AB)=u(A)//u(B);

  3. 3.

    u(AB)={HHu(A)(H//Hu(B))};

  4. 4.

    u(xA)=yVaru(A[y/x]);

  5. 5.

    u(xA)=yVaru(A[y/x]).

A sequent A1,,AnB is true in this model if u(A1)////u(An)u(B) (for n=0, if K0u(B)).

This semantics can be viewed as an instance of intuitionistic phase semantics [15] with the commutative monoid ((T),//,K0) and with the trivial closure operator Cl(X)=X.

The first property of u in Definition 33 relates substitution as a logical operation to substitution as a hypergraph transformation; without it, u(A) and u(A[h]) would be unrelated, which is undesirable. Besides, this property is used to prove correctness. Note that, if h:ΣΣ is a bijection, then u(A[h])=𝑠𝑢𝑏h(u(A)) (apply property 1 twice). Quantifiers are interpreted as additive conjunction and disjunction, which reflects their behaviour correctly.

Lemma 34.
  1. 1.

    u(A)//u(B)u(C) if and only if u(A)u(BC).

  2. 2.

    If u(A)u(B), then u(A[h])u(B[h]) for any substitution h.

Proof.

  1. 1.

    Trivially follows from the definition of a model.

  2. 2.

    Clearly, K0//H=H for any H. Therefore, u(A)u(B) implies K0u(AB). Consequently, according to item 1 of Definition 33, K0=𝑠𝑢𝑏h(K0)u(A[h]B[h]). This implies that u(A[h])u(B[h]), as desired.

The main result is soundness of MILL1 and completeness of its fragment MILL1(,) w.r.t. hypergraph language models.

Theorem 35.
  1. 1.

    MILL1 is sound w.r.t. hypergraph language models.

  2. 2.

    MILL1(,) is complete w.r.t. hypergraph language models.

Proof.

Soundness can be checked straightforwardly by showing that the conclusion of each rule with true premises is also true. The only nontrivial cases are the rules (L) and (R). Assume that Γ,A[z/x]B where z does not occur freely in Γ,B is true in a model T,u. Without loss of generality, let us assume that Γ is empty (otherwise, we can move it to the succeedent using Lemma 34). Under this assumption, we are given that u(A[z/x])u(B). By Lemma 34, for each yVar, u(A[y/x])=u(A[z/x][y/z])u(B[y/z])=u(B). This proves that u(xA)u(B). The case (R) is dealt with similarly.

Completeness of MILL1(,) is proved by constructing a canonical model T,u. Before we do this, let us introduce a new notion used in the construction.

Definition 36.

Assume that a countable sequence of variables ξ1,ξ2, is fixed. Given a formula A, let us read it from left to right and replace the i-th occurrence of a free variable from the left by ξi. We denote the resulting formula by A.

For example, (x(A(x,y,y)zB(z,y,t)))=x(A(x,ξ1,ξ2)zB(z,ξ3,ξ4)). We shall use formulas of the form A as labels of hyperedges in the canonical model with type(A)=FVar(A). So, T:={AAFm(MILL1(,))}. The idea is that, in the canonical model, variables are represented by nodes, while hyperedge labels do not carry information about variables (ξ1,ξ2, are, informally, placeholders for variables).

Given a sequent ΓA where Γ=A1,,An (n0) and given two finite sets of variables X,Y such that YFVar(Γ)X, let us define the hypergraph HΓ;AX;Y=V,E,𝑎𝑡𝑡,𝑙𝑎𝑏,𝑒𝑥𝑡 as follows: V=FVar(Γ)X; E={e1,,en}; 𝑎𝑡𝑡(ei)(x)=hi(x) for xFVar(Ai) where hi:ΣΣ is a function such that Ai=Ai[hi]; 𝑙𝑎𝑏(ei)=Ai; 𝑒𝑥𝑡(x)=x for x(VFVar(A))Y (and undefined otherwise).

Let u(A):={HΓ;AX;YΓAis derivable in MILL1(,)}. The proof that T,u is a hypergraph language model is quite technical and it can be found in [30, Appendix A.4]. Now, assume that A1,,AnB is true in this model. Then, K0u(A1((AnB))), i.e. K0=H;A1((AnB))X;Y, and A1((AnB)) is derivable in MILL1(,). By invertibility of (R), the sequent A1,,AnB is derivable.

6 Conclusion

As we have shown, first-order intuitionistic linear logic does have strong connections to the hypergraph grammar theory, namely, to hypergraph transformation systems and to HR-algrebras. The notion of hypergraph first-order categorial grammars naturally and simply extends the concept of Lambek categorial grammars to hypergraphs. Developing hypergraph MILL1 grammars and relating them to hypergraph transformation systems gave us useful insights into expressive power of string MILL1 grammars. In turn, the notion of a hypergraph language model revealed a previously unknown connection of first-order intuitionistic linear logic to the apparatus of HR-algebras, the latter having been studied mainly in the context of monadic second-order definability.

Two questions remain open for the future work. The first one is whether the converse to Theorem 25 holds; more generally, it is desirable to characterise precisely hypergraph MILL1 grammars in terms of hypergraph transformation systems. The second one is whether MILL1 is complete w.r.t. hypergraph language models.

References

  • [1] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992. doi:10.1093/logcom/2.3.297.
  • [2] Ronald V. Book. Time-bounded grammars and their languages. Journal of Computer and System Sciences, 5(4):397–429, 1971. doi:10.1016/S0022-0000(71)80025-9.
  • [3] Ronald V. Book. On the complexity of formal grammars. Acta Informatica, 9:171–181, 1978. doi:10.1007/BF00289076.
  • [4] Wojciech Buszkowski. Compatibility of a categorial grammar with an associated category system. Mathematical Logic Quarterly, 28(14-18):229–238, 1982. doi:10.1002/malq.19820281407.
  • [5] Wojciech Buszkowski. Type Logics in Grammar, pages 337–382. Springer Netherlands, Dordrecht, 2003. doi:10.1007/978-94-017-3598-8_12.
  • [6] Bruno Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Information and Computation, 85(1):12–75, 1990. doi:10.1016/0890-5401(90)90043-H.
  • [7] Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2012.
  • [8] Frank Drewes, Hans-Jörg Kreowski, and Annegret Habel. Hyperedge replacement graph grammars. In Grzegorz Rozenberg, editor, Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, pages 95–162. World Scientific, 1997. doi:10.1142/9789812384720_0002.
  • [9] Joost Engelfriet. Context-free graph grammars. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 125–213. Springer, 1997. doi:10.1007/978-3-642-59126-6_3.
  • [10] Jean-Yves Girard. Linear logic: A survey. In Friedrich L. Bauer, Wilfried Brauer, and Helmut Schwichtenberg, editors, Logic and Algebra of Specification, pages 63–112, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. doi:10.1007/978-3-642-58041-3_3.
  • [11] Aleksei Gladkii. On complexity of inference in phase-structure grammars. Algebra i Logika. Sem. (in Russian), 3(5-6):29–44, 1964.
  • [12] Annegret Habel. Hyperedge Replacement: Grammars and Languages, volume 643 of Lecture Notes in Computer Science. Springer, 1992. doi:10.1007/BFB0013875.
  • [13] Annegret Habel, Jürgen Müller, and Detlef Plump. Double-pushout graph transformation revisited. Mathematical Structures in Computer Science, 11(5):637–688, 2001. doi:10.1017/S0960129501003425.
  • [14] Laura Kallmeyer. Parsing Beyond Context-Free Grammars. Springer Berlin Heidelberg, 2010. doi:10.1007/978-3-642-14846-0.
  • [15] Max I. Kanovich, Mitsuhiro Okada, and Kazushige Terui. Intuitionistic phase semantics is almost classical. Mathematical. Structures in Comp. Sci., 16(1):67–86, 2006. doi:10.1017/S0960129505005062.
  • [16] Yuichi Komori. Predicate logics without the structure rules. Studia Logica, 45(4):393–404, 1986. doi:10.1007/bf00370272.
  • [17] Barbara König, Dennis Nolte, Julia Padberg, and Arend Rensink. A tutorial on graph transformation. In Reiko Heckel and Gabriele Taentzer, editors, Graph Transformation, Specifications, and Nets - In Memory of Hartmut Ehrig, volume 10800 of Lecture Notes in Computer Science, pages 83–104. Springer, 2018. doi:10.1007/978-3-319-75396-6_5.
  • [18] Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154–170, 1958. doi:10.1080/00029890.1958.11989160.
  • [19] Michael Moortgat. Multimodal linguistic inference. Journal of Logic, Language and Information, 5(3–4):349–385, 1996. doi:10.1007/bf00159344.
  • [20] Richard Moot. Extended Lambek calculi and first-order linear logic. In Claudia Casadio, Bob Coecke, Michael Moortgat, and Philip J. Scott, editors, Categories and Types in Logic, Language, and Physics - Essays Dedicated to Jim Lambek on the Occasion of His 90th Birthday, volume 8222 of Lecture Notes in Computer Science, pages 297–330. Springer, 2014. doi:10.1007/978-3-642-54789-8_17.
  • [21] Richard Moot. Hybrid type-logical grammars, first-order linear logic and the descriptive inadequacy of lambda grammars, 2014. arXiv:1405.6678.
  • [22] Richard Moot and Mario Piazza. Linguistic applications of first order intuitionistic linear logic. Journal of Logic, Language and Information, 10(2):211–232, 2001. doi:10.1023/a:1008399708659.
  • [23] Richard Moot and Christian Retoré. The Logic of Categorial Grammars - A Deductive Account of Natural Language Syntax and Semantics, volume 6850 of Lecture Notes in Computer Science. Springer, 2012. doi:10.1007/978-3-642-31555-8.
  • [24] Glyn Morrill, Oriol Valentín, and Mario Fadda. The displacement calculus. Journal of Logic, Language and Information, 20(1):1–48, 2010. doi:10.1007/s10849-010-9129-2.
  • [25] Mati Pentus. Lambek grammars are context free. In Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pages 429–433, 1993. doi:10.1109/LICS.1993.287565.
  • [26] Mati Pentus. Models for the Lambek calculus. Ann. Pure Appl. Log., 75(1-2):179–213, 1995. doi:10.1016/0168-0072(94)00063-9.
  • [27] Mati Pentus. Lambek calculus is NP-complete. Theoretical Computer Science, 357(1):186–201, 2006. Clifford Lectures and the Mathematical Foundations of Programming Semantics. doi:10.1016/j.tcs.2006.03.018.
  • [28] Tikhon Pshenitsyn. Hypergraph Lambek grammars. Journal of Logical and Algebraic Methods in Programming, 129:100798, 2022. doi:10.1016/j.jlamp.2022.100798.
  • [29] Tikhon Pshenitsyn. Commutative Lambek grammars. Journal of Logic, Language and Information, 32(5):887–936, 2023. doi:10.1007/s10849-023-09407-z.
  • [30] Tikhon Pshenitsyn. First-order intuitionistic linear logic and hypergraph languages, 2025. doi:10.48550/arXiv.2502.05816.
  • [31] Grzegorz Rozenberg. Handbook of Graph Grammars and Computing by Graph Transformation. World Scientific, 1997. doi:10.1142/3303.
  • [32] Sylvain Salvati. A note on the complexity of abstract categorial grammars. In Christian Ebert, Gerhard Jäger, and Jens Michaelis, editors, The Mathematics of Language, pages 266–271, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg.
  • [33] Harold Shellinx. Some syntactical observations on linear logic. Journal of Logic and Computation, 1(4):537–559, September 1991. doi:10.1093/logcom/1.4.537.
  • [34] Sergey Slavnov. Making first order linear logic a generating grammar. Logical Methods in Computer Science, Volume 19, Issue 4, 2023. doi:10.46298/lmcs-19(4:11)2023.
  • [35] Kohtaro Tadaki, Tomoyuki Yamakami, and Jack C.H. Lin. Theory of one-tape linear-time Turing machines. Theoretical Computer Science, 411(1):22–43, 2010. doi:10.1016/j.tcs.2009.08.031.
  • [36] Tadahiro Uesu. A system of graph grammars which generates all recursively enumerable sets of labelled graphs. Tsukuba Journal of Mathematics, 2(none):11–26, 1978. doi:10.21099/tkbjm/1496158502.
  • [37] Johan van Benthem. Language in Action: Categories, Lambdas and Dynamic Logic. MIT Press, 1995.