Stefan Mehner
email: mehner@cs.uni-bonn.de

Daniel Seidel

Lutz Straßburger

Janis Voigtländer

Parametricity and Proving Free Theorems for Functional-Logic Languages

Keywords: F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs, D.1.1 [Programming Techniques]: Applicative (Functional) Programming, D.1.6 [Programming Techniques]: Logic Programming, D.3.1 [Programming Languages]: Formal Definitions and Theory-Semantics, D.3.2 [Programming Languages]: Language Classifications-Multiparadigm languages, D.3.3 [Programming Languages]: Language Constructs and Features-Polymorphism, Recursion, F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages-Denotational semantics, F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs-Functional constructs, Type structure

The goal of this paper is to provide the required foundations for establishing free theorems -statements about program equivalence, guaranteed by polymorphic types -for the functional-logic programming language Curry. For the sake of presentation we restrict ourselves to a language fragment that we call CuMin, and that has the characteristic features of Curry (both functional and logic). We present a new denotational semantics based on partially ordered sets without limits. We then introduce an intermediate language called SaLT that is essentially a lambda-calculus extended with an abstract set type, and again give a denotational semantics. We show that the standard (logical relations) techniques can be applied to obtain a general parametricity theorem for SaLT and derive free theorems from it. Via a translation from CuMin to SaLT that fits the respective semantics, we then derive free theorems for CuMin.

Introduction

One virtue of logic programming languages is their being intrinsically nondeterministic. Functional programming languages are able to emulate this behavior by using lists in order to keep track of the many possibilities. But the price is that one has to deface the syntax by additional combinators to handle those lists. Functional-logic languages like TOY [START_REF] López-Fraguas | TOY: A multiparadigm declarative system[END_REF] and Curry [START_REF] Hanus | Programming Logics -Essays in Memory of Harald Ganzinger[END_REF] combine both paradigms, thus enhancing functional programming through logical features like free variables and choice.

At the same time, TOY and Curry inherit strong polymorphic type systems from their functional background. That brings potential benefits for program analysis, transformation, and performance optimization. A popular type-based reasoning method for establishing semantic properties of and in typed functional languages like Haskell are free theorems [START_REF] Wadler | Theorems for free! In FPCA[END_REF], which are successfully applied in a multitude of ways in the functional programming world [START_REF] Gill | A short cut to deforestation[END_REF][START_REF] Voigtländer | Bidirectionalization for free! In[END_REF], and many others]. A simple example of a free theorem is the following: For every polymorphic function f :: [α] → [α] from lists to lists, arbitrary types τ 1 and τ 2 , and a function g :: τ 1 → τ 2 , we have

f • (map g) = (map g) • f
for the standard function map :: (α → β ) → [α] → [β ] that takes a function and a list and applies that function to every entry of the list. This can be useful, e.g., if one has a "pipeline" (map h) • f • (map g) in a program, which one can now replace by (map h) • (map g) • f and hence by (map (h•g))• f , while in the original expression h and g are not in reach of each other for being fused. The important aspect here is that f can be arbitrary (reverse, tail, . . . ), only its type being [α] → [α] is relevant 1 -that is the sense in which free theorems are free (while there may well be conditions on g, depending on the specific language setting).

Can we bring the powerful tool of free theorems to functional-logic languages? As a matter of fact, the example equation f • (map g) = (map g) • f for polymorphic f does not hold with the same generality there. But what does? Previous work [START_REF] Christiansen | Free theorems for functional logic programs[END_REF] has investigated free theorems for Curry phenomenologically and provides intuition for required premises of free theorems (such as conditions on g in the example above) as well as counterexamples (if said conditions are violated). Proof of the positive claims (such as validity of the free theorem for suitably conditioned g) has been elusive so far, largely because Curry's (as well as TOY's) type system conceals usage of the key feature: nondeterminism. This is convenient for programmers, as they do not have to distinguish between deterministic and nondeterministic values. However, it is a hindrance to formal reasoning: the conditions identified in said work include a notion of (weakened) determinism, and hence a type system capturing this concept would be preferable.

Let be given a typed language with polymorphic types. In order to establish free theorems, one first has to prove a general parametricity theorem [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF]. Roughly speaking, parametricity establishes a relation between two different semantic interpretations of an expression. From this, free theorems can be derived by specializing relations to (the semantics of) functions. A nondeterministic language needs some kind of set-(or multiset-) valued semantics in order to accommodate the ambiguity of evaluation results. Such a semantics has been given for a suitable sublanguage of Curry in [START_REF] Christiansen | An adequate, denotational, functional-style semantics for Typed FlatCurry[END_REF], but no parametricity theorem was proved in this "lifted" setting. Moreover, even if one were proved, the usual machinery for deriving free theorems would not be available anymore, because the relations occurring in the parametricity theorem would no longer be compatible with the graphs of the set-valued functions provided by the semantics of the programming language.

To overcome these difficulties, this paper proceeds in the following steps. In Sections 2 and 3, we describe a representative sublanguage of Curry, called CuMin (for Curry Minor), and establish a denotational semantics for it, which is based on pointed partially ordered sets and can be seen as a simplification of the denotational semantics given in [START_REF] Christiansen | An adequate, denotational, functional-style semantics for Typed FlatCurry[END_REF][START_REF] Christiansen | An adequate, denotational, functional-style semantics for Typed FlatCurry without Letrec[END_REF] based on directed complete partial orders and used as a basis for further semantic investigations into Curry by [START_REF] Christiansen | A semantics for weakly encapsulated search in functional logic programs[END_REF]. Next, we define an intermediate language called SaLT (for Set-and Lambda-Terms) which is a dedicated lambda-calculus with explicit set types and monadic operations on those, along with its semantics (Section 4). We also define a purely syntactic translation from CuMin programs to SaLT programs that preserves the semantics (Section 5). This allows us to express, within the SaLT type system, where in the original CuMin program nondeterminism is or is not actually used (Section 6). Moreover, we can apply the standard techniques to prove a parametricity theorem for SaLT and can derive free theorems from it (Section 7). Finally, we can use our semantics and translation to give formal definitions to the informal conditions from [START_REF] Christiansen | Free theorems for functional logic programs[END_REF] and derive free theorems for CuMin from the corresponding free theorems for SaLT (Section 8). In the end, we give four examples of free theorems for CuMin that are derived using our method (Section 9).

Parametricity in the presence of nondeterminism has been considered before, e.g., as a special case of a general framework for computational effects in [START_REF] Møgelberg | Relational parametricity for computational effects[END_REF]. To our knowledge, such studies have included a choice operator, but not logical free variables (which we show bring extra constraints into the picture). In fact, it is possible that SaLT without the logical feature of free variables could be expressed by choosing an appropriate monad instance in the setup of [START_REF] Møgelberg | Relational parametricity for computational effects[END_REF], provided the latter were extended to cover general recursion. But even then, and even if the monad were successfully enriched to also cover logical free variables, this would not directly result in free theorems for existing functional-logic languages like TOY and Curry. We are not interested here in lambda-calculi with nondeterminism features per se, but as a means to establish reasoning tools for those languages. This does not permit a clean slate approach, rather we have to take the specific semantic intricacies of the existing languages (like call-time choice [START_REF] Hußmann | Nondeterministic algebraic specifications and nonconfluent term rewriting[END_REF]) into account. That explains why coming up with the right semantic setup and appropriate translations forward (of programs) and backward (of free theorems) is an as important part of our development, besides the parametricity theorem for SaLT itself.

The Language CuMin

We introduce a sublanguage CuMin of Curry [START_REF] Hanus | Programming Logics -Essays in Memory of Harald Ganzinger[END_REF]. It is related to FlatCurry, which is a middle-end representation used for example in the PAKCS compiler and also in semantic investigations in the literature [START_REF] Braßel | On a tighter integration of functional and logic programming[END_REF].

The CuMin syntax is shown in Figure 1, where x n represents n variables x 1 . . . x n , and τ m accordingly. Most Curry can be expressed in CuMin2 , though the limited syntax requires some code transformations to eliminate where-clauses, lambda-abstractions, pattern-matching on left-hand sides of function definitions, guards and such. The resulting adjusted code is a sequence of top-level

P ::= D; P | D D ::= f :: κ τ; f x n = e κ ::= ∀ ε α.κ | ∀ * α.κ | ε τ ::= α | Bool | Nat | [τ] | (τ, τ ) | τ → τ e ::= x | f τ m | e 1 e 2 | let x =
pMap :: ∀ ε α. ∀ ε β . (α → β ) → (α, α) → (β , β ); pMap g p = case p of (u, v) → (g u, g v)
The type system of CuMin contains function types, the naturals, Booleans, lists, and pairs, and is an exemplary subset of the somewhat richer type system of Curry. The missing type features are largely orthogonal to the logic features discussed here and can be treated analogously. Types in CuMin can be polymorphic, but only rank-one polymorphism is allowed (hence, no quantifiers within τs). Curry features Hindley-Milner type inference, while in CuMin polymorphic functions and primitives have to be instantiated explicitly. To this end, type variables are introduced by ∀-quantifiers in a function's type annotation and remain in scope throughout its definition.

Figure 2 shows the typing rules for CuMin. An (unordered) typing context Γ = α ν m m , x n :: τ n consists of type variables α with tags ν ∈ {ε, * } and term variables with their respective types, which have to be types within Γ. A type is called a type within Γ if all its type variables are listed among the α ν m m . A typing judgment is of the form Γ e :: τ and states that e is typeable to τ (which must be a type within Γ) under the typing context Γ. If the context in a typing judgment is empty, we simply omit the context. By [τ/α] we mean syntactic replacement of occurrences of a type variable α by a type τ. We use an analogous notation for terms and we use corresponding vector notations for multiple simultaneous replacements. Figure 3 shows how judgments Γ τ ∈ Data for τ being a data type are derived. Data types are types constructed of base types (Booleans and naturals) and algebraic data type constructors (lists and tuples), but not function types or types containing functions at deeper levels.

Typing of terms is always with respect to a given program P, used in the rule for f τ m to access type information about a function defined in P. Formally, typing judgments thus would have to be indexed by that program, but we omit the index for the sake of readability. A CuMin program P is well-typed if for each function definition f x n = e with type annotation f ::

∀ ν 1 α 1 . • • • ∀ ν m α m . τ 1 → • • • → τ n → τ in P the typing judgment α ν m m ,
x n :: τ n e :: τ holds. Note, from the rule for f τ m , that the ∀ ε quantifier abstracts over all (monomorphic) types, while the ∀ * quantifier only abstracts over data types. As seen from the rule for anything τ , that primitive (which corresponds to free variables in Curry) may be used for data types only. In full Curry the restriction is not imposed by the type system, but implementations may fail at runtime if free variables are used for function types or types containing functions at some deeper level. In this respect CuMin's type system is more static, in order to ease a formal treatment.

To improve readability, we often omit the ε-tags (but never the Let us discuss some specific language features. The term constructor let . . . in allows to define local variables and introduces sharing. While these variables may be of function type, they may not be defined by a rule with arguments -i.e., let f = g in . . . is fine, but let f x = e in . . . is not and would have to be given on the top-level instead. Also, and independently of its type, the local variable cannot be used within its own defining expression, which is an actual restriction compared to full Curry. 3 Logic programming features come into CuMin by certain primitives: Computations that always fail are represented by failure. In contrast to Curry, there are no explicit free variables. Instead, and equivalently, there is the anything-primitive representing every possible value of some type. Since anything τ is an ordinary expression, it can be used as a subexpression at will and all occurrences are evaluated independently. But since let-bindings enforce sharing, in an expression like let x = anything τ in e the variable x can be used multiple times within e to represent the same value at each occurrence. Using the anything-primitive, we can define a binary choice operator ∪ that allows to combine two alternatives, like Curry's "?":

Γ τ ∈ Data Γ [τ] ∈ Data Γ τ ∈ Data Γ τ ∈ Data Γ (τ, τ ) ∈ Data
(∪) :: ∀ ε α. α → α → α; (∪) x y = case anything Bool of True → x; False → y

CuMin's Type and Term Semantics

In this section we give a denotational semantics for CuMin, based on pointed partially ordered sets (posets for short), and discuss 3 For example, in Curry the definition let ones = [ ] ?(1 : ones) in ones will only produce two lists: the empty list and an infinite sequence of 1s. This is due to the fact that as soon as the second alternative has been chosen when evaluating to head normal form, the variable ones refers to the selfsame object in the recursive call, is thus already determined and cannot switch back to being the empty list. While in an operational semantics this behavior is quite natural, it hinders a compositional denotational semantics. Thus we do not allow this in CuMin (see the typing rule for let . . . in in Figure 2, preventing the newly defined variable from being used within its own defining expression). Also, note that while [START_REF] López-Fraguas | Equivalence of two formal semantics for functional logic programs[END_REF] showed the equivalence for two established semantics, one operational [START_REF] Albert | Operational semantics for declarative multi-paradigm languages[END_REF][START_REF] Braßel | On a tighter integration of functional and logic programming[END_REF] and one based on rewriting logic [START_REF] González-Moreno | An approach to declarative programming based on a rewriting logic[END_REF], that semantic investigation was also performed in the absence of recursive let-bindings only. the connection to existing semantics for functional-logic languages. Before we do so, we take a look at examples in order to gain some intuition for the kind of nondeterminism we are dealing with.

First of all, we have the famous double coin example, given on the upper left of Figure 4. The expression double coin will only produce 0 and 2 as results, which exemplifies call-time choice: The two occurrences of the variable n in the body of double represent one (shared) value that coin can evaluate to, rather than the expression coin itself. In contrast, coin + coin does allow 1 as a result, because the top-level symbol coin is evaluated twice and every such evaluation is independent. Another way (beside passing an argument to a function) to ensure sharing is using let-bindings as in let c = coin in c + c. Here c also is a variable and thus yields the same value twice. Note that replacing both occurrences of c by the defining expression coin would change the outcome (see above), because it breaks sharing (unlike in Haskell, where even top-level constants are shared). To model call-time choice in our denotational semantics, variables will have single values assigned to them despite the fact that expressions will have a set-valued semantics.

However, call-time choice does not imply that the argument needs to produce any result in order for the function to produce at least one. If we define a function and then apply it as in alwaysTrue failure, the result will still be True. The same is the case for variables that are introduced by letbindings or patterns in case expressions. For example, the expression case (failure, failure) of (x, y) → True does allow True as a result, since neither x nor y is actually used. There are only two kinds of constructs that are strict (i.e., fail if the argument does): Case expressions are strict in the scrutinee and primitive operations (like addition or the equality test) are strict in all arguments. Therefore, case failure of (x, y) → True does not produce a result.

alwaysTrue :: Bool → Bool; alwaysTrue x = True      {⊥} if b = ⊥ e 1 i θ ,σ if b = True e 2 i θ ,σ if b = False case e of Nil → e 1 ; Cons(h,t) → e 2 i θ ,σ = l∈ e i θ ,σ      {⊥} if l = ⊥ e 1 i θ ,σ if l = [ ] e 2 i θ ,σ [h →h,t →t] if l = h : t case e of (l, r) → e 1 i θ ,σ = p∈ e i θ ,σ {⊥} if p = ⊥ e 1 i θ ,σ [l →l,r →r] if p = (l, r) f τ m 0 θ ,σ = {⊥} f τ m i+1 θ ,σ = ↓(λ a 1 . • • • ↓(λ a n . e i [α m → τ m θ ],[x n →a n ] ) • • • ) with f :: ∀ ν 1 α 1 . • • • ∀ ν m α m . τ; f x n = e in P
In the denotational semantics, failure is represented already on the element level, in order to allow variables to hold partial values. These partial values are ordered by a definedness relation, which makes the semantic ranges partially ordered sets.

We also have to take care of recursion. In Haskell the capability of unrestricted recursion allows to define infinite lists, which would not appear in a similar language with only structural recursion (corresponding to folds). Even though expressions defining infinite lists can never be fully evaluated, they have to have some semantic value. This usually requires switching from a semantics based on sets to one based on some kind of domain, i.e., ordered sets with a limit structure -e.g., directed complete partial orders, or dcpos for short. So one way to combine recursion and nondeterminism is to build a set level on top of a dcpo-structure by using power domains as done in [START_REF] Christiansen | An adequate, denotational, functional-style semantics for Typed FlatCurry[END_REF]. However, this makes the technicalities rather intricate. The key insight to evade these complications here is that nondeterminism actually subsumes general fixpoints. Indeed, unrestricted recursion can be recovered from just a form of structural recursion, failure, and free variables. For example,

replicates :: ∀α. α → [α]; replicates x = Nil α ∪ Cons(x, replicates α x)
can also be defined by

gen :: ∀α. (α → [α]) → α → [α]; gen r x = Nil α ∪ Cons(x, r x); replicates :: ∀α. α → [α]; replicates x = let n = anything Nat in foldn gen α failure α→[α] n x
where foldn h x m is m-fold application of h to x, and thus structural recursion over the naturals. 4We do not actually eschew general recursion in favor of only a structural recursion primitive in the syntax, but the just given explanations indicate that no extra provision is necessary for fixpoints in the semantics. Indeed, it is enough for the element level to allow failure, while the set level takes care of nondeterminism and thus automatically of limits. It suffices to draw elements from pointed posets rather than from dcpos since the fixpoint construction will not take place on the element level anyway, but on the set level, and our power set construction will automatically turn a pointed poset at the element level into a dcpo (indeed a semilattice) at the set level, so there is actually no need to require a dcpo structure already at the element level, as [START_REF] Christiansen | An adequate, denotational, functional-style semantics for Typed FlatCurry[END_REF][START_REF] Christiansen | An adequate, denotational, functional-style semantics for Typed FlatCurry without Letrec[END_REF] did.

So, for the element level in our semantics here, types are interpreted as pointed posets (P, ), whose least element will always be denoted by ⊥. Since all posets we are dealing with are pointed, we simply write poset rather than pointed poset from now on. Orderpreserving functions are called monotone and this is not meant to imply being a pointed function as well.

Then, we call a subset A of a poset P a lower set if ⊥ ∈ A and for all x ∈ A and y ∈ P we have that y x implies y ∈ A. If x is an element of P, we write ↓x = {y ∈ P | y x} for the lower set of elements smaller than or equal to x. For the power set construction, the set of all lower sets of a poset P is denoted by P (P). It is itself partially ordered by set inclusion ⊆, making {⊥} the least element ⊥ (since / 0 is no lower set). The function sending x ∈ P to ↓x ∈ P (P) is monotone under this order (and also pointed). While P itself does not have to have any suprema, P (P) contains suprema of arbitrary collections (their union), because a union of lower sets will again be a lower set. If the collection happens to be empty, its union is defined to be the set {⊥}. Thus P (P) is a join semilattice and thus also a dcpo.

To provide for polymorphic types, the type semantics is defined w.r.t. a type environment θ assigning posets to type variables. The defining equations are:

Bool θ = {True, False} ⊥ Nat θ = N ⊥ α θ = θ (α) [τ] θ = {x 1 : • • • : x n : e | n ≥ 0, x i ∈ τ θ , e ∈ {⊥, [ ]}} (τ, τ ) θ = {(l, r) | l ∈ τ θ , r ∈ τ θ } ⊥ τ → τ θ = {f : τ θ → P ( τ θ ) | f monotone}
The sets {True, False} and N are discretely ordered and the lifting operation • ⊥ adds ⊥ as least element. Functions map one element of the input type to a set of elements of the output type. The order on the function space is pointwise and the least defined function λ a.{⊥} serves as least element ⊥. In the semantic interpretation of lists and tuples, entries are single elements, not sets. If x = x 1 : • • • : x n : e x and y = y 1 : • • • : y m : e y with e x , e y ∈ {⊥, [ ]}, then x y holds if n = m and e y = [ ] and x i y i for all 1 ≤ i ≤ n, or n ≤ m and e x = ⊥ and (again) x i y i for all 1 ≤ i ≤ n. The order on tuples is entrywise and the type interpretation contains an explicit ⊥ that is not a tuple.

The term semantics is defined in two stages, first e i θ ,σ in Figure 5, with step index i (and w.r.t. a fixed program P). The step index restricts the number of nested function calls that can be performed. Every further invocation of a function symbol will simply result in failure. Only well-typed (in some typing context Γ) terms are considered. As before, θ is some type environment assigning posets to type variables. We also need a term environment σ mapping (typed) term variables x :: τ in Γ to elements σ (x) ∈ τ θ . Environments are written as a vector of assignments [x i → v i ] or can be given in terms of an already defined environment extended by some new bindings: σ [x → v]. Empty environments are written as / 0. For the semantics of addition and of the equality test, we employ the strict extension of the usual addition and equality test on naturals, in particular evaluating to failure if one of the arguments does. If Γ e :: τ holds, then e i θ ,σ is a lower subset of τ θ for every i ∈ N. The semantics is monotone w.r.t. the variable bindings and the index i. This means that more defined values σ (x) as well as increasing the index i can only lead to more possible results.

The second stage is to define the semantics (without restriction on the number of nested function calls) of an expression as:

e θ ,σ = i∈N e i θ ,σ (1)
This is still monotone w.r.t. the variable bindings.

The semantics presented here is a conceptual simplification, simpler but equally descriptive and expressive, of the denotational semantics based on dcpos given (for a very similar language, called TFLC) by [START_REF] Christiansen | An adequate, denotational, functional-style semantics for Typed FlatCurry[END_REF][START_REF] Christiansen | An adequate, denotational, functional-style semantics for Typed FlatCurry without Letrec[END_REF]. For the language FlatCurry used in implementations we mentioned at the beginning of Section 2, there are an established operational semantics [START_REF] Albert | Operational semantics for declarative multi-paradigm languages[END_REF][START_REF] Braßel | On a tighter integration of functional and logic programming[END_REF] and an established rewriting logic semantics [START_REF] González-Moreno | An approach to declarative programming based on a rewriting logic[END_REF]. Note that [START_REF] López-Fraguas | Equivalence of two formal semantics for functional logic programs[END_REF] showed, without considering recursive let-bindings, that the operational semantics and the rewriting logic semantics are equivalent. So we would be in good company with our semantics for that same setting if we were to formally connect it to either of those latter two semantics. Indeed, the denotational semantics given here can be easily adapted to FlatCurry without recursive let-bindings (only minor syntactic differences remain) and we claim the resulting semantics to be adequate with respect to the operational and rewriting logic semantics. The formal proof of this claim (specifically using the semantics given in [START_REF] Braßel | On a tighter integration of functional and logic programming[END_REF] as reference point) is current work.

We have already discussed, at the beginning of this section, that replacing variables by their defining expressions can change the semantics. The same is true for inlining of function definitions, as could be seen by comparing the semantics of the two CuMinfunctions dc1 and dc2 (the latter of which is the former with double inlined) given in Figure 4. The figure also features an example concerning eta-equivalence: The two CuMin-functions mayInc1 and mayInc2 are not semantically equivalent, which disproves validity of eta-equivalence as a law (for CuMin, as well as for Curry). Note that the difference between the two functions can only be observed when using either as an argument for a higher-order function like pMap. While pMap mayInc1 (0, 0) can only produce (0, 0) and (1, 1) as results, pMap mayInc2 (0, 0) can also result in (0, 1) and (1, 0). Such intricacies make equational reasoning nearly impossible in CuMin. The situation is nicer in SaLT, introduced next.

The Language SaLT and its Semantics

The syntax for SaLT is given in Figure 6. It is largely the same as that of CuMin, the major difference being that nondeterminism is made explicit by using sets on the syntactic level. For example, the following function applies f to every element x of the set s.

sMap

:: ∀α. ∀β . (α → β ) → {α} → {β }; sMap = λ f :: α → β . λ s :: {α}. s x { f x}
As in CuMin, top-level SaLT functions can be (mutually) recursive.

The typing rules for SaLT are mostly the same as for CuMin (see Figure 2), subject to some adjustments: We have added a set type constructor {τ}, which is a lot like the IO type constructor in Haskell or Curry in the sense that there is no way to inspect sets 5 ; they can only be combined using language primitives, like the newly introduced singleton sets {e} and indexed unions e 1 x e 2 (their typing rules are in Figure 7). The latter introduces a new variable x which is in scope throughout e 2 , just like the mathematical notation x∈e 1 e 2 does. 6 The primitive anything that CuMin provided for nondeterminism is now interpreted as acting at set types (see Figure 7). There is no let . . . in, and top-level functions cannot list formal parameters in SaLT (see Figure 6), so these constructs have to be paraphrased using lambda-abstractions. There is no inherent reason against keeping either as in CuMin, but they do not occur in our translation procedure and are therefore unnecessary. Accordingly, the let . . . in typing rule from Figure 2 is deleted, the rule given there for function symbols is restricted to the case n = 0 for SaLT, and the added syntactic form of lambda-abstraction has the usual typing rule (see Figure 7). The membership rules for being a data type (cf. Figure 3) remain unchanged. In particular, set types are not considered to live in Data, so that anything cannot be used to produce nested sets.

A SaLT program P is well-typed if for each function definition f = e with type annotation f ::

∀ ν 1 α 1 . • • • ∀ ν m α m .
τ in P the typing judgment α ν m m e :: τ holds. When writing code in SaLT, we take the same liberties as for CuMin, i.e., omit type annotations and allow user defined infix operators. We sometimes use set brackets as a unary operator, with f ::

∀ ν 1 α 1 . • • • ∀ ν m α m . τ; f = e in P
τ → τ θ = {f : τ θ → τ θ | f monotone} {τ} θ = P ( τ θ )
The first definition changes the interpretation of the function type, which now maps values in τ θ to single values in τ θ instead of to lower sets. The lower set construction only appears in the interpretation of the set type, in the second and newly introduced definition. The other defining equations of the type semantics are taken over from CuMin, but replacing semantics brackets • by • . These brackets are also used for the term semantics of SaLT as given in Figure 8, where the term environment σ maps variables to single values (just like in CuMin). If Γ e :: τ holds, then e i θ ,σ is an element of τ θ for every i ∈ N (unlike in CuMin, where it would be a subset). As for CuMin, the semantics is monotone w.r.t. σ and i. This means that binding variables to more defined values or increasing the index will lead to at least as defined results.

Only for set-typed expressions we define the limit:

e θ ,σ = i∈N e i θ ,σ (2)
As for CuMin, this is still monotone w.r.t. the variable bindings. We define two terms Γ t 1 :: τ and Γ t 2 :: τ to be semantically equivalent, written as t 1 ≡ t 2 , if they are interchangeable as subexpressions (in the sense of preserving the semantics w.r.t. arbitrary environments) of arbitrary set-typed expressions. If the terms are themselves set-typed, this is equivalent to t 1 θ ,σ = t 2 θ ,σ for all environments θ , σ -because of the compositionality of the semantics. Otherwise, {t 1 } θ ,σ = {t 2 } θ ,σ for all environments θ , σ is obviously necessary and also sufficient because of compositionality and equation ( 3

{ f τ m } θ ,σ = i∈N ↓( f τ m i θ ,σ ) = ↓⊥ ∪ i∈N ↓( e i [α m → τ m θ ], / 0 ) = {e[τ m /α m ]} θ ,σ
Moreover, there are interesting equivalences involving the additional concepts: the set type and the primitives using it. Using the above notion of semantic equivalence, we can state the three monad laws for sets:

{e 1 } x e 2 ≡ e 2 [e 1 /x] (3)
e 1 x {x} ≡ e 1 (4)
(e 1 x e 2 ) y e 3 ≡ e 1 x (e 2 y e 3 )

The first one will be used frequently when simplifying translated code. The third one shows the parentheses to be superfluous and we will indeed omit them. Also, if neither x appears in e 2 , nor y in e 1 , indexed unions can be swapped:

The equations ( 3)-( 6) are proved by unfolding (2) and the definitions in Figure 8 and then using the corresponding properties on the semantic level. Also, it is not difficult to see that the binary choice operator ∪ is associative and failure {τ} ≡ {failure τ } (for the relevant τ) is its unit. We also have a distributivity and an idempotence law:

(e 1 ∪ e 2 ) x e 3 ≡ (e 1 x e 3 ) ∪ (e 2 x e 3 )

e ∪ e ≡ e

The set type constructor is not an additive monad, though, since in general {failure} x e ≡ {failure}. By the first monad law, the left-hand side here is equivalent to e[failure/x], and if e does not make use of the variable x, that will not in general be equivalent to {failure}. In this respect our monad is rather like the one in [START_REF] Braßel | Transforming functional logic programs into monadic functional programs[END_REF] than (for example) the plain list monad. However, our translation, which is given in the next section, is different from the one given in [START_REF] Braßel | Transforming functional logic programs into monadic functional programs[END_REF] (which also has a different aim).

x = {x} n = {n} True = {True} False = {False} failure τ = {failure τ } anything τ = anything τ Nil τ = {Nil τ } f τ m = f t τ m let x = e 1 in e 2 =

Translating CuMin into SaLT

We give a purely syntactic way of translating CuMin programs into SaLT programs having the same semantics. Programs are translated function by function. Specifically,

f :: κ τ 1 → • • • → τ n → τ; f x n = e
as a CuMin function definition is translated into SaLT as

f t :: κ { τ 1 → • • • → τ n → τ }; f t = {λ x 1 :: τ 1 . • • • {λ x n :: τ n . e } • • • }
where we make use of the translation functions • for types and • for expressions, defined below. The transition to nested lambdaabstractions allows for the intercalation of set brackets, which produce set-typed terms.

Types are translated from CuMin to SaLT as follows:

Bool = Bool Nat = Nat α = α [τ] = [ τ ] (τ, τ ) = ( τ , τ ) τ → τ = τ → { τ }
The translation function • for expressions is shown in Figure 9. The basic idea is to translate every expression of CuMin into a settyped SaLT expression. Variables, literals and failure are therefore wrapped into singleton sets (which in the case of failure simply means that failure is mapped to failure). All expressions that act on the element level of SaLT are lifted to the set level using indexed unions. This requires the introduction of additional variables with sufficiently fresh names. The anything-primitive already acts on the set level and requires no modification.

The following lemma expresses the expected, and indeed factual, formal properties of the translation and is proved by straightforward inductions. Before seeing the translation in action, let us remark that in particular it translates the user defined binary choice operator from CuMin to SaLT. While it is not true that e 1 ∪ e 2 is syntactically exactly e 1 ∪ e 2 , these two terms are semantically equivalent in SaLT, and we will freely use that fact as a shortcut during translation. Now, consider again the double coin example in Figure 4. The translation of double is double t = {λ n. {n} n {n} n {n + n }} and can be simplified to double t = {λ n. {n + n}} using the first monad law twice. Inlining double t and coin t into dc1 t (which is a semantics-preserving transformation in SaLT) gives dc1 t ≡ {λ n. {n + n}} d ({0} ∪ {1}) c d c. After using the first monad law again and applying beta-reduction, we get dc1 t ≡ ({0} ∪ {1}) c {c + c}, and this clearly results in {0} ∪ {2}. The translation of dc2 does not allow any simplifications using monad laws. We can again inline coin t (while double has already been inlined on the CuMin side) and get dc2 t ≡ ({0} ∪ {1}) c 1 ({0} ∪ {1}) c 2 {c 1 + c 2 }. Since c 1 and c 2 are independent variables, the result is {0} ∪ {1} ∪ {2}.

Determinism

Our reason for going through the laborious process of introducing SaLT was to make the nondeterminism of CuMin explicit. Now, when we want to investigate some CuMin program, we can instead look at its translation into SaLT. After having cleaned up code by using equational reasoning (specifically formula (3)), some set-typed expressions might be identified as singleton sets. If, for example, we can transform a SaLT function Γ f :: τ 1 → {τ 2 } into a semantically equivalent composition { } • f for some f of type τ 1 → τ 2 , then we know f to be deterministic.

In many cases we can even allow a certain degree of nondeterminism: We call a CuMin function Γ g ::

τ 1 → τ 2 multi-deterministic if there is a SaLT term Γ ĝ :: { τ 1 → τ 2 } such that g ≡ sMap (λ ĝ :: τ 1 → τ 2 . { } • ĝ ) ĝ
All such witnesses ĝ for a given g are semantically equivalent. For a g as above, the translation g has the type { τ 1 → { τ 2 }}, and ĝ proves the inner level of set brackets to be cosmetic: Because of the syntactic structure (of the semantically equivalent replacement for g ) only singleton sets can occur there. For example, g = mayInc1 (see Figure 4) is a multi-deterministic CuMin function, which is witnessed by ĝ = {λ x. x} ∪ {λ x. x + 1}:

g ≡ mayInc1 t ≡ id t Nat ∪ inc t ≡ {λ x. {x}} ∪ {λ x. {x + 1}} ≡ {{ } • (λ x. x)} ∪ {{ } • (λ x. x + 1)} ≡ sMap ({ } •) ({λ x. x} ∪ {λ x. x + 1})
The translation of mayInc2, on the other hand, is a (singleton) set containing a truly nondeterministic function (see Figure 4), and therefore mayInc2 is not multi-deterministic.

The discussion in [START_REF] Christiansen | Free theorems for functional logic programs[END_REF] shows (by giving counterexamples) that in order for free theorems to hold, the inner level of nondeterminism has to be restricted, and suggests that the outer level can be tolerated. The formalization of multi-determinism therein -validity of let y = g x in (y, y) ≡ let g = g in let x = x in (g x , g x ) -is implied by the one given above. This can be checked by translating both sides of the semantic equivalence into SaLT and using the witness.

Parametricity in SaLT

Since SaLT is essentially a typed lambda-calculus with some additional features, we can, for proving parametricity, rely on existing work and only need to supply the necessary amendments. As usual, establishing parametricity depends on the definition of a logical relation by induction on the syntactic structure of types. Of course, this means that we have to define how to extend the logical relation from an element type to the according set type.

Let P 1 and P 2 be two posets and R a relation between them. The relation P (R) between P (P 1 ) and P (P 2 ) can be described like this: Two lower sets A ∈ P (P 1 ) and B ∈ P (P 2 ) are related if for every a ∈ A there are elements a ∈ A and b ∈ B related by R, such that a a , and analogously for every b ∈ B. Thus, in order for A and B to be related, it is not necessary for every a ∈ A itself to be related to some b ∈ B7 . The definition we actually use is equivalent to the above description, though we prefer to state it like this:

(A, B) ∈ P (R) ⇐⇒ ∃W ⊆ R. W = / 0 ∧ A = (a,b)∈W ↓a ∧ B = (a,b)∈W ↓b
One possible choice for W is (A × B) ∩ R whenever A and B are related, but other choices might be more useful in proofs at times.

For posets P 1 and P 2 we call a relation R strict if (⊥, ⊥) ∈ R and whole if (P 1 , P 2 ) ∈ P (R). Strictness is relevant because of the polymorphic failure-primitive, wholeness because of the (restrictedly) polymorphic anything-primitive. The following three lemmas establish some basic properties of P (R).

Lemma 7.1. Let P 1 and P 2 be posets and let R ⊆ P 1 × P 2 . If (x, y) ∈ R, then (↓x, ↓y) ∈ P (R).

Proof. Indeed {(x, y)} ⊆ R with ↓x = (a,b)∈{(x,y)} ↓a and accordingly for ↓y. Lemma 7.2. Let P 1 and P 2 be posets and let R ⊆ P 1 × P 2 . Furthermore, let I be some nonempty (index) set, and let A i ∈ P (P 1 ) and B i ∈ P (P 2 ) for i ∈ I be two collections of lower sets. If (A i , B i ) ∈ P (R) for every i ∈ I, then also

( i∈I A i , i∈I B i ) ∈ P (R).
Proof. By the definition of P (R), there is some nonempty W i ⊆ R for every i ∈ I with A i = (a,b)∈W i ↓a and accordingly for B i . Then W = i∈I W i ⊆ R is nonempty and a witness for i∈I A i and i∈I B i being related, since

i∈I A i = i∈I (a,b)∈W i ↓a = (a,b)∈W
↓a and accordingly for i∈I B i . Lemma 7.3. Let P 1 , P 2 , Q 1 , and Q 2 be posets and let R ⊆ P 1 × P 2 and S ⊆ Q 1 × Q 2 . Furthermore, let (A 1 , A 2 ) ∈ P (R) and let f 1 : P 1 → P (Q 1 ) and f 2 :

P 2 → P (Q 2 ) be monotone functions such that ∀(a 1 , a 2 ) ∈ R. (f 1 a 1 , f 2 a 2 ) ∈ P (S). Then a 1 ∈A 1 f 1 a 1 , a 2 ∈A 2 f 2 a 2 ∈ P (S)
Proof. By assumption there is a nonempty U ⊆ R with A j = (a 1 ,a 2 )∈U ↓a j for j ∈ {1, 2}. By another assumption, for every (a 1 , a 2 ) ∈ U there is a nonempty V (a 1 , a 2 ) ⊆ S with f j a j = (b 1 ,b 2 )∈V (a 1 ,a 2 ) ↓b j for j ∈ {1, 2}. Set W = (a 1 ,a 2 )∈U V (a 1 , a 2 ) ⊆ S, which is not empty because neither U nor any V (a 1 , a 2 ) is. This W shows the unions to be related, since for j ∈ {1, 2}:

a j ∈A j f j a j = (a 1 ,a 2 )∈U a j ∈↓a j f j a j = (a 1 ,a 2 )∈U f j a j = (a 1 ,a 2 )∈U (b 1 ,b 2 )∈V (a 1 ,a 2 ) ↓b j = (b 1 ,b 2 )∈W ↓b j Definition 7.4.
Let Γ be a typing context and let ρ map every type variable α in Γ to a relation between θ 1 (α) and θ 2 (α) for two type environments θ 1 and θ 2 . By induction on the syntactic structure of types, we define for every τ that is a type within Γ, a relation ∆ ρ,τ between τ θ 1 and τ θ 2 as given in Figure 10, where Id P is the identity relation on a poset P. Lemma 7.5. If in the situation of Definition 7.4, ρ maps every type variable α in Γ to a strict relation, then the relation ∆ ρ,τ is strict for every type τ.

Proof. For Booleans, the naturals, tuples, and lists, this follows from the construction. For type variables, it is an explicit requirement. The only two induction steps to check are for the set type and the function type. By assumption, ∆ ρ,τ is strict, which means (⊥, ⊥) ∈ ∆ ρ,τ . Using Lemma 7.1 we conclude (↓⊥, ↓⊥) ∈ P ∆ ρ,τ , which means ∆ ρ,{τ} is strict, too.

The least element of each function space is the function mapping every argument to ⊥. And by the definition of ∆ ρ,τ→τ the constant function to ⊥ is indeed related to the constant function to ⊥, since (⊥, ⊥) ∈ ∆ ρ,τ by assumption. Lemma 7.6. If in the situation of Definition 7.4, ρ maps every type variable α that is * -tagged in Γ to a whole 8 relation, and Γ τ ∈ Data holds, then ∆ ρ,τ is whole.

Proof. Again by induction. We have to do five cases, corresponding to the five rules for being a data type (cf. Figure 3). The first case is Γ , α * α ∈ Data. Since ∆ ρ,α = ρ(α) and α is * -tagged, the relation is whole by the assumption on ρ. The cases Γ Bool ∈ Data and Γ Nat ∈ Data are trivial since the relation ∆ ρ,τ is the identity relation in both cases. In the inductive case

Γ τ ∈ Data Γ [τ] ∈ Data
we assume ( τ θ 1 , τ θ 2 ) ∈ P ∆ ρ,τ and want to conclude that

( [τ] θ 1 , [τ] θ 2 ) ∈ P ∆ ρ,[τ]
. By the assumption there is a nonempty U ⊆ ∆ ρ,τ with τ θ 1 = (x,y)∈U ↓x and accordingly for

τ θ 2 . Set W = {(x 1 : • • • : x n : [ ], y 1 : • • • : y n : [ ]) | n ≥ 0, (x i , y i ) ∈ U} ⊆ ∆ ρ,[τ]
, which obviously is nonempty. This W shows the desired conclusion, since

[τ] θ 1 = {x 1 : • • • : x n : e | n ≥ 0, x i ∈ τ θ 1 , e ∈ {⊥, [ ]}} = n≥0 ((x 1 ,y 1 ),...,(x n ,y n ))∈U n {x 1 : • • • : x n : e | x i ∈ ↓x i , e ∈ {⊥, [ ]}} = n≥0 ((x 1 ,y 1 ),...,(x n ,y n ))∈U n ↓(x 1 : • • • : x n : [ ]) = (a 1 ,a 2 )∈W
↓a 1 8 Recall the definition from earlier in this section.

∆ ρ,α = ρ(α)

∆ ρ,{τ} = P ∆ ρ,τ ∆ ρ,Bool = Id Bool / 0 ∆ ρ,Nat = Id Nat / 0 ∆ ρ,τ→τ = {(f, g) ∈ τ → τ θ 1 × τ → τ θ 2 | ∀(x, y) ∈ ∆ ρ,τ . (f x, g y) ∈ ∆ ρ,τ } ∆ ρ,[τ] = {(x 1 : • • • : x n : e, y 1 : • • • : y n : e) | n ≥ 0, (x i , y i ) ∈ ∆ ρ,τ , e ∈ {⊥, [ ]}} ∆ ρ,(τ,τ ) = {(⊥, ⊥)} ∪ {((l 1 , r 1 ), (l 2 , r 2 )) | (l 1 , l 2 ) ∈ ∆ ρ,τ , (r 1 , r 2 ) ∈ ∆ ρ,τ } Figure 10
. Defining equations for the logical relation and accordingly for [τ] θ 2 . The last case, also inductive, is:

Γ τ ∈ Data Γ τ ∈ Data Γ (τ, τ ) ∈ Data
Its proof is analogous to that for the list case above, using

{⊥} ∪ (x 1 ,y 1 )∈U 1 (x 2 ,y 2 )∈U 2 {(x 1 , x 2 ) | x 1 ∈ ↓x 1 , x 2 ∈ ↓x 2 } = (x 1 ,y 1 )∈U 1 (x 2 ,y 2 )∈U 2 ↓(x 1 , x 2 )
as the crucial step for the statement concerning (τ, τ ) θ 1 , and accordingly with y for the statement concerning (τ, τ ) θ 2 .

Note that Lemma 7.6, which is crucial for dealing with the anything-primitive in the proof of the following theorem, would not hold if one would allow non-whole relations for * -tagged α or if function types were allowed in Data. In fact, the parametricity theorem would not hold without the decisions made concerning type variable tagging and Data. To avoid the tagging, we could of course simply require whole relations for all type variables, but that would considerably weaken the power of parametricity and free theorems in situations where the anything-primitive is not, or sparingly, used. Theorem 7.7 (Parametricity for SaLT). Let Γ e :: τ (in SaLT) be valid w.r.t. some program P and let θ 1 , σ 1 and θ 2 , σ 2 be appropriate pairs of type and term environments. Let ρ be given as in Definition 7.4 and let it map every type variable to a strict relation that is also whole for type variables that are * -tagged in Γ. If for all (x :: τ ) ∈ Γ we have (σ 1 (x), σ 2 (x)) ∈ ∆ ρ,τ , then also ( e i θ 1 ,σ 1 , e i θ 2 ,σ 2 ) ∈ ∆ ρ,τ for all i ∈ N. If additionally τ is a set type, then ( e θ 1 ,σ 1 , e θ 2 ,σ 2 ) ∈ ∆ ρ,τ .

or positive. If it is zero, we are in the base case of the outer layer of induction and the semantics of

f τ m is ⊥ both w.r.t. • 0 θ 1 ,σ 1 and • 0 θ 2 ,σ 2 .
Because of Lemma 7.5, ⊥ is related to itself. Otherwise, the semantics of f τ m (both w.r.t. • i θ 1 ,σ 1 and • i θ 2 ,σ 2 ) is defined via the semantics of rhs at the lower index i -1 and we can use the outer layer induction hypothesis. In order to make sure the relation environment [α m → ∆ ρ,τ m ] is appropriate in the induction hypothesis, one has to check that type variables which are * -tagged in f 's type signature are mapped to whole relations, which is the case by Lemma 7.6.

All remaining cases, for the primitives involving set types, are covered by the lemmas we have shown before: Singleton sets are covered by Lemma 7.1, indexed unions by Lemma 7.3, and the anything-primitive by Lemma 7.6.

The conclusion of Theorem 7.7 is that the same expression evaluated in two different semantic environments gives two related semantic values. This can be hard to work with since being related is a rather implicit notion. The standard way to deal with this is to unravel the definition of being related, in order to get semantic equivalence of two different expressions. Another way of harnessing Theorem 7.7 is presented in the following theorem, which proves semantic equivalence of two expressions directly. Here id τ = λ x :: τ. x is an identity function term in SaLT.

Theorem 7.8. Let Γ be some typing context for SaLT such that τ, τ 1 , and τ 2 are types within Γ, and let Γ be an extension of Γ to Γ, α ν , in :: τ 1 → α, out :: α → τ 2 . Let Γ e :: τ 1 → τ 2 and Γ e :: τ be valid SaLT typing judgments. If e failure τ 1 ≡ failure τ 2 , and in case of * -tagged α also Γ τ 1 ∈ Data, Γ τ 2 ∈ Data, and sMap e anything τ 1 ≡ anything τ 2 hold, then e [τ 1 /α, id τ 1 /in, e/out] ≡ e [τ 2 /α, e/in, id τ 2 /out] When this theorem is applied, it looks as though the subexpression e was transported from one place to another. Yet the two placeholders in and out are there all the time and only take turns in being replaced by e. Also, we do not have to commit ourselves as to what the free theorem for some type is. As long as we can construct the more general expression e using the additional type variable α and the two placeholders in and out, we are free to choose.

SaLT terms e that satisfy e failure τ 1 ≡ failure τ 2 are called strict. A SaLT term e is called onto if sMap e anything τ 1 ≡ anything τ 2 holds. The semantics of e does not really have to produce every single value though. It is sufficient that for every value y there is some y y in the image; such functions are called final.

Let us show an example use of Theorem 7.8, namely proving the extensionality property that the type ∀α. α → {α} is only inhabited by failure and { }. Let be given a SaLT program containing a function symbol f with type annotation f :: ∀α. α → {α}. We pick some closed type τ 2 and term x of that type, and invoke Theorem 7.8 with e = λ b. case b of True → x; False → x (which is strict) and e = sMap out ( f α (in True)) (which fixes τ 1 to Bool and τ to {τ 2 }). We get the semantic equivalence sMap e ( f Bool (id Bool True)) ≡ sMap id τ 2 ( f τ 2 (e True)), from which it is easy to see that f τ 2 x ≡ sMap e ( f Bool True). Now let us consider the term f Bool True, which is of type {Bool}. That is not a very rich type. Indeed, f Bool True must be semantically equivalent to one of the following: failure {Bool} , {True}, {False}, anything Bool . Obviously, to which of those four it is equivalent, is independent of the choice of τ 2 and x above. Thus, using the semantics of sMap and e, we obtain that either for every τ 2 and x, f τ 2 x ≡ failure {τ 2 } , or for every τ 2 and x, f τ 2 x ≡ {x}.

We do not give the proof of Theorem 7.8 here. It is largely shared with the proof of Lemma 8.1 given in the next section.

Toward Deriving Free Theorems for CuMin

For simplifying the use of SaLT parametricity in establishing free theorems for CuMin programs, we prepare a theorem (Theorem 8.3 below) similar in spirit to Theorem 7.8 but tailored to specific situations that occur when working with SaLT translations of desired CuMin equivalences. First, we discuss CuMin analogues of the notions strict and onto.

We call a CuMin term Γ g ::

τ 1 → τ 2 strict if g failure τ 1 ≡ failure τ 2 .
As in SaLT, ≡ means having equal semantics for arbitrary environments. If Γ τ 1 ∈ Data and Γ τ 2 ∈ Data, we call g multionto if it is multi-deterministic and any SaLT term ĝ witnessing this (remember, all such witnesses are semantically equivalent to each other) satisfies the following SaLT equivalence:

ĝ ĝ {( ĝ , sMap ĝ anything τ 1 )} ≡ ĝ ĝ {( ĝ , anything τ 2 )}
A good intuition for this is seeing ĝ as a set of surjective functions, though actually finality instead of surjectivity (of the constituents of the semantics of ĝ) is sufficient, as before. Also, not every single member/constituent has to be final, but for every one there has to be a more or equally defined final one. However, it is not sufficient that all member functions together produce every value in the target. For example, the multi-deterministic CuMin function mayInc1 = id Nat ∪ inc is not multi-onto, since for ĝ = {id Nat } ∪ {λ x :: Nat. x + 1} (and thus for every one of the all semantically equivalent witnesses) the left-hand side of the above supposed equivalence will lack any pair with left component the function λ x :: Nat. x + 1 and right component a set containing 0.

In the following, we write G f = {(x, f x) | x ∈ A} for the graph of a function f : A → B. Lemma 8.1. Let Γ be some typing context for SaLT such that τ, τ 1 , and τ 2 are types within Γ, and let Γ be an extension of Γ to Γ, α ν , in :: τ 1 → α, out :: α → τ . Let Γ e :: τ 1 → τ 2 and Γ e :: τ be valid SaLT typing judgments, let θ , σ be some environment pair appropriate for Γ, and let i ∈ N. If G e i θ ,σ is strict, and in case of * -tagged α also whole (and assuming in that case that additionally

Γ τ 1 ∈ Data and Γ τ 2 ∈ Data hold), then e [τ 1 /α, id τ 1 /in, e/out] i θ ,σ = e [τ 2 /α, e/in, id τ 2 /out] i θ ,σ Proof. Define θ 1 = θ [α → τ 1 θ ], θ 2 = θ [α → τ 2 θ ], σ 1 = σ [in → id τ 1 θ , out → e i θ ,σ ], and
σ 2 = σ [in → e i θ ,σ , out → id τ 2 θ ].
(Here id is used for semantic functions, not terms.) Let ρ map every type variable in Γ to an identity relation (at the type prescribed by θ ) and α to G e i θ ,σ . Every type variable is mapped to an appropriate relation since identity relations are strict and whole and the desired properties for G e i θ ,σ are premises. An easy induction proof shows that ∆ ρ,τ is an identity relation for every τ that is a type within Γ, since Γ does not contain α. For all term variables x :: τ in Γ, we have σ 1 (x) = σ 2 (x) ∈ τ θ and therefore (σ 1 (x), σ 2 (x)) ∈ ∆ ρ,τ . Also,

(σ 1 (in), σ 2 (in)) ∈ ∆ ρ,τ 1 →α ⇐⇒ (id τ 1 θ , e i θ ,σ ) ∈ ∆ ρ,τ 1 →α ⇐⇒ ∀(x 1 , x 2 ) ∈ ∆ ρ,τ 1 . (x 1 , e i θ ,σ x 2 ) ∈ ∆ ρ,α ⇐⇒ ∀x ∈ τ 1 θ . (x, e i θ ,σ x) ∈ G e i θ ,σ
is true by the definition of ∆ and G, and a similar argument shows (σ 1 (out), σ 2 (out)) ∈ ∆ ρ,α→τ 2 . Thus, by Theorem 7.7 we conclude ( e i θ 1 ,σ 1 , e i θ 2 ,σ 2 ) ∈ ∆ ρ,τ . Since τ is a type within Γ, the relation ∆ ρ,τ is the identity relation on τ θ . Thus, as desired:

e [τ 1 /α, id τ 1 /in, e/out] i θ ,σ = e i θ 1 ,σ 1 = e i θ 2 ,σ 2 = e [τ 2 /α,
ĝ ĝ e [ τ 1 /α, id τ 1 /in, ĝ /out] ≡ ĝ ĝ e [ τ 2 /α, ĝ /in, id τ 2 /out]
In the case of * -tagged α, the theorem implicitly assumes τ 1 ∈ Data and τ 2 ∈ Data, as the notion "multi-onto" would not apply otherwise.

Proof. We first concentrate on the case that α is not * -tagged. We fix some i ∈ N, some environments θ , σ , and some ĝ ∈ ĝ i θ ,σ . Then

ĝ ⊥ = ĝ failure τ 1 i [ ĝ →ĝ ] ∈ ↓ ĝ failure τ 1 i [ ĝ →ĝ ] ⊆ ĝ ∈ ĝ i θ ,σ ↓ ĝ failure τ 1 i [ ĝ →ĝ ] = ĝ ĝ { ĝ failure τ 1 } i θ ,σ ⊆ ĝ ĝ { ĝ failure τ 1 } θ ,σ = sMap ({ } •) ĝ ĝ ĝ failure τ 1 θ ,σ = g ĝ ĝ failure τ 1 θ ,σ = g failure τ 1 θ ,σ = g failure τ 1 θ ,σ = failure τ 2 θ ,σ = {⊥}
and so ĝ ⊥ = ⊥, making G ĝ a strict relation. Then we can use Lemma 8.1 for the judgments Because of the monotonicity of the semantics, the unions do not change if ĝ itself takes part as well, since it does not contribute anything additional anyway. Therefore, we do after all get the desired equation as in the case where α is not * -tagged.

Examples of Free Theorems for CuMin

In this section, we deduce four, mostly instructive, free theorems highlighting different aspects of our machinery. A common theme is that we benefit from standard equational reasoning once we are on the SaLT side. In each case, we start from a function (or simply value, in the case of the third example) of which we only know the type. Remember, that is the power of free theorems: being able to derive statements about functions without knowing their defining equations.

α → α The first example is the free theorem for the CuMin type α → α, which demonstrates the approach well, despite the derived statement itself being rather obvious (since there are not many functions of that type). Let be given CuMin types τ 1 and τ 2 (both closed), a function symbol f with type annotation f :: ∀α. α → α in the given program, and terms g and x with g :: τ 1 → τ 2 and x :: τ 1 .

We would like to prove the CuMin equivalence g (

f τ 1 x) ≡ f τ 2 (g x).
Here α is ε-quantified, so it can be instantiated with any type and the anything-primitive cannot be used for this type. The claim can be stated (via translation and one of the laws) as the following SaLT equivalence:

g g f τ 1 f x x f x y g y ≡ g g f τ 2 f x x g x z f z
Even though the statement (just) happens to be true in general for strict g, for the derivation we assume g to be also multi-deterministic; i.e., we have g ≡ sMap (λ ĝ ::

τ 1 → τ 2 . λ x :: τ 1 . { ĝ x}) ĝ ≡ ĝ ĝ {{ } • ĝ }
for some ĝ :: { τ 1 → τ 2 }. Using this to replace g in the above, then applying (5), and then getting rid of the variable g by replacing it with { } • ĝ according to (3), leads to:

ĝ ĝ f τ 1 f x x f x y ({ } • ĝ ) y ≡ ĝ ĝ f τ 2 f x x ({ } • ĝ ) x z f z
which after some further manipulations becomes:

ĝ ĝ f t τ 1 f x x sMap ĝ ( f (id x )) ≡ ĝ ĝ f t τ 2 f x x sMap id ( f ( ĝ x ))
Now, since f is a function symbol with type annotation f :: ∀α. α → α in the original program, its translation is a function symbol with type annotation f t :: ∀α. {α → {α}} in the translated program, so the following typing judgment is valid:

α ε , in :: τ 1 → α, out :: α → τ 2 f t α f x x sMap out ( f (in x )) :: { τ 2 }
Hence, Theorem 8.3 can be used with the term from that typing judgment as e , and indeed closes the gap. Strictness of g is really necessary in this example, since the given function could have been f x = failure α .

α → α → (α, α) In CuMin, if f :: ∀α. α → α → (α, α) is a function symbol, τ 1 and τ 2 closed types, g :: τ 1 → τ 2 a strict and multi-deterministic function, and x, y :: τ 1 terms, then we can show pMap g ( f τ 1 x y) ≡ let g = g in f τ 2 (g x) (g y)

where pMap is the function given at the beginning of Section 2. This time, the statement is more interesting than in the previous example, since there are many more possible functions of the given type, e.g., f x y = (x, x ∪ y) ∪ (y, failure α ). The proof is similar to the one of the previous example: translate all expressions to SaLT, make use of g being multi-deterministic, and then apply Theorem 8. Here we really need g multi-deterministic, as f x y = (x, x) and g x = x ∪ (x + 1) would constitute a counterexample otherwise. Note also that on the right-hand side of the overall claim, we use a letbinding to share a common value of g throughout the expression, which is what allows us to deal with multi-deterministic g. This actually is the normal case: Theorem 8.3 always produces two semantically equivalent expressions starting with an indexed union ĝ ĝ . . . , which fits the let g = g in in the CuMin equivalence. However, the left-hand side here uses g only once, and within the function pMap sharing is enforced by call-time choice. Thus, for the left-hand side (as well as for both sides of the previous example) the question of sharing is irrelevant and "let g = g in" can be dropped. where pMap is given as before. This time we have to require g to be multi-onto, because the quantification over α is now restricted to data types and thus c can generate values of type α using the anything primitive. For example, the equivalence does not hold for c = (anything α , anything α ) and the strict, multideterministic, but not multi-onto g = h ∪ k of type Nat → Bool, where h x = (x = = x) and k x = (x = = (x + 1)), despite the fact that g anything Nat ≡ anything Bool holds. (Hint: pMap g c Nat lacks the pairs (False, True) and (True, False).) Using this function, we can state the free theorem for functions f :: ∀α. [α] → [α]: For closed types τ 1 and τ 2 , a strict and multideterministic function g :: τ 1 → τ 2 , and a term x :: [τ 1 ], we can show that map g ( f τ 1 x) ≡ f τ 2 (map g x), i.e., the example from the introduction (the interesting bit being what conditions on g do guarantee the validity -and now we do know for sure).

About the proof: In SaLT we define a function mapM :: ∀α. ∀β . (α → {β }) → [α] → {[β ]} that applies a set-valued function to every entry of a list independently and combines the possible results for each entry to overall generate a set of lists. This function is named after the Haskell function mapM and has similar properties, for example mapM ττ { } τ ≡ { } [τ] as can be checked easily. One can also check that map g ≡ g g {mapM g }, which allows to easily translate applications of CuMin map into SaLT. With these insights we can prove the intended CuMin free theorem.

Conclusion

We have shown how to derive free theorems for functional-logic programming languages like Curry. The utility of free theorems for functional languages has been demonstrated by a variety of uses in the past and we hope the results presented here will help to yield functional-logic counterparts. Our results depend on side conditions constraining nondeterminism, and further investigations will have to show how restrictive these conditions actually are. It is plausible to assume that there are other side conditions under which similar free theorems can be shown, e.g., restrictions concerning sharing rather than nondeterminism. While a lot remains to be done, this paper shows that there are results to be found and that they can be proved in a formally rigorous way.

At the same time, this paper introduces a new denotational semantics for a sublanguage of Curry, which can serve as a basis for further research also apart from parametricity and free theorems. It has helped to promote our understanding of Curry with regards to the interaction of laziness, recursion, and the different flavors of nondeterminism, and we hope others will profit as well.

2 |Figure 1 .

 21 Figure 1. Syntax of CuMin

Figure 3 .

 3 Figure 3. Rules for being a data type

Figure 4 .

 4 Figure 4. Some example functions in CuMin (left) and their translations to SaLT (right)

Figure 5 .

 5 Figure 5. Denotational term semantics for CuMin

PFigure 7 .

 7 Figure 7. Additional/replacement typing rules for SaLT

Figure 8 .

 8 Figure 8. Denotational term semantics for SaLT

  ) below. In contrast to what happens in CuMin, in SaLT common manipulations of expressions such as beta-and eta-reduction or inlining of definitions lead to semantically equivalent terms. Beta-and etareduction do not at all change what the semantics functions • i and • compute, because syntactic function applications in SaLT represent actual function application, which is not true for CuMin or full Curry. Inlining of a function definition f = e may change what the semantics functions compute, since f τ m 0 θ ,σ is ⊥ by definition, while e[τ m /α m ] 0 θ ,σ can be a proper value. But the two terms are semantically equivalent according to the general notion:

e 1 x e 2 y e 3 ≡ e 2 y e 1 x e 3

 33

Figure 9 .

 9 Figure 9. Translation from CuMin expressions to SaLT expressions

Lemma 5 . 1 .

 51 Let Γ = α ν m m , x n :: τ n be given, and define Γ = α ν m m , x n :: τ n . 1. If τ is a CuMin type within Γ, then τ is a SaLT type within Γ . 2. If Γ τ ∈ Data holds, then Γ τ ∈ Data holds as well. 3. If Γ e :: τ holds as a CuMin typing judgment w.r.t. some program P, then Γ e :: { τ } holds as a SaLT typing judgment w.r.t. the translation of P. 4. If θ , σ are a type and term environment for the typing context Γ, then θ , σ are also a type and term environment for Γ . 5. τ θ = τ θ 6. e i θ ,σ = e i θ ,σ 7. e θ ,σ = e θ ,σ

  x ) c c (in y ) b case b of (u, v) → {(out u, out v)}

  ∀ * α. (α, α) In CuMin, if c :: ∀ * α. (α, α) is a polymorphic toplevel constant, τ 1 and τ 2 are closed data types, and g :: τ 1 → τ 2 is a strict, multi-deterministic, and multi-onto function, then pMap g c τ 1 ≡ c τ 2

  [α] → [α] In order to deal with lists in CuMin, we need the map function with type map :: ∀α. ∀β . (α → β ) → [α] → [β ] which applies the first argument to every entry in the second argument.

  Cons(e 1 , e 2 ) = e 1x 1 e 2 x 2 {Cons(x 1 , x 2 )} e 1 + e 2 = e 1 x 1 e 2 x 2 {x 1 + x 2 } e 1 = = e 2 = e 1 x 1 e 2 x 2 {x 1 = = x 2 } (e 1 , e 2 ) = e 1 x 1 e 2 x 2 {(x 1 , x 2 )} case e of True → e 1 ;False → e 2 = e b case b of True → e 1 ; False → e 2 case e of Nil → e 1 ; Cons(h,t) → e 2 = e l case l of Nil → e 1 ; Cons(h,t) → e 2 case e of (l, r) → e 1 = e p case p of (l, r) → e 1

	e 1	x	e 2
	e 1 e 2 = e 1	x 1	e 2	x 2 x 1 x 2

  e/in, id τ 2 /out] i Lemma 8.2. Let g : P 1 → P 2 be a function between two posets. If P 2 = x∈P 1 ↓(g x), then G g is whole.Proof. We need to show (P 1 , P 2 ) ∈ P G g . This means finding a nonempty W ⊆ G g such that P 1 = (x,y)∈W ↓x and P 2 = (x,y)∈W ↓y.Choosing W = G g = {(x, g x) | x ∈ P 1 }works just fine. Theorem 8.3. Let τ 1 and τ 2 be closed CuMin types (i.e., types not containing any type variables). Let τ be a closed SaLT type and let α

	θ ,σ

ν , in :: τ 1 → α, out :: α → τ 2 e :: {τ} be a valid SaLT typing judgment. Let g :: τ 1 → τ 2 be a strict and multi-deterministic CuMin term that in the case of * -tagged α is also multi-onto, and let ĝ :: { τ 1 → τ 2 } be a witness for g being multi-deterministic and possibly multi-onto. Then the following SaLT equivalence holds:

That polymorphic type means that f can operate only on the structure of its argument, not on the elements therein. That restricts what it can do, thus giving rise to the above equation. This would fail for a function not so polymorphic, for example a function of type [Int] → [Int] squaring all input list numbers.

A notable exception is local recursion à la letrec. See also the next footnote further below.

* -tags). We will also take some liberties one would have in Curry, even when actually writing CuMin code: We sometimes omit type instantiations if they can be derived easily, and allow user defined infix operators, which can be translated into proper syntax easily. Γ, x :: τ x :: τ Γ True :: Bool Γ False :: Bool Γ n :: Nat Γ Nil τ :: [τ] Γ e 1 :: τ 1 → τ 2 Γ e 2 :: τ 1 Γ e 1 e 2 :: τ 2 Γ e 1 :: τ 1 Γ, x :: τ 1 e 2 :: τ Γ let x = e 1 in e 2 :: τ( f :: ∀ ν 1 α 1 . • • • ∀ ν m α m . τ; f x n = e) ∈ P Γ f τ m :: τ[τ m /α m ]if for all i with ν i = * we have Γ τ i ∈ Data Γ e 1 :: Nat Γ e 2 :: Nat Γ e 1 + e 2 :: Nat Γ e 1 :: Nat Γ e 2 :: Nat Γ e 1 = = e 2 :: Bool Γ e 1 :: τ 1 Γ e 2 :: τ 2 Γ (e 1 , e 2 ) :: (τ 1 , τ 2 ) Γ e 1 :: τ Γ e 2 :: [τ] Γ Cons(e 1 , e 2 ) :: [τ] Γ e :: [τ ] Γ e 1 :: τ Γ, h :: τ ,t :: [τ ] e 2 :: τ Γ case e of Nil → e 1 ; Cons(h,t) → e 2 :: τ Γ e :: (τ 1 , τ 2 ) Γ, l :: τ 1 , r :: τ 2 e 1 :: τ Γ case e of (l, r) → e 1 :: τ Γ e :: Bool Γ e 1 :: τ Γ e 2 :: τ Γ case e of True → e 1 ; False → e 2 :: τ Γ failure τ :: τ Γ τ ∈ Data Γ anything τ :: τ Figure 2. Typing rules for CuMin Γ, α * α ∈ Data Γ Bool ∈ Data Γ Nat ∈ Data

The general idea here is to replace f x = e, where e contains f , by gen r x = e , where e is e with f replaced by r, and f x = let n = anything Nat in foldn gen failure n x.

τ ::= α | Bool | Nat | [τ] | (τ, τ ) | τ → τ | {τ} e ::= x | λ x :: τ. e | f τ m | e 1 e 2 | n | e 1 + e 2 | e 1 = = e 2 | (e 1 , e 2 ) | case e of (x, y) → e 1 | True | False | case e of True → e 1 ; False → e 2 | Nil τ | Cons(e 1 , e 2 ) | case e of Nil → e 1 ; Cons(x, y) → e 2 | {e} | e 1 x e 2 | failure τ | anything τ Figure 6. Syntax of SaLT Γ, x :: τ 1 e :: τ 2 Γ λ x :: τ 1 . e :: τ 1 → τ 2 Γ τ ∈ Data Γ anything τ :: {τ} Γ e 1 :: τ

Sets are a monad that cannot be escaped.

The expression e 1 is written on the left in our notation in order to avoid nested indices and parentheses.

cf. Lemma 7.1 below, which would be wrong otherwise: ↓x can contain elements a that need not be related to any b ∈ ↓y, even when x and y are related.

Proof. The claim concerning e θ 1 ,σ 1 and e θ 2 ,σ 2 follows directly from applying Lemma 7.2 to the claim concerning e i θ 1 ,σ 1 and e i θ 2 ,σ 2 . We show the latter claim by two nested layers of induction. The outer layer is induction on i and the inner layer is induction on the structure of the expression e. We split cases according to the syntax, and for every syntactic construct we assume the claim to be true for all subexpressions, thus making use of the inner layer induction hypothesis.Most of the syntax is already present in standard deterministic lambda-calculi and the proof for these cases can be found in the literature. Here the case of function application shall serve as an example of how individual cases are done. The typing rule is

Acknowledgments

We thank all the reviewers involved in the development of this paper for their criticism and advice.

The first and second author were supported by the DFG under grant VO 1512/1-2.