著者
井出 陽子 向井 国昭
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.28, no.4, pp.4_108-4_113, 2011-10-25 (Released:2011-11-30)

高階述語の呼び出しなどに便利な無名述語(λ項の拡張)の構文および意味を標準のProlog意味論に基づいて定義し,SWI-Prologの上に実装した.無名述語の呼び出しに標準の単一化がそのまま使えるほか,パラメータを持つ無名述語も扱える.無名述語をコンパイル時に通常の述語として展開するので,通常の述語呼び出しと実行効率は同じである.実行時に動的に生成された無名述語に対しては専用のインタプリタで対応する.使用実験の結果,無名述語の利便性や記述力の高さ,安定性が確認できたので,標準環境として使えるように無名述語機能をパッケージ化した.

1 0 0 0 OA 超集合論

著者
向井 国昭
出版者
日本科学哲学会
雑誌
科学哲学 (ISSN:02893428)
巻号頁・発行日
vol.36, no.2, pp.65-77, 2003-12-30 (Released:2009-05-29)
参考文献数
7

The Cantorian set theory survived the Russell Paradox by means of axiomatizing the theory into the standard theory named ZF. ZF has a set theoretical counterpart named FA (Foundation Axiom) to the vicious-circle principle of Russell's ramified type theory. Despite the principle, circular objects and phenomena are ubiquitous in many applications fields of ZF. For modeling such circular things directly as circular sets, Aczel replaced FA with his Anti-Foundation Axiom (AFA) to allow non-well-founded sets in a strong way. The foundation of the new set theory is explained in details.
著者
井出 陽子 向井 国昭
出版者
Japan Society for Software Science and Technology
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.28, no.4, pp.108-113, 2011

高階述語の呼び出しなどに便利な無名述語(λ項の拡張)の構文および意味を標準のProlog意味論に基づいて定義し,SWI-Prologの上に実装した.無名述語の呼び出しに標準の単一化がそのまま使えるほか,パラメータを持つ無名述語も扱える.無名述語をコンパイル時に通常の述語として展開するので,通常の述語呼び出しと実行効率は同じである.実行時に動的に生成された無名述語に対しては専用のインタプリタで対応する.使用実験の結果,無名述語の利便性や記述力の高さ,安定性が確認できたので,標準環境として使えるように無名述語機能をパッケージ化した.
著者
向井 国昭 井出 陽子
雑誌
情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)
巻号頁・発行日
vol.1, no.3, pp.36-36, 2008-10-27

高階述語の引数としてソート付きのラムダ式を許す評価器 (eval),および,適用可能な部分がなくなるまで書き換え規則を適用する項書き換え器 (reduce),この 2 つの述語を SWI-Prolog の上に実装した.関数を表す通常のラムダ項のほかに関係を表すラムダ項を新たに導入した.この導入により,Prolog の特長であるデータの流れの双方向性を活かす,いわば関係型のラムダ計算を実現した.Eval は代数構造における準同型規則を解釈する述語であり,reduce は等号論理のパラモジュレーション規則を解釈する述語であると見なす.つまりいずれも簡潔明快な根拠を持つ計算モデルに基づいて設計した.適用例として Emacs-lisp・Ajax・Unix シェルをとりあげ,それらと Prolog の間のインタフェースの実現方法を示す.Emacs-lisp へは S 式を送信し,それを実行させることにより制御する.こうして Emacs バッファの複雑な編集・制御に,宣言的な Prolog の限定節を用いることができる.Ajax とのインタフェースは,Ajax が関数式を Prolog CGI に送信し,Prolog はそれを eval 述語で評価し,結果の値を HTML として Ajax のフィルタに返信する,という流れである.Unix シェルの呼び出しは,Bash コマンドをまず Prolog の項として表現・生成・操作し,最後にそれを eval 述語でコマンドラインテキストに変換して Unix シェルに送信する.Two interpreters have been written on Top of SWI-Prolog; the one interprets sorted expressions including lambda calculus as arguments of higher order predicates calls, ant the other interprets term rewriting rules. Not only the functional lambda terms but also relational lambda term are now availabe adapted to bi-directional data flow feature of Prolog. In other words, a class of relational lambda caculus is now in Prolog. The implementation obeys fairly general two views that evaluation is homomorphism between algebras of a same kind, and that that on the other hand term rewriting rules are paramodulation of logics with equality. Thus our implementation is based on theoretical clear justifications. As applictions, some interface codes to Emacs-lisp, Ajax, and Unix-shell are illustrated; the extended prolog controls in a declarative way emacs-lisp using S-expressions and Prolog terms depending on the direction, talks with Ajax in Prolog terms, and communicates Bash shell using abstract unix command syntax in Prolog terms. These heterogeneous communications are described in an elegant and unified way based on the two new interpeters.
著者
向井 国昭 井出 陽子
雑誌
情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)
巻号頁・発行日
vol.1, no.3, pp.36-36, 2008-10-27

高階述語の引数としてソート付きのラムダ式を許す評価器 (eval),および,適用可能な部分がなくなるまで書き換え規則を適用する項書き換え器 (reduce),この 2 つの述語を SWI-Prolog の上に実装した.関数を表す通常のラムダ項のほかに関係を表すラムダ項を新たに導入した.この導入により,Prolog の特長であるデータの流れの双方向性を活かす,いわば関係型のラムダ計算を実現した.Eval は代数構造における準同型規則を解釈する述語であり,reduce は等号論理のパラモジュレーション規則を解釈する述語であると見なす.つまりいずれも簡潔明快な根拠を持つ計算モデルに基づいて設計した.適用例として Emacs-lisp・Ajax・Unix シェルをとりあげ,それらと Prolog の間のインタフェースの実現方法を示す.Emacs-lisp へは S 式を送信し,それを実行させることにより制御する.こうして Emacs バッファの複雑な編集・制御に,宣言的な Prolog の限定節を用いることができる.Ajax とのインタフェースは,Ajax が関数式を Prolog CGI に送信し,Prolog はそれを eval 述語で評価し,結果の値を HTML として Ajax のフィルタに返信する,という流れである.Unix シェルの呼び出しは,Bash コマンドをまず Prolog の項として表現・生成・操作し,最後にそれを eval 述語でコマンドラインテキストに変換して Unix シェルに送信する.