Control Flow Analysis for SF Combinator Calculus

TL;DR

This paper develops a control flow analysis for SF combinator calculus, enabling static reasoning about intensional program transformations, and proves its correctness and invariance under translation from SK-calculus.

Contribution

It introduces the first static control flow analysis for SF-calculus, extending existing SK-calculus analysis, and proves its correctness and translation invariance.

Findings

Analysis is correct and sound.

Analysis is invariant under translation from SK to SF.

Enables static reasoning about intensional programs.

Abstract

Programs that transform other programs often require access to the internal structure of the program to be transformed. This is at odds with the usual extensional view of functional programming, as embodied by the lambda calculus and SK combinator calculus. The recently-developed SF combinator calculus offers an alternative, intensional model of computation that may serve as a foundation for developing principled languages in which to express intensional computation, including program transformation. Until now there have been no static analyses for reasoning about or verifying programs written in SF-calculus. We take the first step towards remedying this by developing a formulation of the popular control flow analysis 0CFA for SK-calculus and extending it to support SF-calculus. We prove its correctness and demonstrate that the analysis is invariant under the usual translation from SK-calculus into SF-calculus.