Mitsuhiro Okada

TCS Journal 2020 Journal Article

Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68]

• Frédéric Blanqui
• Jean-Pierre Jouannaud
• Mitsuhiro Okada

In a previous work (Abstract data type systems, Theoret. Comput. Sci. 173 (2) (1997)), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-calculus enriched by pattern-matching definitions following a certain format, called the “General Schema”, which generalizes the usual recursor definitions for natural numbers and similar “basic inductive types”. This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called “strictly positive”, and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.

TCS Journal 2003 Journal Article

A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic

• Misao Nagayama
• Mitsuhiro Okada

It is well known that every proof net of a non-commutative version of MLL (multiplicative fragment of commutative linear logic) can be drawn as a plane Danos–Regnier graph (drawing) satisfying the switching condition of Danos–Regnier [3]. In this paper, we study the reverse direction; we introduce a system MNCLL which is logically equivalent to the multiplicative fragment of cyclic linear logic introduced by Yetter [9], and show that any plane Danos–Regnier graph drawing with one terminal edge satisfying the switching condition represents a unique non-commutative proof net (i. e. , a proof net of MNCLL). In the course of proving this, we also give the characterization of the non-commutative proof nets by means of the notion of strong planarity, as well as the notion of a certain long-trip condition, called the stack-condition, of a Danos–Regnier graph, the latter of which is related to Abrusci's balanced long-trip condition [2].

TCS Journal 2003 Journal Article

Phase semantics for light linear logic

• Max I Kanovich
• Mitsuhiro Okada
• Andre Scedrov

Light linear logic (Girard, Inform. Comput. 14 (1998) 175–204) is a refinement of the propositions-as-types paradigm to polynomial-time computation. A semantic setting for the underlying logical system is introduced here in terms of fibred phase spaces. Strong completeness is established, with a purely semantic proof of cut elimination as a consequence. A number of mathematical examples of fibred phase spaces are presented that illustrate subtleties of light linear logic.

TCS Journal 2003 Journal Article

Preface

• Jean-Yves Girard
• Mitsuhiro Okada
• Andre Scedrov

TCS Journal 2002 Journal Article

A uniform semantic proof for cut-elimination and completeness of various first and higher order logics

• Mitsuhiro Okada

We present a natural generalization of Girard's (first order) phase semantics of linear logic (Theoret. Comput. Sci. 50 (1987)) to intuitionistic and higher-order phase semantics. Then we show that this semantic framework allows us to derive a uniform semantic proof of the (first order and) higher order cut-elimination theorem (as well as a (first order and) higher order phase-semantic completeness theorem) for various different logical systems at the same time. Our semantic proof works for various different logical systems uniformly in a strong sense (without any change of the argument of proof): it works for both first order and higher order versions and for linear, substructural, and standard logics uniformly, and for both their intuitionistic and classical versions uniformly.

TCS Journal 2002 Journal Article

Inductive-data-type systems

• Frédéric Blanqui
• Jean-Pierre Jouannaud
• Mitsuhiro Okada

In a previous work (“Abstract Data Type Systems”, TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed λ-calculus enriched by pattern-matching definitions following a certain format, called the “General Schema”, which generalizes the usual recursor definitions for natural numbers and similar “basic inductive types”. This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called “strictly positive”, and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.

TCS Journal 1999 Journal Article

Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic

• Mitsuhiro Okada

We give a natural extension of Girard's phase semantic completeness proof of the (first order) linear logic Girard (Theoret. Comput. Sci. , 1987) to a phase semantic cut-elimination proof. Then we extend this idea to a phase semantic cut-elimination proof for higher order linear logic. We also extend the phase semantics for provability to a phase semantics-like framework for proofs, by modifying the phase space of monoid domain to that of proof-structures (untyped proofs) domain, in a natural way. The resulting phase semantic-like framework for proofs provides various versions of proof-normalization theorem.

TCS Journal 1997 Journal Article

Abstract data type systems

• Jean-Pierre Jouannaud
• Mitsuhiro Okada

This paper is concerned with the foundations of an extension of pure type systems by abstract data types, hence the name of Abstract Data Type Systems. ADTS generalize inductive types as they are defined in the calculus of constructions, by providing definitions of functions by pattern matching on the one hand, and relations among constructors of the inductive type on the other. It also generalizes the first-order framework of abstract data types by providing function types and higher-order equations. The first half of the paper describes the framework of ADTS, while the second half investigates cases where ADTS are strongly normalizing. This is shown to be the case for the polymorphic lambda calculus (with possibly subtypes) enriched by higher-order algebraic rules obeying a strong generalization of primitive recursion of higher type that we call the general schema. This covers in particular the case of inductive types whose constructors do not have functional arguments. We conjecture that this result holds true for all calculi of the so-called Barendregt's cube. On the other hand, the definition of a schema for the higher-order rules allowing for more general inductive types is left open.

TCS Journal 1990 Journal Article

A rationale for conditional equational programming

• Nachum Dershowitz
• Mitsuhiro Okada

Conditional equations provide a paradigm of computation that combines the clean syntax and semantics of LISP-like functional programming with Prolog-like logic programming in a uniform manner. For functional programming, equations are used as rules for left-to-right rewriting; for logic programming, the same rules are used for conditional narrowing. Together, rewriting and narrowing provide increased expressive power. We discuss some aspects of the theory of conditional rewriting, and the reasons underlying certain choices in designing a language based on them. The most important correctness property a conditional rewriting program may posses is ground confluence; this ensures that at most one value can be computed from any given (variable-free) input term. We give criteria for confluence. Reasonable conditions for ensuring the completeness of narrowing as an operational mechanism for solving goals are provided; these results are then extended to handle rewriting with existentially quantified conditions and built-in predicates. Some termination issues are also considered, including the case of rewriting with higher-order terms.