ALGI 12

*** 9月5日 *** 13：00−13：05 オープニング 13：05−13：35 講演者 長谷川真人（京都大学数理解析研究所） 演題 Classical linear logic of implications 概要 We give a simple term calculus for the multiplicative exponential fragment of Classical Linear Logic, by extending Barber and Plotkin's system for the intuitionistic case. The calculus has the non-linear and linear implications as the basic constructs, and this design choice allows a technically managable axiomatization without commuting conversions. Despite this simplicity, the calculus is shown to be sound and complete for category-theoretic models given by *-autonomous categories with linear exponential comonads. (To appear in CSL'02, paper available from http://www.kurims.kyoto-u.ac.jp/~hassei/papers/) 13：35−14：05 講演者 上出 哲広（東京工業大学） 演題 Sequent calculi for intuitionistic linear logic with strong negation and their applications 概要 We introduce an extended intuitionistic linear logic with strong negation and modality. The logic presented is a modal extension of Wansing's extended linear logic with strong negation. First, we propose three types of cut-free sequent calculi for this new logic. The first one is named a subformula calculus, which yields the subformula property. The second one is termed a dual calculus, which has positive and negative sequents. The third one is called a triple-context calculus, which is regarded as a natural extension or generalization of Hodas and Miller's dual-context calculus appearing in a linear logic programming language. Second, we present a concurrent process calculus based on the logic. This calculus is an extension of Okada's process calculus. Third, we introduce a Kripke type semantics for a fragment of the logic, and show the completeness theorems with respect to the semantics. Finally, we mention a logic programming language based on the triple-context calculus, and discuss a temporal extension of the logic. 14：20−14：50 講演者 新田直也（奈良先端大学院大学情報科学研究科） 演題 柔軟な設計変更を可能にする論理体系 ソフトウェアの設計変更を容易にする新しい論理体系(依存論理)を 提案する. 大規模なソフトウェア開発において, 要求仕様の形式的 記述の妥当性は工程全体の効率および信頼性を支配している. 特に 形式化のために導入した関数や述語群(設計)が対象領域の正しいモ デルとなっていなかった場合, 後で発生する仕様記述の書き換え作 業は膨大なものとなる. 筆者らが提案している依存論理では, 高階 変数という論理要素を用いそれらの間の依存関係として関数や述語 を構成することが可能である. この特長によって異なる設計間の関 係を形式的記述の中に自然に組み込むことができ, 柔軟な設計変更 に対応することが可能になる. 本発表では, 依存論理の構文, 意味論および健全な公理系について 紹介し, またデータベース設計変更問題への適用法について述べる. 14：50−15：20 講演者 大隈ひとみ（九州大学システム情報科学府） 演題 A completeness theorem for extended order dependencies on relational attribute models in Dedekind categories 概要 Order dependencies in relational database due to Ginsburg and Hull are relationships between attributes with domains of ordered values. In this talk, we introduce the basic notions "comparison systems" and "relational attribute models" in Dedekind categories. A comparison system constitutes a formal structure of possible orders for attribute domains. A relational attribute model is a system of relations on an object (of tuples or records) in Dedekind categories, which can be constructed by a suitable relational interpretation of comparing symbols. Generalizing order dependencies as well as functional dependencies, we introduce extended order dependencies, and their satisfactory relations for relational attribute models. Then we give a simple proof that a revised set of inference rules is sound and complete. 15：35−16：05 講演者 角谷良彦（京都大学数理解析研究所） 演題 Duality between call-by-name recursion and call-by-value iteration 概要 We investigate the duality between call-by-name recursion and call-by-value iteration in the lambda-mu-calculi and their models. Semantically, we consider that iteration is the dual notion of recursion. Syntactically, we extend the call-by-name lambda-mu-calculus and the call-by-value one with a fixed-point operator and an iteration operator, respectively. We show that the dual translations between the call-by-name lambda-mu-calculus and the call-by-value one, which is constructed by Selinger, can be expanded to our extended lambda-mu-calculi. Another result of this study provides uniformity principles for those operators. 16：05−16：35 講演者 松岡聡（産総研） 演題 Exponential-free Typed Böhm Theorem 概要 In the Böhm theorem workshop of last year, Zoran Petric called Statman's``Typical Ambiguity theorem'' typed Böhm theorem. Moreover, he gave a new proof of the theorem based on set-theoretical models of typed lambda calculus. In this talk, we give the linear version of the typed Böhm theorem: given two closed implicational intuitionistic proof nets that have different beta-eta-long normal forms, we can have a context that separates the two proof nets in a clear way. Such a context is the composition of the following contexts: 1. contexts that decrease the orders of proof nets 2. type instantiation operators In these operators additive connectives may occur. 3. choice contexts These contexts can pick up obviously different proof nets by exploiting the information of given different two proof nets with the order less than fourth order. 16：45− ビジネスミーティング 懇親会 *** 9月6日 *** 10：00−10：30 講演者 竹内泉（東邦大学理学部） 演題 グジェゴルチク計算可能性とＢＳＳ計算可能性　 概要 実数計算の概念にはグジェゴルチク計算可能性とＢＳＳ計算可能性 が有名である。今回の発表では、(1) 実はＢＳＳ計算可能は実数計 算ではないこと、(2) グジェゴルチク計算可能性はＢＳＳ計算可能 を包摂した概念であること、この２点を示す。 10：30−11：00 講演者 八杉満利子・辻井芳樹（京都産業大学） 演題 Two notions of sequential computability of a function with jumps 概要 Given a strictly increasing computable sequence of real numbers (with respect to the Euclidean topology), one can define an effective uniform space of the real line, where the elements in the sequence are regarded as isolated. The relation between two notions of computability of real sequences, one with respect to the Euclidean space and one with respect to the uniform space as above, is discussed. As a consequence, we prove the equivalence of two notions of sequential computability of a function which is effectively uniformly continuous on the intervals between the given points and which may jump at those points. 11：15−12：00 講演者 立木秀樹（京都大学総合人間学部） 演題 Uniform domains and Uniform spaces 概要 一様空間は，距離空間を抽象化して，距離関数というものを使わずに 空間の一様性を表現した構造です。そこでは，一様性を導入するのに，被覆が どんどん詳細になっていく列を用います。その列は，空間の有限的な近似構造 となっています。一方で，計算機科学者にとって，何か無限なものを有限な要 素の極限として近似する代表的な構造に，ω代数的領域があります。この講演 では，ω代数的領域に一様的な構造を入れる条件を付け加えれば（一様領域と よぶことにします），それが基本的に可算完全一様空間と等価なものとなるこ とを示します。すなわち一様領域 D において，その極限要素の集合の中の最 小元の集合の上にスコット位相の部分位相を考えたら，それは，可算完全一様 空間となり，また，逆に可算完全一様空間から一様領域を構成できることを示 します。また，一様領域としての表現から，自然に空間の文字列としての表現 が得られること，その表現は，proper という性質をもつことも言います。 12：00−12：30 講演者 Vestergaard, Rene（北陸先端大学院大学） 演題 alpha-Equivalence _is_ Decidable 概要 We discuss and prove the titular result for languages with binding presented as syntax. The curious fact is, namely, that the result by no means is obvious; a point that seems to have been missed in the literature. In particular, it seems that any proof must include a Some/Any Property of (fresh) variable names, a la McKinna-Pollack/Gabbay-Pitts. The specific Some/Any Property we use has an interesting proof in its own right.