Keywords

1 Introduction

Transparency is an increasing concern in computer systems: for complex systems, whose desired behavior may be difficult to formally specify, auditing is an important complement to traditional techniques for verification and static analysis for security [2, 6, 12, 16, 19, 27], program slicing [22, 26], and provenance [21, 24]. However, formal foundations of auditing as a programming language primitive are not yet well-established: most approaches view auditing as an extra-linguistic operation, rather than a first-class construct. Recently, however, Bavera and Bonelli [14] introduced a calculus in which recording and analyzing audit trails are first-class operations. They proposed a \(\lambda \)-calculus based on a Curry-Howard correspondence with Justification Logic [7,8,9,10] called calculus of audited units, or \(\mathbf CAU \). In recent work, we developed a simplified form of \(\mathbf CAU \) and proved strong normalization [25].

The type system of \(\mathbf CAU \) is based on modal logic, following Pfenning and Davies [23]: it provides a type of audited units, where s is “evidence”, or the expression that was evaluated to produce the result of type A. Expressions of this type \(\mathord {!}_qM\) contain a value of type A along with a “trail” q explaining how M was obtained by evaluating s. Trails are essentially (skeletons of) proofs of reduction of terms, which can be inspected by structural recursion using a special language construct.

To date, most work on foundations of auditing has focused on design, semantics, and correctness properties, and relatively little attention has been paid to efficient execution, while most work on auditing systems has neglected these foundational aspects. Some work on tracing and slicing has investigated the use of “lazy” tracing [22]; however, to the best of our knowledge there is no prior work on how to efficiently evaluate a language such as \(\mathbf CAU \) in which auditing is a built-in operation. This is the problem studied in this paper.

A naïve approach to implementing the semantics of \(\mathbf CAU \) as given by Bavera and Bonelli runs immediately into the following problem: a \(\mathbf CAU \) reduction first performs a principal contraction (e.g. beta reduction), which typically introduces a local trail annotation describing the reduction, that can block further beta-reductions. The local trail annotations are then moved up to the nearest enclosing audited unit constructor using one or more permutation reductions. For example:

where \(\mathcal {F}[]\) is a bang-free evaluation context and \(\mathcal {Q}[{\varvec{\beta }}]\) is a subtrail that indicates where in context \(\mathcal {F}\) the \({\varvec{\beta }}\)-step was performed. As the size of the term being executed (and distance between an audited unit constructor and the redexes) grows, this evaluation strategy slows down quadratically in the worst case; eagerly materializing the traces likewise imposes additional storage cost.

While some computational overhead seems inevitable to accommodate auditing, both of these costs can in principle be mitigated. Trail permutations are computationally expensive and can often be delayed without any impact on the final outcome. Pushing trails to the closest outer bang does not serve any real purpose: it would be more efficient to keep the trail where it was created and perform normalization only if and when the trail must be inspected (and this operation does not even actually require an actual pushout of trails, because we can reuse term structure to compute the trail structure on-the-fly).

This situation has a well-studied analogue: in the \(\lambda \)-calculus, it is not necessarily efficient to eagerly perform all substitutions as soon as a \(\beta \)-reduction happens. Instead, calculi of explicit substitutions such as Abadi et al.’s \(\lambda \sigma \) [1] have been developed in which substitutions are explicitly tracked and rewritten. Explicit substitution calculi have been studied extensively as a bridge between the declarative rewriting rules of \(\lambda \)-calculi and efficient implementations. Inspired by this work, we hypothesize that calculi with auditing can be implemented more efficiently by delaying the operations of trail extraction and erasure, using explicit symbolic representations for these operations instead of performing them eagerly.

Particular care must be placed in making sure that the trails we produce still correctly describe the order in which operations were actually performed (e.g. respecting call-by-name or call-by-value reduction): when we perform a principal contraction, pre-existing trail annotations must be recorded as history that happened before the contraction, and not after. In the original eager reduction style, this is trivial because we never contract terms containing trails; however, we will show that, thanks to the explicit trail operations, correctness can be achieved even when adopting a lazy normalization of trails.

Contributions. We study an extension of Abadi et al.’s calculus \(\lambda \sigma \) [1] with explicit auditing operations. We consider a simplified, untyped variant \(\mathbf CAU ^-\) of the Calculus of Audited Units (Sect. 2); this simplifies our presentation because type information is not needed during execution. We revisit \(\lambda \sigma \) in Sect. 3, extend it to include auditing and trail inspection features, and discuss problems with this initial, naïve approach. We address these problems by developing a new calculus \(\mathbf CAU ^-_\sigma \) with explicit versions of the “trail extraction” and “trail erasure” operations (Sect. 4), and we show that it correctly refines \(\mathbf CAU ^-\) (subject to an obvious translation). In Sect. 5, we build on \(\mathbf CAU ^-_\sigma \) to define an abstract machine for audited computation and prove its correctness. Some proofs have been omitted due to space constraints and are included in the extended version of this paper.

2 The Untyped Calculus of Audited Units

The language \(\mathbf CAU ^-\) presented here is an untyped version of the calculi \(\lambda ^h\) [14] and Ricciotti and Cheney’s \(\lambda ^{hc}\) [25] obtained by erasing all typing information and a few other related technicalities: this will allow us to address all the interesting issues related to the reduction of \(\mathbf CAU \) terms, but with a much less pedantic syntax. To help us explain the details of the calculus, we adapt some examples from our previous paper [25]; other examples are described by Bavera and Bonelli [14].

Unlike the typed variant of the calculus, we only need one sort of variables, denoted by the letters \(x, y, z \ldots \). The syntax of \(\mathbf CAU ^-\) is as follows:

figure a

\(\mathbf CAU ^-\) extends the pure lambda calculus with audited units \(\mathord {!}_q M\) (colloquially, “bang M”), whose purpose is to decorate the term M with a log q of its computation history, called trail in our terminology: when M evolves as a result of computation, q will be updated by adding information about the reduction rules that have been applied. The form \(\mathord {!}_q M\) is in general not intended for use in source programs: instead, we will write \(\mathord {!}~M\) for \(\mathord {!}_\mathbf {r}M\), where \(\mathbf {r}\) represents the empty execution history (reflexivity trail).

Audited units can then be employed in larger terms by means of the “let-bang” operator, which unpacks an audited unit and thus allows us to access its contents. The variable declared by a \({{\mathrm{let_!}}}\) is bound in its second argument: in essence \({{\mathrm{let_!}}}(x := \mathord {!}_q M,N)\) will reduce to N, where free occurrences of x have been replaced by M; the trail q will not be discarded, but will be used to produce a new trail explaining this reduction.

The expression form \(q \mathrel {\triangleright }M\) is an auxiliary, intermediate annotation of M with partial history information which is produced during execution and will eventually stored in the closest surrounding bang.

Example 1

In \(\mathbf CAU ^-\) we can express history-carrying terms explicitly: for instance, if we use \(\bar{n}\) to denote the Church encoding of a natural number n, and \( plus \) or \( fact \) for lambda terms computing addition and factorial on said representation, we can write audited units like

$$ \mathord {!}_q \bar{2} \qquad \mathord {!}_{q'} \bar{6} $$

where q is a trail representing the history of \(\bar{2}\) i.e., for instance, a witness for the computation that produced \(\bar{2}\) by reducing \( plus ~\bar{1}~\bar{1}\); likewise, \(q'\) might describe how computing \( fact ~\bar{3}\) produced \(\bar{6}\). Supposing we wish to add these two numbers together, at the same time retaining their history, we will use the \({{\mathrm{let_!}}}\) construct to look inside them:

where the final trail \(q''\) is produced by composing q and \(q'\); if this reduction happens inside an external bang, \(q''\) will eventually be captured by it.

Trails, representing sequences of reduction steps, encode the (possibly partial) computation history of a given subterm. The main building blocks of trails are \({\varvec{\beta }}\) (representing standard beta reduction), \({\varvec{\beta _!}}\) (contraction of a let-bang redex) and \(\mathbf {ti}\) (denoting the execution of a trail inspection). For every class of terms we have a corresponding congruence trail (\(\mathbf {lam}, \mathbf {app}, \mathbf {let_!}, \mathbf {tb}\), the last of which is associated with trail inspections), with the only exception of bangs, which do not need a congruence rule because they capture all the computation happening inside them. The syntax of trails is completed by reflexivity \(\mathbf {r}\) (representing a null computation history, i.e. a term that has not reduced yet) and transitivity \(\mathbf {t}\) (i.e. sequential composition of execution steps). As discussed by our earlier paper [25], we omit Bavera and Bonelli’s symmetry trail form.

Example 2

We build a pair of natural numbers using Church’s encoding:

The trail for the first computation step is obtained by transitivity (trail constructor \(\mathbf {t}\)) from the original trivial trail (\(\mathbf {r}\), i.e. reflexivity) composed with \({\varvec{\beta }}\), which describes the reduction of the applied lambda: this subtrail is wrapped in a congruence \(\mathbf {app}\) because the reduction takes place deep inside the left-hand subterm of an application (the other argument of \(\mathbf {app}\) is reflexivity, because no reduction takes place in the right-hand subterm).

The second beta-reduction happens at the top level and is thus not wrapped in a congruence. It is combined with the previous trail by means of transitivity.

The last term form \(\iota (\vartheta )\), called trail inspection, will perform primitive recursion on the computation history of the current audited unit. The metavariables \(\vartheta \) and \(\zeta \) associated with trail inspections are trail replacements, i.e. maps associating to each possible trail constructor, respectively, a term or a trail:

When the trail constructors are irrelevant for a certain \(\vartheta \) or \(\zeta \), we will omit them, using the notations \(\{ \overrightarrow{M} \}\) or \( \{ \overrightarrow{q} \}\). These constructs represent (or describe) the nine cases of a structural recursion operator over trails, which we write as \(q\vartheta \).

Definition 1

The operation \(q\vartheta \), which produces a term by structural recursion on q applying the inspection branches \(\vartheta \), is defined as follows:

figure b

where the sequence \(\overrightarrow{(q\vartheta )}\) is obtained from \(\overrightarrow{q}\) by pointwise recursion.

Example 3

Trail inspection can be used to count all of the contraction steps in the history of an audited unit, by means of the following trail replacement:

where \( sum \) is a variant of \( plus \) taking nine arguments, as required by the arity of \(\mathbf {tb}\). For example, we can count the contractions in \(q = \mathbf {t}(\mathbf {let_!}({\varvec{\beta }},\mathbf {r}),{\varvec{\beta _!}})\) as:

$$ q\vartheta _+ = plus ~( plus ~\bar{1}~\bar{0})~\bar{1} $$

2.1 Reduction

Reduction in \(\mathbf CAU ^-\) includes rules to contract the usual beta redexes (applied lambda abstractions), “beta-bang” redexes, which unpack the bang term appearing as the definiens of a \({{\mathrm{let_!}}}\), and trail inspections. These rules, which we call principal contractions, are defined as follows:

figure c

Substitution is defined in the traditional way, avoiding variable capture. The first contraction is familiar, except for the fact that the reduct has been annotated with a \({\varvec{\beta }}\) trail. The second one deals with unpacking a bang: from \(\mathord {!}_q M\) we obtain \(q \mathrel {\triangleright }M\), which is then substituted for x in the target term N; the resulting term is annotated with a \({\varvec{\beta _!}}\) trail. The third contraction defines the result of a trail inspection \(\iota (\vartheta )\). Trail inspection will be contracted by capturing the current history, as stored in the nearest enclosing bang, and performing structural recursion on it according to the branches defined by \(\vartheta \). The concept of “nearest enclosing bang” is made formal by contexts \(\mathcal {F}\) in which the hole cannot appear inside a bang (or bang-free contexts, for short):

The definition of the principal contractions is completed, as usual, by a contextual closure rule stating that they can appear in any context :

figure d

The principal contractions introduce local trail subterms \(q' \mathrel {\triangleright }M\), which can block other reductions. Furthermore, the rule for trail inspection assumes that the q annotating the enclosing bang really is a complete log of the history of the audited unit; but at the same time, it violates this invariant, because the \(\mathbf {ti}\) trail created after the contraction is not merged with the original history q.

For these reasons, we only want to perform principal contractions on terms not containing local trails: after each principal contraction, we apply the following rewrite rules, called permutation reductions, to ensure that the local trail is moved to the nearest enclosing bang:

figure e

Moreover, the following rules are added to the \(\xrightarrow {\;\; \tau \;\;}\) relation to ensure confluence:

figure f

As usual, \(\xrightarrow {\;\; \tau \;\;}\) is completed by a contextual closure rule. We prove

Lemma 1

([14]). \(\xrightarrow {\;\; \tau \;\;}\) is terminating and confluent.

When a binary relation on terms is terminating and confluent, we will write \(\mathcal {R}(M)\) for the unique \(\mathcal {R}\)-normal form of M. Since principal contractions must be performed on \(\tau \)-normal terms, it is convenient to merge contraction and \(\tau \)-normalization in a single operation, which we will denote by \(\xrightarrow {\mathbf{CAU ^-}}\):

figure g

Example 4

We take again the term from Example 1 and reduce the outer \({{\mathrm{let_!}}}\) as follows:

This \({{\mathrm{let_!}}}\)-reduction substitutes \(q \mathrel {\triangleright }2\) for x; a \({\varvec{\beta _!}}\) trail is produced immediately inside the bang, in the same position as the redex. Then, we \(\tau \)-normalize the resulting term, which results in the two trails being combined and used to annotate the enclosing bang.

3 Naïve Explicit Substitutions

We seek to adapt the existing abstract machines for the efficient normalization of lambda terms to \(\mathbf CAU ^-\). Generally speaking, most abstract machines act on nameless terms, using de Bruijn’s indices [15], thus avoiding the need to perform renaming to avoid variable capture when substituting a term into another.

Moreover, since a substitution requires to scan the whole term M and is thus not a constant time operation, it is usually not executed immediately in an eager way. The abstract machine actually manipulates closures, or pairs of a term M and an environment s declaring lazy substitutions for each of the free variables in M: this allows s to be applied in an incremental way, while scanning the term M in search for a redex. In the \(\lambda \sigma \)-calculus of Abadi et al. [1], lazy substitutions and closures are manipulated explicitly, providing an elegant bridge between the classical \(\lambda \)-calculus and its concrete implementation in abstract machines. Their calculus expresses beta reduction as the rule

$$ (\lambda .M)~N \longrightarrow M[N] $$

where \(\lambda .M\) is a nameless abstraction à la de Bruijn, and [N] is a (suspended) explicit substitution mapping the variable corresponding to the first dangling index in M to N, and all the other variables to themselves. Terms in the form M[s], representing closures, are syntactically part of \(\lambda \sigma \), as opposed to substitutions , which are meta-operations that compute a term. In this section we formulate a first attempt at adding explicit substitutions to \(\mathbf CAU ^-\). We will not prove any formal result for the moment, as our purpose is to elicit the difficulties of such a task. An immediate adaptation of \(\lambda \sigma \)-like explicit substitutions yields the following syntax:

figure h

where 1 is the first de Bruijn index, the nameless \(\lambda \) binds the first free index of its argument, and similarly the nameless \({{\mathrm{let_!}}}\) binds the first free index of its second argument. Substitutions include the identity (or empty) substitution \(\langle {} \rangle \), lift \(\mathbin {\uparrow }\) (which reinterprets all free indices n as their successor \(n+1\)), the composition \(s \circ t\) (equivalent to the sequencing of s and t) and finally \(M\cdot s\) (indicating a substitution that will replace the first free index with M, and other indices n with their predecessor \(n-1\) under substitution s). Trails are unchanged.

We write \(M[N_1 \cdots N_k]\) as syntactic sugar for \(M[N_1 \cdots N_k \cdot \langle {} \rangle ]\). Then, \(\mathbf CAU ^-\) reductions can be expressed as follows:

figure i

(trail inspection, which does not use substitutions, is unchanged). The idea is that explicit substitutions make reduction more efficient because their evaluation does not need to be performed all at once, but can be delayed, partially or completely; delayed explicit substitutions applied to the same term can be merged, so that the term does not need to be scanned twice. The evaluation of explicit substitution can be defined by the following \(\sigma \)-rules:

figure j

These rules are a relatively minor adaptation from those of \(\lambda \sigma \): as in that language, \(\sigma \)-normal forms do not contain explicit substitutions, save for the case of the index 1, which may be lifted multiple times, e.g.:

$$ 1[\mathbin {\uparrow }^n] = 1[\underbrace{\mathbin {\uparrow }\circ \cdots \circ \mathbin {\uparrow }}_{\text {{ n} times}}] $$

If we take \(1[\mathbin {\uparrow }^n]\) to represent the de Bruijn index \(n+1\), as in \(\lambda \sigma \), \(\sigma \)-normal terms coincide with a nameless representation of \(\mathbf CAU ^-\).

Fig. 1.
figure 1

Non-joinable reduction in \(\mathbf CAU ^-\) with naïve explicit substitutions

Full size image

The \(\sigma \)-rules are deferrable, in that we can perform \(\beta \)-reductions even if a term is not in \(\sigma \)-normal form. We would like to treat the \(\tau \)-rules in the same way, perhaps performing \(\tau \)-normalization only before trail inspection; however, we can see that changing the order of \(\tau \)-rules destroys confluence even when \(\beta \)-redexes are triggered in the same order. Consider for example the reductions in Fig. 1: performing a \(\tau \)-step before the beta-reduction, as in the right branch, yields the expected result. If instead we delay the \(\tau \)-step, the trail q decorating N is duplicated by beta reduction; furthermore, the order of q and \({\varvec{\beta }}\) gets mixed up: even though q records computation that happened (once) before \({\varvec{\beta }}\), the final trail asserts that q happened (twice) after \({\varvec{\beta }}\).Footnote 1 As expected, the two trails (and consequently the terms they decorate) are not joinable.

The example shows that \(\beta \)-reduction on terms whose trails have not been normalized is anachronistic. If we separated the trails stored in a term from the underlying, trail-less term, we might be able to define a catachronistic, or time-honoring version of \(\beta \)-reduction. For instance, if we write \(\left\lfloor {M} \right\rfloor \) for trail-erasure and \(\left\lceil {M} \right\rceil \) for the trail-extraction of a term M, catachronistic beta reduction could be written as follows:

We could easily define trail erasure and extraction as operations on pure \(\mathbf CAU ^-\) terms (without explicit substitutions), but the cost of eagerly computing their result would be proportional to the size of the input term; furthermore, the extension to explicit substitutions would not be straightforward. Instead, in the next section, we will describe an extended language to manipulate trail projections explicitly.

4 The Calculus \(\mathbf CAU ^-_\sigma \)

We define the untyped Calculus of Audited Units with explicit substitutions, or \(\mathbf CAU ^-_\sigma \), as the following extension of the syntax of \(\mathbf CAU ^-\) presented in Sect. 2:

figure k

\(\mathbf CAU ^-_\sigma \) builds on the observations about explicit substitutions we made in the previous section: in addition to closures M[s], it provides syntactic trail erasures denoted by \(\left\lfloor {M} \right\rfloor \); dually, the syntax of trails is extended with the explicit trail-extraction of a term, written \(\left\lceil {M} \right\rceil \). In the naïve presentation, we gave a satisfactory set of \(\sigma \)-rules defining the semantics of explicit substitutions, which we keep as part of \(\mathbf CAU ^-_\sigma \). To express the semantics of explicit projections, we provide in Fig. 2 rules stating that \(\left\lfloor {\cdot } \right\rfloor \) and \(\left\lceil {\cdot } \right\rceil \) commute with most term constructors (but not with \(\mathord {!}\)) and are blocked by explicit substitutions. These rules are completed by congruence rules asserting that they can be used in any subterm or subtrail of a given term or trail.

Fig. 2.
figure 2

\(\sigma \)-reduction for explicit trail projections

Full size image

The \(\tau \) rules from Sect. 2 are added to \(\mathbf CAU ^-_\sigma \) with the obvious adaptations. We prove that \(\sigma \) and \(\tau \), together, yield a terminating and confluent rewriting system.

Theorem 1

\((\xrightarrow {\;\; \sigma \;\;}\cup \xrightarrow {\;\; \tau \;\;})\) is terminating and confluent.

Proof

Tools like AProVE [17] are able to prove termination automatically. Local confluence can be proved easily by considering all possible pairs of rules: full confluence follows as a corollary of these two results.

4.1 Beta Reduction

We replace the definition of \(\beta \)-reduction by the following lazy rules that use trail-extraction and trail-erasure to ensure that the correct trails are eventually produced:

where \(\mathcal {F}\) specifies that the reduction cannot take place within a bang, a substitution, or a trail erasure:

As usual, the relation is extended to inner subterms by means of congruence rules. However, we need to be careful: we cannot reduce within a trail-erasure, because if we did, the newly created trail would be erroneously erased:

This is why we express the congruence rule by means of contexts \(\mathcal {E}_\sigma \) such that holes cannot appear within erasures (the definition also employs substitution contexts \(\mathcal {S}_\sigma \) to allow reduction within substitutions):

figure l

Formally, evaluation contexts are defined as follows:

Definition 2

(evaluation context)

We denote \(\sigma \tau \)-equivalence (the reflexive, symmetric, and transitive closure of ) by means of . As we will prove, \(\sigma \tau \)-equivalent \(\mathbf CAU ^-_\sigma \) terms can be interpreted as the same \(\mathbf CAU ^-\) term: for this reason, we define reduction in \(\mathbf CAU ^-_\sigma \) as the union of and :

(1)

4.2 Properties of the Rewriting System

The main results we prove concern the relationship between \(\mathbf CAU ^-\) and \(\mathbf CAU ^-_\sigma \): firstly, every \(\mathbf CAU ^-\) reduction must still be a legal reduction within \(\mathbf CAU ^-_\sigma \); in addition, it should be possible to interpret every \(\mathbf CAU ^-_\sigma \) reduction as a \(\mathbf CAU ^-\) reduction over suitable \(\sigma \tau \)-normal terms.

Theorem 2

If , then .

Theorem 3

If , then .

Although \(\mathbf CAU ^-_\sigma \), just like \(\mathbf CAU ^-\), is not confluent (different reduction strategies produce different trails, and trail inspection can be used to compute on them, yielding different terms as well), the previous results allow us to use Hardin’s interpretation technique [18] to prove a relativized confluence theorem:

Theorem 4

If and , and furthermore \(\sigma \tau (N)\) and \(\sigma \tau (R)\) are joinable in \(\mathbf CAU ^-\), then N and R are joinable in \(\mathbf{CAU ^-_\sigma } \).

Proof

See Fig. 3.

Fig. 3.
figure 3

Relativized confluence for \(\mathbf{CAU ^-_\sigma } \).

Full size image

While the proof of Theorem 2 is not overly different from the similar proof for the \(\lambda \sigma \)-calculus, Theorem 3 is more interesting. The main challenge is to prove that whenever \(M \xrightarrow {\text {Beta}}N\), we have . However, when proceeding by induction on \(M \xrightarrow {\text {Beta}}N\), the terms \(\sigma \tau (M)\) and \(\sigma \tau (N)\) are too normalized to provide us with a good enough induction hypothesis: in particular, we would want them to be in the form \(q \mathrel {\triangleright }R\) even when q is reflexivity. We call terms in this quasi-normal form focused, and prove the theorem by reasoning on them. The details of the proof are discussed in the extended version.

5 A Call-by-Value Abstract Machine

In this section, we derive an abstract machine implementing a weak call-by-value strategy. More precisely, the machine will consider subterms shaped like , where is a pure \(\mathbf CAU ^-\) term with no explicit operators, and e is an environment, i.e. an explicit substitution containing only values. In the tradition of lazy abstract machines, values are closures (typically pairing a lambda and an environment binding its free variables); in our case, the most natural notion of closure also involves trail erasures and bangs:

figure m

According to this definition, the most general case of closure is a telescope of bangs, each equipped with a complete history, terminated at the innermost level by a lambda abstraction applied to an environment and enclosed in an erasure.

The environment e contains values with dangling trails, which may be captured by bangs contained in ; however, the erasure makes sure that none of these trails may reach the external bangs; thus, along with giving meaning to free variables contained in lambdas, closures serve the additional purpose of making sure the history described by the is complete for each bang.

The machine we describe is a variant of the SECD machine. To simplify the description, the code and environment are not separate elements of the machine state, but they are combined, together with a trail, as the top item of the stack. Another major difference is that a code \(\kappa \) can be not only a normal term without explicit operations, but also be a fragment of abstract syntax tree. The stack \(\pi \) is a list of tuples containing a trail, a code, and an environment, and represents the subterm currently being evaluated (the top of the stack) and the unevaluated context, i.e. subterms whose evaluation has been deferred (the remainder of the stack). As a pleasant side-effect of allowing fragments of the AST into the stack, we never need to set aside the current stack into the dump: D is just a list of values representing the evaluated context (i.e. the subterms whose evaluation has already been completed).

figure n

The AST fragments allowed in codes include application nodes @, bang nodes , incomplete let bindings , and inspection nodes . A tuple in which the code happens to be a term can be easily interpreted as ; however, tuples whose code is an AST fragment only make sense within a certain machine state. The machine state is described by a configuration \(\varsigma \) consisting of a stack and a dump.

Fig. 4.
figure 4

Term and context configurations

Full size image

A meaningful state cannot contain just any stack and dump, but must have a certain internal coherence, which we express by means of the two judgments in Fig. 4: in particular, the machine state must be a term configuration; this notion is defined by the judgment , which employs a separate notion of context configuration, described by the judgment .

We can define the denotation of configurations by recursion on their well-formedness judgment:

Definition 3

  1. 1.

    The denotation of a context configuration is defined as follows:

    where in the last line \(i + j + 1 = 9\).

  2. 2.

    The denotation of a term configuration is defined as follows:

We see immediately that the denotation of a term configuration is a \(\mathbf CAU ^-_\sigma \) term, while that of a context configuration is a \(\mathbf CAU ^-_\sigma \) context (Definition 2).

Fig. 5.
figure 5

Call-by-value abstract machine

Full size image
Fig. 6.
figure 6

Materialization of trails for inspection

Full size image

The call-by-value abstract machine for \(\mathbf CAU ^-\) is shown in Fig. 5: in this definition we use semi-colons as a compact notation for sequences of transitivity trails. The evaluation of a pure, closed term , starts with an empty dump and a stack made of a single tuple : this is a term configuration denoting , which is \(\sigma \tau \)-equivalent to . Final states are in the form , which simply denotes the value V. When evaluating certain erroneous terms (e.g. , where function application is used on a term that is not a function), the machine may get stuck in a non-final state; these terms are rejected by the typed \(\mathbf CAU \). The advantage of our machine, compared to a naive evaluation strategy, is that in our case all the principal reductions can be performed in constant time, except for trail inspection which must examine a full trail, and thus will always require a time proportional to the size of the trail.

Let us now examine the transition rules briefly. Rules 1–3 and 10 closely match the “Split CEK” machine [3] (a simplified presentation of the SECD machine), save for the use of the @ code to represent application nodes, while in the Split CEK machine they are expressed implicitly by the stack structure.

Rule 1 evaluates an application by decomposing it, placing two new tuples on the stack for the subterms, along with a third tuple for the application node; the topmost trail remains at the application node level, and two reflexivity trails are created for the subterms; the environment is propagated to the subterm tuples.

The idea is that when the machine reaches a state in which the term at the top of the stack is a value (e.g. a lambda abstraction, as in rule 3), the value is moved to the dump, and evaluation continues on the rest of the stack. Thus when in rule 2 we evaluate an application node, the dump will contain two items resulting from the evaluation of the two subterms of the application; for the application to be meaningful, the left-hand subterm must have evaluated to a term of the form , whereas the form of the right-hand subterm is not important: the evaluation will then continue as usual on under an extended environment; the new trail will be obtained by combining the three trails from the application node and its subexpressions, followed by a trail representing beta reduction.

The evaluation of \({{\mathrm{let_!}}}\) works similarly to that of applications; however, a term is split intro and (rule 4), so that is never evaluated independently from the corresponding node. When in rule 5 we evaluate the node, the dump will contain a value corresponding to the evaluation of (which must have resulted in a value of the form ): we then proceed to evaluate in an environment extended with V; this step corresponds to a principal contraction, so we update the trail accordingly, by adding ; additionally, we need to take into account the trails from V after substitution into : we do this by extending the trail with .

Bangs are managed by rules 6 and 7. To evaluate , we split it into and a node, placing the corresponding tuples on top of the stack; the original external trail q remains with the node, whereas the internal trail \(q'\) is placed in the tuple with ; the environment e is propagated to the body of the bang but, since it may contain trails, we need to extend \(q'\) with the trails resulting from substitution into . When in rule 7 we evaluate the node, the top of the dump contains the value V resulting from the evaluation of its body: we update the dump by combining V with the bang and proceed to evaluate the rest of the stack.

The evaluation of trail inspections (rules 8 and 9) follows the same principle as that of applications, with the obvious differences due to the fact that inspections have nine subterms. The principal contraction happens in rule 9, which assumes that the inspection branches have been evaluated to and put on the dump: at this point we have to reconstruct and normalize the inspection trail and apply the inspection branches. To reconstruct the inspection trail, we combine q and the \(\overrightarrow{q_i}\) into the trail for the current subterm ; then we must collect the trails in the context of the current bang, which are scattered in the stack and dump: this is performed by the auxiliary operator \(\mathcal {I}\) of Fig. 6, defined by recursion on the well-formedness of the context configuration \(\pi ,D\); the definition is partial, as it lacks the case for \(\epsilon ,\epsilon \), corresponding to an inspection appearing outside all bangs: such terms are considered “inspection-locked” and cannot be reduced. Due to the operator \(\mathcal {I}\), rule 9 is the only rule that cannot be performed in constant time.

\(\mathcal {I}\) returns a \(\sigma \tau \)-normalized trail, which we need to apply to the branches ; from the implementation point of view, this operation is analogous to a substitution replacing the trail nodes () with the respective \(M_i\). Suppose that trails are represented as nested applications of dangling de Bruijn indices from 1 to 9 (e.g. the trail can be represented as (1 2 3) for \(\mathbf {app}=1\), \(\mathbf {r}=2\) and \({\varvec{\beta }}=3\)); then trail inspection reduction amounts to the evaluation of a trail in an environment composed of the trail inspection branches. To sum it up, rule 9 produces a state in which the current tuple contains:

  • a trail (combining the trail of the inspection node, the trails of the branches, and the trail denoting trail inspection

  • the \(\sigma \tau \)-reduced inspection “trail” (operationally, an open term with nine dangling indices) which results from

  • an environment which implements trail inspection by substituting the inspection branches for the dangling indices in the trail.

The machine is completed by rule 10, which evaluates de Bruijn indices by looking them up in the environment. Notice that the lookup operation e(n), defined when the de Bruijn index n is closed by the environment e, simply returns the n-th closure in e, but not the associated trail; the invariants of our machine ensure that this trail is considered elsewhere (particularly in rules 5 and 6).

The following theorem states that the machine correctly implements reduction.

Theorem 5

For all valid \(\varsigma \), \(\varsigma \mapsto \varsigma '\) implies .

6 Conclusions and Future Directions

The calculus \(\mathbf CAU ^-_\sigma \) which we introduced in this paper provides a finer-grained view over the reduction of history-carrying terms, and proved an effective tool in the study of the smarter evaluation techniques which we implemented in an abstract machine. \(\mathbf CAU ^-_\sigma \) is not limited to the call-by-value strategy used by our machine, and in future work we plan to further our investigation of efficient auditing to call-by-name and call-by-need. Another intriguing direction we are exploring is to combine our approach with recent advances in explicit substitutions, such as the linear substitution calculus of Accattoli and Kesner [5], and apply the distillation technique of Accattoli et al. [3]

In our discussion, we showed that the original definition of beta-reduction, when applied to terms that are not in trail-normal form, creates temporally unsound trails. We might wonder whether these anachronistic trails carry any meaning: let us take, as an example, the reduction on the left branch of Fig. 1:

We know that q is the trace left behind by the reduction that led to N from the original term, say R:

We can see that the anachronistic trail is actually consistent with the reduction of \((\lambda .M~1~1)~R\) under a leftmost-outermost strategy:

Under the anachronistic reduction, q acts as the witness of an original inner redex. Through substitution within M, we get evidence that the contraction of an inner redex can be swapped with a subsequent head reduction: this is a key result in the proof of standardization that is usually obtained using the notion of residual ([13], Lemma 11.4.5). Based on this remark, we conjecture that trails might be used to provide a more insightful proof: it would thus be interesting to see how trails relate to recent advancements in standardization [4, 11, 20, 28].