• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

宣言型プログラミング言語のためのAC記号のあるナローイングの計算理論

研究課題

研究課題/領域番号 14780187
研究種目

若手研究(B)

配分区分補助金
研究分野 計算機科学
研究機関東北大学

研究代表者

青戸 等人  東北大学, 電気通信研究所, 助教授 (00293390)

研究期間 (年度) 2002 – 2004
研究課題ステータス 完了 (2004年度)
配分額 *注記
1,100千円 (直接経費: 1,100千円)
2004年度: 400千円 (直接経費: 400千円)
2003年度: 500千円 (直接経費: 500千円)
2002年度: 200千円 (直接経費: 200千円)
キーワード宣言型プログラミング言語 / 項書き換え系 / 高階項書き換え系 / 帰約的定理 / 停止性 / AC記号 / ナローイング / 帰納的定理 / 項書換え系 / 合流性
研究概要

前年度に得られた高階項書き換え系における帰納的定理証明について解析を進めた.第1階の場合には自明に成立するが,高階では一般に成立しない帰納的定理の性質が単調性である.単調性を満たさないと高階帰納的定理の利用に様々な制約が課せられる.そこで,我々は,高階帰納的定理が単調性を持つための条件について考察した.まず,第1階項書き換え系における十分完全性の概念を拡張し,高階十分完全性の概念を与えた.そして,この概念を用いて,等式が単調高階帰納的定理となるための十分条件を明らかにした.次に,高階十分完全性の自動証明について考察を行なった.高階十分完全性の自動証明を行うため,初等性および高階図式という制約を導入し,高階十分完全性が決定可能となる単純型付き項書換え系のクラスを与えた.初等的な高階図式は多くの自然な高階関数プログラムを含む.以上の結果は,項書き換え分野の代表的な国際会議の1つであるRTA(書き換え技法と応用)'04に採録され,国際的な報告を行なった.
前年度に得られた,単純型付き項書き換え系の停止性証明技法の実装について検討を行なった.その実装の第一段階として,より単純な体系である単純型付き適応的項書き換え系の停止性証明技法について考察を行なった.その過程で,適応的項書き換え系についてのみ適用可能な,非常に簡単で,しかも比較的強力な停止性証明技法を考案した.この成果は高階項書き換え系の国際ワークショップHOR'04に採録され,国際的な報告を行なった.

報告書

(3件)
  • 2004 実績報告書
  • 2003 実績報告書
  • 2002 実績報告書
  • 研究成果

    (3件)

すべて その他

すべて 文献書誌 (3件)

  • [文献書誌] 青戸等人: "単純型付き項書換え系における停止性の自動証明"情報処理学会誌:プログラミング. 44.SIG4 PRO17. 67-77 (2003)

    • 関連する報告書
      2003 実績報告書
  • [文献書誌] 青戸等人: "高階関数型プログラムにおける帰納的定理証明"情報技術レターズ. 2. 21-22 (2003)

    • 関連する報告書
      2003 実績報告書
  • [文献書誌] 青戸等人: "単純型付き項書換え系における停止性の自動証明"情報処理学会誌:プログラミング. (印刷中). (2003)

    • 関連する報告書
      2002 実績報告書

URL: 

公開日: 2002-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi