プログラム言語BQLとその処理系
スポンサーリンク
概要
- 論文の詳細を見る
ν行為はプログラムを数学的に表現したものである. 本論文では, ν行為を計算機で解釈・実行するための言語BQLとその解釈系のアルゴリズムを紹介し, その正当性について述べる・ν行為は論理式中の自由変数を少なくとも1つνxなる表現である質変数で置き換えたもので, 自由変数が現在の割当, 質変数が新しい割当を表すものである. たとえば通常のプログラム言語の算術代入文X : = f(X)はνx = f(x)というν行為に対応している. 解釈系が行う基本的な解釈は, ν行為A[x,νx]と自由変数の現在の割当σに対しσ ⊨ ∃ yA[x,y]であるとき新しい割当としてσ ⊨ A[x,a]なる名前aを求めるものである. BQLが対象とするν行為(解釈可能なν行為)は述語論理を基とした型理論の上で記述されたものであり, 関係・集合に対応するアブストラクトを値としてとる高階の質変数などもその中に出現する. そしてこれらのν行為は, 量記号は限量記号に限る, 関数記号×, / にはその2つの引数ともには質変数が出現しない, などの条件を満たすものである. これらは非常に強い制限ではあるが, 通常の手続き型言語で書かれたプログラムの大部分は以上の範囲で表現できる. また, 論理型プログラム言語という視点で考えると, 他の幾つかの言語と異なり, 特殊な形を要求しない, 否定記号を完全に扱えるなどの性質がある.
- 一般社団法人情報処理学会の論文
- 1996-04-15
著者
関連論文
- プログラムにおける実時間問題のν-転換による解析と動作条件
- 時制算術における時制の消去に関する一考察
- 5C-6 ヒューマンファクターを包含する記号論理体系に基づく実時間知的システムの分析(複雑系,一般セッション,人工知能と認知科学)
- 知性と感性の情報学的討究(6)ヒューマンファクターを包含する記号論理体系に基づく信楽列車事故の分析
- 知性と感性の情報学的討究V : 時制に依存する命題の事例化規則とサウンドネス(佐藤照子先生追悼号)
- 知性と感性の情報学的討究(4)人工知能論における協調系の数理的表現について
- 知性と感性の情報学的討究III : @-calculusに基づく協調システムの検証例-アンサンブル・プログラム
- 知性と感性の情報学的討究II : 時制数論体系@-calculusの基礎分析
- 時間の論理の束モデルを用いた並行プログラム系の検証
- ランデブーを含むvirtual textによる自動伴奏システムの表現とその検証
- 軌跡準同型によるプログラムの仕様の保存性
- ν-定義可能行為によるプログラムの検証
- プログラム言語BQLとその処理系
- フレーズの表情付けの図形的表現 : ピアノ演奏の場合
- ブリッジプレイの終盤における必勝戦術の論理的考察
- 有理Presburger算術の決定性について
- 多人数ゲームにおける枝刈りと四人将棋への応用
- プログラムの自動検証