A Pure Demand Semantics]A Pure Demand Operational SemanticsWith Applications to Program Analysis
Scott Smith

The Johns Hopkins University
3400 N. Charles St.

Robert Zhang

The Johns Hopkins University
3400 N. Charles St.

This paper develops a novel minimal-state operational semantics for higher-order functional languages which   uses only the call stack and two source program points as the complete state information: there is no environment, no substitution, no continuation, etc.  We prove this form of operational semantics is equivalent to standard presentations.

We then show how this approach can open the door to potential new applications: we define a program analysis as a direct finitization of this operational semantics.  The program analysis that naturally emerges has a number of novel and interesting properties compared to standard program analyses for higher-order programs: for example, it can infer recurrences, and does not need value widening.  We both give a formal definition of the analysis and describe our current implementation.

§ INTRODUCTION

There are numerous well-known approaches whereby operational semantics can be defined for  functional programming languages: substitution-based reduction from the original $\lambda$-calculus <cit.>, substitution-based call-by-name or call-by-value reduction <cit.>, and various machine-based semantics including  SECD, Krivine, CESK <cit.>, and G-machines.  In this paper we define a minimal-state presentation of operational semantics which dispenses with substitutions, environments, stores, and continuations, and instead relies only on the call stack and two source program points to encapsulate all information about the current state of a computation.

But how can variable values be looked up if the only dynamic state information is the call stack?  In fact, there is enough information in the call stack to trace back in time through the control flow to the original point where a variable was defined.  Because no values are propagated forward, we call it a pure demand semantics: all values are looked up on demand.
Note that pure demand is orthogonal to the laziness of lazy functional languages.  Laziness describes the time during evaluation at which an expression is computed.  On-demand is an orthogonal dimension describing how eagerly a variable-to-(expression-or-value) mapping is propagated.  Pure demand semantics can be defined for both call-by-name and call-by-value evaluation.

For an example of the minimality of a pure demand semantics, consider a factorial definition and invocation:

let rec fact n = (if n = 0 then 1 else (fact (n-1))$^{\reallab 2}$ * n)$^{\reallab 3}$
in (fact 4)$^{\reallab1}$

The superscripts $\reallab 1$ $\reallab 2$ $\reallab 3$ here are labels marking selected source program points: $\reallab 1$ is the initial application site, $\reallab 2 $ is the recursive call site, and $\reallab 3$ is the factorial body.  For this program run, an example state of execution in our operational semantics would be simply $[\reallab 2,\reallab 2,\reallab 1] \vdash \reallab 3 \steps \dots$ where $\stk = [\reallab 2,\reallab 2,\reallab 1]$ is the current call stack (a list of call sites in the source program) and program point $\reallab 3$ is the point in the program evaluation is currently taking place.  That is all the state information that is needed (one more source program point may additionally be needed for non-local variable lookup).  This call stack means the current stack state is an initial call at $\reallab 1$ followed by two recursive calls at $\reallab 2$.  Values for local variables such as  are then looked up by walking back up the stack. Looking up  in the body will be seen to be  by chaining back through the arguments at the call sites at $\reallab 2, \reallab 2, \reallab 1$ in turn.

Accessing non-local variable values in pure demand semantics is more complex than local variable access.  The method we use bears some similarity to access links used in implementations of imperative languages with nested function definitions (but no fully first-class functions) <cit.>: non-local variables are accessed by chaining out to the lexical frame in which they were defined.   Some previous demand-driven presentations of operational semantics also dispense with environments and stores <cit.>, but these systems still need additional state information beyond the call stack.  Pure demand semantics have an extremely minimal state.

We prove that our pure demand approach is equivalent to a standard environment/closure big-step operational semantics: it is not changing the meaning of computation, only the means.

So, what good is it?  First it is arguably interesting purely as mathematics: it is a maximal compression of program state information. But we believe it should also make possible potential new constructions; we will present one such construction in this paper.

A Pure Demand Program Analysis  In the second part of this paper, we will present a specific application to give one detailed example to show how pure demand operational semantics is potentially useful: we define a pure demand program analysis, which is a direct finitization of the pure demand operational semantics a la Abstract Interpreters for Free <cit.>.  Standard constructions of abstract interpreters for functional programming languages define a means to finitize a standard operational semantics, and so guarantee a finite environment/stack/store/etc structure.  In our case we only need to finitize the call stack, and for that we can use the standard notion of keeping only the $k$-most-recent frames.  We use a novel stack stitching heuristic to approximate longer stacks by stitching together overlapping $k$-length fragments to gain more precision.

The analysis that emerges has some interesting and unusual properties.  There is no value widening, and as such there is no need to predefine any finite value domain as is usually the case for program analyses.  The analysis naturally infers constant values, sets of constants, intervals, and even recurrence relations on values.

There are additionally some formal benefits of using a pure demand basis.  We will show how a pure demand program analysis can be formally defined solely by a proof system; analyses normally cannot be presented this way since value widening requires repeating proofs and must be expressed as a meta-algorithm on top of an operational semantics <cit.>.  We call the proof system an all paths system because it considers all possible execution path choices in parallel.

We describe our initial implementation of this analysis and show that it performs correctly on common benchmarks for functional program analyses.

Summary of Contributions
Here we summarize the key contributions of this work.

* The definition of a novel “pure demand” form of operational semantics which propagates no variable bindings forward;

* A proof of its correctness relative to a standard propagation semantics;

* The definition of a program analysis directly  from the pure demand semantics, which naturally infers general value abstractions including recurrences;

* The first known fully-rule-based presentation of a higher-order program analysis algorithm which could for example prove useful in automatic verification efforts;

* The stack-stitching technique used in the analysis, which gives a new approach to the venerable question of call stack finitization.

* An implementation which confirms the soundness and potential usefulness of the ideas.

Section <ref> focuses on the operational semantics and Section <ref> establishes the (non-trivial) proof of its equivalence to a standard environment-based operational semantics.  Section <ref> defines the program analysis.  Section <ref> describes the implementation.  Lastly, we cover related work in Section <ref> and conclude in Section <ref>.  All proofs are found in Appendix <ref>A of the supplementary material.

§ A PURE DEMAND OPERATIONAL SEMANTICS

In this section we define the pure demand operational semantics, first for only the pure lambda-calculus and then with additional features.  We will prove the equivalence of the pure demand and a standard operational semantics in the following section.

We somewhat arbitrarily choose to investigate call-by-value only here; call-by-name proceeds similarly.

§.§ The Core Language

( )^^^

(program point labels)

( )

( )^,

[call stacks]
[, …]

Language and interpreter grammar

The language grammar and auxiliary grammar needed for the operational semantics appears in Figure <ref>. All subexpressions are labeled with a unique $\lab$ to represent program points. We will assume some fixed closed $\gexpr$, and require all expression labels $\lab$ in $\gexpr$ to be unique. We may leave off the $\lab$ from some expression if it is not relevant.  We also assume all variable definition occurrences $\gtfun\ \ev \gtarrow\dots$ are unique; any expression repeating a variable binding could be $\alpha$-renamed to satisfy this restriction.  We will allow a pun of writing $\expr^\lab$ at a point when an $\lab$ alone is expected; it is equivalent to writing $\lab$ alone along with a constraint that $\lab$ occurs in $\gexpr$ labeling expression $\expr$.

Let $\myfun(\lab)$ be the nearest enclosing $(\gtfun\ \ev \gtarrow \expr)^{\lab'}$ from the source program point $\lab$ (emphı.e., $\lab$ occurs in $\expr$).

Stacks $\stk$ are formally lists of labels $\stk = [\lab_1, \ldots, \lab_n]$ which by the above pun we will equivalently view as lists of call sites $[(\expr_1 \expr_1')^{\lab_1},\ldots, (\expr_n \expr_n')^{\lab_n}]$.  List append is notated $[\lab_1, \ldots,\lab_n] \lC [\lab_{n+1}, \ldots,\lab_{n+n'}] = [\lab_1, \ldots,\lab_{n+n'}]$ and we overload $\lab_0 \lC [\lab_1, \ldots,\lab_n]$ to mean $[\lab_0] \lC [\lab_1, \ldots,\lab_n]$.  We define $\lab \in [\lab_1, \ldots,\lab_n]$ iff $\lab = \lab_i$ for some $1\leq i\leq n$.

Value results in the operational semantics are of the form $\reval = (\gtfun\ \ev \gtarrow \expr)^{\lab,\stk}$ with $\lab$ the label on the concrete value returned, and $\stk$ the stack at the control flow point where the value was defined.  The $\stk$ can be viewed as a highly compressed representation of the closure and is used for looking up non-local variable values, as we will describe below.

§.§.§ The Rules

The rules are given in Figure <ref>.  We are using a big-step semantics with judgements of the form $\stk \vdash \expr \steps \reval$.  The stack $\stk$ is the call stack at which $\expr$ is evaluated.  Notice there is no substitution and there is no environment; variable lookup in the Var rules is achieved by walking back along the control flow to find the original definition point, and the call stack alone suffices for this.

Relation $\stk \vdash \expr \steps \reval$ is defined by the rules of Figure <ref>.  For well-formed top-level programs $\gexpr$ we define $\vdash \gexpr \steps \reval$ iff $[] \vdash \gexpr \steps \reval$.

Note there is an invariant in the rules that $\expr^\lab$ appearing anywhere in the rules means it is a sub-expression of the original $\gexpr$ (i.e. there is no substitution or re-labeling), except for the special case of variables, which we allow to re-label with function value labels in the Var Non-Local rule.  Each variable will have a very small number of such relabelings possible in practice, and in the worst case is quadratic in the size of the program.  Note that this means the total state information is formally a list of call sites and a pair of program points: there will be one additional program point if it is a non-local variable being looked up.

⊢( )^( )^,

Var Local
() =

⊢_2 ((_1 _2)^' ) ⊢^

Var Non-Local
() =  _1

⊢_1 ( _1 )^_1,_1

_1 ⊢^_1 ((_1 _2)^_2 ) ⊢^

⊢_1 ( )^_1,_1

⊢_2 _2

() ⊢⊢(_1 _2)^

Operational Semantics rules

§.§.§ On-Demand Variable Lookup

The key feature of this semantics is how variable lookup proceeds.  For a local variable $\ev^\lab$, we know that the top (i.e. leftmost) frame of the stack is the call to this function, and thus the parameter, $\expr_2$ in the Var Local rule, when evaluated is the value of $\ev^\lab$.  So, this is exactly what the rule does.  While this is a sound rule, it is very inefficient as we already evaluated the argument in the Application rule, and threw it away.  However, in an implementation a cache of the form $(\stk,\expr) \mapsto \reval$ is used to map stack/program point pairs to their values and will eliminate the slowdown.  Importantly, the cache is just an optimization and the underlying mathematical basis does not require any caching.

The most interesting rule is the Var Non-Local rule.  Here we observe that the variable occurrence $\ev^\lab$ is not a local variable as the $\myfun$ constraint means $\gtfun\ \ev_1 \gtarrow \expr$ is the nearest enclosing function definition around the occurrence $\ev^\lab$, where $\ev \neq \ev_1$.  To find the value of the non-local variable $\ev^\lab$, the philosophy of this rule is to look up the current function (which is the value of $\expr_1$ as the current function is the most recent call) and from this result obtain a stack $\stk_1$ which is the stack in which this function was defined (the Value rule enforces this invariant). At the point this function was defined we are one lexical level closer to the function in which $\ev$ is a local, so we then look up $\ev$ from this new context, which we achieve by renaming $\ev^\lab$ to $\ev^{\lab_1}$ – put $\ev$ in the context where the current function was defined and look up its value from there.  Eventually such a chain up lexical levels will lead us to be directly inside function $\gtfun\ \ev \gtarrow \dots$ where $\ev$ was defined, and the Var Local rule may then be used to look up the variable.

§.§.§ An Example

Figure <ref> contains an example proof tree for
$$\gexpr = (((\gtfun\ x \gtarrow (\gtfun\ y \gtarrow x^{\reallab 0})^{\reallab y})^{\reallab x}\ 1^{\reallab 1})^{\reallab {x1}}\ 2^{\reallab 2})^{\reallab{e}}$$
computing to $1^{\reallab 1}$ (we use, e.g., $\reallab {x1}$ here to notate concrete labels $\lab$). For conciseness we pun in using expression labels to refer to their labeled expression/result since labels have at most one corresponding (non-variable) expression; so for example, $(\gtfun\ y \gtarrow x^{\reallab 0})^{\reallab y}$ we pun as $\reallab y$, and in results we pun $(\gtfun\ y \gtarrow x^{\reallab 0})^{\reallab y,[\reallab{x1}]}$ as $\reallab y, [\reallab{x1}]$.  We also use integer constants to make the example concise, but we do not include operations on integers in this example and so no new rules are required.  Lastly for simplicity we leave out the middle hypothesis of the Application rule which evaluates the argument and throws it away; this is thus a call-by-name example.

The left proof tree here evaluates $\reallab{x1}$, the application to $1$.  The return value here is $\reallab y$, the function $(\gtfun\ y \gtarrow x^{\reallab 0})$.  Then the right proof tree evaluates the body of this function, $\ev^{\reallab {0}}$, and pushes this call site, $\reallab e$, on the stack since we are now evaluating the body of the function of this call.  $\ev^{\reallab{0}}$ is a non-local variable and so the Var Non-Local rule applies here; the top stack frame $\reallab e$ is $((\ldots)^{\reallab {x1}}\ 2^{\reallab 2})$ and so we first look up function $\reallab{x1}$, and obtain result $(\dots)^{\reallab y, [\reallab{x1}]}$, the key being we obtain the stack $[\reallab{x1}]$ which is the calling context where this function was defined.  So, we then take this calling context and make it the current context and look up $\ev$ from this point, but retagging it with $\reallab y$ to give $\ev^{\reallab y}$,   indicating it is being viewed now as having been defined where the $\reallab y$ function in the source was defined. $\myfun(\reallab y)$ is $\reallab x$ and so this re-tagged $\ev$ is now considered local with respect to this context and the Var Local rule then applies, grabbing the $1$ argument from the top frame on the stack, $\reallab {x1} = ((\dots)\
1^{\reallab 1})$, and returning that as the result.

This simple example nontheless captures the essence of non-local variable lookup.  If the variable is more than one lexical level out, the Var Non-Local rule is repeated.

\frac{
\cfrac{
\cfrac{}{[] \vdash\reallab x \steps \reallab x,[]}\ \ \
\cfrac{}{[\reallab {x1}] \vdash \reallab y \steps \reallab y, [\reallab {x1}]}
{[] \vdash \reallab {x1} \steps \reallab y, [\reallab {x1}]}\ \ \
\cfrac{\cfrac{\cfrac{}{[] \vdash\reallab x \steps \reallab x,[]}\ \ \
\cfrac{}{[\reallab {x1}] \vdash \reallab y \steps \reallab y, [\reallab {x1}]}}{[] \vdash \reallab {x1} \steps \reallab y, [\reallab {x1}]}\ \
\cfrac{\cfrac{}{[] \vdash 1^{\reallab 1} \steps \reallab 1, []}}
{[\reallab {x1}] \vdash x^{\reallab {y}} \steps \reallab 1, []}}
{[\reallab {e}] \vdash x^{\reallab 0} \steps \reallab 1, []}
}{[] \vdash \biggl(\biggl(\bigl(\gtfun\ x \gtarrow (\gtfun\ y \gtarrow x^{\reallab 0})^{\reallab y}\bigr)^{\reallab x}\ 1^{\reallab 1}\biggr)^{\reallab {x1}}\ 2^{\reallab 2}\biggr)^{\reallab{e}}  \steps \reallab 1, []}

An Example Derivation Using the Rules of Figure <ref>

§.§ An Extended Language

In this section we show how the pure demand approach easily scales to full functional languages.  Concretely we flesh out the language of the previous section by adding records, integers, booleans and conditionals.  Language features without variable bindings are relatively easy to add to this theory as they largely mirror standard big-step operational semantics rules.  There is a design choice of how lazy the operators should be, either lazy in that e.g.  returns , or eager in that it returns . Here we will somewhat arbitrarily present the lazy version as we will need to use this form in a program analysis built on this system in Section <ref>.  We define a separate function $\evalval$ with e.g., $\evalval(\texttt{3 + 2})=\texttt{5}$, which does the pulling.

( )^^; …

[program labels]
(program point labels)

[record labels]
(record labels)

0 1 -1 …
( )^; …

[result values]
( )^,
; …()

[call stacks]
[, …]

Extended Language Grammar

The extended grammar appears in Figure <ref>.  The source language of expressions $\expr$ is fairly standard but note we also include $\lbl \gtin \expr$ syntax for runtime checking of the presence of a field in a record; with this operation it is possible to encode variants as records.  For example $\ob \texttt{hd} \gteq \expr; \texttt{tl} \gteq \expr \cb$ plus $\ob \texttt{nil} \gteq 0 \cb$ can encode lists with $\texttt{nil} \gtin \expr$ encoding the check for $\expr$ being an empty list. Only functions, application, and variables need labels $\lab$ in source programs so we leave them off the other constructors.

Result values here are extended to include record values, integers and booleans, and with the lazy operator approach we are taking, mentioned above, the operators will not be evaluated.  The only cases where the concrete value of an operation is needed for execution to continue is the boolean value of a conditional guard to know which conditional branch to take, or for a function result (which could be inside a record and so will need record projections).  We will define a special function $\evalval$ which reduce the operators in value results $\reval$ to produce actual values $\eval$ when needed.

Relation $\stk \vdash \expr \steps \reval$ for the extended language is defined by the rules of Figure <ref>.  For top-level programs $\gexpr$ we define $\vdash \gexpr \steps \reval$ iff $[] \vdash \gexpr \steps \reval$.

Value is not a function

Value Fun
⊢( )^( )^,

Var Local
() =

⊢_2 ((_1 _2)^' ) ⊢^

Var Non-Local
() =  _1

⊢_1 _f

(_f)=( _1 )^_1,_1

_1 ⊢^_1 ((_1 _2)^_2 )  ⊢^

⊢_1 _1

⊢_2 _2
⊢_1 _2 _1 _2

Record Value
⊢_1 _1 …⊢_n _n
⊢_1 _1; …; _n _n _1 _1; …; _n _n

Record Project
⊢_1 _1; …; _n _n

= _i
⊢_1 _1; …; _n _n

Record Inspect
⊢_1 _1; …; _n _n

⊢_1 _1; …; _n _n

() =

⊢_ '
⊢(_ _)^'

⊢_1 _f

(_f)=( )^','

⊢_2 _2

() ⊢⊢(_1 _2)^

Operational Semantics Rules for the Extended Language

Inspecting the rules, for the new syntax they are similar to standard big-step rules modulo the very lazy results returned; the function application and variable lookup logic is basically identical to the core language.

$\evalval$ is defined by induction via the clauses in Figure <ref>.  The function is undefined for cases of type mismatch, e.g. projecting a number or adding records.

§.§.§ Efficiency

It is worthwhile to ask how much efficiency has been lost if an interpreter was implmented with this mechanism compared to standard methods.  If the evaluation relation is cached via a map $(\stk,\expr) \mapsto \reval$, and $\evalval$ is also cached as $\reval \mapsto \eval$, there will be no duplicate computations, and in fact in some cases the cache will speed up computations as it will implicitly memoize all function calls (e.g. a naive Fibonacci implementation will be linear not exponential).  The keys of the cache include the stack $\stk$, which is an unbounded list, but hash-consing should allow “O(1)” cache lookup.

$\evalval(n)  =  n$

$\evalval(\ebool)  =  \ebool$

$\evalval((\gtfun\ \ev \gtarrow \expr)^{\lab,\stk})  =  (\gtfun\ \ev \gtarrow \expr)^{\lab}$

$\evalval(\reval_1 \binop \reval_2) = \evalval(\reval_1) \binop \evalval(\reval_2)$

$\evalval(\reval \gtdot \lbl_i) = \eval_i \text{ where } $

$\evalval(\reval) = \ob  \dots; \lbl_i \gteq \eval_i; \dots \cb$

$\evalval(\lbl \gtin \reval) = \gttrue \text{ if } $

$\evalval(\reval) = \ob \dots; \lbl \gteq \eval; \dots \cb $

$\evalval(\lbl \gtin \reval) = \gtfalse \text{ if } \lbl \not \in \evalval(\reval)$

$\evalval(\ob \lbl_1 \gteq \reval_1; \dots; \lbl_n \gteq \reval_n \cb) =$

$\ob \lbl_1 \gteq \evalval(\reval_1); \dots; \lbl_n \gteq \evalval(\reval_n) \cb $

The Definition of $\evalval(\reval)$

We have implemented a pure demand interpreter for this language and have verified its proper function on a test suite; this will be briefly covered in Section <ref>.

§ SOUNDNESS

In this section we establish that the pure demand operational semantics is provably equivalent to a standard environment/closure operational semantics.  The proof is non-trivial and shows there is a large conceptual gap between the two equivalent forms of operational semantics.  We will prove soundness only over the core language of Section <ref>, because that is where nearly all the novelty is.

We will first will define a standard environment/closure based operational semantics $\vdashe$, the goal being to show this standard system is equivalent to the core system $\vdash$ of Definition <ref>.  The two systems differ considerabily so we will define two intermediate systems $\vdashc$ and $\vdashcc$, and then will show $\mathnormal\vdash \Leftrightarrow \mathnormal\vdashe$ by establishing three lemmas: $\mathnormal\vdash \Leftrightarrow \mathnormal\vdashc$, $\mathnormal\vdashc \Leftrightarrow \mathnormal\vdashcc$, and  $\mathnormal\vdashcc \Leftrightarrow \mathnormal\vdashe$.

Complete proofs of all Lemmas are given in Appendix <ref>A which is part of the supplemental submission information.

§.§ Environment/closure based system

We first start off with $\vdashe$, a standard call-by-value environment/closure big step operational semantics.

( )

[results aka closures]

Environment Semantics Grammar

We let $\envt = [\ev_0 \mapsto \reval_0,\dots,\ev_n \mapsto\reval_n]$ represent an environment mapping variables to their values.  Since the language has no !let! and only functions, we can without loss of generality assume that the head variable mapped, $\ev_0$, is the (single) local variable, $\ev_1$ is the (single) non-local defined in the immediately containing static scope, etc.  Closures are results of the form $\reval = (\gtfun\ \ev \gtarrow \expr)^{\envt}$ where the $\envt$ is of the aforementioned form. We no longer need the program point labels $\lab$ so we remove them.  The revised grammar is in Figure <ref>.  Note that we are reusing metavariable names such as $\expr$ across the different systems but it should be clear from context whether we are in $\vdash$, $\vdashe$, etc.

The big-step operational semantics is completely standard.

Relation $\envt \vdashe \expr \steps \reval$ is defined by the rules of Figure <ref>. $\vdashe \gexpr \steps \reval$ iff $[] \vdashe \gexpr \steps \reval$.

( ) ( )^

[_0 ↦_0,…,_n ↦_n]  _i _i

_1 ( )^_1

_2 _2

[↦_2] _1  (_1 _2)

Operational Semantics With Environment and Closure

§.§ Chaining variable lookup directly

We will now proceed to define two intermediate systems $\vdashc$ and $\vdashcc$ to link $\vdash$ with $\vdashe$.  In this section we define $\vdashc$ which will make the variable lookup of $\vdash$ a step closer to a standard operational semantics by making a single Var rule which does all the scope-chaining in one rule.

$\stk \vdashc \expr \steps \reval$, the chaining version of $\stk \vdash \expr \steps \reval$, is defined by the rules of Figure <ref>.

( ) ( )^

n ≥0

∀0 ≤i < n.  _i ≠_i+1

∀0 ≤i ≤n. _i _i ( _i _i” )^_i+1'

∀0 ≤i ≤n. _i' = ((_i '_i) _i)

_n '_n _0' _n

_1 ( )^_1

_2 _2

((_1 _2) ) (_1 _2)

Operational Semantics With Chaining Var lookup

The grammar of this system is the same as in the original, Figure <ref>, except the labels $\lab$ are no longer needed anywhere so are removed in the rules.  This is possible because we are chaining all of the Var Non-Local together directly and the labels were only required to make this connection.

It is clear in any proof in $\vdash$ that any variable lookup starting at the conclusion node must have $n \geq 0$ Var Non-Local rules in a row followed by a single Var Local rule.  This holds because the only rules in $\vdash$ for looking up variable values are these two rules, and each use of Var Non-Local will require one of the two variable rules to prove its rightmost hypothesis, and this chain must eventually end in a Var Local since the proof tree is finite.

The intuition of the new Var rule is that it is a“proof tree macro”  expressing the chain described above in a single rule.  The number $n$ reflects how deeply the variable $\ev_n$ is lexically nested; $n=0$ represents a local variable.  For the case of a local variable there are no function definitions to chain through in that case, and we can immediately look up the variable by looking up $\expr_0'$ (the rule in fact looks up the function we are calling, $\expr_0$, so local lookup can be more notationally consistent with non-local lookup).  For the case where $n=1$, it means $\ev_1$ is occuring immediately inside a $\gtfun\ \ev_0 \gtarrow\dots$ which occurs immediately inside a $\gtfun\ \ev_1 \gtarrow\dots$.  In this case the lookup proceeds in the same spirit as the original system: we first look up the function $\expr_0$, which as result has stack $\stk_1$, then we take the top frame on this stack, $(\expr_1\ \expr_1')$, and $\expr_1$ in turn must evaluate to a function with $\ev_1$ as parameter by the first forall condition and so the value of $\ev_1$ is then the value of $\expr_1'$, $\reval$.  In general this pattern repeats for arbitrary levels of lexical nesting.

Before proving the systems equivalent we characterize the canonical form that variable lookup subtrees must take in $\vdash$.  Figure <ref> expresses this canonical form.  In this figure all rule applications are Var Non-Local except for the upper right rule which is Var Local.  Note that the hypotheses $\ev_i \neq \ev_{i+1}$ and $\myfun(\lab_i)= \gtfun\ \ev_i \gtarrow \expr_i''$ are elided from the figure for readability.    Recall that the proof of this Lemma and other assertions below are found in the supplementary material.

Any variable lookup subtree in a proof of $\stk \vdash \expr \steps \reval$ must be of the form of Figure <ref>.

_0 ⊢_0 ( _0 _0” )^_1, (_1  _1')_1
_1⊢_1 ( _1 _1” )^_2, (_2  _2')_2
_n ⊢_n' ((_n _n')^_n' _n) ⊢_n^_n _2⊢_2 …  ⋮(_2 _2')^_2'_2 ⊢_n^_2
(_1 _1')^_1'_1 ⊢_n^_1
/((_0 _0')^_0' _0) ⊢_n^_0

Canonical Variable Lookup Proof Tree Structure of $\vdash$

We can now prove the two systems equivalent.

$\stk \vdash \expr \steps \reval$ iff $\stk \vdashc \expr \steps \reval$.

§.§ Tangent: A Display System

There is a natural system which is a hybrid of the previous $\vdashc$ and the subsequent $\vdashcc$ system which is of interest, and we insert it here as a brief tangent; it is not used in the proof.

The approach here is rather than chaining backward for the sequence of $\stk$ needed for non-local variable lookup, we can instead eagerly push forward a list of stacks.  This push-forward approach is in spirit the display optimization technique applied to access links <cit.>: the chain of stack frames to go through is pushed forward as a table (a display).

In this system we need labels again, but only to mark variables with their lexical depth.  We assume for each variable occurrence $\ev$ in the program, it appears as $\ev^n$ where $n$ is constrained to be the number of enclosing non-$\ev$ $\gtfun$ definitions for this particular occurrence of $\ev$ (i.e., it is a DeBruijn index but starting the count at 0 instead of DeBruijn's 1).
For example, $\gtfun\ \texttt{x} \gtarrow \texttt{x}^0$ and  $\gtfun\ \texttt{x} \gtarrow \gtfun\ \texttt{y} \gtarrow (\texttt{x}^1\ \texttt{y}^0)$  are well-formed programs, and $\gtfun\ \texttt{x} \gtarrow \texttt{x}^1$ is not well-formed.   As was required previously, all variable bindings must be globally unique.

The $\display= [F_1,\ldots]$ are displays, lists of stack frames $F$.

Stack frames are also now $F = (\expr_1\ \expr_2)^\display$, each call needs to be able to restore its display when we pop out of the function body.  Note that displays are a recursive data structure as displays themselves contain displays on the frames; this makes them considerably more complex than the classic displays used in compiler optimization.

$\display \vdashal \expr \steps \reval$, the displays version of $\stk \vdash \expr \steps \reval$, is defined by the rules of Figure <ref>.

( ) ( )^

= [F_0, …, F_m,…,F_n]

0 ≤m ≤n

F_m = (_m '_m)^_m

_m '_m ^m

_1 ( )^_1

_2 _2

[(_1 _2)^]_1 (_1 _2)

Operational Semantics With Displays

This system is not as demand-driven as $\vdash$ but since it preserves the property of not propagating forward any actual program values it may have applications. The program analysis of Section <ref> for example could have been based on this underlying operational semantics and would still not propagate values forward.

§.§ Caching Lookups

Getting back to the soundness proof, for the next step we are going to cache all of the function and argument lookups needed in the Var rule of the previous system, producing the $\vdashcc$ system.  With this change the proof tree should be structurally isomorphic to a standard environment/closure semantics proof tree for the same initial expression.

Concretely we add a cache $\cachef = [\la \stk_0,\cachef_0,\cachel_0,\expr_0\ra \mapsto \reval_0, \dots]$ to each proof node to cache function lookups, and a cache $\cachel = [\la \stk,\cachef,\cachel,\expr\ra \mapsto (\reval,\ev)]$ to cache the local argument lookup, and the judgement form in this new cached chaining system will be $\stk, \cachef, \cachel \vdashcc \expr \steps \reval$.  In order to get a strong enough induction invariant for direct proofs the caches also need to cache previous cache states; in the above form it can be seen that we are precisely capturing other judgements in the cache.  We do not need to cache non-local arguments because we will include these local argument caches in our function closures, and so $\cachel$ will either be a singleton list or an empty list (the latter for when we are at the top of the program).  The $\cachel$ also needs to remember the function parameter $\ev$ along with the result $\reval$.  We additionally need to add $\cachef$ and $\cachel$ to the closures so they are now of the form $(\gtfun\ \ev \gtarrow \expr)^{\stk,\cachef,\cachel}$.  The intuition is the function cache will cache lookups $\stk_i \vdashc \expr_i \steps \reval_i$ so they don't need to be repeated in the Var rule, and similarly local argument lookup $\stk \vdashc \expr_0' \steps \reval$ will be cached.  The function cache we represent as a list and not a set of mappings because the rules invariably put the cached items with the innermost static scope at front, next-innermost next, etc.

$\stk, \cachef, \cachel \vdashcc \expr \steps \reval$ is defined by the rules of Figure <ref>.

Observe that only the Application rule adds items to the cache mappings and it adds the lookup of the function and argument that we just performed.  So it is indeed just a cache.
We write $\lC_{0\leq i \leq m} [X_i]$ as shorthand for $[X_0,\ldots, X_m]$.

, , ( ) ( )^,,

0 ≤n ≤m

= _0 ≤i ≤m[_i,_i',_i',_i↦( _i _i” )^_i+1',_i+1,_i+1]

∀0 ≤i < n. _i+1' = ((_i+1 '_i+1) _i+1)

_n = [_n,_n',_n',_n'↦(,_n)]

((_0 _0')_0), , _0 _n

, , _1 ( )^_1,','

, , _2 _2

((_1 _2) ), (,,,_1↦( )^_1,',' '), [,,,_2↦(_2,)] , , (_1 _2)

Operational Semantics With Chaining and Caching

This system is nearly identical to the previous one but rather than repeating the exact same function lookups deeper in the proof we simply cache them.

All of the proof systems are deterministic; we in particular need the fact that $\vdashc$ is deterministic in the Lemma below.  The proof is direct by induction.

$\vdash$, $\vdashc$, $\vdashcc$, and $\vdashe$ are all deterministic: given $\expr$ and all the assumptions to the left of the turnstile, there is at most one proof tree that can be constructed.

We can now prove $\vdashc$ and $\vdashcc$ are equivalent.

For all $\expr$, $[] \vdashc \expr \steps(\gtfun\ \ev \gtarrow \expr)^{\stk}$ iff $[], [], [] \vdashcc \expr \steps (\gtfun\ \ev \gtarrow \expr)^{\stk,\cachef,\cachel}$.

This system is very close to the standard environment/closure system of Section <ref>, because the caches indirectly have all of the environment mappings cached in them.  Concretely, we define a function which will extract variable bindings given the current stack and caches.  The definition is inductive because function values themselves need to have their closure environments extracted.  The definition is well-founded based on lexical nesting depth.

Inductively define $\extractenvt$ and $\extractcl$ as follows.

Let $\extractenvt(\stk_0,\cachef,\cachel_0)$ be
$[\ev_0 \mapsto \reval_0^{\extractcl(\reval_0)}, \dots, \ev_n \mapsto \reval_n^{\extractcl(\reval_n)}]$
$\reval$s in the above are sloppy where

$$\cachef = [\la \stk_0,\expr_0\ra \mapsto (\gtfun\ \ev_{0} \gtarrow \expr_{0}'' )^{\stk_{1}',\cachef_{1}'\cachel_{1}}, \dots, \la \stk_m,\expr_m\ra \mapsto (\gtfun\ \ev_{m} \gtarrow \expr_{m}'' )^{\stk_{m+1}',\cachef_{m+1}',\cachel_{m+1}} ]$$

and where for all  $0\leq i < m$, $\stk_{i+1}' = ((\expr_{i+1}\ \expr'_{i+1}) \lC \stk_{i+1})$, and $\cachel_i = \la \stk_i,\expr_i'\ra \mapsto (\reval_i,\ev_i)$.
Let $\extractcl((\gtfun\ \ev \gtarrow \expr)^{[],[],[]})$  be $[]$ and let $\extractcl((\gtfun\ \ev \gtarrow \expr)^{(\expr_0 \expr_0')\lC\stk,\cachef,\cachel})$
be $\extractenvt(\stk,\cachef,\cachel)$.

§.§ Relating the cached and environment systems

The $\extractenvt$ function links this system with the cache chaining system.  Concretely, we have the following Lemma.

Given fixed source program $\gexpr$, $[],[] \vdashcc \gexpr \steps (\gtfun\ \ev \gtarrow \expr)^{\stk,\cachef,\cachel}$ iff $[] \vdashe \gexpr \steps (\gtfun\ \ev \gtarrow \expr)^{\envt}$, where $\extractenvt(\stk,\cachef,\cachel)=\envt$.

Putting together the Lemmas relating these different systems we directly have the following.

Given fixed source program $\gexpr$, $[] \vdash \gexpr \steps (\gtfun\ \ev \gtarrow \expr)^{\lab, \stk}$ iff $[] \vdashe \gexpr \steps (\gtfun\ \ev \gtarrow \expr)^{\envt}$.

§ A PURE DEMAND PROGRAM ANALYSIS

We now develop an application of pure demand operational semantics: it can be used to derive a program analysis by only having to finitize the possible call stack states since that is the only unbounded state in a judgement; in a standard program analysis the environment and store also need to be finite.

We will force the stacks to the top-$k$ frames for fixed $k$, a simple and standard stack finitization found in many program analyses <cit.>.  In these standard analyses the call stack is only needed to check for repeated states and record the return point, but in our system the stack is critical to demand-driven variable lookup.  For this reason, just keeping the $k$ most recent stack frames for us would lead to a great deal of inaccuracy in variable lookup: with a deep enough call stack there would be a complete loss of information on where a variable value originated from.  But, we can recover more precision by remembering all stack fragments visited thus far, and “stitching” existing stack fragments together where one fragment's suffix matches another fragment's prefix.

As with the operational semantics we will first study the functions-only fragment, and prove properties of that system.  We will then extend it to the larger language syntax of Section <ref>.

§.§ The Core Analysis

We will use the same grammar as for the core language of Figure <ref>.  We use notation $\lC_k$ to denote a list consing which is then shortened to at most $k$ elements by dropping elements from the rear of the list: $\lab_0 \lC_k [\lab_1,\ldots,\lab_{k-1},\ldots] = [\lab_0,\lab_1,\ldots,\lab_{k-1}]$ and $\lab_0 \lC_k [\lab_1,\ldots,\lab_m]$ for $m < k$ $= [\lab_0,\lab_1,\ldots,\lab_{m}]$.  We will use this function to drop some stack frames at calls in order to finitize the analysis. It must be the case that  $k \geq 1$, and practically speaking $k \geq 2$ is needed or no stitching will occur.  We need maintain a history of all maximally-$k$-length stack fragments $\stk$ seen so far in the derivation in set $\sfrags=\{\stk_1,\ldots,\stk_n\}$, as we maintain an invariant that any actual runtime stack has to be a concatenation of fragments from $\sfrags$.

Given fixed $k>0$, relation $\stk, \sfrags \vdasha \expr \steps \reval$ is defined by the rules of Figure <ref>.  For top-level programs $\gexpr$ we define $\vdasha \gexpr \steps \reval$ iff $[], \{\} \vdasha \gexpr \steps \reval$.

,( )^( )^,

Var Local
() =

_0 ∈

_0 = ' '

(') ,_2 _v _v
((_1 _2)^' ),^_v _v

Var Non-Local
() =  _1

_0 ∈

_0 = _2 '

('),_1 ( _1 )^_1,_1 _1

_1,_1 ^_1 _v _v
((_1 _2)^_2 ),^_v _v

,_1 ( )^_1,_1 _1

(), (_1 ∪()) _v _v
,(_1 _2)^_v _v

Pure Function Program Analysis Rules

§.§.§ Explaining the rules

The rules closely mirror the $\vdash$ rules of Figure <ref>, but at application time the call stack $\stk$ is pruned to be at most $k$-length.  Since these are big-step operational semantics there is no issue with call-return alignment when the stack is pruned: a big-step execution implicitly aligns calls and returns.  The only information loss is that the stack may not be accurate when used for variable lookups, and recursion may turn into a cycle by visiting the same stack again.  Note that for simplicity of presentation we have removed the evaluation/discard of the function argument from the Application rule.

Recall that both Var Local and Var Non-Local need to pop off a stack frame and perform a lookup (the argument in the former and the function in the latter).  If we naively followed this approach here, since these stacks may have been pruned, at some point we could “pop off” the end of the stack and would completely lose all context information.  To avoid this imprecision, in the Var rules we don't just pop a frame off the stack, we pop a frame from the top but then potentially add a new frame to the bottom of the stack to maintain up to $k$ frames of stack context. We pick such frames based on the history of all call stack fragments seen thus far in $S$, so we only “stitch” together a new fragment if it aligns with the remnant of the current stack.

Delving into a bit more detail, the $\sfrags$ set can seen to be recording each new stack fragment encountered in every  Application rule: when executing the function body we take the new stack $(\lab \lCk \stk)$ and union it into $\sfrags$ to record it for future stitching.   Then, the Var rules (say Var Non-Local) when popping a frame $\lab_2$ off the stack $\lab_2\lC\stk$ finds an existing stack fragment $\stk_0$ in $\sfrags$ which shares the top $k$ frames with $\lab_2\lC\stk$, plus it has potentially extra frames $\stk'$ which we can use to extend the fragment when we pop off $\lab_2$: we pop $\lab_2$ from the top but then add $\stk'$ to the end at the same time.  $\stk'$ will be either 0 or 1 frames invariably.  A similar stack stitching is performed in Var Local.

Consider for example a Var Non-Local rule instance with $k=2$ where the current stack fragment is $(\expr_1\ \expr_2)^{\lab_2} \lC \stk = [\lab_2, \lab_1]$ (so $\stk = [\lab_1]$) and $S = \{[\lab_2,\lab_1],[\lab_2, \lab_3], [\lab_1, \lab_0]\}$.  The only fragments $\stk_0 \in \sfrags$ which have a required prefix of $[\lab_2,\lab_1]$ are in fact just that stack itself, $[\lab_2,\lab_1]$, and so the popped stack will be just $[\lab_1]$.  Thus far there is no lossiness, but if there was again a Var rule firing with this stack we can see the only fragment in $\sfrags$  with prefix $[\lab_1]$ is $[\lab_1, \lab_0]$ and so upon popping $\lab_1$ we obtain not an empty stack but $[\lab_0]$: we stitched together fragments to maintain full stack accuracy.  If there was additionally a fragment $[\lab_1, \lab_4] \in \sfrags$ there would have been two choices for the popped stack at this point, $[\lab_0]$ and $[\lab_4]$, and only one can be the correct one from the deterministic non-abstract execution; the analysis will nondeterminstically proceed with either stack.  Note it can be seen from the above that if $k<2$ there will be no additional frames gained from stitching with $\sfrags$ so  $k$ should de facto be at least $2$.

It is easy to show the analysis is computable by a raw counting argument.

For all $\gexpr$, the set $\{\reval \mid [],\{\} \vdasha \gexpr \steps \reval\}$ is recursive.

§.§.§ Soundness

A program analysis is sound if for all programs the analysis can produce any value that the operational semantics can.  Soundness is largely straightforward here as the rules are identical besides stack pruning and stitching.  All we need to show is that the concatenation of stack fragments in $\sfrags$ will include enough pieces to glue together the actual runtime stack of a concrete run.  Since each new $k$-length fragment is added to $\sfrags$, the result is direct.

If  $[] \vdash \gexpr \steps (\gtfun\ \ev \gtarrow \expr)^{\lab,\stk}$ then $[], \emptyset \vdasha \gexpr \steps (\gtfun\ \ev \gtarrow \expr)^{\lab,\stk\lceil_k} \globs \sfrags$ for some $\sfrags$.

§.§ An All-Paths Formalization of Program Analysis

The program analysis of Section <ref> does not directly define an efficient implementation: it is both nondeterministic with multiple proof trees possible for the same program, and has infinite cycles of proof construction attempt which need to be pruned with an occurs check.  In standard presentations of higher-order program analyses which use an operational semantics <cit.>, the system of the previous section is as far as the analysis can be specified in a rule-based system.  This is because as more values accrue the same proof derivation will need to be repeated for the wider value space; this is not possible to present in a rule-based system and instead a separate pseudocode algorithm must be given to specify how the rules are realized in an implementation.

Fortunately in our system the stack is the only state, and there is no value widening because there are no values to widen: no values are propagated forward.  So, we can fully specify the program analysis via a single proof system returning a set of possible results at once.  This gives a rule set which serves as a direct basis for the implementation.

[visited states]{ ,,, …}
{ ( )^,, …}

[Seen stacks]
{, …}

Stuctures for All-Paths Analysis

We now present this implementation-based rule system, which we term an all-paths presentation because the rules run all possible combinations of values in parallel. Along with running all paths we also track and prune potentially cyclical proofs in the rules themselves by maintaining a set of visited states $\visited$ in the rules and using special Stub rules to prune proof goals that are provably cyclic.

Figure <ref> presents the changed grammar elements needed for the all-paths analysis. Value results $\reval$ are now sets of function values $\{ (\gtfun\ \ev_1 \gtarrow \expr_1)^{\lab_1,\stk_1}, \ldots, (\gtfun\ \ev_1 \gtarrow \expr_n)^{\lab_n,\stk_n}\}$ where each value represents one possible result of the analysis.
The set can also be empty for the case that there is a cycle (meaning the program provably diverges).  We use visited sets $\visited = \{\la \expr,\stk, \sfrags \ra, \dots \}$ in judgements to enforce an occurs check: we keep an audit trail which includes both every function call frame as well as every variable lookup request ($\expr$ in $\la \expr,\stk, \sfrags \ra$ is either an $\ev^\lab$ or a $(\expr_1\ \expr_2)^\lab$).  Additionally in this set we include the complete snapshot of the state, i.e. the current $\stk$ and $\sfrags$.  We will use this audit trail in $\visited$ to see if we are asking the exact same question previously asked in a parent node in the proof tree, and will “stub” out any proof goal if so as it is provably cycling.

We now define the all-paths analysis relation, $\vdashaa$, with the rules of Figure <ref>.  There we overload $\bigcup$ on a set of pairs of sets to mean $\bigcup$ applied to each component of the pair and coalesced back as a pair.  Let $\suffixes(\lab,\stk,\sfrags) = \{\stk \lC  \stk' \mid \exists \stk'' \in \sfrags. \ \stk'' = \lab \lC \stk \lC \stk'\}$.

Relation $\stk, \sfrags, \visited \vdashaa \expr \steps \reval \globs \sfrags$ is defined by the rules of Figure <ref>.

Observe that Application places the current state in the stack $\visited_\textrm{new}$ which then gets passed up the proof tree. Then, Application Stub checks if the current state is already in $\visited$ and if so it stubs the proof with a leaf node.  The rules need to explicitly perform this stubbing or any program which diverges will not have any (well-founded) proof tree.  Along with stubbing out cycles the analysis takes all paths in parallel; the rules realize this by returning sets of values.

, , ( )^{( )^,}

Var Local
() =

_0 = ((_1 _2)^' )

^, _0,∉

= (',,)

(_1,_1) = ⋃{ (_0,_0) |∃_1 ∈.  _1, , ∪{^, _0, }_2  _0 _0 }
_0, , ^_1 _1

Var Non-Local
() = _f = ( _1 )^_1

_0 = ((_1 _2)^_2 )

^, _0, ∉

= (_2,,)

(_1,_1) = ⋃{ (_0,_0) |∃_1 ∈.
_1, , _1 _0 _0 }

(_2,_2) = ⋃{ (_0',_0') |∃_f^_1,_1 ∈_1. _1, _1, ∪{^, _0, _1}  ^_1 _0' _0'}

_0, , ^_2 _2

Var Stub

^,, ∈

, , ^∅

, ,  ∪_new _1 _1

_new={, , _1∪{}}

(_2,_2) = ⋃{ (_0,_0) |( _1 _1)^_1,_1 ∈_1

(), _1 ∪{}, ∪_new _1 _0 _0 }
, , ( ')^_2 _2

App Stub, , ∈, , ( ')^∅

Core Language All-Paths Program Analysis Rules

The all-paths system $\vdashaa$ is just merging all the possible proof trees of the single-path system $\vdasha$ into a single tree. Note that it treats the $\sfrags$ set slightly differently as it accumulates one set for all possible paths and the single-path rules accumulate an $\sfrags$ on a more accurate per-path basis.  This is analogous to the single-threaded store optimization of conventional analyses <cit.>. In both our system and the conventional systems there is some loss of precision with a single-threaded store, but in return a significant speed-up is gained.

We conjecture that the all-paths system produces in one go at least all the results of the per-path system (it may produce more results due to the potentially larger $\sfrags$).
[All-Paths Soundness]conjectureaisaa

Letting $\reval$ be $\{(\gtfun\ \ev_1 \gtarrow \expr_1)^{\lab_1,\stk_1}, \ldots, (\gtfun\ \ev_n \gtarrow \expr_n)^{\lab_n,\stk_n}\}$, it is the case that for all $1\leq i \leq n$, if $[], \emptyset \vdasha \expr \steps (\gtfun\ \ev_1 \gtarrow \expr_i)^{\lab_i,\stk_i} \globs \sfrags_i$ holds, and $\expr$ has no other values under $\vdasha$, then $[], \emptyset \vdashaa \expr \steps \{(\gtfun\ \ev_1 \gtarrow \expr_1)^{\lab_1,\stk_1}, \ldots, (\gtfun\ \ev_n \gtarrow \expr_n)^{\lab_n,\stk_n},\ldots\} \globs \sfrags'$.

Fixing some $k \geq 1$, for all $\gexpr$, $[], \emptyset \vdashaa \gexpr \steps \reval$.

The above language with only functions leaves out several aspects of program analyses, namely how they approximate atomic data such as integers, and how they approximate recursive data structures such as trees.  We address these dimensions in the following section.

§.§ An All-Paths Analysis for an Extended Language

In this section we extend the core all-paths analysis of the previous section to the extended language grammar of Section <ref>.

Figure <ref> presents the new language constructs for the analysis, extending or modifying those of Figure <ref>.  Results $\reval$ are now sets of more than just functions, they are sets of value atoms $\revalz$ which includes records, functions, operators, etc. Additionally, the components of value atoms themselves may have multiple possibilities so e.g. the components of a binary operator $\revalz = \reval_1 \binop \reval_2$ are $\reval$ which are sets.  So for example  $\revalz = \{1\}+ \{4 , (\{6\} + \{ 7, 2 \})\}$ is possible and represents $\{5, 14, 9\}$.  In some of the examples below we will pun and leave off the $\{\}$ on singleton sets.

[value atoms]
⊩( )^,
= ; …; = ^,

[value results]
{ ,…,}

[path condition]

[visited state sets]
{ ,,, …}

[Seen stacks]
{, …}

Extended Language Analysis Grammar

§.§.§ Results That Are Recurrences

There is a surprisingly natural manner in which recurrences over integer and record data can be extracted as results $\reval$. Arithmetic recurrences can then be translated to constrained horn clauses (CHCs) and a solver can verify them.  We know of no existing analysis which also extracts recurrences and the demand aspect of our formalism is one reason why it is so natural here.  We now outline informally how it works.

The first step is to label result values in the variable and application rules with their state, i.e., their program point label and current stack: $\reval^{\la\lab,\stk\ra}$.  If the analysis visits the same state $\la\lab,\stk\ra$ again deeper in the proof tree, we don't just stub the result and return an empty set as in the core system, we return an explicit stub value $\stub^{\la\lab,\stk\ra}$ which is a recursive reference to the parent node also marked with $\la\lab,\stk\ra$.   With nondeterministic result sets plus recursive values the analysis can infer unbounded ranges of data.  For example, result value $\{ \texttt{0}, (\texttt{1} + \stub^{\la\lab,\stk\ra})\}^{\la\lab,\stk\ra}$ denotes a recurrence: the outer label ${\la\lab,\stk\ra}$ denotes the first time the state $\la\lab,\stk\ra$ is hit, and $\stub^{\la\lab,\stk\ra}$ denotes a stubbed recursive reference back to the top of this result because it is also labeled with the same $\la\lab,\stk\ra$.  The mathematical meaning of such a recurrence follows other forms of recursive definition: it is the unrolling of the recurrence, in this case $\{ \texttt{0}, (\texttt{1} + \{\texttt{0} , (\texttt{1} + \{\texttt{0}, (\texttt{1} + \dots)\})\})\}$, i.e., here it is the non-negative integers.   Similarly, $\{ \texttt{0}, (2 + \stub^{\la\lab,\stk\ra})\}^{\la\lab,\stk\ra}$ would express the non-negative evens, and $\{ \ob \texttt{nil = }\ob\cb\cb, (\ob \texttt{hd = \texttt{1}, tl = }\stub^{\la\lab,\stk\ra}\cb)\}^{\la\lab,\stk\ra}$ would express an arbitrary-length list of 's.

We will define a function $\evalval$ in Definition <ref> below which extracts the actual values from these recursive result sets, for example $\evalval(\{ \texttt{0}, (\texttt{1} + \stub^{\la\lab,\stk\ra})\}^{\la\lab,\stk\ra})=\{0, 1, 2, \ldots\}$.  In the general case such result values could be complex arithmetic recurrence relations which could be uncomputable.  In our implementation we will compile them to constrained horn clauses and automatically solve them using a CHC solver.

To add one more level of precision we also include path sensitivity in this system.  It can both serve to avoid executing conditional code for which the guard provably fails, and to allow even more precise results to be inferred.  These result values are of the form $\pathc \Vdash \reval$, and mean that if $\pathc$ holds then the result is $\reval$, and there is no result here if the condition fails.  The $\{ \texttt{0}, (\texttt{1} + \stub^{\la\lab,\stk\ra})\}^{\la\lab,\stk\ra}$ example above could have been the (simplified) result of evaluating a recursive identity function such as let rec id n =$ $(n=0)?0 : 1 + id (n-1)$ $in id 10 (in our grammar self-passing would in fact need to be used encode this recursion).  Adding path conditions to the analysis for this program will give a result that in simplified form is in spirit

$$\{(\reval_N = \texttt{0} \Vdash \texttt{0}), (\reval_N \neq \texttt{0} \Vdash \texttt{1} + \stub^{\la\lab,\stk\ra})\}^{\la \lab,\stk\ra} \text{\ \ \  with } \reval_N = \{\texttt{10}, (\stub^{\la\lab,\stk\ra} \neq \texttt{0} \Vdash \stub^{\la\lab,\stk\ra} - \texttt{1})\}^{\la\lab,\stk\ra}$$

where $\reval_N$ is the argument value 's result.  It can be deduced that $\texttt{0} \leq \reval_N \leq \texttt{10}$ from this recurrence, since , , …, ,  all hold when unrolling the recurrence but the guard $\stub^{\la\lab,\stk\ra} \neq \texttt{0}$ fails at  and so no negative numbers are admitted.

§.§.§ The Proof Rules

Value is not a function
, , , {}

Value Fun
, , , ( )^{( )^, }

Var Local
() =

_0 = ((_1 _2)^' )

^, _0,∉

= (',,)

(_1,_1) = ⋃{ (_0,_0) |∃_1 ∈.  _1, , , ∪{^, _0,}_2  _0 _0 }
_0, , , ^{_1^^, _0} _1

Var Non-Local
() = _f = ( _1 )^_1

_0 = ((_1 _2)^_2 )

^, _0,∉

= (_2,,)

(_1,_1) = ⋃{ (_0,_0) |∃_1 ∈.
_1, , , _1 _0 _0 }

(_2,_2) = ⋃{ (_0',_0') |∃_f^_1,_1 ∈(_1). _1, _1, , ∪{^, _0,} ^_1 _0' _0'}

_0, , , ^_2 _2

Var Stub

, , , ^{ ^^, }

, , , _1 _1  _1

, _1, , _2 _2  _2
, , , _1 _2 {_1 _2} _2

Record Value
∀i ≤n.  , , , _i _i _i
, , , _1 _1; …; _n _n { _1 _1; …; _n _n } ⋃_i _i

Record Project
, , , _0 _1

, , , {_0 } _1

Record Inspect
, , , _0 _1

, , , {_0 } _1

, , , _cond _0

= (⊩_cond)

∀∈. , , (_cond = ), _ __

, , , _ _ ⋃_∈{_cond = ⊩_}  ∪_∈ _ ∪_0

, , , ∪_new_1 _1

_new={, ,_1∪{}}

(_2,_2) = ⋃{ (_0,_0) |( _1 _1)^_1,_1 ∈(_1)

(), _1 ∪{}, ∪_new_1 _0 _0 }
, , , ( ')^{_2^, ()} _2

App Stub, , ∈, , , ( ')^{^,}

Extended Language Program Analysis Rules

Before defining the proof rules we will define the auxiliary relation $\evalval$ alluded to above which will solve result values, producing a (possibly infinite) flat set.  We use $\evalval$ in the rules when concrete details of the result affect the next control step; this is only required for boolean conditions and function values.  Note that the implementation will use a (quickly) computable approximation to this uncomputable function.

Define $\evalval(\reval)$ for the analysis to be $\evalval(\reval,\emptyset)$, which in turn is defined as the least fixed point of the monotone functional of Figure <ref>.
$\evalval$ is undefined for cases of type mismatch, e.g. projecting a number or adding records.

\evalval(\{\revalz_1,\dots,\revalz_n\}, \map) & = & \bigcup_{1\leq i\leq n} \evalval(\revalz_i, \map)\\[1.2ex]
\evalval(\reval^{\la \lab,\stk\ra}, \map) & = & \evalval(\reval,\map \cup \{\la \lab,\stk\ra \mapsto \reval\})\\
\evalval(\stub^{\la \lab,\stk\ra}, \map) & = &
\begin{cases} \evalval(\map(\la \lab,\stk\ra), \map)\text{, provided }\map(\la \lab,\stk\ra) \text{ is defined}\\
\{\eval \mid \eval \text{ is a value} \} \text{ otherwise}
\end{cases}\\
\evalval(\pathc \Vdash \reval, \map) & = &
\begin{cases}
\evalval(\reval, \map)\text{, provided } \gttrue \in \evalval(\pathc,\map)\\
\{\} \text{ otherwise}
\end{cases}\\
\evalval(\reval_1 \binop \reval_2, \map) & = & \{ \eval \mid \eval_1 \in \evalval(\reval_1, \map) \text{ and } \eval_2 \in \evalval(\reval_2, \map) \text{ and } \eval = \eval_1 \binop \eval_2\}\\
\evalval(\reval \gtdot \lbl_i, \map) & = & \{ \eval_i \mid \ob \lbl_1 \gteq \eval_1; \dots; \lbl_i \gteq \eval_i; \dots;\lbl_n \gteq \eval_n \cb \in \evalval(\reval, \map)\}\\
\evalval(\lbl \gtin \reval, \map) & = & \{ \ebool \mid \ob \lbl_1 \gteq \eval_1; \dots;\lbl_n \gteq \eval_n \cb \in \evalval(\reval, \map)\text{ and } \\
&&\ebool = \gttrue \text{ iff } \lbl \in \{\lbl_1,\dots,\lbl_n\} \}\\
\evalval(\ob \lbl_1 \gteq \reval_1; \dots; \lbl_n \gteq \reval_n \cb, \map) & = & \{ \ob \lbl_1 \gteq \eval_1; \dots; \lbl_n \gteq
\eval_n \cb \mid \forall 1 \leq i \leq n.\ \eval_i \in \evalval(\reval_i, \map)\}\\
\evalval((\gtfun\ \ev \gtarrow \expr, \map)^{\lab,\stk}, \map) & = & \{(\gtfun\ \ev \gtarrow \expr, \map)^{\lab}\}\\
\evalval(n, \map) & = & \{ n\}\\
\evalval(\ebool, \map) & = & \{ \ebool\}
\end{array}
The Definition of $\evalval$ for the Analysis

The $M$ mapping in the figure caches all the recurrence parents and the $\stub$ evaluation unrolls the recurrence.  For a final program result all stubs will have a parent in the tree, but when evaluating conditional expressions mid-evaluation some stubs may not yet have parents; in this case the value is arbitrary.  Note that there could be unbounded cycles so we specify we are taking the least fixed point of the above monotone functional.  For this reason, $\evalval$ is not computable.  We will cover how we approximate $\evalval$ when we describe our implementation.

We may now define the extended all-paths analysis rules.

Relation $\stk, \sfrags, \visited \vdashea \expr \steps \reval \globs \sfrags$ is defined by the rules of Figure <ref>.

The rules follow the core all-paths analysis of Figure <ref> for function application and variable lookup; note that we do not need to stub the new operations as all unbounded control flows must pass through variable lookup and function application.  The primary difference now is whereas in the core system we could just return an empty set of results when the proof was cycling, here we need to not simply prune away such sub-derivations, we instead need to return a stub $\stub^{\la\lab,\stk\ra}$ to explicitly mark the point that the derivation cycled and to allow us to extract recurrences.

The Conditional rule deserves some explanation.  The set $\ebools$ is a subset of $\{\gttrue,\gtfalse\}$ and is the result of $\evalval$-uating the conditional result to extract which condition(s) may hold.  Only the conditional branches in $\ebools$ will fire, giving path-sensitivity. The path conditions $\reval_\textrm{cond} = \ebool$ are added to the assumptions indicating the constraint placed on $\reval_\textrm{cond}$.  Note the path condition is only useful in the case that $\ebools$ is not a singleton: if $\ebools$ is say $\{\gttrue\}$ for example then the constraint will be $\reval_\textrm{cond} = \gttrue$ which is direct from $\evalval(\pathc \Vdash \reval_\textrm{cond}) = \{\gttrue\}$.  Path constraints $\reval_\textrm{cond} = \ebool \Vdash \reval_\ebool$ are added to the results to allow us to extract more precise recurrences, as was described above.

§.§ Runtime Complexity

The classic program analysis for higher-order functional languages is $k$CFA <cit.>, where $k$ is the number of frames of call stack preserved.  It is known to be exponential for $k\geq 1$ <cit.>. Tools which analyze large programs often use $k=0$, which is feasible but loses a lot of precision: all calls to each function are merged, meaning the analysis is monovariant.

$1$CFA is exponential because even with only one stack frame of reference the propagation of the environment forward will be enough to cause a chain of $n$ calls to have $2^n$ branches that need to be explored by the analysis.  Since our analysis is not propagating any environment forward we avoid this blowup.  We will also be less precise in some cases, but the advantage is we will still have a polynomial analysis for stack fragments larger than $0$.

The $\vdashaa$ rules as presented are undecidable due to the $\evalval$ function in the Conditional being undecidable in the general case, but in practice a conservative approximation can be used.  The most simple such approximation is $\evalval(\reval_\textrm{cond}) = \{\gttrue, \gtfalse \}$ which will remove the path-sensitivity, but there are other approximations which retain significant path-sensitivity and are also polynomial-time.  For the complexity analysis we will assume some $\evalval_\textrm{poly}$ is used which returns a strict superset of $\evalval$ results.

Assuming a polynomial-time conservative approximation $\evalval_\textrm{poly}$ for $\evalval$ and fixing some constant $k>0$, given fixed program $\gexpr$ the relation $[], \{\}, \gttrue=\gttrue, \{\} \vdashea \gexpr \steps \reval \globs \sfrags$ is computable as a function from $\gexpr$ to $\reval, \sfrags$ in polynomial time.

While the algorithm is provably polynomial, the degree is high if implemented naively.  We discuss methods for improving efficiency in Section <ref>.

§ IMPLEMENTATION

In this section we outline our implementations.  All implementations are in OCaml.

§.§ The Interpreter Implementation

We have implemented an interpreter for the operational semantics of the extended language of Section <ref> which fully passes a large suite of tests, providing further evidence of the soundness of the system beyond Lemma <ref>.  Our implementation includes a cache mapping $(\stk,\expr) \mapsto \reval$ which avoids repeating the same lookup question, and makes the runtime complexity roughly comparable to a standard interpreter implementation.
Our interpreter is only a proof-of-concept to verify correctness and still needs work on optimizing performance.
Another important performance improvement would be to implement a garbage collector on the cache, important because otherwise the cache will bloat over time with mostly stale entries.  Since no stack can repeat, at application return all items with the just-before-return stack $\stk$ in the key can be flushed.

§.§ The Program Analysis Implementation

Our primary implementation effort has been the program analysis for the extended language found in Section <ref>.  We report here on the current state of our proof-of-concept implementation.

We first describe how we simplify results $\reval$ and how arithmetic and boolean recurrences are solved by the Spacer CHC solver <cit.>.

§.§.§ Simplification of Results

Without any simplification of result values $\reval$ the results can be surprisingly baroque since recursive functions get partly unrolled, control flows not arising in the interpreter are taken to throw out junk, etc.

Simplification is important for several reasons.  Along with the fact that the unsimplified results are unreadable, the CHC solver described in the next subsection will be many times more efficient if fed simplified clauses.  So, we have implemented a simplification function in OCaml which takes in an $\reval$ and produces an equivalent but simplified version $\reval'$.  Simplification is also critical because, while Spacer can deal with constraints involving integers or booleans, recursive records are not handled by Spacer and so we also need to perform record projections appearing in $\reval$. The challenge of simplification is to avoid unbounded computation; the $\evalval$ function of Section <ref> is uncomputable due to the unbounded recurrences.

We implement simplification as a term rewriting system which includes the following rewrites:

* Non-recurrence simplification: $\reval$ simplifies to $\evalval(\reval)$ if $\reval$ contains no stubs

* Constant folding: e.g.,  simplifies to

* Associativity: e.g.,  simplifies to

* Record projection: e.g., !(hd =
$$ 1, tl = $$
nil =
$$ 0$$
).hd! simplifies to

* Unrolling of recurrences: $(\stub^{\la\lab,\stk\ra})\gtdot \lbl$ expands to $\reval_0 \gtdot \lbl$ if $\reval_0$ has label $\la \lab,\stk\ra$ in the original $\reval$

* Distribution of operations into sets: e.g., $\{$$\}$ simplifies to

* Merging of cycles: e.g., $\reval_1^{\la\lab,\stk\ra} + \reval_2^{\la\lab,\stk\ra}$ simplifies to $(\reval_1 + \reval_2)^{\la\lab,\stk\ra}$

* Merging of path conditions: e.g., $(\pathc\Vdash\reval_1) + (\pathc\Vdash\reval_2)$ simplifies to $\pathc\Vdash(\reval_1 + \reval_2)$

We limit unrolling of recurrences to only the case where the result of $(\stub^{\la\lab,\stk\ra})\gtdot \lbl'$ or $\lbl' \gtin(\stub^{\la\lab,\stk\ra})$ is required (to obtain either a function or boolean result for Conditional, App, or ).  In order to avoid unbounded expansion we mark each syntactic $\expr \gtdot \lbl$ and only expand each projection occurrence once.  This will allow e.g.,  to simplify to  in a context of a parent label $(\ob \texttt{hd = \texttt{1}, tl = }\stub^{\la\lab,\stk\ra}\cb)^{\la\lab,\stk\ra}$ since each  projection is syntactically distinct: we can unroll the record twice.  Associativity can only be applied in one direction to avoid nontermination.

The simplifier still needs refining and is one reason why the analysis is sometimes slow.

§.§.§ Evaluating Arithmetic Recurrences Via CHCs

Integer recurrences are not generally decidable, but a heuristic solver for these recurrences can be constructed by translating the $\evalval$ definition for a fixed $\reval$ to a set of constrained horn clauses (CHC's).  We define the translation function here; in the implementation we use Z3's CHC solver, Spacer <cit.> to determine if the clauses produced by our translator have a solution.  Spacer is just a heuristic which may not terminate, so it needs to be run with a time-out, and in the case of time-out we must fall back to an unconstrained result such as all integers.

Assume given a fixed $\reval$.  We assume there is a function $\id(\reval_0)$ which for each non-stub sub-expression occurrence $\reval_0$ in $\reval$ returns a unique ID $\glab$.  For the stub and parent labeled nodes we require $\id(\reval_0^{\la \lab,\stk\ra})=\id(\stub^{\la \lab,\stk\ra})$. We use notation $\vec\pathc$ for a vector of path conditions, $\vec\pathc = (\pathc_1, \dots, \pathc_n)$.  We notate truncation of vectors as $(\pathc_1, \dots, \pathc_m,\ldots,\pathc_n)\lceil^m = (\pathc_1, \dots, \pathc_m)$.

$\tochc(\reval,\vec{\pathc},P)$ is defined by cases on $\reval/\revalz$ in Figure <ref>.
The result is undefined for cases of type mismatch, e.g. adding booleans.  It is also undefined for records and record operations as the CHC clauses are only used for numerical and boolean constraints.  We define the top-level $\tochc(\reval)$ as

= \{\forall x_{\id(\reval_1)}, \ldots, x_{\id(\reval_n)}.\phi \mid \phi \in \tochc(\reval,\gttrue,\{\}) \land {\sc FV}(\phi)=x_{\id(\reval_1)}, \ldots, x_{\id(\reval_n)}\}$$

\tochc(\reval,\vec{\pathc},P) & = & \bigcup_{1\leq i \leq n}\{  X_{\id(\revalz_i)}(x_{\id(\revalz_i)}) \land \pathcond(\vec\pathc) \Rightarrow X_{\id(\reval)}(x_{\id(\revalz_i)})\}\cup \\ && \bigcup_{1\leq i\leq n} \tochc(\revalz_i,\vec{\pathc},P)\\
&&\text{ where }\reval = \{\revalz_1,\dots,\revalz_n\}\\[1.5ex]
\tochc(\reval^{\la \lab,\stk\ra}, \vec{\pathc},P) & = & \tochc(\reval,\vec{\pathc},P\cup \{\la \lab,\stk\ra \})\\
\tochc(\stub^{\la \lab,\stk\ra}, \vec{\pathc},P) & = &
\begin{cases} \{\} \text{ provided } \la \lab,\stk\ra \in P\\
\{ X_{\la \lab,\stk\ra}(x_{\la \lab,\stk\ra}) \} \text{ otherwise}
\end{cases}\\
\tochc(\stub^{\la \lab,\stk\ra}, \vec{\pathc},P) & = & \{\}\\
\tochc(\reval = \ebool \Vdash \reval_0, \vec{\pathc},P) & = &  \tochc(\reval_0,(\vec{\pathc}, \reval = \ebool)) \cup \tochc(\reval,\vec{\pathc},P)\\
\tochc(\reval_1 \binop \reval_2, \vec{\pathc},P) & = &  = \{X_{\id(\reval_1)}(x_{\id(\reval_1)}) \land X_{\id(\reval_2)}(x_{\id(\reval_2)}) \land \pathcond(\vec\pathc) \Rightarrow \\
&& X_{\id(\reval)}(x_{\id(\reval_1)} \binop x_{\id(\reval_2)})\}\cup \tochc(\reval_1,\vec{\pathc},P) \cup \tochc(\reval_2,\vec{\pathc},P)\\
%  \tochc(\reval_0 \gtdot \lbl_i, \vec{\pathc}) & = & \text{TBA}\snote{TO DO!}\\
%  \tochc(\lbl \gtin \reval_0, \vec{\pathc}) & = & \text{TBA}\\
%  \tochc(\ob \lbl_1 \gteq \reval_1; \dots; %  \lbl_n \gteq \reval_n
%  \cb, \vec{\pathc}) & = & \text{TBA}\\
\tochc((\gtfun\ \ev \gtarrow \expr)^{\lab,\stk}, \vec{\pathc},P) & = & \{\}\\
\tochc(n, \vec{\pathc},P) & = & \{ \pathcond(\vec\pathc) \Rightarrow X_{\id(\revalz)}(n)\}\text{ where }\revalz = n\\
\tochc(\ebool, \vec{\pathc},P) & = & \{ \pathcond(\vec\pathc) \Rightarrow X_{\id(\revalz)}(\ebool)\}\text{ where }\revalz = \ebool\\
\pathcond(\reval_1 = \ebool_1, \dots, \reval_n = \ebool_n) & = & X_{\id(\reval_1)}(x_{\id(\reval_1)}) \land \ldots \land X_{\id(\reval_n)}(x_{\id(\reval_n)}) \land \\
&& (x_{\id(\reval_1)} \gteq \ebool_1) \land \ldots \land (x_{\id(\reval_n)} \gteq \ebool_n)\\
\end{array}

$\tochc$ Translation of Results $\reval$ to Constrained Horn Clauses

In this definition the $x_{\id(\reval_0)}$'s are the logic variables for graph point $\reval_0$ and the $X_{\id(\reval_0)}$ are the corresponding predicates for what values those points can take on: for example, $X_{\id(\reval_0)}(5)$ would mean that sub-expression $\reval_0$ has value 5.
A key aspect of the translation is how recurrences will translate to self-referential clauses since the parent and stub with the same label will use the same underlying predicate.

The $\pathc \Vdash$ in the $\reval$ guard the return values with the condition they were under; they are added as preconditions in the $\tochc$ clauses, which will allow the solver to take them into account.

Given this translation, to approximate $\evalval(\reval_\textrm{cond})$ in the Conditional rule, two CHC queries should be performed.  Along with the above constraints $\tochc(\reval_\textrm{cond})$ we first issue a query with the additional clause $X_{\id(\reval_\textrm{cond})}(\gtfalse) \Rightarrow \gtfalse$; if this query is satisfiable that means we can only evaluate the $\gttrue$ branch as the $\gtfalse$ branch can never hold.  If this query is unsatisfiable all it means is we cannot only evaluate the $\gttrue$ branch.  The check as to whether we can only evaluate the $\gtfalse$ branch is the mirror image.

§.§.§ Overview of the Analysis Implementation

Our implementation largely aims to follow the rules of Section <ref>, replacing the uncomputable $\evalval$ with the CHC solver described in the previous section. The stack fragments $\sfrags$ are implemented using monadic state over an immutable set which is more efficient than an imperative set since we need to checkpoint the current $\sfrags$ in the visited set $\visited$ as per the rules.  We fix $k$ to $2$ as that is the minimal $k$ for which stitching is effective.

We include an additional  syntax in our language which we can use to write assertions on result values which Spacer can then verify.

§.§.§ Results Produced By the Analysis

Here we summarize some of the results produced by the current implementation.

let id = fun self -> fun n ->
if n = 0 then 0
else 1 + self self (n - 1)
in letassert r = id id 10 in r >= 2

A Recursive Integer  Example and its Result

Figure <ref> gives the source code of a simple recursive identity function, and a graph of the result automatically produced by the analysis showing the recurrences: both the  from-node and the parent to-node on the back edge have the same $\la\lab,\stk\ra$. The path conditions are elided from the result as they do not refine it in this case. Path sensitivity does refine the running of the analysis, for example 0 and 1 are ruled out as results since before the analysis hits a cycle (i.e., a previously visited state in $\visited$) Spacer can show that  and  are both non-zero and so the base case can be skipped in the Conditional rule for the first two recursions.  Spacer can prove that the result here is greater than or equal to two based on the recurrence result extracted: the !letassert! in the source is fed into Spacer and is reported satisfiable.  Note the !let! syntax is sugar which we inline in the front-end.

let id = (fun xx -> xx) in
let map = (fun f -> fun l ->
let lp = fun self -> fun lst ->
if (if (hd in lst) then
false else true) then
else ( hd = id f (lst.hd);
tl = self self (lst.tl) )
lp lp l) in
map (id (fun b -> 1 + b))
( hd = 7; tl =
hd = 8; tl =
hd = 9; tl =    )

A  Example and its Result

Figure <ref> gives the source code of a map over a list and the graph result.  Again the result starts out fully accurate as the $k$ frames have not been exhausted, but at some point we revist the same state in $\visited$ and a  is generated with a back-edge to its parent.

The current proof-of-concept implementation successfully completes many other examples but it still needs refinement before it will be able to be practically useful. For a rough idea of the performance we can compare it with benchmarks run on DDPA <cit.> and P4F <cit.>, two related higher-order program analyses.  Of the 19 benchmarks listed in DDPA <cit.> Figure 33 it very quickly terminates on 11, takes around ten seconds on one, twenty seconds on another, times out after ten minutes on three, and three cannot be expressed due to the limits of our current syntax (for example we currently have no strings).  Of the 10 benchmarks in P4F <cit.> Figure 2&3, it quickly terminates on 7, takes around twenty seconds on one, and times out on two.  We then downloaded the DDPA artifact and re-ran DDPA with their benchmarks on our hardware, and comparing the running time of the 13 benchmarks both systems worked on, the median time for our system was 34ms and for DDPA it was  198ms.  This shows if the performance problems on some of the benchmarks is solved we could have quite good performance.

§.§.§ Improving Performance

Up to now we have primarily been focused on developing a sound analysis implementation which constructs and solves recurrences, and the analysis performance still needs considerable work. We need to improve result simplification, better optimize data structures for performance, limit the overhead of Spacer by restricting its use in some cases, and will need to cache to avoid repeating evaluations.

Caching in particular is very important for performance as pure demand semantics must do considerably more work looking up variables if there is no cache; the proof of a polynomial-time algorithm in Theorem <ref> requires a cache. For the interpreter implementation described above, we used a mapping  $(\stk,\expr) \mapsto \reval$ as a cache and obtained interpreter running times similar to a standard implementation of an interpreter.  Caching the $\stk, \sfrags, \pathc, \visited \vdashea  \expr \steps \reval \globs \sfrags$ relation of the analysis is more challenging: in order to be sound we can use a cached result only when the exact same question is asked again, and this means a cache initially appears to require a mapping $(\stk, \sfrags, \pathc, \visited,\expr) \mapsto \reval$ which would greatly limit the number of cache hits (it still is polynomial as per Theorem <ref>, but will have many more cache misses due to the $\sfrags$ and $\visited$ sets in the domain).  The current proof-of-concept implementation has no cache but it should be possible to add a caching mechanism, for example a finitary version of the display-based theory of Section <ref> would prevent repeating function lookups in non-local variable access.

§ RELATED WORK

§.§ Related Operational Semantics

The operational semantics here only uses the call stack and two program points as its state.  We know of no such precedent, but the DDSE operational semantics <cit.> relies only on a call stack, a non-locals stack, and a control flow graph.

For imperative languages supporting nested function definitions, access links are a classic compiler implementation for non-local variable access <cit.>.  Access links are a chain of activation records linking to successively higher lexical levels.  Our approach is similar in how there is a back-chaining to find values, but access-link-based implementations still push data forward in stack frames so we are more demand-driven.  DDSE uses a similar approach.

Optimal lambda-reduction <cit.> is a $\lambda$-reduction method which provably requires the fewest number of $\beta$-reductions.  Running our interpreter with a cache has the related property that applications are never repeated.  Whether any concrete optimality property can be proven about a pure demand semantics is an open question.

§.§ Related program analyses

We believe our approach to program analysis for functional languages is nearly unique in that it is not directly propagating any data; all state is captured in the call stack.  Functional language program analyses in the literature invariably push (abstract) values forward.  Data flow analysis for imperative programs also may push data backwards, but again data is being propagated directly.

All program analyses for languages with higher-order recursive functions must somehow finitize the call stack.  The classic approach here is $k$CFA <cit.>, which is an abstract interpretation <cit.> that trims the stack to the most recent $k$ calls.  Many extensions and improvements to $k$CFA have been made over the years including <cit.>.
Our stitching of past stack histories to approximate past stack states appears to be a novel feature of our analysis.  It is particularly important for demand variable lookup.

We prove that our analysis runs in polynomial time (Theorem <ref>).  Most higher-order program analyses are exponential; for example $k$CFA has been shown to be complete for EXPTIME <cit.>. There has been some previous work on reducing the exponential burden of $k$CFA to polynomial-time <cit.>.  At a high level these approaches flatten the non-local variable environments to reduce the blowup of exponentially many combinations of the environments chain.  Our stack stitching approach allows for a less draconian shrinking of the chain, keeping a $k$-local distinctness window in on-demand variable lookups.

The higher-order program analysis closest to this work is DDPA <cit.> and its generalization Plume <cit.>, which also uses an underlying form of operational semantics with no substitution or environment.  By contrast, DDPA-like analyses rely on more than just a call stack to model program state: a flow graph and an additional non-locals stack is needed.  Here we perform a more direct finitization of the (infinitary) operational semantics by simply finitizing the rules by stack pruning, in the spirit of Abstract Interpreters for Free <cit.>; DDPA translates analysis questions into equivalent PDA reachability questions.  DDPA does not perform stack stitching, but it would likely benefit from it since it also looks up variables on-demand.  DDPA is also polynomial in $k$.  DDPA does not extract recurrence results as we do here.

The standard numerical abstractions in the field of abstract interpretation <cit.> include for example numerical sign (positive, zero, or negative), constant-value, set-of-constants, interval, and congruence domains.  The recurrences our analysis infers generalize these domains as it can infer sign, constant, and range values. Relational domains in abstract interpretations additionally can relate multiple variables.  For example, two variables could only be known to be positive separately but it could be known collectively that one is always larger than the other.  Relational domains should in principle be inferrable in an extension of our analysis.

Our analysis is built on a big-step formalization of operational semantics; this is another non-standard aspect as a small-step basis is used with only a few exceptions <cit.>.  Big step operational semantics has an advantage of calls and returns always aligning since the call and return point is the same node in the proof tree.

We show in Section <ref> how the program analysis algorithm can be fully specified in a deterministic all-paths proof system.  We believe this is novel, and the greater degree of rigor of a fully proof-theoretic presentation will be potentially useful in full formal verification with a theorem prover.

We know of no higher-order program analysis which extracts recurrence relations on numerical data as we do, but the more general theme of analyses aiming to extract stronger invariant properties is an active area of research <cit.>. We currently do not infer inductive input-output relationships <cit.> but that should be possible in principle by synchronizing the input /ouput recurrences.

§ CONCLUSIONS

This paper addresses the question: what is the minimal amount of state information that must be maintained in the operational semantics of a higher-order functional language?  The answer here is it suffices to only use a call stack consisting of source program call sites, plus two source program points; no variable environment, substitution, store, or any other structure is needed.  We prove this form of operational semantics is equivalent to a standard presentation.

Then, to illustrate how this pure demand approach can open the door to new applications, we defined a program analysis as a direct finitization of this operational semantics.  The program analysis has a number of novel properties compared to standard program analyses for higher-order programs.  The analysis has been implemented and preliminary results look promising.

§ DATA-AVAILABILITY STATEMENT

The implementation of the interpreter of Section <ref> and the analyses of Section <ref> are publicly available on GitHub and a link will be included in the final submission.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

authorpersonH. Barendregt.
booktitleThe Lambda Calculus: Its Syntax and
Semantics (edition2nd ed.).

[Cousot and Cousot(1977)]
authorpersonPatrick Cousot and
personRadhia Cousot. year1977.
Abstract Interpretation: A Unified Lattice Model
for Static Analysis of Programs by Construction or Approximation of
Fixpoints. In booktitleProceedings of the 4th ACM
SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los
Angeles, California) (seriesPOPL '77).
publisherACM, addressNew York, NY, USA,

[Facchinetti et al(2019)]
authorpersonLeandro Facchinetti,
personZachary Palmer, and personScott Smith.
Higher-Order Demand-Driven Program Analysis.
journalTOPLAS  volume41
(dateJuly year2019).
Issue 3.

[Fachinetti et al(2020)]
authorpersonLeandro Fachinetti,
personZachary Palmer, personScott F. Smith,
personKe Wu, and personAyaka Yorihiro.
A Set-Based Context Model for Program Analysis. In
booktitleProgramming Languages and Systems: 18th Asian
Symposium, APLAS 2020, Fukuoka, Japan, November 30 – December 2, 2020,
Proceedings (Fukuoka, Japan). publisherSpringer-Verlag,
addressBerlin, Heidelberg, pages3–24.

[Felleisen and Friedman(1987)]
authorpersonMatthias Felleisen and
personDaniel P. Friedman. year1987.
Control operators, the SECD-machine, and the
\(\lambda\)-calculus. In booktitleFormal Description of
Programming Concepts - III: Proceedings of the IFIP TC 2/WG 2.2 Working
Conference on Formal Description of Programming Concepts - III, Ebberup,
Denmark, 25-28 August 1986, editorpersonMartin
Wirsing (Ed.). publisherNorth-Holland,

authorpersonCharles Fischer.
titleCS536 Lecture Notes.

<https://pages.cs.wisc.edu/ fischer/cs536.s05/course.hold/html/NOTES/8.RUNTIME-VAR-ACCESS.html#accessLink>

[Gilray et al(2016)]
authorpersonThomas Gilray, personSteven
Lyde, personMichael D. Adams, personMatthew Might,
and personDavid Van Horn. year2016.
Pushdown Control-flow Analysis for Free. In
booktitleProceedings of the 43rd Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (St. Petersburg, FL, USA)
(seriesPOPL '16). publisherACM,
addressNew York, NY, USA, pages691–704.

[Gonthier et al(1992)]
authorpersonGeorges Gonthier,
personMartín Abadi, and personJean-Jacques
Lévy. year1992.
The Geometry of Optimal Lambda Reduction. In
booktitleProceedings of the 19th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (Albuquerque, New Mexico,
USA) (seriesPOPL '92). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

authorpersonArie Gurfinkel.
Program Verification with Constrained Horn Clauses
(Invited Paper). In booktitleComputer Aided Verification,
editorpersonSharon Shoham and
personYakir Vizel (Eds.). publisherSpringer
International Publishing, addressCham, pages19–29.

[Jagannathan and Weeks(1995)]
authorpersonSuresh Jagannathan and
personStephen Weeks. year1995.
A Unified Treatment of Flow Analysis in
Higher-Order Languages. In booktitleProceedings of the 22nd
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San
Francisco, California, USA) (seriesPOPL '95).
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, pages393–407.

[Kaki and Jagannathan(2014)]
authorpersonGowtham Kaki and personSuresh
Jagannathan. year2014.
A Relational Framework for Higher-Order Shape
Analysis. In booktitleProceedings of the 19th ACM SIGPLAN
International Conference on Functional Programming (Gothenburg, Sweden)
(seriesICFP '14). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

authorpersonJohn Lamping.
An Algorithm for Optimal Lambda Calculus
Reduction. In booktitleProceedings of the 17th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San
Francisco, California, USA) (seriesPOPL '90).
publisherACM, addressNew York, NY, USA,

authorpersonMatthew Might.
Abstract Interpreters for Free. In
booktitleProceedings of the 17th International Conference on
Static Analysis (Perpignan, France) (seriesSAS'10).
publisherSpringer-Verlag, addressBerlin, Heidelberg,
3-642-15768-8, 978-3-642-15768-4

[Might et al(2010)]
authorpersonMatthew Might, personYannis
Smaragdakis, and personDavid Van Horn.
Resolving and Exploiting the K-CFA Paradox:
Illuminating Functional vs. Object-Oriented Program Analysis. In
booktitleProceedings of the 31st ACM SIGPLAN Conference on
Programming Language Design and Implementation (Toronto, Ontario, Canada)
(seriesPLDI '10). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

authorpersonAntoine Miné.
Tutorial on Static Inference of Numeric Invariants
by Abstract Interpretation.
journalFound. Trends Program. Lang.
volume4, number3–4 (datedec
year2017), pages120–372.

[Mitchell and Apt(2003)]
authorpersonJohn C. Mitchell and
personKrzysztof Apt. year2003.
booktitleConcepts in Programming Languages.
publisherCambridge University Press,

[Montagu and Jensen(2020)]
authorpersonBenoît Montagu and
personThomas Jensen. year2020.
Stable Relations and Abstract Interpretation of
Higher-Order Programs.
journalProc. ACM Program. Lang.
volume4, numberICFP, Article articleno119
(dateaug year2020), numpages30 pages.

[Palmer et al(2020)]
authorpersonZachary Palmer, personTheodore
Park, personScott Smith, and personShiwei Weng.
Higher-Order Demand-Driven Symbolic Evaluation.
journalProc. ACM Program. Lang.
volume4, numberICFP, Article articleno102
(dateaug year2020), numpages28 pages.

authorpersonG.D. Plotkin.
"Call-by-name, call-by-value and the
journalTheoretical Computer Science
volume1, number2 (year1975),

authorpersonGordon Plotkin.
A Structural Approach to Operational Semantics.
journalJ. Log. Algebr. Program.
volume60-61 (date07 year2004),

authorpersonDavid A. Schmidt.
Trace-Based Abstract Interpretation of Operational
journalLISP and Symbolic Computation
volume10, number3 (date01 May
year1998), pages237–271.

authorpersonOlin Grigsby Shivers.
titleControl-flow Analysis of Higher-order
thesistypePh. D. Dissertation.
addressPittsburgh, PA, USA.
UMI Order No. GAX91-26964.

[Van Horn and Mairson(2008)]
authorpersonDavid Van Horn and
personHarry G. Mairson. year2008.
Deciding kCFA is Complete for EXPTIME. In
booktitleProceedings of the 13th ACM SIGPLAN International
Conference on Functional Programming (Victoria, BC, Canada)
(seriesICFP '08). publisherACM,
addressNew York, NY, USA, pages275–282.

[Van Horn and Might(2010)]
authorpersonDavid Van Horn and
personMatthew Might. year2010.
Abstracting Abstract Machines. In
booktitleICFP (Baltimore, Maryland, USA).
publisherACM, addressNew York, NY, USA,

[Vardoulakis and Shivers(2010)]
authorpersonDimitrios Vardoulakis and
personOlin Shivers. year2010.
CFA2: A Context-Free Approach to Control-Flow
Analysis. In booktitleProceedings of the 19th European
Conference on Programming Languages and Systems (Paphos, Cyprus)
(seriesESOP'10). publisherSpringer-Verlag,
addressBerlin, Heidelberg, pages570–589.
3-642-11956-5, 978-3-642-11956-9

[Zhu et al(2016)]
authorpersonHe Zhu, personGustavo Petri,
and personSuresh Jagannathan. year2016.
Automatically Learning Shape Specifications.
journalSIGPLAN Not. volume51,
number6 (datejun year2016),

§ PROOFS

This Appendix contains proofs of all lemmas and theorems from the paper.

§.§ Operational Semantics Proofs

First, it must be the case that since Var Non-Local in turn always requires another variable lookup, and no rules other than Var Local and Var Non-Local apply to variable expressions that all variable lookups must be a chain in the proof tree of a series of $n-1$ Var Non-Local applications and then a Var Local ending the sequence.  Figure <ref> then is nothing more than a description of this general proof tree.

By Lemma <ref> we know any variable lookup sub-proof in $\vdash$ is of the form of Figure <ref>.  Now, observe that if all of the preconditions of this subtree are assembled in a single rule, we have the Var rule of $\vdashc$.  The variable names used in the figure were designed to correspond to the variable names of the Var rule.  The condition in Var requiring all $\ev_i \neq \ev_{i+1}$ is equivalent to the same individual conditions of the Var Non-Local rules.  There are no  $\myfun(\lab_i)= \gtfun\ \ev_i \gtarrow \expr_i''$ constraints in the Var rule, but those add no extra constraint given that $\ev_0 \neq \ldots \neq \ev_n$.

Before starting the proof proper we need to define some notation.

We will use the convenience notation $\nofl(\eval^{\stk,\cachef,\cachel}) = \eval^\stk$.

Define $\la \stk_0,\cachef_0,\cachel_0,\expr_0\ra \mapsto \eval_0^{\stk_0',\cachef_0',\cachel_0'} \in\in \cachef$ to mean either $\la \stk_0,\cachef_0,\cachel_0,\expr_0\ra \mapsto \eval_0^{\stk_0',\cachef_0',\cachel_0'}  \in \cachef$, or for some $\la \stk_1,\cachef_1,\cachel_1,\expr_1\ra \mapsto \eval_1^{\stk_1',\cachef_1',\cachel_1'} \in\in \cachef$ inductively $\la \stk_0,\cachef_0,\cachel_0,\eval_0^{\stk_0',\cachef_0',\cachel_0'} \ra \mapsto \reval_0 \in\in \cachef_1 \cup \cachel_1 \cup \cachef'_1 \cup \cachel_1'$.  The definition for $\in \in \cachel$ is completely analogous.if we can remove the x from the L cache we can make these one definition.

We show each direction in turn.

$\Rightarrow$ Direction:

We generalize the assertion to show that for all $\expr$, $\stk$, and $\cachef$ and $\cachel_0$, if

* $\stk \vdashc \expr \steps \eval^{\stk'}$,

* if $\stk = (\expr_0\ \expr_0') \lC \stk_0$ (also implying $\stk$ is non-empty) then

* $\cachef$ is the list of all lexically-enclosing function lookups for $\expr$:

$$\cachef = \lC_{0 \leq i \leq m}[\la \stk_i,\cachef_i',\cachel_i',\expr_i\ra \mapsto (\gtfun\ \ev_{i} \gtarrow \expr_{i}'' )^{\stk_{i+1}',\cachef_{i+1},\cachel_{i+1}}]$$

where for all $i \leq m$, $\stk_{i+1}' = ((\expr_{i+1}\ \expr'_{i+1}) \lC \stk_{i+1})$, and we also have $\stk_i\vdashc \expr_i \steps (\gtfun\ \ev_{i} \gtarrow \expr_{i}'' )^{\stk_{i+1}',\cachef_{i+1},\cachel_{i+1}}$

* Each $\cachel_i$ caches the lookup of the top argument on the stack of the above lexical chain: for all $0 \leq i \leq m$,

$$\cachel_i = [\la \stk_i,\cachef_i',\cachel_i',\expr_i'\ra \mapsto (\reval_i,\ev_i)] \text{ and } \stk_i \vdashc \expr_i' \steps (\reval_i,\ev_i)$$

then there exist $\cachef$, $\cachel_0$ such that

* $\stk, \cachef, \cachel_0 \vdashcc \expr \steps \eval^{\stk',\cachef',\cachel'_0}$,

* if $\stk' = (\expr_0\ \expr_0') \lC \stk_0'$ (also implying $\stk'$ is non-empty) then

$$\cachef' = \lC_{0 \leq i \leq m}[\la \stk_i',\cachef_i'',\cachel_i'',\expr_i\ra \mapsto (\gtfun\ \ev_{i} \gtarrow \expr_{i}'' )^{\stk_{i+1}',\cachef_{i+1}',\cachel_{i+1}'}]$$

where for all $i \leq m$, $\stk_{i+1}'' = ((\expr_{i+1}\ \expr'_{i+1}) \lC \stk_{i+1}')$, and additionally $\stk_i'\vdashc\expr_i \steps (\gtfun\ \ev_{i} \gtarrow \expr_{i}'' )^{\stk_{i+1}',\cachef_{i+1}',\cachel_{i+1}'}$;

* Each $\cachel_i'$ caches the lookup of the top argument on the stack of the above lexical chain: for all $0 \leq i \leq m$,

$$\cachel_i' = [\la \stk_i',\cachef_i'',\cachel_i'',\expr_i'\ra \mapsto (\reval_i,\ev_i)] \text{ and } \stk_i'\vdashc \expr_i' \steps (\reval_i,\ev_i).$$

Note that this generalized statement implies the result because picking the caches to be empty will make (2) vacuously true.

Proceed by induction on the height of the assumption (1) proof tree to show that (1)-(2) implies (i)-(ii).

For the base case of the Value rule the conclusion is direct: the assumption (1) in this case is $\stk \vdashc \eval \steps \eval^{\stk}$ and (ii) is immediate from (2), and (i), $\stk, \cachef, \cachel_0 \vdashcc \eval \steps \eval^{\stk,\cachef, \cachel_0}$, is immediate from the $\vdashcc$ Value rule.

For the induction step, assume the goal for smaller proof trees, and assume arbitrary $\cachef$, $\cachel_0$ with (1)-(2) holding, and (1) being $\stk \vdashc \expr \steps \reval$.

For the Application case, we must have $\expr = (\expr_1\ \expr_2)$ so we have $\stk \vdashc (\expr_1\ \expr_2) \steps \reval$.  We can directly apply the induction hypothesis for the function and argument lookup subgoals in the rule, choosing $\cachef$ and $\cachel_0$ there to be the assumed arbitrary ones above.  Since these caches are the same we directly inherit the requirement (2) for the induction hypotheses of these sub-derivations from the assumed (2) for the conclusion, and so obtain from (i) for the first hypothesis that $\stk, \cachef,\cachel_0 \vdashcc \expr_1 \steps (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel_0'}$ for some $\expr',\stk_1,\cachef',\cachel_0'$, and similarly obtain $\stk, \cachef,\cachel_0 \vdashcc \expr_2 \steps \eval_2^{\stk'',\cachef'',\cachel_0''}$ for some $\stk'',\eval_2,\cachef'',\cachel_0''$ for the second hypothesis.Check prime/subscript stuff here.  In order to apply the inductive hypothesis to the established

$$((\expr_1\ \expr_2) \lC \stk) \vdashc \expr' \steps \reval$$

probably need $\eval$ here not $\reval$.
rule precondition we need to construct caches such that (2) holds for this hypothesis.  Using the $\vdashcc$ Application rule as a guidepost, pick the $\cachef$ for this precondition to be $(\la \stk,\cachef,\cachel_0,\expr_1\ra \mapsto (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'} \lC\cachef')$, and pick the $\cachel_0$ in that assumption to be $[\la \stk,\cachef,\cachel_0,\expr_2\ra \mapsto (\reval_2,\ev)]$.  Precondition (2) then follows because by inspection of (2)'s definition we can see we have just added one more frame to the front of the $\cachef'$ chain which preserves (2). Probably need to write this out  So, with all preconditions (2) satisfied for each rule we have both (i) and (ii) for all three preconditions.  In particular for the third precondition we now have
$((\expr_1\ \expr_2) \lC \stk), (\la \stk,\cachef,\cachel_0,\expr_1\ra \mapsto (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'} \lC\cachef'),[\la \stk,\cachef,\cachel_0,\expr_2\ra \mapsto (\reval_2,\ev)] \vdashcc \expr' \steps \reval$ turn e to v here Putting the three $\vdashcc$ proofs established above we may apply the $\vdashcc$ Application rule to obtain the desired $\stk,\cachef,\cachel_0 \vdashcc \expr \steps \eval^{\stk',\cachef'',\cachel_0''}$, and (ii) follows directly as they are the same result caches as those occurring on the third assumption conclusion.

For the Var case, assumption (1) is of the form $((\expr_0\ \expr_0')\lC \stk_0)\vdashc \ev_n \steps \reval$.  By assumption (2) we have that for all $0 \leq i \leq m$, $\la \stk_i,\cachef_i',\cachel_i', \expr_i \ra \mapsto (\gtfun\ \ev_{i} \gtarrow \expr_{i}'' )^{\stk_{i+1}',\cachef_{i+1},\cachel_{i+1}}$, where for all $0 \leq i < n$, $\stk_{i+1}' = ((\expr_{i+1}\ \expr'_{i+1}) \lC \stk_{i+1})$, and in addition for all $0 \leq i \leq m$, $\la \stk_i,\cachef_i',\cachel_i', \expr_i'\ra \mapsto (\reval_i,\ev_i)$.  These subsume the preconditions of the $\vdashcc$ Var rule, noting that we want to pick the $n$th clause of the former mapping, where $\reval = \reval_n$ by Lemma <ref>: there is only one possible proof tree so these variables must be identical. So we have established (i), namely $((\expr_0\ \expr_0')\lC \stk_0), \cachef,\cachel_0 \vdashcc \ev_n \steps \reval$make a $\eval$.  For requirement (ii), take the established assumptions $\forall 0 \leq i \leq n.\ \stk_i \vdashc \expr_i \steps (\gtfun\ \ev_{i} \gtarrow \expr_{i}'' )^{\stk_{i+1}'}$ and $\forall 0 \leq i < n.\ \stk_{i+1}' = ((\expr_{i+1}\ \expr'_{i+1}) \lC \stk_{i+1})$ plus $\stk_n \vdashc \expr'_n \steps \reval$ and $\stk_n \vdashc \expr'_n \steps \reval$ of the $\vdashc$ Var rulemake sure variable names align, just pasted the rule in for now.  We can establish that (2) holds for each of these preconditions by induction on $n$.  For the base case, the caches are the ones in the rule itself so it is trivial.  The inductive case is direct.  Need more here.  So, in particular we have (ii) for the assumption $\stk_n \vdashc \expr'_n \steps \reval$ and since the $\vdashcc$ Var rule inherits these caches in its result this establishes (ii) for this case.  The $\Rightarrow$ direction is now complete.

$\Leftarrow$ Direction:

Assume for $\vdashcc$ and show for $\vdashc$.  We generalize the assertion to show that if

* $\stk, \cachef, \cachel \vdashcc \expr \steps \eval^{\stk',\cachef',\cachel'}$,

* For each $\la \stk_0,\cachef_0,\cachel_0,\expr_0\ra \mapsto \reval_0 \in\in \cachef$, we have $\stk_0,\cachef_0,\cachel_0 \vdashcc \expr_0 \steps \reval_0$ and $\stk_0 \vdashc \expr_0 \steps \nofl(\reval_0)$,

* For each $\la \stk_0,\cachef_0,\cachel_0,\expr_0\ra \mapsto (\reval_0,\ev_0) \in\in \cachel$, we have $\stk_0,\cachef_0,\cachel_0 \vdashcc \expr_0 \steps \reval_0$ and $\stk_0 \vdashc \expr_0 \steps \nofl(\reval_0)$,

* $\stk \vdashc \expr \steps \eval^{\stk'}$.

* For each $\la \stk_0,\cachef_0,\cachel_0,\expr_0\ra \mapsto \reval_0 \in\in \cachef'$, we have $\stk_0,\cachef_0,\cachel_0 \vdashcc \expr_0 \steps \reval_0$ and $\stk_0 \vdashc \expr_0 \steps \nofl(\reval_0)$,

* For each $\la \stk_0,\cachef_0,\cachel_0,\expr_0\ra \mapsto (\reval_0,\ev_0) \in\in \cachel'$, we have $\stk_0,\cachef_0,\cachel_0 \vdashcc \expr_0 \steps \reval_0$ and $\stk_0 \vdashc \expr_0 \steps \nofl(\reval_0)$,

Note that this generalized statement implies the result because the caches are empty there and so the strengthened assumptions (2)-(3) are vacuously true.

Proceed by induction on the height of the sub-proof of $\gexpr$ to show that (1)-(3) implies (i)-(iii).

For the base case of the Value rule the conclusion is direct: the assumption (1) in this case is $\stk, \cachef, \cachel \vdashcc \eval \steps \eval^{\stk,\cachef,\cachel}$ and (ii) is immediate from (2), (iii) from (3), and (i), $\stk \vdashc \eval \steps \eval^{\stk}$, is immediate from the $\vdashc$ Value rule.

For the induction step, assume the goal for smaller proof trees, and assume (1)-(3) with (1) being $\stk, \cachef, \cachel \vdashcc \expr \steps \reval$.

For the Application case, we must have $\expr = (\expr_1\ \expr_2)$ so we have $\stk, \cachef, \cachel \vdashcc (\expr_1\ \expr_2) \steps \reval$.  We can directly apply the induction hypothesis for the function and argument lookup subgoals in the rule: since the input caches do not change we directly inherit the requirements (2) and (3) for the induction hypotheses of these sub-derivations and obtain from (i) both $\stk \vdashc \expr_1 \steps (\gtfun\ \ev \gtarrow \expr')^{\stk_1}$ for some $\expr'$ and $\stk \vdashc \expr_2 \steps \eval_2^{\stk'}$.  In order to apply the inductive hypothesis to the established

$$((\expr_1\ \expr_2) \lC \stk), (\la \stk,\cachef,\cachel_0,\expr_1\ra \mapsto (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'} \lC\cachef'), [\la \stk,\cachef,\cachel_0,\expr_2\ra \mapsto (\reval_2,\ev)] \vdashcc \expr' \steps \reval$$

rule precondition we need to show that (2) and (3) hold for the caches in this assumption. For (2) this fact is direct as we established the preconditions (1)-(3) for the first assumption in the rule and so can conclude (ii) for the mappings $\cachef'$ in this assumption. The new mapping added in the precondition, $\la \stk,\cachef,\cachel_0,\expr_1\ra \mapsto (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'}$, is exactly the caching of the first assumption of the $\vdashcc$ rule and so by (ii) for that assumption we have that this mapping and all component mappings are provable.  So, every mapping in the function cache $(\la \stk,\cachef,\cachel_0,\expr_1\ra \mapsto (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'} \lC\cachef')$ is provable in both systems.  For precondition (3), the cache $[\la \stk,\cachef,\cachel_0,\expr_2\ra \mapsto (\reval_2,\ev)]$ of the rule precondition is exactly the second precondition of the $\vdashcc$ rule.  So, given that (ii) and (iii) hold for this precondition as established above we can conclude
$((\expr_1\ \expr_2) \lC \stk) \vdashc \expr' \steps \nofl(\reval)$ as well as (ii) and (iii) for the result caches.  Putting the three $\vdashc$ proofs established above we may apply the $\vdashc$ Application rule to obtain the desired $\stk \vdashc \expr \steps \nofl(\reval)$, and (ii) and (iii) follow directly as they are the same result caches as those occurring on the third assumption.

For the Var case, assumption (1) is of the form $((\expr_0\ \expr_0')\lC \stk_0), \cachef, \cachel \vdashcc \ev_n \steps \reval$, by the assumptions of this rule and the fact that all cached mappings are $\vdashcc$-provable by assumptions (2) and (3) we have that for all $0 \leq i \leq m$, $\stk_i,\cachef_i',\cachel_i' \vdashcc \expr_i \steps (\gtfun\ \ev_{i} \gtarrow \expr_{i}'' )^{\stk_{i+1}',\cachef_{i+1},\cachel_{i+1}}$, where for all $0 \leq i < n$, $\stk_{i+1}' = ((\expr_{i+1}\ \expr'_{i+1}) \lC \stk_{i+1})$, and in addition $\stk_n,\cachef_n',\cachel_n' \vdashcc \expr_n' \steps \reval$.  And, (2) and (3) also guarantee the analogous facts hold in the $\vdashc$ system and so we also have that for all $0 \leq i \leq m$, $\stk_i, \vdashc \expr_i \steps (\gtfun\ \ev_{i} \gtarrow \expr_{i}'' )^{\stk_{i+1}'}$, where for all $0 \leq i < n$, $\stk_{i+1}' = ((\expr_{i+1}\ \expr'_{i+1}) \lC \stk_{i+1})$, and in addition $\stk_n \vdashc \expr_n' \steps \nofl(\reval)$.  These are exactly the preconditions of the $\vdashc$ Var rule and so we have established (i), namely $((\expr_0\ \expr_0')\lC \stk_0) \vdashc \ev_n \steps \nofl(\reval)$.  For requirements (ii) and (iii), the result caches here are those on $\reval$ from $\stk_n,\cachef_n',\cachel_n' \vdashcc \expr_n' \steps \reval$, and by the meaning of $\in\in$ on cached values we also have that (ii) and (iii) hold for $\reval$'s caches. need to write out result caches explicitly here and elsewhere

Before starting the proofn, we define a bit of shorthand notation:

$\cachetoenvt((\gtfun\ \ev \gtarrow \expr)^{\stk,\cachef,\cachel}) = (\gtfun\ \ev \gtarrow \expr)^{\extractcl((\gtfun\ \ev \gtarrow \expr)^{\stk,\cachef,\cachel})}$.

We show each direction in turn. Probably need $\cachel$ to be $\cachel_0$ in all this to align with definitions and rules.

$\Rightarrow$ Direction:

We generalize the assertion to show that if

* $\stk, \cachef, \cachel \vdashcc \expr \steps \eval^{\stk',\cachef',\cachel'}$,

* $\extractenvt(\stk,\cachef,\cachel) = \envt$ for some $\envt$

* $\envt \vdashe \expr \steps \eval^{\envt'}$ for some $\envt'$,

* $\extractenvt(\stk',\cachef',\cachel') = \envt'$.

Note that this generalized statement implies the result because picking the caches to be empty will extract an empty environment.

Proceed by induction on the height of the assumption (1) proof tree to show that (1)-(2) implies (i)-(ii).

For the base case of the Value rule the conclusion is direct: the assumption (1) in this case is $\stk, \cachef, \cachel \vdashcc \eval \steps \eval^{\stk,\cachef,\cachel}$ and so (ii) is immediate from (2) picking $\envt' = \envt$ and (i), $\stk, \envt \vdashc \eval \steps \eval^{\envt}$, is immediate from the $\vdashe$ Value rule.

For the induction step, assume the goal for smaller proof trees, and assume (1)-(2) with (1) being $\stk, \cachef, \cachel \vdashcc \expr \steps \reval$.

For the Application case, we must have $\expr = (\expr_1\ \expr_2)$ so we have $\stk, \cachef, \cachel \vdashcc (\expr_1\ \expr_2) \steps \reval$.  We can directly apply the induction hypothesis for the function and argument lookup subgoals in the rule: since the input caches do not change we directly inherit the requirement (2) for the induction hypotheses of these sub-derivations and obtain from (i) both $\envt \vdashe \expr_1 \steps (\gtfun\ \ev \gtarrow \expr')^{\envt_1}$ for some $\expr'$ and $\envt \vdashe \expr_2 \steps \eval_2^{\envt'}$.  In order to apply the inductive hypothesis to the established

$$((\expr_1\ \expr_2) \lC \stk), (\la \stk,\cachef,\cachel_0,\expr_1\ra \mapsto (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'} \lC\cachef'), [\la \stk,\cachef,\cachel_0,\expr_2\ra \mapsto (\reval_2,\ev)] \vdashcc \expr' \steps \reval$$

rule precondition we need to show that (2) holds for the caches in this assumption.
By (ii) of the first assumption we have that $\extractenvt(\stk_1,\cachef',\cachel') = \envt_1$ for some $\envt_1$.  From this and the definition of $\extractenvt$ we can obtain
\begin{array}{c}
\extractenvt(\stk_1,((\expr_1\ \expr_2) \lC \stk), (\la \stk,\cachef,\cachel_0,\expr_1\ra \mapsto (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'} \lC\cachef'),[\la \stk,\cachef,\cachel_0,\expr_2\ra \mapsto (\reval_2,\ev)])\\ = \\
\ [\ev \mapsto \extractcl(\reval_2)]\lC \envt_1
\end{array}$$

Verify this step, being sloppy for now  This establishes precondition (2) for the third hypothesis, and so we may conclude (i) for that hypothesis, namely
$[\ev \mapsto \extractcl(\reval_2)]\lC \envt_1 \vdashe \expr' \steps \cachetoenvt(\reval)$ and additionally (ii) there write out?.  Putting the three $\vdashe$ proofs established above we may apply the $\vdashe$ Application rule to obtain the desired $\envt \vdashe \expr \steps \cachetoenvt(\reval)$, and (ii) follows directly as they are the same result caches as those occurring on the third assumption conclusion (ii).

For the Var case, assumption (1) is of the form $((\expr_0\ \expr_0')\lC \stk_0), \cachef, \cachel \vdashcc \ev_n \steps \reval$.  By assumption (2) we have $\extractenvt((\expr_0\ \expr_0')\lC \stk_0,\cachef,\cachel) = \envt$ for some $\envt$.  Further, from the definition of $\extractenvt$ it can be seen that $\ev_n \mapsto \cachetoenvt(\reval) \in \envt$ fill in, skipping details for now, and so $\envt \vdashe \ev_n \steps \cachetoenvt(\reval)$ by the $\vdashe$ Var rule, establishing (i) for this case. For (ii), expanding definition it amounts to requiring $\extractcl(\reval) = \extractcl(\reval)$ which follows by reflexivity. Check this and clean up notation.  Again I think $r$ to $v$ would overall be clearer here.

$\Leftarrow$ Direction:

Assume for $\vdashe$ and show for $\vdashcc$.
We generalize the assertion to show that for all $\stk$, $\cachef$ and $\cachel$, if

* $\envt \vdashe \expr \steps \eval^{\envt'}$ for some $\envt'$,

* $\extractenvt(\stk,\cachef,\cachel) = \envt$

* $\stk, \cachef, \cachel \vdashcc \expr \steps \eval^{\stk',\cachef',\cachel'}$,

* $\extractenvt(\stk',\cachef',\cachel') = \envt'$.

Note that this generalized statement implies the result because the stack, environment and caches can be picked to be empty and so the strengthened assumption (2) is trivially true.

Proceed by induction on the height of the sub-proof of $\gexpr$ to show that (1)-(2) implies (i)-(ii).

For the base case of the Value rule the conclusion is direct: the assumption (1) in this case is $\envt \vdashe \eval \steps \eval^{\envt}$ and (i), $\stk, \cachef, \cachel \vdashcc \eval \steps \eval^{\stk,\cachef, \cachel}$, is immediate from the $\vdashcc$ Value rule.  (ii) is then immediate from (2),

For the induction step, assume the goal for smaller proof trees, and assume arbitrary $\stk, \cachef$, $\cachel$ with (1)-(2) holding, and (1) being $\envt \vdashe \expr \steps \reval$.

For the Application case, we must have $\expr = (\expr_1\ \expr_2)$ so we have $\envt \vdashe (\expr_1\ \expr_2) \steps \reval$.  We can directly apply the induction hypothesis for the function and argument lookup subgoals in the rule, choosing $\stk$ $\cachef$ and $\cachel$ there to be the assumed arbitrary ones above.  Since these are the same we directly inherit the requirement (2) for the induction hypotheses of these sub-derivations from the assumed (2) for the conclusion, and so obtain from (i) for the first hypothesis that $\stk, \cachef,\cachel \vdashcc \expr_1 \steps (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'}$ for some $\expr',\stk_1,\cachef',\cachel'$, and similarly obtain $\stk, \cachef,\cachel \vdashcc \expr_2 \steps \eval_2^{\stk'',\cachef'',\cachel''}$ for some $\stk'',\eval_2,\cachef'',\cachel''$ for the second hypothesis.Check prime/subscript stuff here.  In order to apply the inductive hypothesis to the established

$$[\ev \mapsto \reval_2] \lC \envt_1 \vdashe \expr' \steps \reval$$

rule precondition we need to show (2) holds for this environment.  Using the $\vdashcc$ application rule as a guidepost, pick the $\stk$ for this precondition to be $\stk_1,((\expr_1\ \expr_2) \lC \stk)$, pick $\cachef$ to be $(\la \stk,\cachef,\cachel_0,\expr_1\ra \mapsto (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'} \lC\cachef')$, and pick the $\cachel$ to be $[\la \stk,\cachef,\cachel_0,\expr_2\ra \mapsto (\reval_2,\ev)]$.we aim to show

\begin{array}{c}
\extractenvt(\stk_1,((\expr_1\ \expr_2) \lC \stk), (\la \stk,\cachef,\cachel,\expr_1\ra \mapsto (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'} \lC\cachef'),[\la \stk,\cachef,\cachel,\expr_2\ra \mapsto (\reval_2',\ev)])\\ = \\
\ [\ev \mapsto \reval_2]\lC \envt_1
\end{array}$$

where $\extractcl(\reval_2')=\reval_2$.

Precondition (2) then follows because by inspection of (2)'s definition we can see we have just added one more frame to the front of the $\cachef'$ chain which preserves (2). Probably need to write this out  So, with all preconditions (2) satisfied for each rule we have both (i) and (ii) for all.  In particular for the third precondition we now have
$((\expr_1\ \expr_2) \lC \stk), (\la \stk,\cachef,\cachel_0,\expr_1\ra \mapsto (\gtfun\ \ev \gtarrow \expr')^{\stk_1,\cachef',\cachel'} \lC\cachef'),[\la \stk,\cachef,\cachel,\expr_2\ra \mapsto (\reval_2,\ev)] \vdashcc \expr' \steps \reval$ turn e to v here Putting the three $\vdashcc$ proofs established above we may apply the $\vdashcc$ Application rule to obtain the desired $\stk,\cachef,\cachel_0 \vdashcc \expr \steps \eval^{\stk',\cachef'',\cachel_0''}$, and (ii) follows directly as they are the same result caches as those occurring on the third assumption conclusion.super sloppy initial draft of this case.

For the Var case, assumption (1) is of the form $\envt \vdashe \ev_n \steps \reval$.  By assumption (2) we have $\extractenvt(\stk,\cachef,\cachel) = \envt$.  So by expanding this definition it means we have for all $0 \leq i \leq m$ that $\la \stk_i,\cachef_i',\cachel_i', \expr_i \ra \mapsto (\gtfun\ \ev_{i} \gtarrow \expr_{i}'' )^{\stk_{i+1}',\cachef_{i+1},\cachel_{i+1}}$, where for all $0 \leq i < n$, $\stk_{i+1}' = ((\expr_{i+1}\ \expr'_{i+1}) \lC \stk_{i+1})$, and in addition for all $0 \leq i \leq m$, $\la \stk_i,\cachef_i',\cachel_i', \expr_i'\ra \mapsto (\reval_i,\ev_i)$.  These subsume the preconditions of the $\vdashcc$ Var rule, noting that we want to pick the $n$th clause of the former mapping, where $\reval = \cachetoenvt(\reval_n)$ and so we have established (i), namely $((\expr_0\ \expr_0')\lC \stk_0), \cachef,\cachel \vdashcc \ev_n \steps \reval_n$make a $\eval$.  Requirement (ii) is direct from the definition of $\extractenvt$.Also super sloppy draft here.

By chaining Lemmas <ref>, <ref>, and <ref>.

§.§ Analysis Proofs

First, the set of possible $\stk$ are at most $k$ in length by inspection of the rules, and there are finitely many possible stack frames because the frames are invariably call sites in the source program.  And, results $\expr$ in the proofs are invariably subterms of the original $\gexpr$ (except for the case of relabeled variables but those two sets are finite) so they are also finite.  $\sfrags$ is finite since it is a set of elements drawn from a finite domain.  So, $\stk, \sfrags \vdasha \expr \steps \reval$ has only finitely many possible quadruples to check and so all possible proofs can be enumerated and checked in finite time.

Before proceeding with the proof proper we need to define some notation.

We use notation $\stk_0 \ll_k \stk$ to indicate that $\stk$ occurs as a subsequence of $\stk$ with $|\stk_0| = k$, or $\stk = \stk_0 \lC \stk'$ and $|\stk_0| < k$.  $\stk\lceil_k$ is the first $k$ elements of $\stk$, or is $\stk$ if $|\stk|$ is less than $k$.

The Theorem is proved by establishing the following more general assertion:

For arbitrary $\stk, e, \sfrags$ where for each $\stk_0 \ll_k \stk$, $\stk_0 \in \sfrags$, if  $\stk \vdash \expr \steps (\gtfun\ \ev \gtarrow \expr)^{\lab,\stk'}$ then $\stk\lceil_k, \sfrags \vdasha \expr \steps (\gtfun\ \ev \gtarrow \expr)^{\lab',\stk\lceil k} \globs \sfrags'$ for some $\sfrags'$.

The theorem follows immediately from this statement picking $\stk = []$ and $\sfrags = \emptyset$.  We assume the antecedents and proceed by induction on the height of the $\vdasha$ proof.  Proceed by cases on the rule at the root of the proof tree.  Consider the Application rule.  The first subgoal of the abstract execution follows directly by induction from the analogous subgoal for the concrete execution.  For the second subgoal, since we have assumption that each $\stk_0 \ll_k \stk$, $\stk_0 \in \sfrags$, in the analogous concrete subgoal  $(\lab \lC \stk) \vdash \expr \steps \reval$ we are only adding frame $\lab$ to the stack, and in the corresponding analysis rule we also add the same frame to the fragments set $(\sfrags_2 \cup (\lab \lCk \stk))$, maintaining the invariant that all sub-stacks of the concrete execution $\stk$ are in this new fragment set.  So, this allows us to apply the induction hypothesis and obtain the second subgoal and thus the goal.

For the variable lookup rules, since $\sfrags$ includes all possible fragments of the actual run by assumption, there will be some stitching of those fragments that realizes this actual stack, resulting by induction in the analogous value returned.

We are currently calling the above only a conjecture because it is delicate to show that stubbings are invariably infinite cycles which will never be provable in the $\vdasha$ rules.  Here is an outline of a proof.  The intuition is that the visited set $\visited$ is fully caching all previous "questions" asked on the current proof path, and the Stub rules will only activate if the exact same question is asked on the same path, indicating that we must be constructing an infinite proof tree which is not a proof in an inductive proof system.  The stack fragments $\sfrags$ need to be placed in the visited set to guarantee the question is exactly the same.  Besides the stubbing non-proof case, it is not hard to see that any individual run of the $\vdasha$ rules is realized as one deterministic slice of the nondeterministic set of runs of the $\vdashaa$ rules.The $\expr_1$ lookup subgoal is not put in the visited set, need to address that.  Note that I think we could give that subgoal the same $\visited \cup\{\la\ev^\lab, \stk_0, \sfrags_1\ra\}$ kind of thing to guarantee it would not cycle.

The crux of the proof is there are only polynomially distinct proof judgement questions that can be asked, and if all such questions are cached as they are answered, the overall execution must be polynomial.

Consider how many distinct proof “input” states $\la \expr, \stk,\sfrags,\visited \ra$ in proof judgements $\stk, \sfrags, \pathc, \visited \vdashea \expr \steps \reval \globs \sfrags'$ can exist.  For a program of size $n$ there are at most $n^k$ stacks of length $k$.  Since $k$ is fixed ($2$ in our current implementation) this is polynomial.  Possible $\expr$ are also polynomial since each $\expr$ in any proof is either directly a sub-expression of the original $\gexpr$ or it is $\ev^\lab$ for some $\lab$ already in $\gexpr$.  For $\sfrags$, consider how many distinct sets $\sfrags$ arise in a derivation.  Observe the cardinality of the set is bounded by a polynomial since as observed above there are at most $n^k$ stacks of length $k$. Next, observe that $\sfrags$ is monotonically increasing in a traversal of the proof tree, so there must be at most polynomially many distinct $\sfrags$ in any proof tree: sort $\sfrags$ into a list based on the order in time the $\stk$ were added, and all $\sfrags$ occurring in the proof will be prefixes of this list and there are only polynomially distinct prefixes to a polynomial-length list.  Visited sets $\visited$ are a product of $\lab$, $\stk$, and $\sfrags$ and as shown above there are polynomially many options for each and so $\visited$ is also polynomial in size.  So, there are only polynomially possible distinct $\la \expr, \stk, \sfrags,\visited\ra$ states.  The $\pathc$,  $\reval$, and final fragments $\sfrags'$ components of judgements are directly dependent on the proof tree structure of only the $\la \expr, \stk, \sfrags,\visited\ra$ components.   So, there are only polynomially many distinct judgements matching pattern $\stk, \sfrags, -, \visited \vdashea \expr \steps - \globs -$ in any proof tree.

So, all that remains to show is that it is not possible to repeat the same  $\la \expr, \stk, \sfrags,\visited\ra$-judgement in a single proof tree.  By inspection of the rules it can be seen that no $\la \expr, \stk, \sfrags,\visited\ra$ state in $\vdashaa$ will be visited more than once on any path from root to leaf in a proof tree: $\visited$ must be extended so the state will change.  The same goal could appear in different parts of the proof tree, but an algorithm using a cache indexed by $\la \expr, \stk, \sfrags,\visited\ra$ can construct any such common sub-proofs only once.  So, we can conclude that at most polynomially many nodes of the proof tree need to be constructed starting from the initial goal $[], \{\}, \gttrue=\gttrue, \{\} \vdashea \gexpr \steps \reval \globs \sfrags$. The cost of constructing all subgoals of any particular goal is at most polynomial as all of the data structure operations needed are polynomial.  So, at most polynomially many nodes constructed in polynomial time implies the analysis is polynomial time.

Here are some notes defining the display version of the analysis.  To warm up here is a repeat of the display system.

= [F_0, …, F_m,…,F_n]

0 ≤m ≤n

F_m = (_m '_m)^_m

_m '_m ^m

_1 ( )^_1

_2 _2

[(_1 _2)^]_1 (_1 _2)

§.§ Single-path analysis for core theory with displays

We first define the stack finitization operations for displays.

Define $\display \lceil_k$ by the following clauses

* $\display \lceil_0 = []$

* $[(\expr_0\ \expr_0')^{\display_0}, \ldots, (\expr_n\ \expr_n')^{\display_n}] \lceil_{k+1} = [(\expr_0\ \expr_0')^{\display_0\lceil_k}, \ldots, (\expr_n\ \expr_n')^{\display_n\lceil_k}]$

For the analysis we will again use a set of fragments $\sfrags$ but they will now be display fragments: $\sfrags = \{\display_1,\dots,\display_n\}$.

The following operation defines how an $\display$ fragment can match another fragment.

Define $\display \sqsubseteq \display'$ by the following clauses:

* $\display \sqsubseteq \display$

* $[] \sqsubseteq \display$

* $[(\expr_0\ \expr_0')^{\display_0}, \ldots, (\expr_n\ \expr_n')^{\display_n}] \sqsubseteq [(\expr_0\ \expr_0')^{\display'_0}, \ldots, (\expr_n\ \expr_n')^{\display'_n}]$ if for all $i\leq n$, $\display_i \sqsubseteq \display_i'$.

Notice in the last clause that all the call sites must be identical.

OK now let's finitize things in a new ruleset.

= [F_0, …, F_m,…,F_n]

0 ≤m ≤n

' ∈

' @ m = (_m '_m)^_m'

_m','_m '

, _1 ( )^_1 '

' =([(_1 _2)^]_1)⌈_k

', (' ∪') ”
, (_1 _2) ”

§.§ All paths display system for the core

Only the app and var rules are involved in variable lookup so we will just give the core all-paths modified system here; all the other features are just passing on data structures.  Also any $\stk$ in labels etc is replaced with $\display$ in the full system.

[visited states]{ ( ),,, …}  ∪{ ^m,,, …}
{ ( )^, …}

[Seen D fragments]
{, …}

Putting the full $\display$ in $\sfrags$ will make it take much longer to cycle, so since the display is nothing but a cache the idea is to use the old theory's $\stk$ as the thing to put in the visited set.  We can extract a stack from a display by simply taking the head of all the lists:

$\vfrag(\display)$ by the following clauses

* $\vfrag([]) = []$

* $\vfrag([(\expr_0 \ \expr_1)^{\display'}] \lC \display) = [(\expr_0 \ \expr_1)^{\vfrag(\display')}]$

And, $\vfrag(\sfrags) = \{ \vfrag(\display) \mid \display \in \sfrags \}$

Note this is just a list not a tree now, the second clause could also have result $[(\expr_0 \ \expr_1)]\lC\vfrag(\display')$, a list of call sites like $\stk$.  I kept in the form above since it still is a "$\display$" as far as the grammar goes.

OK here are the rules.  We use $\display @ m$ as notation to extract the $m$-th element from the $\display$ list.

, , ( ) {( )^}

0 ≤m ≤n

^m, _0,()∉

(_1,_1) = ⋃{ (_0,_0) |∃_1 ∈. _0 ⊑_1  and  _1 @ m = (_m '_m)^_2 and

_2, , ∪{^m, _0, ()}_m'  _0 _0 }

_0, , ^m  _1 _1

Var Stub
^m,, ()∈

, , ^m  ∅

, ,  ∪_newfun _1 _1

_newfun={( '), , () }

_new={( '), , (_1∪_new)}

_new = {([( ')^]_1)⌈_k  | ( _1 _1)^_1 ∈_1}

(_2,_2) = ⋃{ (_0,_0) |( _1 _1)^_1 ∈_1

([( ')^]_1)⌈_k, _1 ∪_new, ∪_new _1 _0 _0 }

, , ( ') _2 _2

App Stub( '), , ()∈, , ( ') ∅

Random notes here.

§.§ Observations on Call by Name

I decided to switch to call-by-value mainly because the correspondence is better.  But also the envt/closure interpreter is really intended for call-by-value.  In looking through related work it is interesting that I can't find a cbn version of the standard environment/closure interpreter that is used in call-by-value.  All of the cbn interpreters are “machines” such as the Krivine abstract machine. The interpreter of Figure <ref> seems fairly obvious and straightforward and I'm pretty sure someone somewhere did something very similar but I could not find such.  It is also not too far from the Kirvine machine, but is different in a few ways.

§.§ Notes on Side Effects

Side effects require control operators: the Pred function of the ANF formulation is needed to order the effects.  So, in the label-based formulation there would need to be an analogous Pred function which gives the previous redex position label for a given program point.

Also, side effects require either global constraints on the lookup trees, or a formulation as a single-step relation where lookups are “queued up”.  I made some hand-written notes on a single-step relation version of the pure theory to show how single-stepping is possible in the environment-free operational semantics.  This plus the Pred relation above should allow for a re-formulation of the state theory as a single-step relation.

§.§ Algebraic Laws

One advantage of an environment-free presentation is how there can be a more concise algebra since the state is smaller.  Here are some very rough notes on some potential algebraic relations and what they can be used for.

* There is a total order on (program point,stack) pairs which can be defined independent of the operational semantics trace: the stacks totally order calls and within a call the program points order local computations.

* Note that all pairs will be related, including pairs which did not occur on the same computation (either because there are nondeterministic things like input or because they are call sequences that can never arise).

* Since the stack solely serves to demarcate a point in execution, a metric on stack similarity will induce a metric on how close two program states are on an execution trace.

* For a given program it is possible to define a metric which relates how “far apart” any two inputs are in terms of the difference in the execution path.  A simple version is just to run the two inputs on our new interpreter (envt-free) and compare how much overlap is in the respective caches.  For more fancy versions we can count “close” states in the cache, i.e. similar but not necessarily identical stacks.  Note this is also possible for other operational semantics but there is a lot more data to sort through, and some data can differ but not change the control flow.  In fact just comparing stacks produced will give good data for any notion of a program run (even just tracing a compiled code run), but this theory proves that is good as opposed to viewing it as a random heuristic. All we need is to use recursion for looping and do no tail call optimization.

* It is also possible to do this for two programs which are nearly similar.  The idea is to use a diff on the syntax tree to relate as many common nodes as possible, and then to use that to identify common runs: inputs which produce isomorphic caches on both program variations.  It is then possible to also measure the distance between two caches if they are not isomorphic, and again to add various notions of “close” to different cache data, e.g. if a new function added to one program ignore it on the stack etc.  This can be used to measure how much change a given commit is doing to the control flow of the program, line changes alone can be misleading.

§.§ Implementation

This is a tangential topic, we may want to just summarize it in the paper.  Its in Notes for now.  The rules here are super outdated notation-wise.

A key reason for producing this theory is to compare our demand execution with forward execution running time, to make sure we have obtained all the efficiencies possible.

In a basic implementation of this operational semantics, a hash table could be used to cache all lookups, similar to the current implementations of DDSE.  At first this sounds efficient, but the keys in the hash are lists (stacks) and so hashing is expensive – that is the main cost compared to a forward run.

Fortunately it seems like there is a better solution.  Here are some key points.

* Observe that the only place we really need to remember values is for variable lookups (the other rules are standard big-step rules)

* For Var Local, the current rule gives a call-by-name semantics (lazy without caching), and standard methods to make it lazy could be used.