Chapter 12 Structural Induction

We build on Danvy and Nielsen's first-order program transformation into continuation-passing style (CPS) to present a new correctness proof of the converse transformation, i.e., a one-pass transformation from CPS back to direct style. Previously published proofs were based on, e.g., a one-pass higher-order CPS transformation, and were complicated by having to reason about higher-order functions. In contrast, this work is based on a one-pass CPS transformation that is both compositional and first-order, and therefore the proof simply proceeds by structural induction on syntax.

Download Full-text

Structural induction: towards automatic ontology elicitation

10.31274/rtd-180813-17073 ◽

2008 ◽

Author(s):

Adrian Silvescu

Keyword(s):

Structural Induction

Download Full-text

A First-Order One-Pass CPS Transformation

BRICS Report Series ◽

10.7146/brics.v8i49.21709 ◽

2001 ◽

Vol 8 (49) ◽

Author(s):

Olivier Danvy ◽

Lasse R. Nielsen

Keyword(s):

Control Flow ◽

Logical Relation ◽

Correctness Proof ◽

First Order ◽

Structural Induction ◽

Flow Information

We present a new transformation of call-by-value lambda-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Because it operates in one pass, it directly yields compact CPS programs that are comparable to what one would write by hand. Because it is compositional, it allows proofs by structural induction. Because it is first-order, reasoning about it does not require the use of a logical relation.<br /> <br />This new CPS transformation connects two separate lines of research. It has already been used to state a new and simpler correctness proof of a direct-style transformation, and to develop a new and simpler CPS transformation of control-flow information.

Download Full-text