• 検索結果がありません。

限定継続命令shift/reset付きλ計算の評価器の抽出

N/A
N/A
Protected

Academic year: 2021

シェア "限定継続命令shift/reset付きλ計算の評価器の抽出"

Copied!
1
0
0

読み込み中.... (全文を見る)

全文

(1)情報処理学会論文誌. プログラミング. Vol.5 No.4 45 (Sep. 2012). 発表概要. 限定継続命令 shift/reset 付き λ 計算の評価器の抽出 廣田 知子1,a). 浅井 健一1. 2012年3月16日発表. 種々の数学的命題を,定理証明系の手法を使って constructive に証明できれば,この証明過程からきわ めて信頼性の高いプログラムが自動的に抽出可能であることが一般的に知られている.本発表では,定理 証明系 Coq を用いて,let 文および継続を扱う命令 shift/reset 文を含んだ多相の型付きラムダ計算におけ る評価器を抽出する.まず,型システムの定式化は,Aydemir らのライブラリを利用して行った.この 定式化において,α-equality の問題を解消するため,変数の名前付けには locally nameless 手法を用いて いる.次に,上記ラムダ計算が強正規化性の性質を満たすことの constructive な証明を Coq により定式 化した.この証明は論理述語を用いて行われている.この証明の定式化により,このラムダ計算における OCaml 言語の評価器プログラムが自動的に抽出された.このプログラムは,入力値の項に型が付くなら ば,必ずプログラムの実行が無限ループを起こすことなく停止することが保証されている.しかし抽出さ れたプログラムの構成は複雑で,そのままでは内部の挙動がどうなっているのかを理解することができな い.ゆえに,抽出したプログラムを手動で簡単化し,プログラム内部の挙動の解釈を行った.また,本発 表では,我々が抽出したプログラムがより有用となりうるための諸点に関しても述べる.. Extraction of Normalizer of Typed Lambda Calculus with Shift/Reset Noriko Hirota1,a). Kenichi Asai1. Presented: March 16, 2012. If various mathematical propositions are constructively proved using a proof assistant, we are able to automatically extract a reliable program from the constructive proof. In this report, we deal with the extraction of the normalizer program of the typed lambda calculus with control operators shift/reset and let-polymorphism using the proof assistant Coq. First, the type system in our study is formalized by fully utilizing the library of Aydemir et al, employing the locally nameless method in order to avoid a complex problem of alpha-renaming. Next, the proof of “strong normalization” on the above lambda calculus has been formalized in Coq by using a particular logical predicate. This formalization leads us to automatically extract the normalizer program in OCaml. An actual implementation of this program is guaranteed to terminate without infinite loop if the input term is well-typed. However, since the program that has been extracted is so complicated to accurately understand its behavior, we have added, by hand, a simplifying process to such extracted program so as to make our interpretation easier. Finally, this report states a couple of points which have to be overcome in order to make our study here more effective and useful.. 1. a). お茶の水女子大学理学部情報科学科 Department of Information Science, Ochanomizu University, Bunkyo, Tokyo 112–8610, Japan [email protected]. c 2012 Information Processing Society of Japan . 45.

(2)

参照

関連したドキュメント

The only thing left to observe that (−) ∨ is a functor from the ordinary category of cartesian (respectively, cocartesian) fibrations to the ordinary category of cocartesian

For example, a maximal embedded collection of tori in an irreducible manifold is complete as each of the component manifolds is indecomposable (any additional surface would have to

It is suggested by our method that most of the quadratic algebras for all St¨ ackel equivalence classes of 3D second order quantum superintegrable systems on conformally flat

Now it makes sense to ask if the curve x(s) has a tangent at the limit point x 0 ; this is exactly the formulation of the gradient conjecture in the Riemannian case.. By the

[3] Chen Guowang and L¨ u Shengguan, Initial boundary value problem for three dimensional Ginzburg-Landau model equation in population problems, (Chi- nese) Acta Mathematicae

We present sufficient conditions for the existence of solutions to Neu- mann and periodic boundary-value problems for some class of quasilinear ordinary differential equations.. We

Then it follows immediately from a suitable version of “Hensel’s Lemma” [cf., e.g., the argument of [4], Lemma 2.1] that S may be obtained, as the notation suggests, as the m A

Our method of proof can also be used to recover the rational homotopy of L K(2) S 0 as well as the chromatic splitting conjecture at primes p > 3 [16]; we only need to use the