8 Pages
English
Gain access to the library to view online
Learn more

A Non Uniform Finitary Relational Semantics of System T Lionel Vaux

-

Gain access to the library to view online
Learn more
8 Pages
English

Description

Niveau: Supérieur, Doctorat, Bac+8
A Non-Uniform Finitary Relational Semantics of System T Lionel Vaux? Laboratoire de Mathématiques de l'Université de Savoie UFR SFA, Campus Scientifique, 73376 Le Bourget-du-Lac Cedex, FRANCE August 11, 2009 Abstract We study iteration and recursion operators in the denotational semantics of typed ? -calculi de- rived from the multiset relational model of linear logic. Although these operators are defined as fixpoints of typed functionals, we prove them finitary in the sense of Ehrhard's finiteness spaces. 1 Introduction Finiteness spaces were introduced by Ehrhard [1], refining the purely relational model of linear logic. A finiteness space is a set equipped with a finiteness structure, i.e. a particular set of subsets which are said to be finitary; and the model is such that the relational denotation of a proof in linear logic is always a finitary subset of its conclusion. By the usual co-Kleisli construction, this also provides a model of the simply typed ? -calculus: the cartesian closed category Fin. The main property of finiteness spaces is that the intersection of two finitary subsets of dual types is always finite. This feature allows to reformulate Girard's quantitative semantics [2] in a standard algebraic setting, where morphisms interpreting typed ? -terms are analytic functions between the topological vector spaces generated by vectors with finitary supports.

  • standard encoding

  • finiteness spaces

  • suitable ?

  • typed ? -calculi

  • holds only

  • following additional

  • constant function


Subjects

Informations

Published by
Reads 27
Language English

Exrait

A Non-Uniform Finitary Relational Semantics of System T
Lionel Vaux
Laboratoire de Mathématiques de l’Université de Savoie
UFR SFA, Campus Scientifique, 73376 Le Bourget-du-Lac Cedex, FRANCE
August 11, 2009
Abstract
We study iteration and recursion operators in the denotational semantics of typed l-calculi de-
rived from the multiset relational model of linear logic. Although these operators are defined as
fixpoints of typed functionals, we prove them finitary in the sense of Ehrhard’s finiteness spaces.
1 Introduction
Finiteness spaces were introduced by Ehrhard [1], refining the purely relational model of linear logic. A
finiteness space is a set equipped with a finiteness structure, i.e. a particular set of subsets which are said
to be finitary; and the model is such that the relational denotation of a proof in linear logic is always a
finitary subset of its conclusion. By the usual co-Kleisli construction, this also provides a model of the
simply typedl-calculus: the cartesian closed category Fin. The main property of finiteness spaces is that
the intersection of two finitary subsets of dual types is always finite. This feature allows to reformulate
Girard’s quantitative semantics [2] in a standard algebraic setting, where morphisms interpreting typed
l-terms are analytic functions between the topological vector spaces generated by vectors with finitary
supports. This provided the semantical foundations of Ehrhard-Regnier’s differentiall-calculus [3] and
motivated the general study of a differential extension of linear logic (e.g., [4, 5, 6, 7, 8, 9, 10]).
It is worth noticing that finiteness spaces can accomodate typed l-calculi only. In particular, the
relational semantics of fixpoint combinators is never finitary. The whole point of the finiteness construc-
tion is actually to reject infinite computations, ensuring the intermediate sets involved in the relational
interpretation of a cut are all finite. Despite this restrictive design, Ehrhard proved that a limited form of
recursion was available, by defining a finitary tail-recursive iteration operator.
The main result of the present paper is that finiteness spaces can actually accomodate the standard
notion of primitive recursion in l-calculus, Gödel’s system T : we prove Fin admits a weak natural
number object in the sense of [11, 12], and we more generally exhibit a finitary recursion operator for
this interpretation of the type of natural numbers. This achievement is twofold:
Before considering finiteness, we must define a recursion operator in the cartesian closed category
deduced from the relational model of linear logic. For that purpose, we cannot follow Ehrhard and
use the flat interpretation of the type Nat of natural numbers. Indeed, if t, u and v are terms of
types respectively Nat, Nat) X) X and X, the recursion step R(St)uv; ut(Rt uv) puts t in
argument position. In case u is a constant function, t is not used in the reduced form. The recursor
R must however discriminate between St and O, hence the successor S cannot be linear: it must
produce information independently from its input. Though it might be obscure for the reader not
familiar with the relational or coherence semantics, this argument will be made formal in the paper.
This was already noted by Girard in coherence spaces [13]: we adopt the solution he proposed,
and interpret terms of typeNat by so-called lazy natural numbers. An notable outcome is that our
This work has been partially funded by the French ANR projet blanc “Curry Howard pour la Concurrence” CHOCO
ANR-07-BLAN-0324.
1
savoie.frlionel.vaux@univ-A Non-Uniform Finitary Relational Semantics of System T Lionel Vaux
interpretation provides a semantic evidence of the well-known gap in expressive power between
the iterator and recursor variants of system T .
The second aspect of our work is to establish that this relational semantics is finitary. This is far
from immediate because the recursion operator is defined as the fixpoint of finitary approximants:
since fixpoints themselves are not finitary relations, it is necessary to obtain stronger properties of
these approximants to conclude.
Structure of the paper. In section 2, we briefly describe two cartesian closed categories: the category
Rel of sets and relations from multisets to points, and the category Fin of finiteness spaces and finitary
relations from multisets to points. In section 3, we give an explicit presentation of the relational semantics
of typedl-calculi in Rel and Fin, which we extend to system T in section 4. In section 5, we establish a
uniformity property of iteration-definable morphisms, which does not hold for recursion in general.
2 Sets, Relations and Finiteness Spaces
!If A is a set, denote byP(A) the powerset of A, byP (A) the set of all finite subsets of A and by Af
nthe set of all finite multisets of A. If(a ;:::;a )2 A , we write a =[a ;:::;a ] for the corresponding1 n 1 n
multiset, and denote multiset union additively. Let f A B be a relation from A to B, we write
?f =f(b;a); (a;b)2 fg. For all a A, we set f a=fb2 B;9a2 a; (a;b)2 fg. We write Rel for
!the coKleisli category of the comonad( ) in the relational model of linear logic (see e.g. [14]): objects
!are sets and Rel(A;B)=P A B ; the identity on A is id =f([a];a); a2 Ag; if f2 Rel(A;B) andAn o
n !g2 Rel(B;C) then g f = ( a ;g);9b =[b ;:::;b ]2 B ; (b;g)2 g^8i(a ;b)2 f .? i 1 n i ii=1
The category Rel is cartesian closed. The cartesian product is given by the disjoint union of sets A]
B=(f1gA)[(f2gB), with terminal object the empty set 0./ Projections aref([(1;a)];a); a2 Ag2
Rel(A] B;A) andf([(2;b)];b); b2 Bg2 Rel(A] B;B). If f2 Rel(C;A) and g2 Rel(C;B), pairing
is given by: h f;gi=f(g;(1;a)); (g;a)2 fg[f(g;(2;b)); (g;b)2 gg2 Rel(C;A] B). The unique
!morphism from A to 0/ is 0./ The adjunction for closedness is Rel(A] B;C)= Rel(A;BC) which boils
! ! !down to the bijection(A] B) A B .=
We recall the few notions we shall use on finiteness spaces. For a detailled presentation, the obvious
?reference is [1]. LetFP(A) be any set of subsets of A. We define the pre-dual ofF in A asF =
0 0fa A;8a2F; a\ a2P (A)g. By a standard argument, we have the following immediate properties:f
? ?? ? ? ? ???P (A)F ;FF ; ifGF,F G . By the last two, we getF =F . A finiteness structuref
??on A is a setF of subsets of A such thatF =F. Then a finiteness space is a dependant pairA =
(jAj;F(A)) wherejAj is the underlying set, called the web ofA , andF(A) is a finiteness structure ?? ? ? onjAj. We writeA for the dual finiteness space: A =jAj andF A =F(A) . The elements
ofF(A) are called the finitary subsets ofA .
?For all set A, (A;P (A)) is a finiteness space and (A;P (A)) = (A;P(A)). In particular, eachf f
finite set A is the web of exactly one space: (A;P (A))=(A;P(A)). We introduce the emptyf
finiteness spaceT =(0/;f0/g) and the finiteness space of flat natural numbersN =(N;P (N)). IfAf
andB are finiteness spaces, we defineA &B andA)B as follows. LetjA &Bj=jAj]jBj and
!F(A &B)=fa] b; a2F(A)^ b2F(B)g. LetjA)Bj=jAjjBj and set f2F(A)B) iff:
! ? !8a2F(A), f a 2F(B), and8b2jBj, ( f fbg)\ a is finite. It is easily seen thatA &B is a
finiteness space, but the same result forA)B is quite technical and the only known proof uses the
axiom of choice [1]. We call finitary relations the elements ofF(A)B).
Notice thatF(A)B) Rel(jAj;jBj). We write Fin for the category of finiteness spaces with
Fin(A;B)=F(A)B) and composition defined as in Rel. It is cartesian closed with terminal object
2A Non-Uniform Finitary Relational Semantics of System T Lionel Vaux
a2C(Var) (Unit) A
(Const)G;x : A;D‘ x : A G‘hi :> G‘ a : A
G;x : A‘ s : B G‘ s : A! B G‘ t : A
(Abs) (App)
G‘ st : BG‘lxs : A! B
G‘ s : A G‘ t : B G‘ s : A B G‘ s : A B
(Pair) (Right)(Left)
G‘hs;ti : A B G‘p s : A G‘p s : Bl r
Figure 1: Rules of typedl-calculi with products
a2C a2 JaKJVarK A
[] [a] [] a JConstKG ;x : A;D ‘ x : A [] aG ‘ a : A
a b ([a ;:::;a ];b) a a1 k 1 kG;x : A‘ s : B G ‘ s : A! B G ‘ t : A G ‘ t : A0 1 kJAbsK JAppK
(a;b) k bG ‘ st : BG‘lxs : A! B ? jj=0
a (2;b)G‘ s : A (1;a)ii G‘ s : A BG‘ s : A BJPair K JRightKi JLeftKa(i;a) bG‘p s : A G‘p s : BG‘hs ;si : A A l r1 2 1 2
Figure 2: Computing points in the relational semantics
T , product & and exponential ) : the definitions of those functors on morphisms, the natural
transformations, and the adjunction required for cartesian closedness are exactly the same as for Rel.
3 The Multiset Relational Semantics of Typedl-Calculi
Typedl-calculi. In this section, we give an explicit description of the interpretation in Rel and Fin of
the basic constructions of typedl-calculi with products. Type and term expressions are given by:
A;B ::= Xj A! Bj A Bj> and s;t ::= xj ajlxsj stjhs;tijp sjp sjhil r
where X ranges over a fixed set A of atomic types, x ranges over term variables and a ranges over
term constants. To each variable or constant, we associate a type, and we writeC for the collection ofA
constants of type A. A typing judgement is an expressionG‘ s : A derived from the rules in Figure 1
where contextsG andD range over lists(x : A ;:::;x : A ) of typed variables. The operational semantics1 1 n n
of a typedl-calculus is given by a contextual equivalence relation’ on typed terms: if s’ t, then s and t
have the same type, say A; we then writeG‘ s’ t : A for any suitableG. In general, we will give’ as the
reflexive, symmetric and transitive closure of a contextual relation > on typed terms. We define > as0
the least one such that: phs;ti> s,phs;ti> t and(lxs)t > s[x :=t] (with the obvious assumptions0 r 0 0l
ensuring typability), and we write’ for the corresponding equivalence.0
Relational interpretation and finiteness property. Assume a set JXK is given for each base type X;
!then we interpret type constructions by JA! BK=JAKJBK, JA BK=JAK]JBK and J>K= 0./ Further
assume that with every constant a2C is associated a subset JaK JAK. The relational semantics ofA
!a derivable typing judgement x : A ;:::;x : A ‘ s : A will be a relation JsK JA K1 1 n n 1x :A ;:::;x :A1 1 n n
!
JA KJAK. We first introduce the deductive system of Figure 2. In this system, derivable judgementsn
a1 a anare semantic annotations of typing judgements: x : A ;:::;x : A ‘ s : A stands for(a ;:::;a ;a)21 n 1 n1 n
! []JsK where each a 2 JA K and a2 JAK. In rules JVarK and JConstK,G denotes an annotatedi ix :A ;:::;x :A1 1 n n
3A Non-Uniform Finitary Relational Semantics of System T Lionel Vaux
[] []
context of the form x : A ;:::;x : A . In rule JAppK, the sum of annotated contexts is defined point-1 n n1
0 0 0 0
a a a a +a a +aa 1 n1 1 n 1 nnwise: x : A ;:::;x : A + x : A ;:::;x : A = x : A ;:::;x : A . The semantics1 n 1 n n 1 n nn1 1 1n o
a1 a anof a term is the set of its annotations: JsK = (a ;:::;a ;a); x : A ;:::;x : A ‘ s : A .1 n 1 nx :A ;:::;x :A 1 n1 1 n n
Notice there is no rule forhi in Figure 2, hence JhiK = 0/ for allG.G
Theorem 3.1 (Invariance). IfG‘ s’ t : A then JsK = JtK .0 G G
Proof. We followed the standard interpretation of typed l-calculi in cartesian closed categories, in
the particular case of Rel. A direct proof is also easy, first proving a substitution lemma: if G ;x :0
b[a ;:::;a ] b a k k1 k jA ;D ‘ s : B, and, for all j2f1;:::;kg,G ;D ‘ t : A, then G ; D ‘ s[x :=t] : B.? ?0 j j j jj=0 j=0
The relational interpretation also defines a semantics in Fin: assume a finiteness structureF(X) is
given for all atomic type X, so that X =(JXK;F(X)) is a finiteness space, and set(A! B) = A ) B ,
(A B) = A & B and> =T . Then, further assuming that, for all a2C , JaK2F(A ), we obtain:A
Theorem 3.2 (Finiteness). If x : A ;:::;x : A ‘ s : A then JsK 2F(A )) A ) A ).1 1 n n nx :A ;:::;x :A 11 1 n n
Proof. This is a straightforward consequence of the fact that the cartesian closed structure of Fin is given
by the same morphisms as in Rel. A direct proof is also possible, by induction on typing derivations.
Examples. Pure typedl-calculi are those with no additional constant or conversion rule: fix a setA of
Aatomic types, and writeL for the calculus whereC = 0/ for all A, and s’ t iff s’ t. This is the mostA 00
basic case and we have just shown that Rel and Fin model’ . Be aware that if we introduce no atomic0
0/type, then the semantics is actually trivial: inL , all types and terms are interpreted by 0./0
By contrast, we can consider the internal languageL of Rel in which all relations can be described:Rel
fixA as the collection of all sets (or a fixed set of sets) andC =P(JAK). Then set s’ t iff JsK =JtK ,A Rel G G
for any suitableG. The point in defining such a monstrous language is to enable very natural notations
for relations: in general, we will identify closed terms inL with the relations they denote in the emptyRel
context. For instance, we write id =lxx with x of type A; and if f2 Rel(A;B) and g2 Rel(B;C), weA
have g f =lx(g( f x)). Similarly, the internal languageL of Fin, whereA is the collection of allFin
finiteness spaces andC =F(A ), allows to denote conveniently all finitary relations.A
The main contribution of the present paper is to establish that Fin models Gödel’s system T , which
can be presented in various ways. The iterator version of system T is the typed l-calculus with an
atomic type Nat of natural numbers, and constants O of type Nat, S of type Nat!Nat and for all type
A, I of type Nat!(A! A)! A! A and subject to the following additional conversions: IOuv> vA
andI(St)uv> u(It uv) (we will in general omit the type subscript of such parametered constants). The
recursor variant is similar, but the iterator is replaced with R of type Nat!(Nat! A! A)! A! AA
subject to conversions ROuv> v and R(St)uv> ut(Rt uv). Those systems allow to represent exactly
nthe same functions on the set of natural numbers, where the number n is denoted by S O: this is the
consequence of a normalization theorem (see [13]). In fact, we can define a recursor using iteration
and products with the standard encoding rec=lxlylzp (Ix(lwhy(p w)(p w);S(p w)i)hz;Oi), andl r l r
n nwe get rec(S O)uv’ R(S O)uv: the idea is to reconstruct the integer argument on the fly. But this
encoding is valid only for ground terms of typeNat: rec(St)uv’ ut(rect uv) holds only if we suppose
nt is of the form S O, or reduces to such a term. By contrast, the encoding of the iterator by iter=
0lxlylz(Rx(lx y)z) is extensionally valid: iterOuv’ v and iter(St) uv’ u(itert uv) for all t;u;v.
The fact that one direction of the encoding holds only on ground terms indicate that the algorithmic
properties of both systems may differ. And these differences will appear in the semantics (see the final
section). Also, recall the discussion in our introduction: the tail recursive variant of iterator,J subject to
4A Non-Uniform Finitary Relational Semantics of System T Lionel Vaux
J(St)uv>Jt u(uv), uses its integer argument linearly. This enabled Ehrhard to define a semantics of
iteration, withNat =N =(N;P (N)), JOK=O=f0g and JSK=S =f([n];n+ 1); n2 Ng. Such anf
interpretation of natural numbers, however, fails to provide a semantics ofI orR, in Rel or Fin.
Lemma 3.1. Assume JNatK=jNj, JOK=O and JSK=S , and let A be any type such that JAK= 0/. Then
there is noI JNat!(A! A)! A! AK such that, setting JI K=I , we obtain JIOuvK = JvKA A A G G
and JI(St) uvK = Ju(It uv)K as soon asG‘ t :Nat,G‘ u : A! A andG‘ v : A.G G
Proof. By contradiction, assume the above equations hold. By the second equation and Theorem 3.1,
a0 [] [a] [] 0JI(Sx)(lz y) zK=JyK, and thus x :Nat;y : A;z : A‘I(Sx)(lz y) z : A. Inversing the rules of Figure
2, we obtain that([];[([];a)];[];a)2JIK and then([([];a)];[];a)2JIOK. Since JAK= 0,/ this contradicts
the fact that, by the first equation: JIOK= Jlylz(IOyz)K= JlylzzK=f([];[a];a); a2 JAKg.
4 A finitary relational interpretation of primitive recursion
a[] [a] [] 0Lazy natural numbers. That x :Nat;y : A;z : A‘I(Sx)(lz y) z : A implies([];[([];a)];[];a)2
JIK holds because JSK =S is linear, hence strict: this reflects the general fact that, if s2 Rel(A;B)
contains no([];b) then, for all t2 Rel(B;C), ([];g) in t s iff([];g)2 t. Such a phenomenon was also
noted by Girard in his interpretation of system T in coherence spaces [13]. His evidence that there was
no interpretation of the iteration operator using the linear successor relied on a coherence argument. The
previous lemma is stronger: it holds in any web based model as soon as the interpretation of successor is
strict.
In short, strict morphisms cannot produce anything ex nihilo; but the successor of any natural number
should be marked as non-zero, for the iterator to distiguish between both cases. Hence the successor be affine: similarly to Girard’s solution, we will interpret Nat by so-called lazy natural numbers.
> >LetN =(jNj;P (jNj)) be such thatjNj= N[ N , where N is just a disjoint copy of N. Thefl l l l
> > >elements of N are denoted by k , for k2 N: k represents a partial number, not fully determined but
+ > >strictly greater than k. If n2jNj, we define n as k+ 1 if n = k and(k+ 1) if n = k . Then we setl
> +S =f([];0 )g[f([n];n )g, which is affine. Notice thatO2F(N) andS 2F(N)N).l l l l l
Fixpoints. For all finiteness spaceA , writeRec[A]=N)(N)A)A))A)A . We want tol l
introduce a recursion operatorR 2F(Rec[A]) intuitively subject to the following definition:R t uv=A
O 7! v
match t with . This definition is recursive, and a natural means to obtain such0 0 0St 7! ut (R t uv)

O 7! z
an operator is as the fixpoint ofS tep = lX lxlylz match x with .0 0 0Sx 7! yx (X x yz)
The cartesian closed category Rel is cpo-enriched, the order on morphisms being inclusion. Hence it
S
khas fixpoints at all types: for all set A and f2 Rel(A;A), the least fixpoint of f is f 0,/ which isk0
an increasing union. The least fixpoint operator is itself definable as the supremum of its approximants, S (k) (0) (k+1) (k) (k+1)
F ix = F ix , whereF ix = 0/ andF ix =l f f F ix f , more explicitlyF ix =A k0 A A A A An o
(k)n([([a ;:::;a ];a)]+? j ;a);8i; (j ;a)2F ix . Notice that these approximants are finitary:1 n ii=1 i i A
(k) (k)ifA is a finiteness space then, for all k,F ix =F ix 2F((A)A))A). The fixpoint, however,
A jAj
>is not finitary in general: for instanceF ixS = N 62F(N) henceF ix 62F((N)N))N). Sol l N l l ll
(k) (k)
we proceed in two steps: we first introduce the finitary approximantsR 2F(Rec[A]) byR =A A
S (k)kS tep 0,/ then we proveR = R 2F(Rec[A]).A k0A A
5
66A Non-Uniform Finitary Relational Semantics of System T Lionel Vaux
Pattern matching on lazy natural numbers. We introduce a finitary operatorC ase, intuitively de-
O 7! v
fined as:C aset uv= match t with . More formally:0 0St 7! ut

! + + +Definition 4.1. If n =[n ;:::;n ]2jNj , we write n = n ;:::;n . Then for all set A, letC ase =1 k l A1 nn o
!> +f([0];[];[a];a); a2 Ag[ ([0 ]+n ;[(n;a)];[];a); n2jNj^a2 A .l
Lemma 4.1. Pattern matching is finitary:C ase =C ase 2F(N)(N)A))A)A). More-A jAj l l
over, y :N)A;z :A‘C aseO yz’ z :A and x :N ;y :N)A;z :A‘C ase(S x)yz’ yx :A .l l l l
Proof. That the equations hold is a routine exercise. To proveC ase is finitary, we check the defi-
nition of F() ). For the first direction: for all n2F(N), C asenf([];[a];a); a2jAjg[l
+ ! 0 +([(n;a)];[];a); n 2 n^a2jAj ; hence, setting n =fn; n 2 ng2F(N), we obtainC asenl
0(lylzz)[(lylz(yn)), and we conclude since the union of two finitary subsets is finitary. In the re-
0 ? ! 0j j fgverse direction, we prove that, for all g2 (N)A))A)A , setting N =C ase g , n\ N isl
0finite; this is immediate because N has at most one element.
A recursor in Rel. We introduce the relationR as the fixpoint ofS tep.
0 0 0Definition 4.2. Fix a set A. LetS tep = lX lxlylz(C ase x(lx (yx (X x yz)))z). and, for allA A
S(k) (k)kk2 N, letR =S tep 0/. Then we defineR = R , and fix JRK=R.A k0A A A
Lemma 4.2. For all finiteness spaceA ,S tep =S tep 2F(Rec[A])Rec[A]) and, for all k,A jAj
(k) (k) (0) (k+1)
R =R 2F(Rec[A]). Moreover, we have:R = 0/ andR =f([0];[];[a];a); a2jAjg[A j j A AAn o (k)+> n n n[0 ]+ n ;[(n ;[a ;:::;a ];a)]+ j ; a ;a ;8i; (n ;j ;a ;a)2R .? ? ?0 1 n i i i ii=0 i i=1 i i=1 i A
(k)
Proof. The finiteness of the approximants follows from Theorem 3.2. The explicit description ofR is
A
a direct application of the definition of the relational semantics.
Theorem 4.3 (Correctness). For all suitableG andD, JROyzK =JzK andJR(Sx)yzK =Jyx(Rxyz)K .G G D D
Proof. This follows directly from Lemma 4.1 and the fact thatR=S tepR.
Finiteness. It only remains to proveR is finitary. Following the definition of () ), we proceed
in two steps: the image of a finitary subset ofN is finitary; conversely, the preimage of a singleton isl
“anti-finitary”.
!Definition 4.4. Ifa=[a ;:::;a ]2 a , we denote the support ofa by Supp(a)=fa ;:::;ag a, and1 k 1 k
>the size ofa by #(a)= k. If n2F(N), we set max(n)= maxfk; k2 n_ k 2 ng, with the conventionl
! !max(0/)= 0. Then if n2jNj we set max(n)= max(Supp(n)), and if n n for some n2F(N),l lS
max(n)= max( Supp(n)).n2n
(max(n)+1)
Lemma 4.3. For allg =(n;j;a;a)2R ,g2R .A A
Proof. By induction on max(n), using Lemma 4.2.
Lemma 4.4. If n2F(N), thenR n2F((N)A)A))A)A).l A l
(max(n)+1) (max(n)+1)
Proof. The previous Lemma entailsR n=R n. We conclude recalling thatR n2A A A
(max(n)+1)F((N)A)A))A)A), becauseR 2Rec[A].l A
6