一覧に戻る

タイトル
  • en NII Technical Report (NII-2008-005E)：Inhabitance of Existential Types is Decidable in Negation-Product Fragment
作成者
    • ja 龍田, 真 en Tatsuta, Makoto
    • ja 藤田, 憲悦 en Fujita, Ken-etsu
    • ja 長谷川, 立 en Hasegawa, Ryu
    • ja 中野, 洋 en Nakano, Hiroshi
主題
  • Other ja テクニカルレポート
  • Other en Technical Report
内容注記
  • Abstract en This paper shows the inhabitance in the lambda calculus with negation, product, and existential types is decidable. This is proved by showing existential quantification can be eliminated and reducing the problem to provability in intuitionistic propositional logic. By the same technique, this paper also shows existential quantification followed by negation can be replaced by a specific witness in both that system and the system with implication and bottom.
出版者 ja 国立情報学研究所
日付
    Issued2008-04-04
言語
  • eng
資源タイプ departmental bulletin paper
資源識別子 DOI https://doi.org/10.20736/0000001243 , URI https://repository.nii.ac.jp/records/1243
ID
  • JaLC 10.20736/0000001243
収録誌情報
    • ISSN 1346-5597
      • ja NIIテクニカル・レポート en NII Technical Report
      • 開始ページ1 終了ページ13
ファイル
コンテンツ更新日時 2023-06-26