著者

坂口 和彦 亀山 幸義

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.10, no.1, pp.14-28, 2017-01-06

---

本研究は,対話的定理証明器Coqの有限型と有限ドメイン関数に関する既存ライブラリを改良し,従来のライブラリを用いた証明をほとんど変更することなく,その証明から抽出されるプログラムの効率を大幅に改善したものである.CoqのSSReflect/Mathematical Componentsライブラリは,有限型と有限ドメイン関数をサポートするライブラリfintypeとfinfunを提供し,これらのデータに対する証明の手間を大幅に削減することに成功している.しかし,その証明からプログラム抽出の手法で作成したプログラムは,多くの場合において非常に効率が悪いという問題がある.本研究では,fintypeやfinfunを改善したライブラリを実装した.このライブラリを用いて作成した証明から抽出したOCamlコードは,既存ライブラリの場合と比べて非常に高速である.例として,行列積の計算では,計算時間をおよそO(n5)からO(n3)へ改善できたことを示す.また,既存のSSReflectライブラリを用いたCoqの証明は,ほとんど書き換えることなく本研究のライブラリを用いた証明となる.例として,GonthierらのFeit-Thompson定理の約17万行におよぶ形式証明が,わずか10行以下の修正で,本研究のライブラリを用いた証明にできたことを示す.

著者

坂口 和彦

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.7, no.5, pp.10-10, 2014-12-05

---

本発表では,スタック指向プログラミング言語PS0と定理証明支援系Coq上に実装したPS0の対話的プログラミング環境を紹介する.この対話的プログラミング環境では,ユーザはまず目的のプログラムがスタックの状態をどう変化させるかを表す形でプログラムの仕様を与え,次にプログラムの断片や証明を順番に与えていくことでプログラムを完成させる.このとき,記述するべき残りのプログラムの仕様は今までに入力したプログラムでどのような状態のスタックに遷移するかを表しているため,一般化されたスタックの状態を見ながらプログラムを記述できる.また,PS0のプログラムをPostScriptのプログラムに変換し,GhostScript等のPostScriptインタプリタの上で実行できることを確認した.We introduce a stack-oriented programming language PS0 and its interactive programming environment implemented in the Coq proof assistant. In this programming environment, first, a user writes the specification of a program as to how the program mutates the stack. Next, the user interactively fills unspecified part of the program. Finally, the user obtains the complete program that proved satisfying the specification. At each step, the environment shows the specification of the program that we should fill. The specification describes the property of the initial and final state of the stacks. Therefore, we can write the program with the generalized state of the stack given. We also implemented a translator from PS0 programs to PostScript programs. It was confirmed that PostScript programs generated by the translator can be executed on PostScript interpreters (e.g., Ghostscript) properly.

著者

山路 剛 金 春峰 石原 好之 戸高 敏之 坂口 和彦 内藤 和文 橋口 伸樹

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会技術研究報告. EE, 電子通信エネルギー技術 (ISSN:09135685)

巻号頁・発行日

vol.106, no.337, pp.19-24, 2006-11-03

被引用文献数

8

---

本稿では,非接触給電システムにおいて並列共振と倍電流整流方式を適用した場合の諸特性について報告する.非接触給電に用いられるトランスの1次側と2次側の間には大きなgap(5mm)を挟み物理的に分離されているため,トランスの結合が悪く大きな漏れインダクタが存在する.トランスの2次側に並列接続したコンデンサとトランスの漏れインダクタは並列共振を行い,更に整流回路には倍電流整流方式を適用することにより高い出力電圧変換率と電力が得られる.解析及び実験結果により,入力24V,出力24V/2Aの試作器において各スイッチのZVS動作と76%の効率が得られたことを確認した.