Proof normalization with nonstandard objects

Shigeki Goto

研究成果: Article査読

抄録

It is well known that formal proof systems can serve as programming languages. A proof that describes an algorithm can be executed by Prawitz's normalization procedure. This paper extends the computational use of proofs to realize a lazy computation formally. It enables computation of a proof over stream objects (infinitely long lists) as in concurrent Prolog. In this paper we follow the natural deduction formalism. Our presentation of natural deduction differs from Gentzen's system in the existential elimination rule. We apply the Borkowski-Słupecki's device. There is no difference between Gentzen's rule and Borkowski-Słupecki's rule as far as formula provability is concerned. However, the new rule is essential to proof normalization. A new concept, the pseudonormal proof, is introduced to formalize our normalization method. To deal with infinitely long objects we extend the number theory to incorporate infinite numbers. This is an application of nonstandard analysis to computer programs. We show that the rule of mathematical induction can be extended to cover infinite numbers with appropriate computational meaning.

本文言語English
ページ(範囲)333-351
ページ数19
ジャーナルTheoretical Computer Science
85
2
DOI
出版ステータスPublished - 1991 8 12
外部発表はい

ASJC Scopus subject areas

  • 計算理論と計算数学

フィンガープリント

「Proof normalization with nonstandard objects」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル