圏論的結合子の操作的意味について
スポンサーリンク
概要
- 論文の詳細を見る
Curienは,カルテシアン閉圏(cartesian closed category,以下,CCCと略す)の定義における普遍写像性を,圏論的結合子と呼ばれる特別な射に関する等式に翻訳し,この等式を書き換え規則とみなすことで,関数型言語の操作的意味が圏論を通じて与えられることを示唆した.特にCCCの圏論的結合子から型,すなわち定義域と値域に関する情報と,終対象に関する結合子を取り除いた代数系(C-モノイドと呼ばれる)を用いれば,型なしのラムダ計算を従来の項書換え系として扱うことができる.横内も独立して,型なしの場合に圏論的結合子の等式を書き換え規則として扱うことを提唱した.しかし圏の射はf:A→Bのように定義域Aと値域Bによって型付けられた存在であり,射の結合は一方の値域と他方の定義域が一致するような射の対に対してのみ部分的に定義される.個々の結合子についても,異なる対象の上で同様に作用し得るという多相的な性質を持っている.たとえ型なしのC-モノイドを扱うとしても,結合子に関する個々の等式がどのような計算的・意味論的性質に連係しているのかが明らかでないので,合流性や停止性といった項書換え系の性質を考察することが困難である.本稿では,まずCCCのための圏論的結合子とその等式を随伴関手から直接導き出し,自由圏を生成する逐次式計算系を定義する.そしてこの体系におけるカット除去を圏論的結合子の操作的意味として用いることを提案する.
- 一般社団法人情報処理学会の論文
- 1994-09-20
著者
関連論文
- PCTE : ソフトウェアツールを移植可能にし, 共通に利用するための環境
- オブジェクトシステムの形式的仕様記述に向けて
- ソフトウエア仕様記述におけるカテゴリ論の応用について
- 部分計算を用いた等式仕様の変換と実行
- プロセス統合に用いられるユーザインタフェースの設計
- 実体・関連モデルへの意味的制約の統合とPCTEデータモデルへの展開
- 実体・関連モデルへの意味的制約の統合とPCTEデ-タモデルへの展開 (ソフトウェア工学)
- 大規模データベースを用いた計画問題とその並列処理方式
- データベースを用いた計画作成における並列処理方式
- PCTEスキーマから導出されるデータ操作プログラムについて
- ソフトウェア設計方法論に関する一考察 (日本のソフトウェア開発方法)
- システムインテグレーション技術の展望
- 大規模データベースを用いた戦略的計画の作成方式
- ソフトウェアエンジニアリング・データベースKyotoDB の設計と実現
- ソフトウェア科学とソフトウェア工学
- 圏と射によるソフトウェア設計プロセスの表現
- ソフトウェア仕様書間の関係記述の一手法
- ソフトウェアエンジニアリングデータベースKyotoDBにおけるユーザインタフェースと協調活動支援機能の実現
- ソフトウェアエンジニアリングデータベースKyotoDB核のプロトタイピング
- 2.CASE 環境の基礎技術 (CASE環境)
- ソフトウェアエンジニアリングデータベースSEDB/OKBLのデータモデルについて
- 制御用マルチコンピュ-タの一方式における応答性改善について
- シミュレーションによる制御用計算機の性能予測
- 随伴関手を用いた圏論的結合子の導出
- 圏によるソフトウェア意味の可視化 ( 情報の可視化)
- 圏論的結合子の操作的意味について
- 複雑系として技術史を観る
- ソフトウェアプロジェクトにおける協力と協調を支援する計算機環境
- 計測と制御用ソフトウェアのためのCASE環境 (計測と制御におけるソフトウェアの開発環境)