Home   Papers   Teaching   CV   Leisure

|Esperanto| |English|

Some publications of Mati Pentus

In this file

See also papers in Russian (with English abstracts).

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Papers in English

(preliminary versions)
 

Equivalent Types in Lambek Calculus and Linear Logic

Mati Pentus

Abstract

In 1958 J. Lambek introduced a calculus L of syntactic types and defined an equivalence relation on types: "x~y means that there exists a sequence x=x1,...,xn=y (n>0), such that xi->xi+1 or xi+1->xi (0<i<n)". We show that this equivalence of types is decidable for directed and non-directed Lambek calculi and for multiplicative fragments of ordinary and non-commutative linear logics. Moreover, we characterize equivalent types in these calculi in terms of simple derivability invariants (primitive type counts, balance, etc.).

 

BibTeX

@techreport{Pentus1992LCS2,
author="Pentus, M.",
title="Equivalent Types in {L}ambek Calculus and Linear Logic",
type="MIAN Prepublication Series for Logic and Computer Science",
institution="Steklov Mathematical Institute",
number="LCS-92-02",
address="Moscow",
year=1992,
month="April",
note="21 pages",
}

Download

PDF (172 KiB)
 

Lambek grammars are context free

Mati Pentus

Abstract

In this paper the Chomsky Conjecture is proved: all languages recognized by the Lambek calculus are context free.

 

BibTeX

@inproceedings{Pentus93LICS,
author="Pentus, M.",
title="{L}ambek grammars are context free",
booktitle="Proceedings of the 8th Annual {IEEE} Symposium on Logic in Computer Science",
pages="429--433",
publisher="{IEEE} Computer Society Press",
address="Los Alamitos, California",
year=1993
}

Download

DVI.zip (16 KiB)
PostScript (646 KiB)
PostScript.zip (353 KiB)
PDF (218 KiB)
 

The conjoinability relation in Lambek calculus and linear logic

Mati Pentus

Abstract

In 1958 J. Lambek introduced a calculus L of syntactic types and defined an equivalence relation on types: "x~y means that there exists a sequence x=x1,...,xn=y (n>0), such that xi->xi+1 or xi+1->xi (0<i<n)". He pointed out that x~y if and only if there is join z such that x->z and y->z.

This paper gives an effective characterization of this equivalence for the Lambek calculi L and LP, and for the multiplicative fragments of Girard's and Yetter's linear logics. Moreover, for the non-directed Lambek calculus LP and the multiplicative fragment of Girard's linear logic, we present linear time algorithms deciding whether two types are equal, and finding a join for them if they are.

 

BibTeX

@techreport{Pentus93ILLC,
author="Pentus, M.",
title="The conjoinability relation in {L}ambek calculus and linear logic",
type="ILLC Prepublication Series",
number="ML--93--03",
institution="Institute for Logic, Language and Computation, University of Amsterdam",
year=1993
}

Download

DVI.zip (27 KiB)
PostScript (1089 KiB)
PostScript.zip (589 KiB)
PDF (376 KiB)
 

Models for the Lambek calculus

Mati Pentus

Abstract

We prove that the Lambek calculus is complete w.r.t. L-models, i.e., free semigroup models. We also prove the completeness w.r.t. relativized relational models over the natural linear order of integers.

 

BibTeX

@article{Pentus95APAL,
author="Pentus, M.",
title="Models for the {L}ambek calculus",
journal="Annals of Pure and Applied Logic",
volume=75,
number="1--2",
pages="179--213",
year=1995
}

Download

DVI.zip (48 KiB)
PostScript (1282 KiB)
PostScript.zip (657 KiB)
PDF (490 KiB)
 

Product-free Lambek calculus and context-free grammars

Mati Pentus

Abstract

In this paper we prove the Chomsky Conjecture (all languages recognized by the Lambek calculus are context-free) for both the full Lambek calculus and its product-free fragment. For the latter case we present a construction of context-free grammars involving only product-free types.

 

BibTeX

@article{Pentus97JSL,
author="Pentus, M.",
title="Product-free {L}ambek calculus and context-free grammars",
journal="Journal of Symbolic Logic",
volume=62,
number="2",
pages="648--660",
year=1997
}

Download

DVI.zip (22 KiB)
PostScript (935 KiB)
PostScript.zip (505 KiB)
PDF (321 KiB)
 

Free monoid completeness of the Lambek calculus allowing empty premises

Mati Pentus

Abstract

We prove that the Lambek syntactic calculus allowing empty premises is complete with respect to the class of all free monoid models (i. e., the class of all string models, allowing the empty string).

 

BibTeX

@incollection{Pentus98FMC,
author="Pentus, M.",
title="Free monoid completeness of the {L}ambek calculus allowing empty premises",
booktitle="Logic Colloquium '96: proceedings of the colloquium held in San Sebastian, Spain, July 9--15, 1996",
editor="Larrazabal, J.~M. and Lascar D. and Mints G.",
publisher="Springer",
pages="171--209",
note="Lecture Notes in Logic, 12",
year=1998
}

Download

DVI.zip (55 KiB)
PostScript (1661 KiB)
PostScript.zip (870 KiB)
PDF (617 KiB)
 

Lambek Calculus and Formal Grammars

Mati Pentus

Abstract

We prove context-freeness of languages generated by categorial grammars based on any of the following calculi: the Lambek calculus, the Lambek calculus allowing empty premises, the Lambek calculus with the unit, the multiplicative fragment of cyclic linear logic.

We prove that all elementary fragments of the Lambek calculus have the Craig interpolation property.

We prove that the conjoinability relation (on syntactic types) is decidable and that it is complete with respect to the free group interpretation.

This is the English translation of the Ph.D. thesis of Mati Pentus.

 

BibTeX

@incollection{Pentus99AMS,
author="Pentus, M.",
title="{L}ambek Calculus and Formal Grammars",
booktitle="Provability, Complexity, Grammars",
publisher="American Mathematical Society",
address="Providence, Rhode Island",
number=192,
series="American Mathematical Society Translations--Series 2",
pages="57--86",
year=1999,
}

Download

DVI.zip (49 KiB)
PostScript (1596 KiB)
PostScript.zip (844 KiB)
PDF (577 KiB)
 

Lambek calculus is NP-complete

Mati Pentus

Abstract

We prove that for both the Lambek calculus L and the Lambek calculus allowing empty premises L* the derivability problem is NP-complete. It follows that also for the multiplicative fragments of cyclic linear logic and noncommutative linear logic the derivability problem is NP-complete.

 

BibTeX

@techreport{Pentus2003CUNY,
author="Pentus, M.",
title="{L}ambek calculus is {NP}-complete",
type="CUNY Ph.D. Program in Computer Science Technical Report",
institution="CUNY Graduate Center",
number="TR--2003005",
address="New York",
year=2003,
month="May",
note="http://www.cs.gc.cuny.edu/tr/techreport.php?id=79",
note="20 pages",
}

Download

DVI.zip (82 KiB)
PostScript.zip (200 KiB)
PDF (306 KiB)
 
Home   Papers   Teaching   CV   Leisure
 
MPLocation: http://lpcs.math.msu.su/~pentus/abstr.htm
Last modified 14.11.2006.
Mati Pentus
Tel/fax: + 7 - 495 - 939 30 31