Automating induction over mutually recursive functions

Deepak Kapur, M. Subramaniam

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

Abstract

In order to automate proofs by induction a crucial problem that needs to be addressed is to decide on an induction scheme that leads to appropriate induction hypotheses for carrying out the proof. Boyer and Moore proposed in [5] the use of terminating function definitions for generating induction schemes. Inspired by Boyer and Moore's work, Zhang, Kapur and Krishnamoorthy introduced the cover set induction method for mechanizing induction for equational specifications in [14]. Both these approaches do not consider interaction among function definitions. Induction schemes are generated by considering function definitions in isolation, one at a time. In applications involving mutually recursive definitions, exploiting interactions among the definitions seems crucial. The cover set method implemented in the theorem prover RRL [13] as well as the methods implemented for induction in Boyer and Moore's theorem prover Nqthm based on the above approaches, do not perform well when the definitions involved are mutually recursive. Proving even very simple properties over such definitions by these methods requires some form of user intervention. We discuss how the cover set induction method implemented in RRL can be extended to automatically prove inductive properties of mutual recursive functions. An algorithm for generating cover sets from mutually recursive definitions is given. The proposed method has been implemented in the theorem prover RRL and has been extensively experimented with good results. The effectiveness of the method is illustrated using a nontrivial example of showing the equivalence of the call by value and call by name bottom-up evaluation of arithmetic expressions. A comparison of the method with those employed in Nqthm and also with an approach based on implicit induction [7, 3, 2] implemented in the theorem prover Spike is given.

Original languageEnglish (US)
Title of host publicationAlgebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings
EditorsMaurice Nivat, Martin Wirsing
PublisherSpringer Verlag
Pages117-131
Number of pages15
ISBN (Print)9783540614630
StatePublished - Jan 1 1996
Event5th International Conference on Algebraic Methodology and Software Technology, AMAST 1996 - Munich, Germany
Duration: Jul 1 1996Jul 5 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1101
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other5th International Conference on Algebraic Methodology and Software Technology, AMAST 1996
CountryGermany
CityMunich
Period7/1/967/5/96

Fingerprint

Recursive functions
Recursive Functions
Proof by induction
Set Cover
Specifications
Theorem
Bottom-up
Spike
Interaction
Isolation
Equivalence

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kapur, D., & Subramaniam, M. (1996). Automating induction over mutually recursive functions. In M. Nivat, & M. Wirsing (Eds.), Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings (pp. 117-131). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1101). Springer Verlag.

Automating induction over mutually recursive functions. / Kapur, Deepak; Subramaniam, M.

Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings. ed. / Maurice Nivat; Martin Wirsing. Springer Verlag, 1996. p. 117-131 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1101).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kapur, D & Subramaniam, M 1996, Automating induction over mutually recursive functions. in M Nivat & M Wirsing (eds), Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1101, Springer Verlag, pp. 117-131, 5th International Conference on Algebraic Methodology and Software Technology, AMAST 1996, Munich, Germany, 7/1/96.
Kapur D, Subramaniam M. Automating induction over mutually recursive functions. In Nivat M, Wirsing M, editors, Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings. Springer Verlag. 1996. p. 117-131. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Kapur, Deepak ; Subramaniam, M. / Automating induction over mutually recursive functions. Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings. editor / Maurice Nivat ; Martin Wirsing. Springer Verlag, 1996. pp. 117-131 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{3644c319a6b84ec7b4eb61acf475d063,
title = "Automating induction over mutually recursive functions",
abstract = "In order to automate proofs by induction a crucial problem that needs to be addressed is to decide on an induction scheme that leads to appropriate induction hypotheses for carrying out the proof. Boyer and Moore proposed in [5] the use of terminating function definitions for generating induction schemes. Inspired by Boyer and Moore's work, Zhang, Kapur and Krishnamoorthy introduced the cover set induction method for mechanizing induction for equational specifications in [14]. Both these approaches do not consider interaction among function definitions. Induction schemes are generated by considering function definitions in isolation, one at a time. In applications involving mutually recursive definitions, exploiting interactions among the definitions seems crucial. The cover set method implemented in the theorem prover RRL [13] as well as the methods implemented for induction in Boyer and Moore's theorem prover Nqthm based on the above approaches, do not perform well when the definitions involved are mutually recursive. Proving even very simple properties over such definitions by these methods requires some form of user intervention. We discuss how the cover set induction method implemented in RRL can be extended to automatically prove inductive properties of mutual recursive functions. An algorithm for generating cover sets from mutually recursive definitions is given. The proposed method has been implemented in the theorem prover RRL and has been extensively experimented with good results. The effectiveness of the method is illustrated using a nontrivial example of showing the equivalence of the call by value and call by name bottom-up evaluation of arithmetic expressions. A comparison of the method with those employed in Nqthm and also with an approach based on implicit induction [7, 3, 2] implemented in the theorem prover Spike is given.",
author = "Deepak Kapur and M. Subramaniam",
year = "1996",
month = "1",
day = "1",
language = "English (US)",
isbn = "9783540614630",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "117--131",
editor = "Maurice Nivat and Martin Wirsing",
booktitle = "Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings",

}

TY - GEN

T1 - Automating induction over mutually recursive functions

AU - Kapur, Deepak

AU - Subramaniam, M.

PY - 1996/1/1

Y1 - 1996/1/1

N2 - In order to automate proofs by induction a crucial problem that needs to be addressed is to decide on an induction scheme that leads to appropriate induction hypotheses for carrying out the proof. Boyer and Moore proposed in [5] the use of terminating function definitions for generating induction schemes. Inspired by Boyer and Moore's work, Zhang, Kapur and Krishnamoorthy introduced the cover set induction method for mechanizing induction for equational specifications in [14]. Both these approaches do not consider interaction among function definitions. Induction schemes are generated by considering function definitions in isolation, one at a time. In applications involving mutually recursive definitions, exploiting interactions among the definitions seems crucial. The cover set method implemented in the theorem prover RRL [13] as well as the methods implemented for induction in Boyer and Moore's theorem prover Nqthm based on the above approaches, do not perform well when the definitions involved are mutually recursive. Proving even very simple properties over such definitions by these methods requires some form of user intervention. We discuss how the cover set induction method implemented in RRL can be extended to automatically prove inductive properties of mutual recursive functions. An algorithm for generating cover sets from mutually recursive definitions is given. The proposed method has been implemented in the theorem prover RRL and has been extensively experimented with good results. The effectiveness of the method is illustrated using a nontrivial example of showing the equivalence of the call by value and call by name bottom-up evaluation of arithmetic expressions. A comparison of the method with those employed in Nqthm and also with an approach based on implicit induction [7, 3, 2] implemented in the theorem prover Spike is given.

AB - In order to automate proofs by induction a crucial problem that needs to be addressed is to decide on an induction scheme that leads to appropriate induction hypotheses for carrying out the proof. Boyer and Moore proposed in [5] the use of terminating function definitions for generating induction schemes. Inspired by Boyer and Moore's work, Zhang, Kapur and Krishnamoorthy introduced the cover set induction method for mechanizing induction for equational specifications in [14]. Both these approaches do not consider interaction among function definitions. Induction schemes are generated by considering function definitions in isolation, one at a time. In applications involving mutually recursive definitions, exploiting interactions among the definitions seems crucial. The cover set method implemented in the theorem prover RRL [13] as well as the methods implemented for induction in Boyer and Moore's theorem prover Nqthm based on the above approaches, do not perform well when the definitions involved are mutually recursive. Proving even very simple properties over such definitions by these methods requires some form of user intervention. We discuss how the cover set induction method implemented in RRL can be extended to automatically prove inductive properties of mutual recursive functions. An algorithm for generating cover sets from mutually recursive definitions is given. The proposed method has been implemented in the theorem prover RRL and has been extensively experimented with good results. The effectiveness of the method is illustrated using a nontrivial example of showing the equivalence of the call by value and call by name bottom-up evaluation of arithmetic expressions. A comparison of the method with those employed in Nqthm and also with an approach based on implicit induction [7, 3, 2] implemented in the theorem prover Spike is given.

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

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

M3 - Conference contribution

AN - SCOPUS:84886703490

SN - 9783540614630

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 117

EP - 131

BT - Algebraic Methodology and Software Technology - 5th International Conference, AMAST 1996, Proceedings

A2 - Nivat, Maurice

A2 - Wirsing, Martin

PB - Springer Verlag

ER -