Inductive and Functional Types in Ludics
Alice Pavaux
cs.LO


Notes on the Kitaev ⇔ Tight-binding correspondence

extracted from a BSc project in Physics presented at Universidade de Aveiro
    Rui Carlos Andrade Martins
 Departamento de Física, Universidade de Aveiro
    July 14, 2017
===============================================================================================================================




  Ludics is a logical framework in which types/formulas are modelled by sets of terms with the same computational behaviour. This paper investigates the representation of inductive data types and functional types in ludics. We study their structure following a game semantics approach. Inductive types are interpreted as least fixed points, and we prove an internal completeness result giving an explicit construction for such fixed points. The interactive properties of the ludics interpretation of inductive and functional types are then studied. In particular, we identify which higher-order functions types fail to satisfy type safety, and we give a computational explanation.




§ INTRODUCTION




 §.§ Context and Contributions




    Context
  Ludics was introduced by Girard <cit.> as a variant of game semantics with interactive types. Game Semantics has successfully provided fully abstract models for various logical systems and programming languages, among which PCF <cit.>. Although very close to Hyland–Ong (HO) games, ludics reverses the approach: in HO games one defines first the interpretation of a type (an arena) before giving the interpretation for the terms of that type (the strategies), while in ludics the interpretation of terms (the designs) is primitive and the types (the behaviours) are recovered dynamically as well-behaved sets of terms. This approach to types is similar to what exists in realisability <cit.> or geometry of interaction <cit.>.

The motivation for such a framework was to reconstruct logic around the dynamics of proofs. Girard provides a ludics model for (a polarised version of) multiplicative-additive linear logic (MALL); a key role in his interpretation of logical connectives is played by the internal completeness results, which allow for a direct description of the behaviours' content. As most behaviours are not the interpretation of MALL formulas, an interesting question, raised from the beginning of ludics, is whether these remaining behaviours can give a logical counterpart to computational phenomena. In particular, data and functions <cit.>, and also fixed points <cit.> have been studied in the setting of ludics. The present work follows this line of research.

Real life (functional) programs usually deal with data, functions over it, functions over functions, etc. Data types allow one to present information in a structured way. Some data types are defined inductively, for example:
[caption=Example of inductive types in OCaml]
> type nat = Zero | Succ of nat ;;
> type 'a list = Nil | Cons of 'a * 'a list ;;
> type 'a tree = Empty | Node of 'a * ('a tree) list ;;

Upon this basis we can consider functional types, which are either first-order – from data to data – or higher-order – i.e., taking functions as arguments or returning functions as a result. This article aims at interpreting constructively the (potentially inductive) data types and the (potentially higher-order) functional types as behaviours of ludics, so as to study their structural properties. Inductive types are defined as (least) fixed points. As pointed out by Baelde, Doumane and Saurin <cit.>, the fact that ludics puts the most constraints on the formation of terms instead of types, conversely to game semantics, makes it a more natural setting for the interpretation of fixed points than HO games <cit.>.



    Contributions

The main contributions of this article are the following:


  * We prove that internal completeness holds for infinite unions of behaviours satisfying particular conditions (Theorem <ref>), leading to an explicit construction of the least fixed points in ludics (Proposition <ref>).

  * Inductive and functional types are interpreted as behaviours, and we prove that such behaviours are regular (Corollary <ref> and Proposition <ref>). Regularity (that we discuss more in § <ref>) is a property that could be used to characterise the behaviours corresponding to μMALL formulas <cit.> – i.e., MALL with fixed points.

  * We show that a functional behaviour fails to satisfy purity, a property ensuring the safety of all possible executions (further explained in § <ref>), if and only if it is higher order and takes functions as argument (Proposition <ref>); this is typically the case of ( A ⊸ B) ⊸ C. In § <ref> we discuss the computational meaning of this result.

The present work is conducted in the term-calculus reformulation of ludics by Terui <cit.> restricted to the linear part – the idea is that programs call each argument at most once.



    Related Work

 The starting point for our study of inductive types as fixed points in ludics is the work by Baelde, Doumane and Saurin <cit.>. In their article, they provide a ludics model for μMALL, a variant of multiplicative-additive linear logic with least and greatest fixed points. The existence of fixed points in ludics is ensured by Knaster-Tarski theorem, but this approach does not provide an explicit way to construct the fixed points; we will consider Kleene fixed point theorem instead. Let us also mention the work of Melliès and Vouillon <cit.> which introduces a realisability model for recursive (i.e., inductive and coinductive) polymorphic types.

 The representation of both data and functions in ludics has been studied previously. Terui <cit.> proposes to encode them as designs in order to express computability properties in ludics, but data and functions are not considered at the level of behaviours. Sironi <cit.> describes the behaviours corresponding to some data types: integers, lists, records, etc. as well as first-order function types; our approach generalises hers by considering generic data types and also higher order functions types.

 

 §.§ Background
 



    Behaviours and Internal Completeness
 A behaviour B is a set of designs which pass the same set of tests B^⊥, where tests are also designs. B^⊥ is called the orthogonal of B, and behaviours are closed under bi-orthogonal: B^⊥⊥ =  B. New behaviours can be formed upon others using various constructors. In this process, internal completeness, which can be seen as a built-in notion of observational equivalence, ensures that two agents reacting the same way to any test are actually equal. From a technical point of view, this means that it is not necessary to apply a ⊥⊥-closure for the sets constructed to be behaviours.



    Paths: Ludics as Game Semantics
 This paper makes the most of the resemblance between ludics and HO game semantics. The connections between them have been investigated in many pieces of work <cit.> where designs are described as (innocent) strategies, i.e., in terms of the traces of their possible interactions. Following this idea, Fouqueré and Quatrini define paths <cit.>, corresponding to legal plays in HO games, and they characterise a behaviour by its set of visitable paths. This is the approach we follow. The definitions of regularity and purity rely on paths, since they are properties of the possible interactions of a behaviour.



    Regularity: Towards a Characterisation of μMALL?
 Our proof that internal completeness holds for an infinite union of increasingly large behaviours (Theorem <ref>) relies in particular on the additional hypothesis of regularity for these behaviours. Intuitively, a behaviour B is regular if every path in a design of B is realised by interacting with a design of B^⊥, and vice versa. This property is not actually ad hoc: it was introduced by Fouqueré and Quatrini <cit.> to characterise the denotations of MALL formulas as being precisely the regular behaviours satisfying an additional finiteness condition. In this direction, our intuition is that – forgetting about finiteness – regularity captures the behaviours corresponding to formulas of μMALL. Although such a characterisation is not yet achieved, we provide a first step by showing that the data patterns, a subset of positive μMALL formulas, yield only regular behaviours (Proposition <ref>).



    Purity: Type Safety
 Ludics has a special feature for termination which is not present in game semantics: the daimon . On a computational point of view, the daimon is commonly interpreted as an error, an exception raised at run-time causing the program to stop (see for example the notes of Curien <cit.>). Thinking of Ludics as a programming language, we would like to guarantee type safety, that is, ensure that “well typed programs cannot go wrong” <cit.>. This is the purpose of purity, a property of behaviours: in a pure behaviour, maximal interaction traces are -free, in other words whenever the interaction stops with  it is actually possible to “ask for more” and continue the computation. Introduced by Sironi <cit.> (and called principality in her work), this property is related to the notions of winning designs <cit.> and pure designs <cit.>, but at the level of a behaviour. As expected, data types are pure (Corollary <ref>), but not always functional types are; we identify the precise cases where impurity arises (Proposition <ref>), and explain why some types are not safe.



 §.§ Outline


In Section <ref> we present ludics and we state internal completeness for the logical connectives constructions.
In Section <ref> we recall the notion of path, so as to define formally regularity and purity and prove their stability under the connectives.
Section <ref> studies inductive data types, which we interpret as behaviours; Kleene theorem and internal completeness for infinite union allows us to give an explicit and direct construction for the least fixed point, with no need for bi-orthogonal closure; we deduce that data types are regular and pure.
Finally, in Section <ref>, we study functional types, showing in what case purity fails.





§ COMPUTATIONAL LUDICS
 

This section introduces the ludics background necessary for the rest of the paper, in the formalism of Terui <cit.>. The designs are the primary objects of ludics, corresponding to (polarised) proofs or programs in a Curry-Howard perspective. Cuts between designs can occur, and their reduction is called interaction. The behaviours, corresponding to the types or formulas of ludics, are then defined thanks to interaction. Compound behaviours can be formed with logical connectives constructions which satisfy internal completeness.



 §.§ Designs and Interaction
 

Suppose given a set of variables 𝒱_0 and a set 𝒮, called signature, equipped with an arity function ar: 𝒮→ℕ. Elements a, b, …∈𝒮 are called names. A positive action is either  (daimon), Ω (divergence), or a with a ∈𝒮; a negative action is a(x_1, …, x_n) where a ∈𝒮, ar(a)=n and x_1, …, x_n ∈𝒱_0 distinct. An action is proper if it is neither  nor Ω.

  Positive and negative designs[In the following, the symbols d,  e, … refer to designs of any polarity, while p,  q, … and m,  n, … are specifically for positive and negative designs respectively.] are coinductively defined by:
    
    p  ::= Ωxa n_1 n_ar(a) n_0a n_1 n_ar(a)
        n  ::= ax^a_1x^a_ar(a) p_a



Positive designs play the same role as applications in λ-calculus, and negative designs the role of abstractions, where each name a ∈𝒮 binds ar(a) variables.

Designs are considered up to α-equivalence. We will often write a( x) (resp. a⟨ n⟩) instead of a(x_1, …, x_n) (resp. a⟨ n_1 … n_n ⟩). Negative designs can be written as partial sums, for example a(x, y). p + b(). q instead of a(x, y). p + b(). q + ∑_c ≠ a, c ≠ b c(z^c).Ω.

  Given a design d, the definitions of the free variables of d, written fv( d), and the (capture-free) substitution of x by a negative design n in d, written d[ n/x], can easily be inferred. The design d is closed if it is positive and it has no free variable. A subdesign of d is a subterm of d. A cut in d is a subdesign of d of the form n_0a n, and a design is cut-free if it has no cut.

In the following, we distinguish a particular variable x_0, that cannot be bound. A positive design p is atomic if fv( p) ⊆{x_0}; a negative design n is atomic if fv( n) = ∅.

A design is linear if for every subdesign of the form xa n (resp. n_0a n), the sets {x}, fv( n_1), …, fv( n_ar(a)) (resp. the sets fv( n_0), fv( n_1), …, fv( n_ar(a))) are pairwise disjoint. This article focuses on linearity, so in the following when writing “design” we mean “linear design”.


  The interaction corresponds to reduction steps applied on cuts:
  
    ∑_a ∈𝒮 a(x^a_1, …, x^a_ar(a)). p_a | b⟨ n_1, …,  n_k⟩ p_b[ n_1/x^b_1, …,  n_k/x^b_k]


We will later describe an interaction as a sequence of actions, a path (Definition <ref>).

Let p be a design, and let ^* denote the reflexive transitive closure of ; if there exists a design q which is neither a cut nor Ω and such that p ^*  q, we write p ⇓ q; otherwise we write p ⇑. The normal form of a design, defined below, exists and is unique <cit.>.

 The normal form of a design d, noted d, is defined by:

    p =  p ⇓       p = xa n_1 n_n p ⇓xa n_1 n_n
        p = Ω p ⇑      ax^a p_a = ax^a p_a


Note that the normal form of a closed design is either  (convergence) or Ω (divergence). Orthogonality expresses the convergence of the interaction between two atomic designs, and behaviours are sets of designs closed by bi-orthogonal.


Two atomic designs p and n are orthogonal, noted p ⊥ n, if p[ n/x_0] =.

Given an atomic design d, define d^⊥ =  e d ⊥ e; if E is a set of atomic designs of same polarity, define E^⊥ =  d∀ e ∈ E,  d ⊥ e.

    
  A set B of atomic designs of same polarity is a behaviour[Symbols A,  B, … will designate behaviours of any polarity, while M,  N … and P,  Q, … will be for negative and positive behaviours respectively.] if B^⊥⊥ =  B. A behaviour is either positive or negative depending on the polarity of its designs.

Behaviours could alternatively be defined as the orthogonal of a set E of atomic designs of same polarity – E corresponds to a set of tests or trials. Indeed, E^⊥ is always a behaviour, and every behaviour B is of this form by taking E =  B^⊥.

The incarnation of a behaviour B contains the cut-free designs of B whose actions are all visited during an interaction with a design in B^⊥. Those correspond to the cut-free designs that are minimal for the stable ordering ⊑, where d' ⊑ d if d can be obtained from d' by substituting positive subdesigns for some occurrences of Ω.

  Let B be a behaviour and d ∈ B cut-free.
  
  
  * The incarnation of d in B, written | d|_ B, is the smallest (for ⊑) cut-free design d' such that d' ⊑ d and d' ∈ B. If | d|_ B =  d we say that d is incarnated in B.
  
  * The incarnation | B| of B is the set of the (cut-free) incarnated designs of B.
  




 §.§ Logical Connectives
  

Behaviour constructors – the logical connectives – can be applied so as to form compound behaviours. These connectives, coming from (polarised) linear logic, are used for interpreting formulas as behaviours, and will also indeed play the role of type constructors for the types of data and functions. In this subsection, after defining the connectives we consider, we state the internal completeness theorem for these connectives.

Let us introduce some notations. In the rest of this article, suppose the signature 𝒮 contains distinct unary names , _1, _2 and a binary name , and write = , _1 = _1, _2 = _2 and =. Given a behaviour B and x fresh, define B^x =  d[x/x_0] d ∈ B; such a substitution operates a “delocation” with no repercussion on the behaviour's inherent properties. Given a k-ary name a ∈𝒮, we write a⟨ N_1, …,  N_k ⟩ or even a⟨ N⟩ for x_0a n n_i ∈ N_i, and write a( x). P for a( x). p p ∈ P. For a negative design n = ax^a p_a and a name a ∈𝒮, we denote by na the design a(x^a). p_a (that is a(x^a). p_a + ∑_b ≠ a b(x^b).Ω).


  
    N = ⟨ N ⟩^⊥⊥      
        P = ((x). P^x)^⊥⊥      
        M ⊕ N = (_1 ⟨ M ⟩∪_2 ⟨ N ⟩)^⊥⊥      
        M ⊗ N = ⟨ M,  N ⟩^⊥⊥      
        N ⊸ P = ( N ⊗ P^⊥)^⊥



Our connectives , , ⊕ and ⊗ match exactly those defined by Terui <cit.>, who also proves the following internal completeness theorem stating that connectives apply on behaviours in a constructive way – there is no need to close by bi-orthogonal. For each connective, we present two versions of internal completeness: one concerned with the full behaviour, the other with the behaviour's incarnation.


  
    N = ⟨ N ⟩∪{}       | N| = ⟨ | N| ⟩∪{}
        P =  n n∈(x). P^x       | P| = (x).| P^x| 
        M ⊕ N = _1 ⟨ M ⟩∪_2 ⟨ N ⟩∪{}       | M ⊕ N| = _1 ⟨ | M| ⟩∪_2 ⟨ | N| ⟩∪{}
        M ⊗ N = ⟨ M,  N ⟩∪{}       | M ⊗ N| = ⟨ | M|, | N| ⟩∪{}





§ PATHS AND INTERACTIVE PROPERTIES OF BEHAVIOURS
 

Paths are sequences of actions recording the trace of a possible interaction. For a behaviour B, we can consider the set of its visitable paths by gathering all the paths corresponding to an interaction between a design of B and a design of B^⊥. This notion is needed for defining regularity and purity and proving that those two properties of behaviours are stable under (some) connectives constructions.



 §.§ Paths
 

This subsection adapts the definitions of path and visitable path from <cit.> to the setting of computational ludics. In order to do so, we need first to recover location in actions so as to consider sequences of actions.

Location is a primitive idea in Girard's ludics <cit.> in which the places of a design are identified with loci or addresses, but this concept is not visible in Terui's presentation of designs-as-terms. We overcome this by introducing actions with more information on location, which we call located actions, and which are necessary to:


  * represent cut-free designs as trees – actually, forests – in a satisfactory way,

  * define views and paths.


 
  A located action[Located actions will often be denoted by symbol κ, sometimes with its polarity: κ^+ or κ^-.] κ is one of: xax_1x_ar(a) a_x(x_1, …, x_ar(a)) 

where in the last two cases (positive proper and negative proper respectively), a ∈𝒮 is the name of κ, the variables x, x_1, …, x_ar(a) are distinct, x is the address of κ and x_1, …, x_ar(a) are the variables bound by κ.

In the following, “action” will always refer to a located action. Similarly to notations for designs, xa x stands for xax_1x_n and a_x( x) for a_x(x_1, …, x_n).

 
  We show how cut-free designs can be represented as trees of located actions in this example. Let a^2, b^2, c^1, d^0 ∈𝒮, where exponents stand for arities. The following design is represented by the tree of Fig. <ref>.
  
    d = a(x_1,x_2).(x_2ba(x_3, x_4). + c(y_1).(y_1d), c(y_2).(x_1d))


  
Such a representation is in general a forest: a negative design ax^a p_a gives as many trees as there is a ∈𝒮 such that p_a ≠Ω. The distinguished variable x_0 is given as address to every negative root of a tree, and fresh variables are picked as addresses for negative actions bound by positive ones. This way, negative actions from the same subdesign, i.e., part of the same sum, are given the same address. A tree is indeed to be read bottom-up: a proper action κ is justified if its address is bound by an action of opposite polarity appearing below κ in the tree; otherwise κ is called initial. Except the root of a tree, which is always initial, every negative action is justified by the only positive action immediately below it. If κ and κ' are proper, κ is hereditarily justified by κ' if there exist actions κ_1, …, κ_n such that κ = κ_1, κ' = κ_n and for all i such that 1 ≤ i < n, κ_i is justified by κ_i+1.

Before giving the definitions of view and path, let us give an intuition. On Fig. <ref> are represented a view and a path of design d. Views are branches in the tree representing a cut-free design (reading bottom-up), while paths are particular “promenades” starting from the root of the tree; not all such promenades are paths, though. Views correspond to chronicles in original ludics <cit.>.

For every positive proper action κ^+ = xay define κ^+ = a_x(y), and similarly if κ^- = a_x(y) define κ^- = xay. Given a finite sequence of proper actions s = κ_1 …κ_n, define s = κ_1…κ_n. Suppose now that if s contains an occurrence of , it is necessarily in last position; the dual of s, written s, is the sequence defined by:
  
  
  * s =  s if s does not end with ,
  
  * s =  s' if s =  s'.
  
Note that s =  s. The notions of justified, hereditarily justified and initial actions also apply in sequences of actions.
  An alternated justified sequence (or aj-sequence) s is a finite sequence of actions such that:
  
  
  * (Alternation) Polarities of actions alternate.
  
  * (Daimon) If  appears, it is the last action of s.
  
  * (Linearity) Each variable is the address of at most one action in s.
  

The (unique) justification of a justified action κ in an aj-sequence is noted just(κ), when there is no ambiguity on the sequence we consider.


A view v is an aj-sequence such that each negative action which is not the first action of v is justified by the immediate previous action. Given a cut-free design d, v is a view of d if it is a branch in the representation of d as a tree (modulo α-equivalence).

The way to extract the view of an aj-sequence is given inductively by:
  
    
  * ϵ = ϵ, where ϵ is the empty sequence,
    
  * sκ^+ =  sκ^+,
    
  * sκ^- =  s_0κ^- where s_0 is the prefix of s ending on just(κ^-), or s_0 = ϵ if κ^- initial.
  
The anti-view of an aj-sequence, noted s, is defined symmetrically by reversing the role played by polarities; equivalently s =  s.

 
  A path s is a positive-ended aj-sequence satisfying:
  
  
  * (P-visibility) For all prefix s' κ^+ of s, just(κ^+) ∈ s'
  
  * (O-visibility) For all prefix s' κ^- of s, just(κ^-) ∈ s'
  
  Given a cut-free design d, a path s is a path of d if for all prefix s' of s, s' is a view of d.

Remark that the dual of a path is a path.

Paths are aimed at describing an interaction between designs. If d and e are cut-free atomic designs such that d ⊥ e, there exists a unique path s of d such that s is a path of e. We write this path d e, and the good intuition is that it corresponds to the sequence of actions followed by the interaction between d and e on the side of d. An alternative way defining orthogonality is then given by the following proposition.
 
  d ⊥ e if and only if there exists a path s of d such that s is a path of e.


At the level a behaviour B, the set of visitable paths describes all the possible interactions between a design of B and a design of B^⊥.


A path s is visitable in a behaviour B if there exist cut-free designs d ∈ B and e ∈ B^⊥ such that s =  d e. The set of visitable paths of B is written B.

Note that for every behaviour B, B = B^⊥.



 §.§ Regularity, Purity and Connectives
 

The meaning of regularity and purity has been discussed in the introduction. After giving the formal definitions, we prove that regularity is stable under all the connectives constructions. We also show that purity may fail with ⊸, and only a weaker form called quasi-purity is always preserved.


  B is regular if the following conditions are satisfied:
  
  
  * for all d ∈ |B| and all path s of d, s ∈B,
  
  * for all d ∈ |B^⊥| and all path s of d, s ∈B^⊥,
  
  * The sets B and B^⊥ are stable under shuffle.
  
  where the operation of shuffle () on paths corresponds to an interleaving of actions respecting alternation of polarities, and is defined below. 

Let s s' refer to the subsequence of s containing only the actions that occur in s'. Let s and t be paths of same polarity, let S and T be sets of paths of same polarity. We define:


  * s  t =  u  s  t u s =  s  u t =  t if s,  t negative,

  * s  t = κ^+  u  u ∈ s'  t' if s = κ^+  s' and t = κ^+  t' positive with same first action,

  * S  T =  u ∃ s ∈ S, ∃ t ∈ T  s  t  u ∈ s  t,


In fact, a behaviour B is regular if every path formed with actions of the incarnation of B, even mixed up, is a visitable path of B, and similarly for B^⊥. Remark that regularity is a property of both a behaviour and its orthogonal since the definition is symmetrical: B is regular if and only if B^⊥ is regular.


A behaviour B is pure if every -ended path s ∈ B is extensible, i.e., there exists a proper positive action κ^+ such that s κ^+ ∈B.

Purity ensures that when an interaction encounters , this does not correspond to a real error but rather to a partial computation, as it is possible to continue this interaction. Note that daimons are necessarily present in all behaviours since the converse property is always true: if s κ^+ ∈B then s ∈B.

 
Regularity is stable under , , ⊕, ⊗ and ⊸.


 
Purity is stable under , , ⊕ and ⊗.


Unfortunately, when N and P are pure, N ⊸ P is not necessarily pure, even under regularity assumption. However, a weaker form of purity holds for N ⊸ P.


  A behaviour B is quasi-pure if all the -ended well-bracketed paths in V_ B are extensible.

We recall that a path s is well-bracketed if, for every justified action κ in s, when we write s =  s_0 κ'  s_1 κ s_2 where κ' justifies κ, all the actions in s_1 are hereditarily justified by κ'.

 
  If N and P are quasi-pure and regular then N ⊸ P is quasi-pure.




§ INDUCTIVE DATA TYPES
 

Some important contributions are presented in this section. We interpret inductive data types as positive behaviours, and we prove an internal completeness result allowing us to make explicit the structure of fixed points. Regularity and purity of data follows.

Abusively, we denote the positive behaviour {} by  all along this section.



 §.§ Inductive Data Types as Kleene Fixed Points
 

We define the data patterns via a type language and interpret them as behaviours, in particular μ is interpreted as a least fixed point. Data behaviours are the interpretation of steady data patterns.

Suppose given a countably infinite set 𝒱 of second-order variables: X, Y, …∈𝒱. Let 𝒮' = 𝒮∖{, _1, _2, } and define the set of constants Const =  C_aa ∈𝒮' which contains a behaviour C_a = {x_0aΩ^-}^⊥⊥ (where Ω^- := ax^aΩ) for each a ∈𝒮', i.e., such that a is not the name of a connective. Remark that V_ C_a = { , x_0a x}, thus C_a is regular and pure.


The set 𝒫 of data patterns is generated by the inductive grammar:

    A, B ::=  X ∈𝒱 a ∈𝒮'  A ⊕^+ B  A ⊗^+ B μ X. A


The set of free variables of a data pattern A ∈𝒫 is denoted by FV(A).

 
Let b, n, l, t ∈𝒮' and X ∈𝒱. The data types given as example in the introduction can be written in the language of data patterns as follows:

    𝔹ool    = b ⊕^+ b ℕat = μ X.( n ⊕^+ X) 𝕃ist_A = μ X.(l ⊕^+ (A ⊗^+ X)) 
       𝕋ree_A = μ X.(t ⊕^+ (A ⊗^+ 𝕃ist_X)) = μ X.(t ⊕^+ (A ⊗^+ μY.(l ⊕^+ (X ⊗^+ Y))))



Let ℬ^+ be the set of positive behaviours. Given a data pattern A ∈𝒫 and an environment σ, i.e., a function that maps free variables to positive behaviours, the interpretation of A in the environment σ, written A^σ, is the positive behaviour defined by:

    X^σ = σ(X)    A ⊕^+ B^σ    = (A^σ) ⊕ (B^σ) 
       a^σ =  C_a    A ⊗^+ B^σ    = (A^σ) ⊗ (B^σ) 
       μ X. A^σ = lfp(ϕ^A_σ)

where lfp stands for the least fixed point, and the function ϕ^A_σ: ℬ^+ →ℬ^+,  P ↦A^σ, X↦ P is well defined and has a least fixed point by Knaster-Tarski fixed point theorem, as shown by Baelde, Doumane and Saurin <cit.>. Abusively we may write ⊕^+ and ⊗^+, instead of (·) ⊕ (·) and (·) ⊗ (·) respectively, for behaviours. We call an environment σ regular (resp. pure) if its image contains only regular (resp. pure) behaviours. The notation σ, X↦ P stands for the environment σ where the image of X has been changed to P.

In order to understand the structure of fixed point behaviours that interpret the data patterns of the form μ X.A, we need a constructive approach, thus Kleene fixed point theorem is best suited than Knaster-Tarski. We now prove that we can apply this theorem.

Recall the following definitions and theorem. A partial order is a complete partial order (CPO) if each directed subset has a supremum, and there exists a smallest element, written . A function f : E → F between two CPOs is Scott-continuous (or simply continuous) if for every directed subset D ⊆ E we have ⋁_x ∈ D f(x) = f(⋁_x ∈ Dx).


  Let L be a CPO and let f:L → L be Scott-continuous. The function f has a least fixed point, defined by
  
    lfp(f) = ⋁_n ∈ℕf^n()


The set ℬ^+ ordered by ⊆ is a CPO, with least element ; indeed, given a subset ℙ⊆ℬ^+, it is directed and we have ⋁ℙ = (⋃ℙ)^⊥⊥. Hence next proposition proves that we can apply the theorem.

   Given a data pattern A ∈𝒫, a variable X ∈𝒱 and an environment σ : FV(A) ∖{X}→ℬ^+, the function ϕ^A_σ is Scott-continuous.


  For every A ∈𝒫, X ∈𝒱 and σ : FV(A) ∖{X}→ℬ^+,
  
    μ X.A^σ = ⋁_n ∈ℕ (ϕ^A_σ)^n() = (⋃_n ∈ℕ (ϕ^A_σ)^n())^⊥⊥


This result gives an explicit formulation for least fixed points. However, the ⊥⊥-closure might add new designs which were not in the union, making it difficult to know the exact content of such a behaviour. The point of next subsection will be to give an internal completeness result proving that the closure is actually not necessary.

Let us finish this subsection by defining a restricted set of data patterns so as to exclude the degenerate ones. Consider for example 𝕃ist_A' = μ X. (A ⊗^+ X), a variant of 𝕃ist_A (see Example <ref>) which misses the base case. It is degenerate in the sense that the base element, here the empty list, is interpreted as the design . This is problematic: an interaction going through a whole list will end with an error, making it impossible to explore a pair of lists for example. The pattern ℕat' = μ X.X is even worse since ℕat' =. The point of steady data patterns is to ensure the existence of a basis; this will be formalised in Lemma <ref>.


  The set of steady data patterns is the smallest subset 𝒫^s ⊆𝒫 such that:
  
  
  * 𝒮' ⊆𝒫^s
  
  * If A ∈𝒫^s and B is such that B^σ is pure if σ is pure, then A ⊕^+ B∈𝒫^s and B ⊕^+ A ∈𝒫^s
  
  * If A ∈𝒫^s and B∈𝒫^s then A ⊗^+ B ∈𝒫^s
  
  * If A ∈𝒫^s then μ X.A ∈𝒫^s
  


The condition on B in the case of ⊕^+ admits data patterns which are not steady, possibly with free variables, but ensuring the preservation of purity, i.e., type safety; the basis will come from side A. We will prove (§ <ref>) that behaviours interpreting steady data patterns are pure, thus in particular a data pattern of the form μ X.A is steady if the free variables of A all appear on the same side of a ⊕^+ and under the scope of no other μ (since purity is stable under , , ⊕, ⊗). We claim that steady data patterns can represent every type of finite data.

  A data behaviour is the interpretation of a closed steady data pattern.




 §.§ Internal Completeness for Infinite Union


Our main result is an internal completeness theorem, stating that an infinite union of simple regular behaviours with increasingly large incarnations is a behaviour: ⊥⊥-closure is useless.


  
  
  * A slice is a design in which all negative subdesigns are either Ω^- or of the form a( x). p_a, i.e., at most unary branching. c is a slice of d if c is a slice and c ⊑ d. A slice c of d is maximal if for any slice c' of d such that c ⊑ c', we have c =  c'.
  
  * A behaviour B is simple if for every design d ∈ | B|:
    
    
  * d has a finite number of maximal slices, and
    
  * every positive action of d is justified by the immediate previous negative action.
    
  


Condition (2) of simplicity ensures that, given d ∈ | B| and a slice c ⊑ d, one can find a path of c containing all the positive proper actions of c until a given depth; thus by condition (1), there exists k ∈ℕ depending only on d such that k paths can do the same in d.

Now suppose ( A_n)_n ∈ℕ is an infinite sequence of simple regular behaviours such that for all n ∈ℕ, | A_n| ⊆ | A_n+1| (in particular we have A_n ⊆ A_n+1).

 
  The set ⋃_n ∈ℕ A_n is a behaviour.

A union of behaviours is not a behaviour in general. In particular, counterexamples are easily found if releasing either the inclusion of incarnations or the simplicity condition. Moreover, our proof for this theorem relies strongly on regularity. Under the same hypotheses we can prove V_⋃_n ∈ℕ A_n = ⋃_n ∈ℕ V_ A_n and |⋃_n ∈ℕ A_n| = ⋃_n ∈ℕ | A_n|, hence the following corollary.

 
  
  
  * ⋃_n ∈ℕ A_n is simple and regular;
  
  * if moreover all the A_n are pure then ⋃_n ∈ℕ A_n is pure.
  




 §.§ Regularity and Purity of Data
 

The goal of this subsection is to show that the interpretation of data patterns of the form μ X.A can be expressed as an infinite union of behaviours ( A_n)_n ∈ℕ satisfying the hypotheses of Theorem <ref>, in order to deduce regularity and purity. We will call an environment σ simple if its image contains only simple behaviours.

 
For all A ∈𝒫, X ∈𝒱, σ : FV(A) ∖{X}→ℬ^+ simple and regular[The hypothesis “simple and regular” has been added, compared to the CSL version of this article, for correction.], and n ∈ℕ we have

    |(ϕ^A_σ)^n()| ⊆ |(ϕ^A_σ)^n+1()|



  
For all A ∈𝒫 and simple regular environment σ, A^σ is simple regular.



  By induction on data patterns. If A = X or A = a the conclusion is immediate. If A = A_1 ⊕^+ A_2 or A = A_1 ⊗^+ A_2 then regularity comes from Proposition <ref>, and simplicity is easy since the structure of the designs in A^σ is given by internal completeness for the logical connectives (Theorem <ref>). So suppose A = μ X.A_0. By induction hypothesis, for every simple regular behaviour P ∈ℬ^+ we have ϕ^A_0_σ( P) = A_0^σ, X ↦ P simple regular. From this, it is straightforward to show by induction that for every n ∈ℕ, (ϕ^A_0_σ)^n() is simple regular. Moreover, for every n ∈ℕ we have |(ϕ^A_0_σ)^n()| ⊆ |(ϕ^A_0_σ)^n+1()| by Lemma <ref>, thus by Corollary <ref> and Theorem <ref>, μ X.A_0^σ  = ⋁_n ∈ℕ (ϕ^A_σ)^n() = (⋃_n ∈ℕ(ϕ^A_0_σ)^n())^⊥⊥ = ⋃_n ∈ℕ(ϕ^A_0_σ)^n().
Consequently, by Corollary <ref>, μ X.A_0^σ is simple regular.

Remark that we have proved at the same time, using Theorem <ref>, that behaviours interpreting data patterns μ X.A admit an explicit construction:
 
  If A ∈𝒫, X ∈𝒱, and σ : FV(A)∖ X →ℬ^+ is simple regular,
  
    μ X.A^σ = ⋃_n ∈ℕ (ϕ^A_σ)^n()



 
  Data behaviours are regular.


We now move on to proving purity. The proof that the interpretation of a steady data pattern A is pure relies on the existence of a basis for A (Lemma <ref>). Let us first widen (to -free paths) and express in a different way (for -ended paths) the notion of extensible visitable path.

 Let B be a behaviour.
  
  
  * A -free path s ∈ B is extensible if there exists t ∈ B of which s is a strict prefix.
  
  * A -ended path s∈ B is extensible if there exists a positive action κ^+ and t ∈ B of which sκ^+ is a prefix.
  

Write V_ B^max for the set of maximal, i.e., non extensible, visitable paths of B.
  
 
  Every steady data pattern A ∈𝒫^s has a basis, i.e., a simple regular behaviour B such that for all simple regular environment σ we have
  
  
  * B ⊆A^σ,
  
  * for every path s ∈ V_ B, there exists t ∈ V_ B^max -free extending s (in particular B pure),
  
  * V_ B^max⊆ V_A^σ^max.
    



  If A = a, a basis is C_a. If A = A_1 ⊕^+ A_2, and A_i is steady with basis B_i, then ⊗_i  B_i:=_i⟨ B_i⟩ is a basis for A. If A = A_1 ⊗^+ A_2, a basis is B_1 ⊗^+  B_2 where B_1 and B_2 are basis of A_1 and A_2 respectively. If A = μ X.A_0, its basis is the same as A_0.


 
  If A ∈𝒫^s of basis B, X ∈𝒱, and σ : FV(A)∖ X →ℬ^+ simple regular,
  
    μ X.A^σ = ⋃_n ∈ℕ (ϕ^A_σ)^n( B)




  Since B is a basis for A we have ⊆ B ⊆A^σ, X → = ϕ^A_σ(). The Scott-continuity of the function ϕ^A_σ implies that it is increasing, thus (ϕ^A_σ)^n() ⊆ (ϕ^A_σ)^n( B) ⊆ (ϕ^A_σ)^n+1() for all n ∈ℕ.
  Hence A^σ = ⋃_n ∈ℕ(ϕ^A_σ)^n() = ⋃_n ∈ℕ (ϕ^A_σ)^n( B).



   For all A ∈𝒫^s and simple regular pure environment σ, A^σ is pure.



  By induction on A. The base cases are immediate and the connective cases are solved using Proposition <ref>. Suppose now A = μ X.A_0, where A_0 is steady with basis B_0. We have A^σ = ⋃_n ∈ℕ (ϕ^A_0_σ)^n( B_0) by Proposition <ref>, let us prove it satisfies the hypotheses needed to apply Corollary <ref>(2). By induction hypothesis and Proposition <ref>, for every simple, regular and pure behaviour P ∈ℬ^+ we have ϕ^A_0_σ( P) = A_0^σ, X ↦ P simple, regular and pure, hence it is easy to show by induction that for every n ∈ℕ, (ϕ^A_0_σ)^n( B_0) is as well. Moreover, for every n ∈ℕ we prove that |(ϕ^A_0_σ)^n( B_0)| ⊆ |(ϕ^A_0_σ)^n+1( B_0)| similarly to Lemma <ref>, replacing  by the basis B_0. Finally, by Corollary <ref>, A^σ is pure.


 
  Data behaviours are pure.



Although here the focus is on the interpretation of data patterns, we should say a word about the interpretation of (polarised) μMALL formulas, which are a bit more general. These formulas are generated by:
  
    P, Q     ::=  X_P  X_N^⊥ 1  0  M ⊕ N  M ⊗ N  N μ X.P 
    
        M, N     ::=  P^⊥

  where the usual involutive negation hides the negative connectives and constants, through the dualities 1/, 0/⊤, ⊕/, ⊗/, /, μ/ν . The interpretation as ludics behaviours, given in <cit.>, is as follows: 1 is interpreted as a constant behaviour C_a, 0 is the daimon , the positive connectives match their ludics counterparts, μ is interpreted as the least fixed point of a function ϕ^A_σ similarly to data patterns, and the negation corresponds to the orthogonal. Since in ludics constants and  are regular, and since regularity is preserved by the connectives (Proposition <ref>) and by orthogonality, the only thing we need in order to prove that all the behaviours interpreting μMALL formulas are regular is a generalisation of regularity stability under fixed points (for now we only have it in our particular case: Corollary <ref> together with Proposition <ref>).
  
Note however that interpretations of μMALL formulas are not all pure. Indeed, as we will see in next section, orthogonality (introduced through the connective ⊸) does not preserve purity in general.





§ FUNCTIONAL TYPES
 

In this section we define functional behaviours which combine data behaviours with the connective ⊸. A behaviour of the form N ⊸ P is the set of designs such that, when interacting with a design of type N, outputs a design of type P; this is exactly the meaning of its definition N ⊸ P :=  ( N ⊗ P^⊥)^⊥.
  We prove that some particular higher-order functional types – where functions are taken as arguments, typically (A ⊸ B) ⊸ C – are exactly those who fail at being pure, and we interpret this result from a computational point of view.



 §.§ Where Impurity Arises
 

We have proved that data behaviours are regular and pure. However, if we introduce functional behaviours with the connective ⊸, purity does not hold in general. Proposition <ref> indicates that a weaker property, quasi-purity, holds for functional types, and Proposition <ref> identifies exactly the cases where purity fails.

Let us write 𝒟 for the set of data behaviours.


A functional behaviour is a behaviour inductively generated by the grammar below, where P ⊸^+  Q stands for (( P) ⊸ Q).
 
    P,  Q ::=  P_0 ∈𝒟 P ⊕^+  Q  P ⊗^+  Q  P ⊸^+  Q


 
From Propositions <ref>, <ref> and <ref> we easily deduce the following result.
 
  Functional behaviours are regular and quasi-pure.


For next proposition, consider contexts defined inductively as follows (where P is a functional behaviour):

    𝒞 ::= [ ] 𝒞⊕^+  P  P ⊕^+ 𝒞𝒞⊗^+  P  P ⊗^+ 𝒞 P ⊸^+ 𝒞


 
  A functional behaviour P is impure if and only if there exist contexts 𝒞_1, 𝒞_2 and functional behaviours Q_1,  Q_2,  R with R ∉Const such that
  
    P = 𝒞_1[ 𝒞_2[ Q_1 ⊸^+  Q_2] ⊸^+  R ]





 §.§ Example and Discussion
 

Proposition <ref> states that a functional behaviour which takes functions as argument is not pure: some of its visitable paths end with a daimon , and there is no possibility to extend them. In terms of proof-search, playing the daimon is like giving up; on a computational point of view, the daimon appearing at the end of an interaction expresses the sudden interruption of the computation. In order to understand why such an interruption can occur in the specific case of higher-order functions, consider the following example which illustrates the proposition.

   
  Let Q_1,  Q_2,  1 be functional behaviours, with 1 ∈Const. Define Bool =  1 ⊕^+  1 and consider the behaviour P = ( Q_1 ⊸^+  Q_2) ⊸^+ Bool: this is a type of functions which take a function as argument and output a boolean. Let α_1, α_2, β be respectively the first positive action of the designs of Q_1,  Q_2,  1. It is possible to exhibit a design p ∈ P and a design n ∈ P^⊥ such that the visitable path s =  p n is -ended and maximal in P, in other words s is a witness of the impurity of P. The path s contains the actions α_1 and α_2 in such a way that it cannot be extended with β without breaking the P-visibility condition, and there is no other available action in designs of P to extend it. Reproducing the designs p and n and the path s here would be of little interest since those objects are too large to be easily readable (s visits the entire design p, which contains 11 actions). We however give an intuition in the style of game semantics: Fig. <ref> represents s as a legal play in a strategy of type P = ( Q_1 ⊸^+  Q_2) ⊸^+ Bool (note that only one “side” ⊕_1  1 of Bool is represented, corresponding for example to , because we cannot play in both sides). This analogy is informal, it should stand as an intuition rather than as a precise correspondence with ludics; for instance, and contrary to the way it is presented in game semantics, the questions are asked on the connectives, while the answers are given in the sub-types of P. On the right are given the actions in s corresponding to the moves played. The important thing to remark is the following: if a move b corresponding to action β were played instead of  at the end of this play, it would break the P-visibility of the strategy, since this move would be justified by move q_.


  
The computational interpretation of the -ended interaction between p and n is the following: a program p of type P launches a child process p' to compute the argument of type Q_1 → Q_2, but p starts to give a result in Bool before the execution of p' terminates, leading to a situation where p cannot compute the whole data in Bool. The interaction outputs , i.e., the answer given in Bool by p is incomplete.

Moreover by Proposition <ref> functional behaviours are quasi-pure, therefore the maximal -ended visitable paths are necessarily not well-bracketed. This is indeed the case of s: remark for example that the move q_⊕_1 appears between a_1 and its justification q_ in the sequence, but q_⊕_1 is not hereditarily justified by q_.
In HO games, well-bracketedness is a well studied notion, and relaxing it introduces control operators in program. If we extend such an argument to ludics, this would mean that the appearance of  in the execution of higher-order functions can only happen in the case of programs with control operators such as jumps, i.e. programs which are not purely functional.




§ CONCLUSION


This article is a contribution to the exploration of the behaviours of linear ludics in a computational perspective. Our focus is on the behaviours representing data types and functional types. Inductive data types are interpreted using the logical connectives constructions and a least fixed point operation. Adopting a constructive approach, we provide an internal completeness result for fixed points, which unveils the structure of data behaviours. This leads us to proving that such behaviours are regular – the key notion for the characterisation of MALL in ludics –  and pure – that is, type safe.
But behaviours interpreting types of functions taking functions as argument are impure; for well-bracketed interactions, corresponding to the evaluation of purely functional programs, safety is however guaranteed.



    Further Work
 Two directions for future research arise naturally:


  * Extending our study to greatest fixed points ν X.A, i.e., coinduction, is the next objective. Knaster–Tarski ensures that such greatest fixed point behaviours exist <cit.>, but Kleene fixed point theorem does not apply here, hence we cannot find an explicit form for coinductive behaviours the same way we did for the inductive ones. However it is intuitively clear that, compared to least fixed points, greatest ones add the infinite “limit” designs in (the incarnation of) behaviours. For example, if ℕat_ω = ν X. (1 ⊕ X) then we should have |ℕat_ω| = |ℕat| ∪{ d_ω} where d_ω = succ( d_ω) = x_0|_2⟨(x). d_ω^x⟩.

  * Another direction would be to get a complete characterisation of μMALL in ludics, by proving that a behaviour is regular – and possibly satisfying a supplementary condition – if and only if it is the denotation of a μMALL formula.




    Acknowledgement
 I thank Claudia Faggian, Christophe Fouqueré, Thomas Seiller and the anonymous referees for their wise and helpful comments.

plainurl




