{'fraction_non_alphanumeric': 0.04563778430299109, 'fraction_numerical': 0.007863435027123875, 'mean_word_length': 4.011472752213493, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 29, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Program Equivalence in Linear Contexts

Program equivalence in linear contexts, where programs are used or executed exactly once, is an important issue in programming languages. However, existing techniques like those based on bisimulations and logical relations only target at contextual equivalence in the usual (non-linear) functional languages, and fail in capturing non-trivial equivalent programs in linear contexts, particularly when non-determinism is present. We propose the notion of linear contextual equivalence to formally characterize such program equivalence, as well as a novel and general approach to studying it in higher-order languages, based on labeled transition systems specifically designed for functional languages. We show that linear contextual equivalence indeed coincides with trace equivalence - it is sound and complete. We illustrate our technique in both deterministic (a linear version of PCF) and non-deterministic (linear PCF in Moggi's framework) functional languages.


Introduction
Contextual equivalence is an important concept in programming languages and can be used to formalize and reason about many interesting properties of computing systems. For functional languages, there are many techniques that can help to prove contextual equivalence. Among others, applicative bisimulations [1,14] and logical relations [25,28] are particularly successful.
On the other side, linear logic (and its term correspondence often known as linear λcalculus) has seen significant applications in computer science ever since its birth, due to its native mechanism of describing restricted use of resources. For example, the linear λ-calculus provides the core of a functional programming language with an expressive type system, in which statements like "this resource will be used exactly once" can be formally expressed and checked. Such properties become useful when introducing imperative concepts into functional programming [13], structural complexity theory [12], or analyzing memory allocation [30]. Moreover, linear λ-calculus, when equipped with dependent types, can serve as a representation language within a logical framework, a general meta-language for the formalization of deductive systems [6].
Introducing linearity also leads to novel observation over program equivalences. In particular, if we consider a special sort of contexts where candidate programs must be used linearly (we call these contexts linear contexts), program equivalence with respect to these contexts should be a coarser relation than the usual notion of contextual equivalence, especially when non-determinism is present. For instance, take Moggi's language for non-determinism [19], where we have a primitive ⊓ for non-deterministic choice (same as the internal choice in CSP [11]), and consider the following two functions: (1)).
Existing techniques such as bisimulation or logical relations distinguish these two functions. In fact, it is easy to show that they are not equivalent in arbitrary contexts, by considering, e.g., the context bind f = [_] in bind x = f (0) in bind y = f (0) in val(x = y).
The context makes a double evaluation of the function by applying it to concrete arguments (noticing that Moggi's language enforces a call-by-value evaluation of nondeterministic computations): with the first function f 1 , the two evaluation of f (0) can return different values since the non-deterministic choice is inside the function body; with the second function f 2 , the non-deterministic choice is made before both evaluations of f (0) and computation inside the function is deterministic, so the two evaluations always return the same value. But if we consider only linear contexts, where programs will be evaluated exactly once, then the two functions must be equivalent. However, no existing technique, at least to the best of our knowledge, can characterize such an equivalence relation with respect to linear contexts.

Related work
The motivation of the work first comes from the second author's work on building a logic (namely CSLR) for reasoning about computational indistinguishability, which is an essential concept in complexity-theoretic cryptography and helps to define many important security criteria [32,8]. The CSLR logic is based on a functional langage which characterizes probabilistic polynomial-time computations by typing, where linearity plays an important role. A rule that can identify program equivalence in linear contexts 3 can help to simplify many proofs, e.g., the IND-CPA proof of the El-Gamal encryption, which is currently in the form of so-called game-based proofs [20]. Although the language of the CSLR logic is probabilistic, a general proof technique of linear contextual equivalence is missing from the literature, particularly in the setting of purely non-determinism where there exist programs that are equivalent in linear contexts but not in general, as we described previously. Program equivalence with respect to non-linear contexts has been widely investigated. Logical relations are one of the powerful tools for proving contextual equivalence in typed lambda-calculi, in both operational [22,23,5] and denotational settings [25,18,10]. They are defined by induction on types, hence are relatively easy to use. But it is known that completeness of (strict) logical relations are often hard to achieve, especially for higher-order types. It is even worse for monadic types, particularly when non-determinism is present [17].
Characterization in terms of simulation relation has been studied in functional languages [14,9,21,16], as well as languages with linear type systems [4]. Due to the higher-order features of the languages, it is difficult to directly prove the precongruence property of similarity. A common feature crucial to this line of research is then to follow Howe's approach [14], which requires to first define a precongruence candidate, a precongruence relation by construction, and then to show the coincidence of that relation with simulation. An alternative approach, such as environmental bisimulation proposed in [27], has a built-in congruence property, but then the definition itself has very complex conditions.

Contribution
In this paper we consider contextual equivalence with respect to linear contexts only. Our approach is developed in a linear version of PCF and we propose a formal definition of the so-called linear contextual equivalence, which characterizes the notion of program equivalence when they are used only once. We give a sound and complete characterization of the linear contextual equivalence in terms of trace equivalence, based on appropriate labeled transition semantics for terms. In order to show the congruence property of trace equivalence, we exploit the internal structure of linear contexts, instead of relying on Howe's approach.
While term transitions are a relatively standard concept, the notion of context transitions that we have introduced in the development is novel. It models the interactions between programs and contexts and may have potential use in game semantics [2,15]. We also notice that such context transitions (along with program transitions) conforms to the idea of rely-guarantee reasoning, which has been successfully applied in the verification of concurrent programs [31,29,7], and may suggest an alternative approach.
Although the entire development is based on an operational treatment, the technique is general enough to be adapted in other languages with linear type systems. Indeed, we show that our approach can be applied in a non-deterministic extension of the linear PCF based on Moggi's framework with monadic types, where trace equivalence also serves as a sound and complete characterization of linear contextual equivalence. The result particularly helps us to prove the equivalence of the two functions in the previous example, as we can show that they are trace equivalent.
One can probably employ Howe's approach when proving linear contextual equivalence in a deterministic language. While Howe's approach applies to a wider variety of occasions, it is more involved; our approach is much simpler because we take advantage of linearity in resource usage. Furthermore, in non-deterministic languages, simulation based techniques fail to characterize linear contextual equivalence.

Outline
The rest of the paper is organized as follows: Section 2 defines briefly a linear version of call-by-name PCF with a dual type system, as well as its operational semantics. In particular, a labeled transition system for the language is presented and the notion of trace equivalence is defined. In Section 3 we introduce the notion of linear contextual equivalence and show that trace equivalence in linear PCF coincides with linear contextual equivalence. Section 4 extends our approach in a non-deterministic circumstance with monadic types, where technical development follows the previous two sections, and we establish the coincidence between trace equivalence and linear contextual equivalence. With this result, we show that the two functions in the previous example are indeed equivalent in linear contexts. Section 5 concludes the paper.

The call-by-name linear PCF
We start with a linear version of PCF (LPCF for short) with a call-by-name evaluation strategy. Types are given by the following grammar: Here τ & τ ′ and τ ⊗ τ ′ are usual product and tensor product respectively. Linear functions will be given types in the form τ ⊸ τ ′ . Following [26], we choose to make intuitionistic function types τ → τ ′ primitive rather than introducing exponential types. The choice makes our technical development simpler but does not affect the heart of the approach -one can certainly express non-linear function types in terms of !-types, using Girard's decompositon: τ → τ ′ = !τ ⊸ τ ′ , and adapt our technique accordingly.
Terms are built up from constants (boolean and integer values plus integer operations and fix-point recursion) and variables, using the following constructs.
e, e ′ , . . . : Integer operations | λx . e | e e ′ Abstractions and applications | true | false Booleans | if e 1 then e 2 else e 3 Conditionals | e 1 , e 2 | proj i (e) Products and projections | fix τ Fix-point recursions | e 1 ⊗ e 2 | let x ⊗ y = e in e ′ Tensor products and projections Most of the language constructs are standard: the λ-abstraction λx.e defines a function, whose linearity will be judged by the type system, and the application e e ′ applies the function e to the argument e ′ ; the conditional if e 1 then e 2 else e 3 evaluates like e 2 or e 3 , according to whether the boolean term e 1 evaluates to true or false; e 1 , e 2 , proj 1 e and proj 2 e are normal products and corresponding projections; the term fix τ e represents the least fix-point of the function e. The tensor product and tensor projection are related to linearity -the constructs actually force that no single component of a product can be discarded while the other is preserved. Tensor products are also useful for currying linear functions.
Variables appearing in the λ-binder and the let-binder (in tensor projections) are bound variables of LPCF programs. We write FV (e), FLV (e), FNV (e) for the sets of, respectively, free variables, free linear variables, and free non-linear variables in term e. We will not distinguish α-equivalent terms, which are terms syntactically identical up to renaming of bound variables. If e and e ′ are terms and x is a variable, then e[e ′ /x] denotes the term resulting from substituting e ′ for all free occurrences of x in e. More generally, given a list e 1 , ..., e n of terms and a list x 1 , ..., x n of distinct variables, we write e[e 1 /x 1 , ..., e n /x n ] for the result of simultaneously substituting each term e i for free occurrences in e of the corresponding variable x i .
A typing assertion takes the form Γ ; ∆ ⊢ e : τ , where Γ and ∆ are finite partial functions from variables to types, e is a term, and τ is a type. We adopt the notation from dual intuitionistic linear logic [3] by using Γ and ∆ to represent typing environments for, respectively, non-linear variables and linear variables. It is assumed that the codomains of the non-linear and linear typing environments are disjoint. The type assignment relation for the linear PCF consists of all typing assertions that can be derived from the axioms and rules in Figure 1, which are very standard. The notation Γ, x : τ denotes the partial function which properly extends Γ by mapping x to τ , so it is implicitly assumed that x is not in the domain of Γ . We write Prog(τ ) = {e | ∅; ∅ ⊢ e : τ } for the set of all closed programs of type τ .

The operational semantics
We first define the notion of values of LPCF.
v, v ′ , . . . : These are also canonical forms of LPCF terms. The one-step reduction ❀ between terms is inductively defined by the axioms where E is the evaluation context generated by the grammar We often call a term E[x] an evaluation context, if x is the only free variable of the term. The operational semantics that we define for LPCF is essentially a call-by-name evaluation. Although our later development depends on the operational semantics, it does not really matter whether the evaluation strategy is call-by-name or call-by-value -one can easily adapt our approach to a call-by-value semantics. The only crucial point is that we should not allow the following forms of evaluation contexts: E, e , e, E , if e then E else e ′ , if e then e ′ else E. This is because these contexts adopt syntactically duplicated linear variables without breaking linearity restriction, hence if we substitute a reducible term for such a variable, which makes multiple copies of the term in the context, then one of them may be reduced while all other copies remain unchanged. We shall see how this fact affects our approach in more detail. Indeed, such restriction over evaluation contexts conforms to the semantics of linearity -as long as a program is allowed to be "used" only once, it should not be reduced for multiple times, hence we can safely adopt such evaluation restriction in languages with linear types.
It is clear that LPCF terms in canonical form do not reduce. The following proposition also shows that every closed non-reducible term must be in the canonical form. We write e ❀ when there does not exist a term e ′ such that e ❀ e ′ , and ❀ * denotes the reflexive transitive closure of ❀.

Proposition 1.
If e is a closed term and e ❀, then e must be in the canonical form.
Proof. We prove by induction on the structure of e. Below is the analysis for noncanonical forms: e ≡ if e ′ then e 1 else e 2 . Here e ′ must be closed and not reducible (otherwise the whole term can be reduced since if [ ] then e 1 else e 2 is an evaluation context). By induction e ′ must be canonical, i.e., either true or false, but in both cases, the original term can be reduced.
Here e ′ must be closed and not reducible (since proj i [ ] is an evaluation context), and by induction, must be the canonical form e 1 , e 2 , which makes the original term reducible. -e ≡ let x ⊗ y = e ′ in e ′′ . Here e ′ must be closed and not reducible, and by induction, must be the canonical form e 1 ⊗ e 2 , which makes the original term reducible. -e ≡ e ′ e ′′ . Here e ′ must be closed and not reducible, and by induction, must be canonical: if e ′ is an abstraction or a fix-point, then the whole term can be reduced; if e ′ ∈ {succ, pred, iszero}, then e ′′ must be canonical, which will be an integer, hence the whole term can be reduced too.

⊓ ⊔
Evaluation in LPCF is deterministic and preserves typing. 1. If e ❀ * v ❀ and e ❀ * v ′ ❀ then v = v ′ . 2. Every well-typed term either converges or all of its reduction do not terminate.
Proof. It suffices to prove that the evaluation is deterministic, that is, there is at most one reduction rule that applies in any situation. This can be proved by induction on the structure of terms.

⊓ ⊔
Because the reduction is deterministic in LPCF, for any closed term e, we say e converges and write e ⇓ if it reduces to a value. Conversely, we say e diverges if the reduction of e does not terminate and we write e ⇑. We also define a specific class of terms Ω Ω Ω τ def = fix τ (λx . x), to represent non-terminating programs.

A labeled transition system for LPCF
In [9], Gordon defines explicitly a labeled transition system in order to illustrate the applicative bisimulation technique in PCF. We follow this idea to define a labeled transition system for LPCF, upon which we can define the notions of traces and trace equivalence and develop our framework.
Transition rules are listed in Figure 2: we make the typing of terms explicit in the rules as the type system plays an important role in LPCF.

Fig. 2. Labeled transition system for LPCF
The last rule in Figure 2 says that term reductions are considered as internal transitions -external transitions are labeled by actions. Note that in the sequel, we shall write e α − → e ′ for a single external transition without preceding internal transitions, and make internal transitions explicit when e ❀ · · · ❀ α − → e ′ . Intuitively, external transitions represent the way terms interact with environments (or contexts). For instance, a λ-abstraction can "consume" (application of itself to) a term, which is supplied by the environment as an argument, and forms a β-reduction. The first rule says that, what an integer or boolean constant can provide to the environment is the value of itself, and after that it can no more provide any information, hence no external transitions can occur any more. We represent this by a transition, labeled by the value of the constant, into a non-terminating program Ω Ω Ω of appropriate type.
It should be noticed that transitions are defined in general for LPCF terms, including open terms, but they never introduce new free variables. This is particularly true for @and ⊗-transitions according to their typing premises.
Let s be a finite sequence of actions α 1 α 2 . . . α n (n ≥ 1). We write e s − → if there exist terms e 1 , e 2 , . . . , e n such that e ❀ * α1 We also write α · s and s 1 · s 2 for the traces obtained by, respectively, prefixing trace s with an action α and concatenating s 1 and s 2 .
Given two traces s 1 and s 2 , we say s 1 is a subtrace of s 2 if s 1 is a prefix of s 2 when they are viewed as strings. A trace of a LPCF term e is maximal if it is not a subtrace of any other trace of Tr (e). A computational trace is a maximal trace of the form s · c, where c is a boolean or integer constant. In other words, a computational trace ends with some observable value, while a non-computational trace may end with an action in the forms @e, proj i , ⊗e or T.
The empty trace, denoted by ǫ, can be taken by any program. Meanwhile, if ǫ is the only trace that a term can take, which means the term cannot take any external action, then the term must diverge, i.e, Tr (e) = {ǫ} iff e ⇑.
We define the trace preorder ⊑ T between terms: e 1 ⊑ T e 2 iff Tr (e 1 ) ⊆ Tr (e 2 ). Two terms e 1 and e 2 are trace equivalent, written e 1 ≃ T e 2 , iff e 1 ⊑ T e 2 and e 2 ⊑ T e 1 . Proof. The first statement can be proved by contradiction; the second one is proved by induction on the length of s; the third one is a direct consequence of the definition of trace preorder.

Linear contextual equivalence
Defining a context in a language with linear types must be treated carefully, since holes can hide bound variables and consequently breaks the typing if the variable is linear [4]. We choose to replace the context hole by an explicit free variable and restrict attention to equivalence between closed terms, so as to avoid extra syntactic machinery. Intuitively, a linear context is a context where programs under examination will be evaluated and used exactly once 4 . In a linear functional language, we can formalize it by a restricted notion of contexts: a linear context C x:τ in LPCF is a term with a single linear variable x and no non-linear variables, i.e., ∅; x : τ ⊢ C x:τ : σ. We often omit the variable and type subscription when it is clear from the texts or irrelevant.

Definition 1 (Linear contextual equivalence).
We write e 1 ⊑ C e 2 for e 1 , e 2 ∈ Prog(τ ), if C[e 1 /x] ⇓ implies C[e 2 /x] ⇓ for all linear context C x:τ . The relation ⊑ C is called the linear contextual preorder between closed programs. Linear contextual equivalence ≃ C is defined as the symmetrization of ⊑ C : e 1 ≃ C τ e 2 iff e 1 ⊑ C τ e 2 and e 2 ⊑ C τ e 1 .
In [5], the definition of ground contextual equivalence (Definition 2.1) says that contexts must be of exponential types, because they are necessary for a program to adopt recursions in their type system. In LPCF non-linear function types are primitive, with no exponential types, and the type for fix-point operator indicates that recursions must be taken within non-linear functions. Hence, the above definition admits the requirement of the definition of ground contextual equivalence in [5].

Linear context transitions
Corresponding to the transition system for terms, we also define transitions for linear contexts, which only occur in evaluation contexts: Linear context transitions represent the way a context interact with programs under testing. A linear context transition often eliminates the free variable in the context or transforms it into another variable of a different type (in which case we often use a variable with a different name for the sake of clarity), which indicates that a reduction can occur involving both the candidate program and (a subterm of) the context.
Linear context transitions do not necessarily transform a linear context into another linear context -linear contexts can also be transformed into closed terms, which do not contain any free variables. This particularly happens when the program under testing is a boolean or integer constant, which, after transition, cannot provide any information to the context.
Notice that linear contexts themselves are LPCF terms, so they can also take normal transitions as defined in Figure 2. We have used explicitly distinguished notations for the two kinds of transitions.

Lemma 4 (Transition lemma).
Fro every linear context C x:τ and LPCF program e ∈ Prog(τ ) such that C[e/x] ❀, a transition from C[e/x] must be either of the two forms: Proof. Since C[e/x] ❀, it must be in the canonical form, then C must be one of the forms: x, C 1 ⊗ e ′ , e ′ ⊗ C 1 , C 1 , C 2 , λy . C 1 , where e ′ is a closed term and C 1 , C 2 are linear contexts with free variable x.
It is clear that if C ≡ x, the transition must be of the second form. In all other forms, it can be easily checked that the transition will be of the first form, with the context C itself being transformed into another term with the free linear variable x, which forms another linear context. ⊓ ⊔

Linear context reductions
Reductions of linear contexts filled with programs can be classified into several forms, called linear context reductions (LCR for short), which characterize the interaction between linear contexts and programs.

Definition 2 (Linear context reduction). Let C x:τ be a linear context and e ∈ Prog(τ ) be a LPCF program. A reduction of C[e/x] (if it is reducible) is called a linear context
reduction if it is either of the following forms: We y] for the third form of linear context reduction, indicating explicitly that the transitions involved are labeled by α.
also a linear context reduction.
Proof. Direct consequence of the definition of linear context transitions.

⊓ ⊔
The so-called linear context reduction lemma below says that, the reduction of a linear context filled with a program in LPCF must be a linear context reduction. This is the core lemma of proving precongruence of trace equivalence w.r.t. linear contexts. Proof. We prove by induction on the structure of the linear context.
-C cannot be any constant since it must contain a linear free variable. And it cannot be a normal product, a tensor product or an abstraction, as all these forms cannot be reduced any more, no matter what e is. -The simplest linear context x is an evaluation context. If e can be reduced, then it is the second case. -C ≡ if C ′ then e 1 else e 2 , where C ′ is another linear context. If C ′ [e/x] can be reduced, by induction, it must be either of the following cases: and C[e/x] can take a similar reduction.
If C ′ [e/x] cannot reduce, then it is a canonical boolean term, which is either true or false, and the only possibility of C ′ is the simplest case x, with e being a boolean constant. In this case both C and e can take the transition itself can be reduced, then by induction, it must be in one of the three forms of linear context reduction. In each case, it is easy to see that C[e/x] will take the same form of reduction.
is not reducible, then it must be of the form _, _ . There are two cases , which is the first form of linear context reduction.
• C ′ ≡ x and e ≡ e 1 , e 2 . Now both C and e can take the transition This is the third form of linear context reduction.
-C ≡ let y 1 ⊗ y 2 = C ′ in e ′ . If C ′ is reducible, by induction, the reduction of C ′ [e/x] must be a linear context reduction, then the reduction of C[e/x] will be a linear context reduction of the same form.
is not reducible, then there are two cases:  , an integer n, then C ′ ≡ x and e ≡ n. Now both C and e can take a n − → transition and C[e/x] will reduce to another integer or a boolean constant, depending on which constant e ′ is.
⊓ ⊔ The linear context reduction lemma is not true if the context is not linear or the language does not have linear types at all, because duplicated use of programs in the context will adopt reductions that cannot be characterized by LCR, particularly when the program itself is reducible, i.e., C[e/x] ❀ C[e ′ /x] is not true when e ❀ e ′ and C makes multiple copies of e. The reduction strategy also interferes, as we have mentioned when defining the operational semantics: introducing improper evaluation contexts like E, e breaks the linear context lemma, for the same reason as using non-linear contexts.

Soundness and completeness of trace equivalence
We show that in LPCF, the trace preorder relation is precongruent with respect to linear contexts. It then enables us to show that trace equivalence actually coincides with linear contextual equivalence.
The following theorem says that trace preorder in LPCF is a precongruence relation with respect to linear contexts. As LPCF is a deterministic language, the proof can be done by induction on (the length of) traces. We distinguish two cases.
By the linear context lemma, the reduction must be a linear context reduction, which is one of the following cases: • By Lemma 4, the first transition has two forms: It follows that C[e 2 /x]  The base case is trivial. For non-empty traces, we analyze by cases: − −−− →. According to the definition of linear context reduction, C must be an evaluation context, hence This is proved as follows. Suppose C[e 1 /x] ⇓ but C[e 2 /x] ⇑. We observe that all reduction sequence starting from C must terminate in order to ensure C[e 1 /x] ⇓. So we can proceed by induction on the length of the reduction sequence.
-If C is already an evaluation context, then we are done by setting C ′ to be C.
-C cannot be a normal product, a tensor product or an abstraction, as all these forms cannot be reduced any more, and are not able to meet the requirement that e 2 ⇑.
-For all other cases, if C ❀ C 1 then C 1 is also a linear context and by determinacy of reduction semantics, Proposition 3, we have C[e 1 /x] ❀ C 1 [e 1 /x] ⇓ and C[e 2 /x] ❀ C 1 [e 2 /x] ⇑. By induction applied to C 1 , there exists some evaluation context C ′ such that C 1 ❀ * C ′ , C ′ [e 1 /x] ⇓ and C ′ [e 2 /x] ⇑. Hence C ❀ * C ′ and we can find the required C ′ .
We now show that, for any terms e 1 , e 2 of the same type with e 1 ≃ C e 2 and any action sequence s, if e 1 s − → then e 2 s − →, which establishes e 1 ⊑ T e 2 . Similarly we can prove e 2 ⊑ T e 1 but we shall omit the details.
We proceed by induction on the length of the transition e 1 s − →. The base case is trivial. For the inductive step, we distinguish two cases.
e 1 ❀ e ′ 1 s − →. Clealy, we can prove, by induction on the structure of context, that e ′ 1 ⊑ C e 1 , then e ′ 1 ⊑ C e 2 . By induction, we obtain that e 2 s − →.
There are a few subcases, depending on the form of α.
• α ≡ n. Both e 1 and e 2 have type Nat, and e 1 n − → Ω Ω Ω, so e 1 ⇓ and e 1 ≡ n. Because e 1 ≃ C e 2 , e 2 ⇓ too (otherwise the simple linear context x can distinguish them). We claim that for every possible reduction sequence e 2 ❀ * e ′ 2 ❀, e ′ 2 ≡ n. First, because e 2 has type Nat, by Proposition 1, e ′ 2 has to be an integer constant. Assume that e 2 ❀ * m and m = n. Then the context C x ≡ if x = n then 0 else Ω Ω Ω will distinguish e 1 from e 2 , which contradicts e 1 ≃ C e 2 . Similar is the case where α is a boolean constant.
• α ≡ @e. In this case e 1 and e 2 must have a function type, and clearly e 1 is in the canonical form:  Suppose for a contradiction that e 11 ⊑ C e 21 . There exists some linear context C such that C[e 11 /y] ⇓ but C[e 21 /y] ⇑. By property (*), C can be assumed to be an evaluation context. Then we can construct another context

The non-deterministic linear PCF
In this section we shall extend our language with non-determinism, where emerges the example in Section 1. We show that our approach can still be applied to characterize linear contextual equivalence in the non-deterministic setting. The extension of non-determinism is made in Moggi's computational framework [19], which provides a call-by-value wrapping of imperative features in pure functional languages, using monadic types. We use Moggi's framework also because our original semantics of LPCF is a call-by-name evaluation strategy, while we need the call-byvalue evaluation of non-deterministic choice for illustrating interesting effects. Were the original semantics call-by-value, we would not have to use Moggi's framework.
The types of the non-deterministic LPCF (NLPCF for short) are extended by a unary type constructor T -Tτ is the type for non-deterministic computations that return, if terminate, values of type τ . The language then has extra constructs related to nondeterminism: The typing for sequential computation must respect the linearity restriction. Also, linear variables appear in both branches of the non-deterministic choice, since eventually only one branch will be executed. We write Prog N L (τ ) for the set of programs (closed terms) of type τ in NLPCF.

Operational semantics
The operational semantics of NLPCF is extended with the following basic reduction rules bind x = val(e ′ ) in e ❀ (λx . e)e ′ , where e ′ ❀, e 1 ⊓ e 2 ❀ e i (i = 1, 2), together with the extension for evaluation contexts: According to linearity, we do not allow evaluation contexts E ⊓ e and e ⊓ E. The ⊓ operator behaves like the internal choice in CSP [11]. We can also add the external choice operator , together with rules In accord with linearity, the typing rule for will be different from that of ⊓ : Our later development only considers the internal choice operator, but it can be easily adapted to languages with the external choice, with careful treatment of the reduction which can discard linear variables.
Canonical terms of NLPCF, besides the canonical terms of LPCF, now include terms of the form val(v) where v ❀. The propositions about canonical form and subject reduction still hold.

Proposition 4.
If e is a NLPCF program and e ❀, then e must be in canonical form.
The reduction system for NLPCF is non-deterministic and a term does not necessarily reduce to a unique value even if it converges -there is no confluence property in NLPCF. For any closed term e, we say e may converge (written as e ⇓) if there exists a value v such that e ❀ * v ❀; -e must converge (written as e ) if there is no infinite reduction starting from e, i.e., a reduction of e always terminates; -e may diverge (written as e ⇑) if e has an infinite reduction sequence e ❀ e 1 ❀ e 2 ❀ · · · ; -e must diverge (written as e ⇈) if there is no value v such that e ❀ * v ❀, i.e., e never reduces to a value.

Labeled transition system
The labeled transition system for NLPCF is extended by the following rule: The rule represents how programs of monadic types interact with contexts. Similar as in LPCF, we can define trace, trace preorder (written as ⊑ N T ) and trace equivalence (written as ≃ N T ) for NLPCF. Example 1. Consider the two programs f 1 and f 2 in Section 1. Both of them have, among many others, the trace T, @e, T, 1 because of the following inference The definition of linear context is as in LPCF, so correspondingly we have the following linear context transitions: where x ′ is a fresh variable. The linear context transition lemma still holds: Lemma 9 (Linear context transition lemma in NLPCF). For every linear context C x:τ and NLPCF program e ∈ Prog N L (τ ) such that C[e/x] ❀, a transition from C[e/x] must be either of the two forms: Proof. Similar as in Lemma 4. ⊓ ⊔

Linear contextual equivalence in NLPCF
The Morris-style contextual equivalence depends on the notion of convergence, but in NLPCF, we need to choose between the may and must notions of convergence. The notions of convergence/divergence in NLPCF accordingly leads to the following notions of equivalence relations of programs. Let e 1 , e 2 ∈ Prog N L (τ ) for arbitrary type τ , It can be easily checked that ≃ ⇓ = ≃ ⇈ and ≃ ⇑ = ≃ .
Must convergence equivalence ≃ does not conform to trace equivalence in a nondeterministic language. If the reduction is deterministic or confluent, we can conclude that a term converges as long as it has non-empty traces, however it is not true for must convergence in a non-deterministic language -by observing the traces of a term we can no longer tell whether a term has a non-terminating reduction sequence, since every term can take the empty trace, which by itself can represent divergence. In the contrary, if a term has only the empty trace, then we can conclude that the term must diverge.
The linear contextual equivalence in NLPCF is defined based on the notion of may convergence.

Definition 3 (Non-deterministic linear contextual equivalence).
We write e 1 ⊑ N C τ e 2 for e 1 , e 2 ∈ Prog N L (τ ) if C[e 1 /x] ⇓ implies C[e 2 /x] ⇓ for all linear context C x:τ . The relation ⊑ N C is called non-deterministic linear contextual preorder. Nondeterministic linear contextual equivalence ≃ N C is defined as the symmetrization of The definition of linear context reductions remains the same as in LPCF, except that we are considering the extended transition system for NLPCF. The linear context reduction lemma still holds, from which the precongruence of trace preorder follows, which in turn enables us to prove the soundness of trace preorder with respect to linear contextual equivalence in NLPCF. The above theorem allows us to prove the equivalence of the two functions in Example 1: it is easy to check that both functions have traces T, @e, T, 0 and T, @e, T, 1 (where e is an arbitrary closed NLPCF term of proper type) as well as their subtraces, and they have no other traces.

Completeness of trace equivalence in NLPCF
The rest of the section is devoted to proving the completeness of trace equivalence with respect to linear contextual equivalence in NLPCF. Unlike the proof of Theorem 3, an induction over the length of traces does not work in a non-deterministic language, therefore we propose a novel proof for completeness.
We begin with constructing trace-specific linear contexts which "recognize" the corresponding traces. Given a trace s, we define the s-context C s x:τ by induction on s: It can be easily checked that ∅; x : τ ⊢ C s x:τ : Tτ ′ for some type τ ′ , if x is a linear variable, and we call it a linear s-context. In particular, if s is a computational trace then τ ′ is Nat. We shall often omit the type information when it is obvious or irrelevant.
In the definition we do not consider traces c · s with boolean/integer constant c followed by non-empty trace s, because a valid trace must be taken by a program, while a program that takes the c-transition must be c itself, which no longer takes any external action after the transition (c s ≡ @e ′ · s ′ . If e has the trace @e ′ · s ′ , i.e., with e ′ a closed term of proper type and e ′′ ❀, then it follows that Since s ′ is a shorter trace than s, by induction, we know from If e has the trace proj 1 · s ′ , i.e., e ❀ * e 1 , e 2 Since s ′ is a shorter trace than s, by induction, we know from e ′ If e has the trace ⊗e ′ · s ′ , i.e., with ∅; z 1 : τ 1 , z 2 : τ 2 ⊢ e ′ : τ ′ (τ ≡ τ 1 ⊗ τ 2 ) and e ′′ ❀, then it follows that Since s ′ is a shorter trace than s, by induction, we know from with e ′ ❀, then it follows that Proof. We prove by induction over the length of s, with an NLPCF program e.
s = c, where c is a boolean or integer constant. Assume that c is an integer (the case of booleans is similar). Since C s x [e/x] ≡ if e = c then val(0) else Ω Ω Ω ⇓, it must hold that e may converge and e ❀ * c, hence e ❀ * c c − →.
s = @e ′ · s ′ , with e ′ a closed term of proper type. Since [e/x] ≡ bind y = val(proj 1 (e)) in C s ′ y ⇓, there must be a reduction sequence The case s ≡ proj 2 · s ′ is similar. Proof. We first note that s is not a computational trace. Otherwise the program e ′ derived from a computational trace would be Ω, which cannot make an external action α, a contradiction to the hypothesis that e ′ α − →. Let e ∈ Prog N L (τ ) be an arbitrary NLPCF program. Similar to the proof of Lemma 11, we prove by induction on the length of s. with e 1 a closed term of proper type and e ′′ ❀, then it follows that Since s ′ is a shorter trace than s, by induction, we know from e ′′ s ′ − − → e ′ α − → that C s ′ y [e ′′ /y] ❀ * val(e ′ ), therefore C s x [e/x] ❀ * val(e ′ ) by transitivity of the relation ❀ * . -s = proj 1 · s ′ . If e has the trace proj 1 · s ′ , i.e., e ❀ * e 1 , e 2 with e ′ 1 ❀, then it follows that Since s ′ is a shorter trace than s, by induction, we know from e ′ If e has the trace ⊗e ′′ · s ′ , i.e., with ∅; z 1 : τ 1 , z 2 : τ 2 ⊢ e ′′ : τ ′ (τ ≡ τ 1 ⊗ τ 2 ) and e ′′′ ❀, then it follows that  Proof. Similar to the proof of Lemma 12. We prove by induction over the length of s, with an NLPCF program e.
s = ǫ. Then C s x [e/x] ≡ val(e) ⇓. It means that e ⇓. Clearly we also have e ǫ − → e.
s = @e ′′ · s ′ , with e ′′ a closed term of proper type. Since  Proof. Assume that e 1 , e 2 are two programs and e 1 ≃ N C e 2 . Suppose e 1 s − → for some trace s. We distinguish two cases.
s is a computational trace. By Lemma  and e ′ 2 ⇓. By Lemma 2, which also holds for NLPCF, we see that e ′ 2 has the same type as e ′ 1 . Since s is not a computational trace, α must be in one of the forms @e, proj i , ⊗e or T. Depending on the type of e 1 , in each case there exists some e ′′ 2 such that e ′′ 2 ❀ and e ′ 2 ❀ * e ′′ Symmetrically, any trace of e 2 is also a trace of e 1 . Therefore, we obtain e 1 ≃ N T e 2 .

Conclusion
We have presented a novel approach for characterizing program equivalence in linear contexts, via trace equivalence in appropriate labeled transition systems. The technique is both sound and complete, and as we have shown in the paper, is general enough to be adapted for languages with linear type systems. Linear contextual equivalence is indeed a restricted notion of program equivalence and one may question its use in practice. As we have explained in the beginning of the paper, it does have application in security since we can use linearity to limit adversaries' behaviour. We also believe that such a notion of program equivalence can be useful in reasoning about programs in systems where only restricted access to resources is allowed, particularly when side effects are present. The result in non-deterministic languages already enables us to prove linear contextual equivalence between non-trivial programs.