Publications

[CGT12] Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. Algebraic proof theory for substructural logics: Cut-elimination and completions. Ann. Pure Appl. Logic, Vol. 163, No. 3, pp. 266-290, 2012.
[ bib | http | .pdf ]
We carry out a unified investigation of two prominent topics in proof theory and order algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices.

We introduce the substructural hierarchy - a new classification of logical axioms (algebraic equations) over full Lambek calculus FL, and show that a stronger form of cut-elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide up to the level N2 in the hierarchy. Negative results, which indicate limitations of cut-elimination and the MacNeille completion, as well as of the expressive power of structural sequent calculus rules, are also provided.

Our arguments interweave proof theory and algebra, leading to an integrated discipline which we callalgebraic proof theory.

[Ter12] Kazushige Terui. Semantic evaluation, intersection types and complexity of simply typed lambda calculus, 2012. Submitted.
[ bib | .pdf ]
Consider the following problem: given a simply typed lambda term of Boolean type and of order r, does it normalize to ``true''? A related problem is: given a term M of word type and of order r together with a finite automaton D, does D ``accepts'' the normal form of M? We prove that these problems are n-EXPTIME complete for r= 2n +2, and n-EXPSPACE complete for r = 2n + 3.

While the hardness part is relatively easy, the membership part is not so obvious; in particular, simply applying beta reduction does not work. Some preceding works employ semantic evaluation in the category of sets and functions, but it is not efficient enough for our purpose.

We present an algorithm for the above type of problem that is a fine blend of beta reduction, Krivine abstract machine and evaluation in the category of posets and order ideals. The semantic evaluation can also be presented as intersection type checking.

[Ter11] Kazushige Terui. Computational ludics. Theor. Comput. Sci., Vol. 412, No. 20, pp. 2048-2071, 2011.
[ bib | http | .pdf ]
We reformulate the theory of ludics introduced by J.-Y. Girard from a computational point of view. We introduce a handy term syntax for designs, the main objects of ludics. Our syntax also incorporates explicit cuts for attaining computational expressivity. In addition, we consider design generators that allow for finite representation of some infinite designs. A normalization procedure in the style of Krivine's abstract machine directly works on generators, giving rise to an effective means of computation over infinite designs. The acceptance relation between machines and words, a basic concept in computability theory, is well expressed in ludics by the orthogonality relation between designs. Fundamental properties of ludics are then discussed in this concrete context. We prove three characterization results that clarify the computational powers of three classes of designs. (i) Arbitrary designs may capture arbitrary sets of finite data. (ii) When restricted to finitely generated ones, designs exactly capture the recursively enumerable languages. (iii) When further restricted to cut-free ones as in Girard's original definition, designs exactly capture the regular languages. We finally describe a way of defining data sets by means of logical connectives, where the internal completeness theorem plays an essential role.
[HT11] Rostislav Horcík and Kazushige Terui. Disjunction property and complexity of substructural logics. Theor. Comput. Sci., Vol. 412, No. 31, pp. 3992-4006, 2011.
[ bib | http | .pdf ]
We systematically identify a large class of substructural logics that satisfy the disjunction property (DP), and show that every consistent substructural logic with the DP is PSPACE-hard. Our results are obtained by using algebraic techniques. PSPACE-completeness for many of these logics is furthermore established by proof theoretic arguments.
[CGT11] Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. Macneille completions of fl-algebras. Algebra Universalis, Vol. 66, No. 4, pp. 405-420, 2011.
[ bib | http | .pdf ]
We show that a large number of equations are preserved by Dedekind-MacNeille completions when applied to subdirectly irreducible FL-algebras/residuated lattices. These equations are identified in a systematic way, based on proof-theoretic ideas and techniques in substructural logics. It follows that many varieties of Heyting algebras and FL-algebras admit completions.
[BT10c] Aloïs Brunel and Kazushige Terui. Church => scott = ptime: an application of resource sensitive realizability. In DICE, pp. 31-46, 2010.
[ bib | http | http ]
We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed by a standard non-linear type `Church,' while the Scott encodings (purely linear representations of words) are by a linear type `Scott.' We give a characterization of polynomial time functions, which is derived from (Leivant and Marion 93): a function is computable in polynomial time if and only if it can be represented by a term of type Church => Scott.

To prove soundness, we employ a resource sensitive realizability technique developed by Hofmann and Dal Lago.

[BT10a] Michele Basaldella and Kazushige Terui. Infinitary completeness in ludics. In LICS, pp. 294-303, 2010.
[ bib | http | .pdf ]
Traditional Gödel completeness holds between finite proofs and infinite models over formulas of finite depth, where proofs and models are heterogeneous. Our purpose is to provide an interactive form of completeness between infinite proofs and infinite models over formulas of infinite depth (that include recursive types), where proofs and models are homogenous.

We work on a nonlinear extension of ludics, a monistic variant of game semantics which has the same expressive power as the propositional fragment of polarized linear logic. In order to extend the completeness theorem of the original ludics to the infinitary setting, we modify the notion of orthogonality by defining it via safety rather than termination of the interaction. Then the new completeness ensures that the universe of behaviours (interpretations of formulas) is Cauchy-complete, so that every recursive equation has a unique solution.

Our work arises from studies on recursive types in denotational and operational semantics, but is conceptually simpler, due to the purely logical setting of ludics, the completeness theorem, and use of coinductive techniques.

[BT10b] Michele Basaldella and Kazushige Terui. On the meaning of logical completeness. Logical Methods in Computer Science, Vol. 6, No. 4, 2010.
[ bib | http | http ]
Gödel's completeness theorem is concerned with provability, while Girard's theorem in ludics (as well as full completeness theorems in game semantics) are concerned with proofs. Our purpose is to look for a connection between these two disciplines. Following a previous work [3], we consider an extension of the original ludics with contraction and universal nondeterminism, which play dual roles, in order to capture a polarized fragment of linear logic and thus a constructive variant of classical propositional logic. We then prove a completeness theorem for proofs in this extended setting: for any behaviour (formula) A and any design (proof attempt) P, either P is a proof of A or there is a model M of the orthogonal of A which defeats P. Compared with proofs of full completeness in game semantics, ours exhibits a striking similarity with proofs of Goedel's completeness, in that it explicitly constructs a countermodel essentially using Koenig's lemma, proceeds by induction on formulas, and implies an analogue of Loewenheim-Skolem theorem.
[ACT09] Agata Ciabattoni, Lutz Straßburger and Kazushige Terui. Expanding the realm of systematic proof theory, 2009. CSL.
[ bib | .pdf ]
This paper is part of a general project of developing a systematic and algebraic proof theory for nonclassical logics. Generalizing our previous work on intuitionistic-substructural axioms and single-conclusion (hyper)sequent calculi, we define a hierarchy on Hilbert axioms in the language of classical linear logic without exponentials. We then give a systematic procedure to transform axioms up to the level P3' of the hierarchy into inference rules in multiple-conclusion (hyper)sequent calculi, which enjoy cut-elimination under a certain condition. This allows a systematic treatment of logics which could not be dealt with in the previous approach. Our method also works as a heuristic principle for finding appropriate rules for axioms located at levels higher than P3'. The case study of Abelian and Lukasiewicz logic is outlined.
[BT09b] Michele Basaldella and Kazushige Terui. On the meaning of logical completeness. In TLCA, pp. 50-64, 2009.
[ bib | http | .pdf ]
Gödel's completeness theorem is concerned with provability, while Girard's theorem in ludics (as well as full completeness theorems in game semantics) is concerned with proofs. Our purpose is to look for a connection between these two disciplines. Following a previous work (Faggian, Basaldella 09), we consider an extension of the original ludics with contraction and universal nondeterminism, which play dual roles, in order to capture a polarized fragment of linear logic and thus a constructive variant of classical propositional logic.

We then prove a completeness theorem for proofs in this extended setting: for any behaviour (formula) A and any design (proof attempt) P, either P is a proof of A or there is a model M of the negation of A which beats P. Compared with proofs of full completeness in game semantics, ours exhibits a striking similarity with proofs of Gödel's completeness, in that it explicitly constructs a countermodel essentially using König's lemma, proceeds by induction on formulas, and implies an analogue of Löwenheim-Skolem theorem.

[BT09a] Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda calculus. Information and Computation, Vol. 207, No. 1, pp. 41-62, 2009.
[ bib | .pdf ]
We present a polymorphic type system for lambda calculus ensuring that well-typed programs can be executed in polynomial time: dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one modality. It corresponds to a fragment of light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms (and not only on proof-nets): subject reduction is satisfied and a well-typed term admits a polynomial bound on the length of any of its beta reduction sequences. We also give a translation of LAL into DLAL and deduce from it that all polynomial time functions can be represented in DLAL.
[CGT08a] Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. Algebraic proof theory for substructural logics: Cut-elimination and completions, 2008. Submitted.
[ bib | .pdf ]
We carry out a unified investigation of two prominent topics in proof theory and algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices.

We introduce the substructural hierarchy - a new classification of logical axioms (algebraic equations) over full Lambek calculus FL, and show that cut-elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide up to the level N2 in the hierarchy. Negative results, which indicate limitations of cut-elimination and the MacNeille completion, as well as of the expressive power of structural sequent rules, are also provided.

Our arguments interweave proof theory and algebra, leading to an integrated discipline which we call algebraic proof theory.

[Ter08] Kazushige Terui. Computational ludics, 2008. To appear in Theoretical Computer Science.
[ bib | .pdf ]
We reformulate the theory of ludics introduced by J.-Y. Girard from a computational point of view. We introduce a handy term syntax for designs, the main objects of ludics. Our syntax also incorporates explicit cuts for attaining computational expressivity. We also consider design generators that allow for finite representation of some infinite designs. A normalization procedure in the style of Krivine's abstract machine directly works on generators, giving rise to an effective means of computation over infinite designs.

The acceptance relation between machines and words, a basic concept in computability theory, is well expressed in ludics by the orthogonality relation between designs. Fundamental properties of ludics are then discussed in this concrete context. We prove three characterization results that clarify the computational powers of three classes of designs. (i) Arbitrary designs may capture arbitrary sets of finite data. (ii) When restricted to finitely generated ones, designs exactly capture the recursively enumerable languages. (iii) When further restricted to cut-free ones as in Girard's original definition, designs exactly capture the regular languages.

We finally describe a way of defining data sets by means of logical connectives, where the internal completeness theorem plays an essential role.

[CGT08] Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. From axioms to analytic rules in nonclassical logics. In Proceedings of LICS'08, pp. 229-240, 2008.
[ bib | http | .pdf ]
We introduce a systematic procedure to transform large classes of (Hilbert) axioms into equivalent inference rules in sequent and hypersequent calculi. This allows for the automated generation of analytic calculi for a wide range of propositional nonclassical logics including intermediate, fuzzy and substructural logics. Our work encompasses many existing results, allows for the definition of new calculi and contains a uniform semantic proof of cut-elimination for hypersequent calculi.
[ABT07] Vincent Atassi, Patrick Baillot, and Kazushige Terui. Verification of ptime reducibility for system f terms: Type inference in dual light affine logic. Logical Methods in Computer Science, Vol. 3, No. 4, 2007.
[ bib | http ]
In a previous work Baillot and Terui introduced Dual light affine logic (DLAL) as a variant of Light linear logic suitable for guaranteeing complexity properties on lambda calculus terms: all typable terms can be evaluated in polynomial time by beta reduction and all Ptime functions can be represented. In the present work we address the problem of typing lambda-terms in second-order DLAL. For that we give a procedure which, starting with a term typed in system F, determines whether it is typable in DLAL and outputs a concrete typing if there exists any. We show that our procedure can be run in time polynomial in the size of the original Church typed system F term.
[Ter07a] Kazushige Terui. Light affine lambda calculus and polynomial time strong normalization. Archive for Mathematical Logic, Vol. 46, No. 3-4, pp. 253-280, 2007.
[ bib | http | .pdf ]
Light Linear Logic (LLL) and Intuitionistic Light Affine Logic (ILAL) are logics that capture polynomial time computation. It is known that every polynomial time function can be represented by a proof of these logics via the proofs-as-programs correspondence. Furthermore, there is a reduction strategy which normalizes a given proof in polynomial time. Given the latter polynomial time weak normalization theorem, it is natural to ask whether a strong form of polynomial time normalization theorem holds or not.

In this paper, we introduce an untyped term calculus, called Light Affine Lambda Calculus (lambda-LA), which corresponds to ILAL. Lambda-LA is a bi-modal lambda-calculus with certain constraints, endowed with very simple reduction rules. The main property of lambda-LA is the polynomial time strong normalization: any reduction strategy normalizes a given lambda-LA term in a polynomial number of reduction steps, and indeed in polynomial time. Since proofs of ILAL are structurally representable by terms of lambda-LA, we conclude that the same holds for ILAL.

[Ter07b] Kazushige Terui. Which structural rules admit cut elimination? an algebraic criterion. Journal of Symbolic Logic, Vol. 72, No. 3, pp. 738-754, 2007.
[ bib | http | .pdf ]
Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics.

We consider full Lambek calculus (FL), i.e., intuitionistic logic without any structural rules, as our basic framework. Residuated lattices are the algebraic structures corresponding to FL. In this setting, we introduce a criterion, called the propagation property, that can be stated both in syntactic and algebraic terminologies. We then show that, for any set R of structural rules, the cut elimination theorem holds for FL enriched with R if and only if R satisfies the propagation property.

As an application, we show that any set R of structural rules can be completed into another set R*, so that the cut elimination theorem holds for FL enriched with R*, while the provability remains the same.

[CT06b] Agata Ciabattoni and Kazushige Terui. Towards a semantic characterization of cut-elimination. Studia Logica, Vol. 82, No. 1, pp. 95-119, 2006. Corrigenda: http://www.kurims.kyoto-u.ac.jp/~terui/corrigendaSL.pdf.
[ bib | http | .pdf ]
We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.
[CT06a] Agata Ciabattoni and Kazushige Terui. Modular cut-elimination: Finding proofs or counterexamples. In Proceedings of LPAR'06, pp. 135-149. LNAI 4246, 2006.
[ bib | http | .pdf ]
Modular cut-elimination is a particular notion of cut-elimination in the presence of non-logical axioms that is preserved under the addition of suitable rules. We introduce syntactic necessary and sufficient conditions for modular cut-elimination for standard calculi, a wide class of (possibly) multiple-conclusion sequent calculi with generalized quantifiers. We provide a universal modular cut-elimination procedure that works uniformly for any standard calculus satisfying our conditions. The failure of these conditions generates counterexamples for modular cut-elimination and, in certain cases, for cut-elimination.
[ABT06] Vincent Atassi, Patrick Baillot, and Kazushige Terui. Verification of ptime reducibility for system F terms via dual light affine logic. In Proceedings of CSL'06, pp. 150-166, 2006. See [ABT07] for the journal version.
[ bib | http ]
In a previous work we introduced Dual Light Affine Logic (DLAL) as a variant of Light Linear Logic suitable for guaranteeing complexity properties on lambda-calculus terms: all typable terms can be evaluated in polynomial time and all Ptime functions can be represented. In the present work we address the problem of typing lambda-terms in second-order DLAL. For that we give a procedure which, starting with a term typed in system F, finds all possible ways to decorate it into a DLAL typed term. We show that our procedure can be run in time polynomial in the size of the original Church typed system F term.
[KOT06] Max I. Kanovich, Mitsuhiro Okada, and Kazushige Terui. Intuitionistic phase semantics is almost classical. Mathematical Structures in Computer Science, Vol. 16, pp. 1-20, 2006.
[ bib | http | .pdf ]
We study the relationship between classical phase semantics for classical linear logic (LL) and intuitionistic phase semantics for intuitionistic linear logic (ILL). We prove that (i) every intuitionistic phase space is a subspace of a classical phase space, and (ii) every intuitionistic phase space is phase isomorphic to an almost classical phase space. Here, by an `almost classical phase space we mean a phase space having a double-negation-like closure operator. Based on these semantic considerations, we give a syntactic embedding of propositional ILL into LL.
[BT05] Patrick Baillot and Kazushige Terui. A feasible algorithm for typing in elementary affine logic. In Proceedings of TLCA'05, pp. 55-70. LNCS 3461, 2005.
[ bib | http | .pdf ]
We give a new type inference algorithm for typing lambda-terms in Elementary Affine Logic (EAL), which is motivated by applications to complexity and optimal reduction. Following previous references on this topic, the variant of EAL type system we consider (denoted EAL*) is a variant where sharing is restricted to variables and without polymorphism. Our algorithm improves over the ones already known in that it offers a better complexity bound: if a simple type derivation for the term is given our algorithm performs EAL* type inference in polynomial time in the size of the derivation.
[Ter04a] Kazushige Terui. Light affine set theory: A naive set theory of polynomial time. Studia Logica, Vol. 77, No. 1, pp. 9-40, 2004.
[ bib | http | .pdf ]
In (Girard 1998), a naive set theory is introduced based on a polynomial time logical system, Light Linear Logic (LLL). Although it is reasonably claimed that the set theory inherits the intrinsically polytime character from the underlying logic LLL, the discussion there is largely informal, and a formal justification of the claim is not provided sufficiently. Moreover, the syntax is quite complicated in that it is based on a non-traditional hybrid sequent calculus which is required for formulating LLL.

In this paper, we consider a naive set theory based on Intuitionistic Light Affine Logic (ILAL), a simplification of LLL introduced by (Asperti 1998), and call it Light Affine Set Theory (LAST). The simplicity of LAST allows us to rigorously verify its polytime character. In particular, we prove that a function over words is computable in polynomial time if and only if it is provably total in LAST.

[BT04] Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda-calculus. In Proceedings of LICS'04, pp. 266-275, 2004. See [BT08] for the journal version.
[ bib | http ]
We propose a new type system for lambda-calculus ensuring that well-typed programs can be executed in polynomial time: Dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one modality. It corresponds to a fragment of Light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms: subject reduction is satisfied and a well-typed term admits a polynomial bound on the reduction by any strategy. Finally we establish that as LAL, DLAL allows to represent all polytime functions.
[Ter04b] Kazushige Terui. Proof nets and boolean circuits. In Proceedings of LICS'04, pp. 182-191, 2004.
[ bib | http | .pdf ]
We study the relationship between proof nets for mutiplicative linear logic (with unbounded fan-in logical connectives) and Boolean circuits. We give simulations of each other in the style of the proofs-as-programs correspondence; proof nets correspond to Boolean circuits and cut-elimination corresponds to evaluation. The depth of a proof net is defined to be the maximum logical depth of cut formulas in it, and it is shown that every unbounded fan-in Boolean circuit of depth n, possibly with stCONN2 gates, is polynomially simulated by a proof net of depth O(n) and vice versa. here, stCONN2 stands for st-connectivity gates for undirected graphs of degree 2. Let APNi be the class of languages for which there is a polynomial size, log i-depth family of proof nets. We then have APNi = ACi(stCONN2).
[MT03] Harry G. Mairson and Kazushige Terui. On the computational complexity of cut-elimination in linear logic. In Proceedings of ICTCS'03, pp. 23-36. LNCS 2841, 2003.
[ bib | .pdf ]
Given two proofs in a logical system with a confluent cut-elimination procedure, the cut-elimination problem (CEP) is to decide whether these proofs reduce to the same normal form. This decision problem has been shown to be PTIME-complete for Multiplicative Linear Logic (Mairson 2003). The latter result depends upon a restricted simulation of weakening and contraction for boolean values in MLL; in this paper, we analyze how and when this technique can be generalized to other MLL formulas, and then consider CEP for other subsystems of Linear Logic. We also show that while additives play the role of nondeterminism in cut-elimination, they are not needed to express deterministic PTIME computation. As a consequence, affine features are irrelevant to expressing PTIME computation. In particular, Multiplicative Light Linear Logic (MLLL) and Multiplicative Soft Linear Logic (MSLL) capture PTIME even without additives nor unrestricted weakening. We establish hierarchical results on the cut-elimination problem for MLL (PTIME-complete), MALL (coNP-complete), MSLL (EXPTIME-complete), and for MLLL (2EXPTIME-complete).
[Ter02] Kazushige Terui. Light Logic and Polynomial Time Computation. PhD thesis, Keio University, March 2002.
[ bib | .pdf ]
[Ter01] Kazushige Terui. Light affine lambda calculus and polytime strong normalization. In Proceedings of LICS'01, 2001. See [Ter07a] for the journal version.
[ bib ]
Light linear logic (LLL) and its variant, intuitionistic light affine logic (ILAL), are logics of polytime computation. All polynomial-time functions are representable by proofs of these logics (via the proofs-as-programs correspondence), and, conversely, that there is a specific reduction (cut-elimination) strategy which normalizes a given proof in polynomial time (the latter may well be called the polytime weak normalization theorem). In this paper, we introduce an untyped term calculus, called the light affine lambda calculus (lambda-LA), generalizing the essential ideas of light logics into an untyped framework. It is a simple modification of the lambda-calculus, and has ILAL as a type assignment system. Then, in this generalized setting, we prove the polytime strong normalization theorem: any reduction strategy normalizes a given lambda-LA term (of fixed depth) in a polynomial number of reduction steps, and indeed in polynomial time
[OT99] Mitsuhiro Okada and Kazushige Terui. The finite model property for various fragments of intuitionistic linear logic. Journal of Symbolic Logic, Vol. 64, No. 2, pp. 790-802, 1999.
[ bib | http ]
Recently (Lafont 1997) showed the finite model property for the multiplicative additive fragment of linear logic (MALL) and for affine logic (LLW), i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL (which we call IMALL), and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model property for contractive linear logic (LLC), i.e., linear logic with contraction, and for its intuitionistic version (ILLC). The finite model property for related substructural logics also follow by our method. In particular, we shall show that the property holds for all of FL and GL-systems except FLc and GLc of (Ono 1994), that will settle the open problems stated in (Ono 1996).
[Ter99] Kazushige Terui. Labelled tableau calculi generating simple models for substructural logics, 1999. ILLC Research Report PP-1999-04, University of Amsterdam.
[ bib | .pdf ]
In this paper we apply the methodology of Labelled Deductive Systems to the tableau method in order to obtain a deductive framework for substructural logics which incorporates the facility of model generation. For this special purpose, we propose new labelled tableau calculi TL and TLe for two substructural logics L (essentially the Lambek calculus) and Le (the multiplicative fragment of intuitionistic linear logic). The use of labels makes it possible to generate countermodels in terms of a certain very simple semantics based on monoids, which we call the simple semantics. We show that, given a formula C as input, every nonredundant tableau construction procedure for TL and TLe terminates in finitely many steps, yielding either a tableau proof of C or a finite countermodel of C in terms of the simple semantics. It shows the finite model property for L and Le with respect to the simple semantics.
[OT98] Mitsuhiro Okada and Kazushige Terui. Completeness proofs for linear logic based on the proof search method (preliminary report). In J. Garrigue, editor, RIMS Koukyuroku: Type theory and its applications to computer systems, pp. 57-75. Research Institute for Mathematical Sciences, Kyoto University, 1998.
[ bib | .pdf ]
We investigate a method of completeness proofs based on the labelled proof search in Linear Logic framework. This method is obtained from the usual proof search methods in classical and intuitionistic logic by considering the resource-sensitivity and concurrency of the Linear Logic. By using this method, we prove that some computationally meaningful fragments of Linear Logic are complete with respect to naive phase semantics, which is a simplification of phase semantics (the standard Tarskian-style semantics of Linear Logic).

Under the proofs-as-processes correspondence, Linear Logic proof search can be identified with a theory of asyncronous concurrent process calculus. Based on this paradigm, we apply our technique to construct a denotational semantics for the concurrent process calculus.

[Ter98] Kazushige Terui. Anaphoric linking at run time: A type-logical account of discourse representation, 1998. ILLC Research Report LP-1998-17, University of Amsterdam.
[ bib | .pdf ]
A number of attempts have been made to combine Discourse Representation Theory with type-logical grammar in order to obtain a compositional (bottom-up) framework for discourse representation (e.g., Muskens 1994, van Eijck and Kamp 1997). In those attempts, however, it is usually assumed that anaphoric links are given in advance of the construction of discourse representation structures (DRSs). This assumption causes a difficulty, typically dealing with plural anaphora, because generally suitable referents of plural pronouns are not present before the construction, but should be created through the construction of DRSs.

To settle this difficulty, we shall propose a new type-logical framework of DRT in which anaphoric linking takes place during the construction of DRSs (Run Time Anaphoric Linking). The construction is bottom-up in the sense that it is based on the sequent calculus proof search of Lambek calculus. We exploit quantifier types to represent the run time anaphoric linking mechanism. We shall briefly illustrate how plural anaphora are treated in our framework. In particular, we shall show that Summation and Abstraction, which are used to create suitable antecedent discourse referents for plural pronouns in (Kamp and Reyle 1993), are available in our type-logical setting using the linear logic modality.

[OT97] Mitsuhiro Okada and Kazushige Terui. Semantic characterizations for reachability and trace equivalence in a linear logic-based process calculus. In T. Arai, editor, RIMS Koukyuroku: Symposium on Proof Theory and Ordinals, pp. 146-168. Research Institute for Mathematical Sciences, Kyoto University, 1997.
[ bib | .pdf ]
We give semantic characterizations for reachability and trace equivalence in a version of asynchronous process calculus based on linear logic.

Usually the reachability relation in linear logic-based process calculi is characterized by the logical notion of provability, which is in turn characterized by model-theoretic semantics such as phase semantics. We introduce considerably simplified phase models, which we call naive phase models, and show that reachability is also characterized by the completeness with respect to the naive phase models.

On the other hand, logical provability does not provide any satisfactory notion of equivalence on processes. We consider the trace equivalence (Hoare 1980) on our process calculus and introduce certain algebraic models, which we call trace models. Then the trace equivalence is characterized by the completeness with respect to the trace models.


This file has been generated by bibtex2html 1.79