直観主義自然数論とGodel Interpretationに基づくプログラム合成のLiST処理への拡張

• Item type: SIG Technical Reports(1)
• 公開日: 1980-06-19
• タイトル: 直観主義自然数論とGodel Interpretationに基づくプログラム合成のLiST処理への拡張
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 北大工学部
• 著者名: 水上達就
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: プログラムの仕様からプログラムを抽出することを目的として各種のプログラム合成法が研究されてきた。直観主義自然数とGodel Interpretationに基づくプログラム合成の方法は高須氏［1］，佐藤氏［2］，後藤氏［3］によって研究されている。このプログラム合成方法は次のように定義されている。すなわち、xをinput vector，yをoutput vectorとし、ψ（x）をinput述語，〓 （x z）をoutput述語とし、プログラムの仕様を∀_x（ψ（x）⊃^∃zψ（x z））とする。この仕様を直観主義自然数論によって証明し、その証明からGodel Interpretationを用いてψ（x）が成立する時〓（x f(x)）を満たす関数f（x）を抽出する。このプログラム合成法は直観主義自然数論によって仕様の証明を行う為処理するData-typeは自然数のみに限定されている。本論文はLiST構造を処理可能となるようにプログラム合成法を拡張し、さらにGuttag氏［4］，Goguen氏［5］等により研究されているAbstract Data typeによるプログラム作成の手法をこのプログラム合成法に取入れ各種Data-typeを使用したプログラム合成を可能とする方法の提示を目的とする。LiST構造は自然数上で定義するが各自然数を記号と見なすことで記号上のLiST構造を考えることができる。LiST構造処理の為の拡張はLiST構造およびその上でのoperationをData-typeのoperationを使った公理化と同じように公理化し直観主義自然数論に付加しLiST構造およびoperationを帰納的関数によって解釈しGodel InterpretationによるLiST構造を持つ直観主義自然数論の解釈を可能とすることで行っている。また、Godel Interpretationにより解釈可能となることでSchutte氏［5］の直観主義自然数論無矛盾定理と同様にLiST構造を持つ直観主義自然数論は無矛盾であることが証明できる。Data-typeによるプログラム作りはTop-DownでData-typeを考えそれを使ってプログラムを記述し更にその時使用したData-typeをより詳細なData-typeを作りそれで記述しこれを繰返して計算機で実行可能なData-typeにまで行いプログラムとすることである。また、このData-typeによる記述はGuttag氏等の述べるようにData-typeによる証明であり、implementationである。Abstract Data-typeはこの各種Data-typeの数学的記述による共通項であり、これらを設定することにより各種Data-typeの定義を容易ならしめている。プログラムのData-typeによる記述が証明というのは上記プログラム合成の考え方と同一である。無論、証明の仕方で意味論的とSyntactics的の相違があるが証明の基本的考えは同じである。従って、LiST構造を付加するのと同様にAbstract Data-typeをLiST構造上に構成することで各種Data-typeを使ったプログラム合成が可能となる。以下でこのことをDutch National FLagの問題を解くことにより説明する。
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10485570
• 書誌情報: 情報処理学会研究報告プログラミング（PRO）; 巻 1980, 号 9(1980-PRO-012), p. 9-15, 発行日 1980-06-19
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会