• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2004 Fiscal Year Annual Research Report

λμ計算の表示的意味論に関する研究

Research Project

Project/Area Number 14540119
Research InstitutionGunma University

Principal Investigator

藤田 憲悦  群馬大学, 工学部, 助教授 (30228994)

Co-Investigator(Kenkyū-buntansha) 近藤 通朗  東京電機大学, 情報環境学部, 教授 (40211916)
Keywordsλμ計算 / CPS変換(継続) / 多相型関数 / 抽象データ型 / カリー・ハワード同型 / ガロア対応 / 制御オペレータ / 双対性
Research Abstract

直観主義論理と型付きラムダ計算との対応関係は,カリー・ハワードの同型対応として古くから知られている.λμ計算とは,この対応関係を古典論理にまで拡張することによりM.Parigotが導入した論理体系である.λμ計算はλ計算の自然な拡張となっており,計算モデルとしてそれ自体興味深い体系となっている.平成14年度,15年度における研究成果として,
(1)タイプフリーλμ計算及び単純型付きλμ計算からλ計算へのCPS変換
(2)継続の概念に基づくλμ計算の表示的意味論及びCモノイド
(3)CPS変換と表示的意味論との完備半順序集合上の模倣関係
などについて明らかにしてきた.これらの成果を発展させるために,本研究では多相型λ計算を対象として,次の結果が得られた.
(4)存在型計算体系の導入
連言,2階存在型などを持つ存在型計算体系を新しく導入した.例えば,抽象データ型はこの体系で型付け可能となっている.そして,多相型λ計算と存在型計算体系間の変換及び逆変換を与え,変換規則が単射を形成していることが示された.
(5)多相型λ計算と存在型計算体系とのガロア対応
多相型λ計算と存在型計算体系におけるそれぞれの計算規則は,変換規則及び逆変換に関して単調性を有しており,二つの計算モデル間にはいわゆるガロア対応関係が存在していることが解明された.
(6)多相型λ計算の基本的な性質
多相型λ計算の正規化性,合流性などの基本的な性質は,ガロア対応関係にある存在型計算体系のそれらより帰結されることがわかった.
さらに,本研究で導入された概念は,多相型λμ計算に拡張しても機能することが確認されている.また,存在型計算体系は,知る限りにおいては,これまでに研究されていなかったようであり,この計算モデルの性質を解析することは,多相型λ計算を含む計算体系に新たなかつ興味深い視点を与えるものと期待される.なお,これらの成果は,日本ソフトウェア科学会第21回大会で公表された.

  • Research Products

    (4 results)

All 2005 2004

All Journal Article (4 results)

  • [Journal Article] Galois embedding from polymorphic types into existential types2005

    • Author(s)
      Ken-etsu Fujita
    • Journal Title

      Lecture Notes in Computer Science 3461

      Pages: 194-208

    • Description
      「研究成果報告書概要(和文)」より
  • [Journal Article] ガロア埋め込み:多相型関数と抽象データ型の証明双対性2004

    • Author(s)
      藤田 憲悦
    • Journal Title

      日本ソフトウェア科学会第21回大会講演論文集 (CD-R)

    • Description
      「研究成果報告書概要(和文)」より
  • [Journal Article] Characterization theorem of lattice implication algebras2004

    • Author(s)
      Michio Kondo
    • Journal Title

      Proc.34th International Symposium on Multiple-Valued Logics

      Pages: 257-206

    • Description
      「研究成果報告書概要(和文)」より
  • [Journal Article] On the class of QS-algebras2004

    • Author(s)
      Michio Kondo
    • Journal Title

      International Journal of Mathematics and Mathematical Sciences 49-1

      Pages: 2629-2639

    • Description
      「研究成果報告書概要(和文)」より

URL: 

Published: 2006-07-12   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi