Proof normalization with nonstandard objects

Shigeki Goto

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish
Pages (from-to)333-351
Number of pages19
JournalTheoretical Computer Science
Volume85
Issue number2
DOIs
Publication statusPublished - 1991 Aug 12
Externally publishedYes

Fingerprint

Normalization
Number theory
Natural Deduction
Computer programming languages
Computer program listings
Mathematical Induction
Nonstandard Analysis
Formal Proof
Proof System
Prolog
Programming Languages
Elimination
Concurrent
Object
Cover

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

Proof normalization with nonstandard objects. / Goto, Shigeki.

In: Theoretical Computer Science, Vol. 85, No. 2, 12.08.1991, p. 333-351.

Research output: Contribution to journalArticle

Goto, Shigeki. / Proof normalization with nonstandard objects. In: Theoretical Computer Science. 1991 ; Vol. 85, No. 2. pp. 333-351.
@article{e5a41bd444eb4f9983fddb4192084dda,
title = "Proof normalization with nonstandard objects",
abstract = "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.",
author = "Shigeki Goto",
year = "1991",
month = "8",
day = "12",
doi = "10.1016/0304-3975(91)90186-6",
language = "English",
volume = "85",
pages = "333--351",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "2",

}

TY - JOUR

T1 - Proof normalization with nonstandard objects

AU - Goto, Shigeki

PY - 1991/8/12

Y1 - 1991/8/12

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0026206523&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0026206523&partnerID=8YFLogxK

U2 - 10.1016/0304-3975(91)90186-6

DO - 10.1016/0304-3975(91)90186-6

M3 - Article

AN - SCOPUS:0026206523

VL - 85

SP - 333

EP - 351

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 2

ER -