単純型付き項書き換え系における静的依存対法とその周辺
スポンサーリンク
概要
- 論文の詳細を見る
我々が提案した関数プログラムの強力な停止性証明法である静的依存対法は一般には適用できないため取り扱うプログラムに一定の制限を課す必要がある.このような制限として我々は直接関数渡しと呼ばれる性質を提案した.本論文ではより適用範囲の広い関数渡しの安全条件を提案し,このクラスで静的依存対法が健全であることを示す.また,依存対法で停止性を証明する際には,引数切り落とし法や実効規則が重要となる.本論文では,既存の引数切り落とし法と異なり型の構造を破壊しない引数切り落とし法も与える.さらに,実効規則の既存の成果を拡張して引数切り落とし法と組合せた実効規則の概念を与える.
- 社団法人電子情報通信学会の論文
- 2008-02-25
著者
関連論文
- 基本対称関数に基づく節をもつCNF論理式の充足可能性判定(計算論,計算モデル)
- ビットエラー通信路におけるスケーラブルCANの動作解析
- 条件付き等式の変換に基づくプログラム生成 (ソフトウェアサイエンス)
- 右線形右シャローな項書換え系における文脈依存停止性の決定可能性について (ソフトウェアサイエンス)
- シャローな依存対から構成される項書換え系の停止性の決定可能性
- 基本対称関数を付加したCNF論理式の充足可能性判定
- 制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序
- プレスブルガー文付き項書換え系における書換え帰納法について
- フォーマルアプローチ論文特集の発行にあたって
- 例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム(ディペンダブルコンピューティング)
- 等式を規則化する変換の停止条件
- 単純型付き項書き換え系における静的依存対法とその周辺
- 動的型言語への柔らかい型付けによるエラー検出
- 対話型埋込みによる数独問題の設計ツール
- プログラム生成系GeneSysにおける等式仕様への否定の導入
- 導出木からのループ検出による論理プログラムの非停止性証明法
- 振舞等価性の証明のための等式付き書換えに基づく潜在帰納法
- 左線形な定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン
- 二階の書換え系における引数切り落とし法
- 難解言語Malbolgeのチューリング完全性について (ソフトウェアサイエンス)
- 制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み
- 高階書換え系における引数切り落とし法と実効規則
- 項書き換えシステムの合流性自動判定
- 難解言語Malbolgeのチューリング完全性について
- A-033 S式書き換えシステムの停止性を保証するカリー化について(モデル・アルゴリズム・プログラミング,一般論文)
- 右線形右シャローな項書換え系における文脈依存停止性の決定可能性について
- 条件付き等式の変換に基づくプログラム生成
- 反証機能付き書き換え帰納法のための補題自動生成法
- 制約付き項書換え系における書換え帰納法
- プレスブルガー文付き項書換え系における書換え帰納法について
- 非完全な仕様における振舞等価性の自動証明法
- 暗号プロトコル記述からカラーペトリネットへの変換による機密性検証
- 関数プログラムの停止性証明のための辞書式経路順序
- 順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について (ソフトウェアサイエンス)
- 高階書換え系における引数切り落とし法と実効規則
- 単純型項書換え系における定理自動証明系HOPSYS
- 項書換え系の拡張された階層的結合における停止性のモジェラー性
- 例外処理付きオブジェクト指向言語における情報流の安全性解析
- 例外処理付きオブジェクト指向言語における情報流の安全性解析
- 等式理論を法とするDPLL遷移系について
- 項正規表現に基づくSpi計算の機密性検証
- 等式付き書換え系の等式数を削減する変換
- ナローイング計算の停止性証明のための依存グラフ法
- 単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け(基礎理論,フォーマルアプローチ論文)
- 単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け
- LA-001 関数プログラムの再帰構造解析と強計算性に基づく十分完全性の証明法(A分野:モデル・アルゴリズム・プログラミング)
- 強計算性に基づいた単純型項書換え系の停止性証明法
- 制約付き木オートマトンとその閉包性 (ソフトウェアサイエンス)
- 静的依存対法による高階書換え系の停止性証明
- 強計算依存対法による高階書換え系の停止性証明
- A-032 多重Knuth-Bendix完備化における危険対除去手法の導入(モデル・アルゴリズム・プログラミング,一般論文)
- GeneSysによるプログラム生成例とIntroduction規則の追加
- GeneSysによるプログラム生成例とIntroduction規則の追加
- A-034 基底項書き換え系の合流性自動判定(モデル・アルゴリズム・プログラミング,一般論文)
- 優先順序付き項書換え系の頭必須戦略の決定可能性
- 配列を扱う非線形先頭再帰プログラムからの再帰除去 (計算機科学基礎理論とその応用)
- 左線形シャローなどの項書換え系の停止性の決定性
- 準構成子項書換え系における停止性の決定問題
- 重なりを持つTRSにおける最外戦略の完全性について
- 代数的仕様の論理型プログラムへの変換法
- 例外処理を持つ関数型プログラムの停止性・非停止性証明法
- 高階書換え系の決定可能な計算戦略について
- 高階書換え系におけるディセンダントと頭必須書換えの頭正規化性
- 項集合書換え系の完備化について
- 紐解かれた項書換え系の文脈依存条件の除去のための変換(計算理論とアルゴリズムの新展開)
- 順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について
- 制約付き木オートマトンとその閉包性
- 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み
- 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み
- 左辺が一致するオーバレイ性を持つ左線形TRSの正規化戦略 (計算機科学基礎理論の新展開)
- 分散JoinJAVAプログラムの通信エラーに対する型判定システム
- 2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み
- 弱最内戦略を完全にする項書換え系の等価変換 (計算機科学基礎理論とその応用)
- 難読プログラミング言語Malbolgeにおけるプログラム構成手法
- 変換と部分評価に基づく非左辺正規なメタ項の停止性証明 (計算機科学基礎理論とその応用)
- 項到達可能性の判定における成長TRSに対する手法と正規化規則による手法の関係 (計算機科学基礎理論とその応用)
- 融合変換を模倣するプログラム生成変換の戦略
- 限量子付き等式理論の変換に基づく仕様からのプログラム生成
- Malbolgeの高級アセンブリ言語への配列機能の追加 (ソフトウェアサイエンス)
- 高階書換え系における引数切り落とし関数の下での実効規則について (システム数理と応用)
- 高階書換え系における引数切り落とし関数の下での実効規則について (ソフトウェアサイエンス)
- 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成 (システム数理と応用)
- 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成 (ソフトウェアサイエンス)
- 語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて (システム数理と応用)
- 語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて (ソフトウェアサイエンス)
- On Extending Matching Operation in Grammar Programs for Program Inversion (知能ソフトウェア工学)
- On Extending Matching Operation in Grammar Programs for Program Inversion (ソフトウェアサイエンス)
- 三値関数を実現するMalbolge命令列の発見のためのSATエンコーディング
- 語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて
- 語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて
- 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成
- 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成
- 高階書換え系における引数切り落とし関数の下での実効規則について
- 高階書換え系における引数切り落とし関数の下での実効規則について
- 単純型付き項書換え系における書換え帰納法について
- 単純型付き項書換え系における書換え帰納法について
- 高階書換え系における引数切り落とし関数の下での実効規則について
- 単純型付き項書換え系における書換え帰納法について
- 語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて
- 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成