Hejmo   Artikoloj   Instruado   Vivprotokolo   Libertempo

|Esperante| |English|

Kelkaj anglalingvaj publikaĵoj de Mati Pentus

En tiu ĉi dosiero

Vidu ankaŭ ruslingvajn artikolojn.

La dokumentoj, cirkuligitaj per tiu ĉi servilo, estas liveritaj de la kontribuantaj aŭtoroj kiel rimedo por certigi ĝustatempan dissemon de sciencaj kaj teknikaj verkoj sur nekomerca bazo. Kopirajton kaj ĉiujn rajtojn, konsistantajn ĝin, plu tenas la aŭtoroj aŭ aliaj kopirajtposedantoj, malgraŭ tio, ke ili proponis la verkojn tie ĉi elektronike. Estas supozata, ke ĉiuj personoj, kopiantaj la informon, sekvos la kondiĉojn kaj limigojn, altruditajn de la kopirajto de la aŭtoroj. Tiuj ĉi verkoj ne povas esti reafiŝitaj sen eksplicita permeso de la kopirajtposedanto.

Anglalingvaj artikoloj

(preparaj versioj)
 

Ekvivalentaj tipoj en la lambek-kalkulo kaj lineara logiko

Mati Pentus

Resumo

En 1958 J. Lambek enkondukis kalkulon L de sintaksaj tipoj kaj difinis ekvivalentrilaton en la aro de tipoj: "x~y signifas, ke ekzistas tia finia vico x=x1,...,xn=y (n>0), ke xi->xi+1 aŭ xi+1->xi (0<i<n)". Ni montras, ke tiu ekvivalentrilato de tipoj estas decidebla por la direkta kaj nedirekta lambek-kalkuloj kaj por la multiplikaj fragmentoj de la ordinara kaj nekomuteca linearaj logikoj. Krome, ni karakterizas ekvivalentajn tipojn en tiuj kalkuloj per simplaj deriveblecinvariantoj (kalkulado de primitivaj tipoj, bilanco ktp).

 

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",
}

Elŝuti

PDF (172 Kbajt)
 

Lambekaj gramatikoj estas senkuntekstaj
(angle)

Mati Pentus

Resumo

Ni pruvas la konjekton de Chomsky: ĉiuj lingvoj, generataj de la lambek-kalkulo, estas senkuntekstaj.

 

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
}

Elŝuti

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

La rilato de kunigebleco en la lambek-kalkulo kaj lineara logiko
(angle)

Mati Pentus

Resumo

En 1958 J. Lambek enkondukis kalkulon L de sintaksaj tipoj kaj difinis ekvivalentrilaton en la aro de tipoj: "x~y signifas, ke ekzistas tia finia vico x=x1,...,xn=y (n>0), ke xi->xi+1 aŭ xi+1->xi (0<i<n)". Li montris, ke x~y, se kaj nur se ekzistas tia tipo z, ke x->z kaj y->z (alivorte, ekzistas kunigilo de x kaj y).

Tiu ĉi artikolo donas efektivan kriterion por tiu ekvivalentrilato en la lambek-kalkuloj L kaj LP, kaj en la multiplikaj fragmentoj de la linearaj logikoj de Girard kaj Yetter. Krome, por la nedirekta lambek-kalkulo LP kaj la multiplika fragmento de la lineara logiko de Girard ni prezentas algoritmon, funkciantan en lineara tempo, por decidi, ĉu du tipoj estas ekvivalentaj, kaj por trovi kunigilon, se ili estas ekvivalentaj.

 

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
}

Elŝuti

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

Modeloj por la lambek-kalkulo
(angle)

Mati Pentus

Resumo

Ni pruvas, ke la lambek-kalkulo estas kompleta rilate al la L-modeloj, tio estas la modeloj sur liberaj duongrupoj. Ni pruvas ankaŭ la kompletecon rilate al la relativigitaj rilataj modeloj super la natura ordo de entjeroj.

 

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
}

Elŝuti

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

Senproduta lambek-kalkulo kaj senkuntekstaj gramatikoj
(angle)

Mati Pentus

Resumo

Ni pruvas la konjekton de Chomsky (ĉiuj lingvoj, generataj de la lambek-kalkulo, estas senkuntekstaj) por la plena lambek-kalkulo kaj ĝia senproduta fragmento. En la pruvo pri tiu fragmento ni prezentas metodon por konstrui senkuntekstan gramatikon, uzantan nur senprodutajn tipojn.

 

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
}

Elŝuti

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

Kompleteco de la lambek-kalkulo, allasanta malplenajn antaŭmembrojn, rilate al la modeloj sur liberaj monoidoj
(angle)

Mati Pentus

Resumo

Ni pruvas, ke la lambeka sintaksa kalkulo, allasanta malplenajn antaŭmembrojn, estas kompleta rilative al la klaso de ĉiuj modeloj sur liberaj monoidoj (tio estas la klaso de ĉiuj signoĉenaj modeloj, allasantaj la malplenan signoĉenon).

 

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
}

Elŝuti

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

La lambek-kalkulo kaj formalaj gramatikoj
(angle)

Mati Pentus

Resumo

Ni pruvas senkuntekstecon de la lingvoj, generitaj de kategoriaj gramatikoj, bazitaj sur iu ajn el la sekvaj kalkuloj: (1) la lambek-kalkulo, (2) la lambek-kalkulo, allasanta malplenajn antaŭmembrojn, (3) la lambek-kalkulo kun la unuo kaj (4) la multiplika fragmento de la cikla lineara logiko.

Ni pruvas, ke ĉiuj elementaraj fragmentoj de la lambek-kalkulo havas la krejgan interpolan econ.

Ni pruvas, ke la rilato de kunigebleco (sur sintaksaj tipoj) estas decidebla kaj ke ĝi estas kompleta rilate al la modelo sur libera grupo.

Tio estas la angla traduko de la doktora disertacio de 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,
}

Elŝuti

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

La Lambek-kalkulo estas NP-kompleta

Mati Pentus

Resumo

Ni pruvas, ke por la lambek-kalkulo L kaj por la lambek-kalkulo, allasanta malplenajn antaŭmembrojn, L* la problemo pri derivebleco estas NP-kompleta. Sekve ankaŭ por la multiplikaj fragmentoj de la cikla lineara logiko kaj de la nekomuteca lineara logiko la problemo pri derivebleco estas NP-kompleta.

 

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",
}

Elŝuti

DVI.zip (82 Kbajt)
PostScript.zip (200 Kbajt)
PDF (306 Kbajt)
 
Hejmo   Artikoloj   Instruado   Vivprotokolo   Libertempo
 
MPAdreso: http://lpcs.math.msu.su/~pentus/abstreo.htm
Laste modifita 14.11.2006.
Mati Pentus
Tel/fakso: + 7 - 495 - 939 30 31