Read anywhere, anytime
Description
Subjects
Informations
Published by | mijec |
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 Scientiﬁque, 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 deﬁned as
ﬁxpoints of typed functionals, we prove them ﬁnitary in the sense of Ehrhard’s ﬁniteness spaces.
1 Introduction
Finiteness spaces were introduced by Ehrhard [1], reﬁning the purely relational model of linear logic. A
ﬁniteness space is a set equipped with a ﬁniteness structure, i.e. a particular set of subsets which are said
to be ﬁnitary; and the model is such that the relational denotation of a proof in linear logic is always a
ﬁnitary 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 ﬁniteness spaces is that
the intersection of two ﬁnitary subsets of dual types is always ﬁnite. 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 ﬁnitary
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 ﬁniteness spaces can accomodate typed l-calculi only. In particular, the
relational semantics of ﬁxpoint combinators is never ﬁnitary. The whole point of the ﬁniteness construc-
tion is actually to reject inﬁnite computations, ensuring the intermediate sets involved in the relational
interpretation of a cut are all ﬁnite. Despite this restrictive design, Ehrhard proved that a limited form of
recursion was available, by deﬁning a ﬁnitary tail-recursive iteration operator.
The main result of the present paper is that ﬁniteness 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 ﬁnitary recursion operator for
this interpretation of the type of natural numbers. This achievement is twofold:
Before considering ﬁniteness, we must deﬁne 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 ﬂat 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 ﬁnitary. This is far
from immediate because the recursion operator is deﬁned as the ﬁxpoint of ﬁnitary approximants:
since ﬁxpoints themselves are not ﬁnitary relations, it is necessary to obtain stronger properties of
these approximants to conclude.
Structure of the paper. In section 2, we brieﬂy describe two cartesian closed categories: the category
Rel of sets and relations from multisets to points, and the category Fin of ﬁniteness spaces and ﬁnitary
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-deﬁnable 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 ﬁnite subsets of A and by Af
nthe set of all ﬁnite 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 ﬁniteness spaces. For a detailled presentation, the obvious
?reference is [1]. LetFP(A) be any set of subsets of A. We deﬁne 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 ﬁniteness structuref
??on A is a setF of subsets of A such thatF =F. Then a ﬁniteness space is a dependant pairA =
(jAj;F(A)) wherejAj is the underlying set, called the web ofA , andF(A) is a ﬁniteness structure ?? ? ? onjAj. We writeA for the dual ﬁniteness space: A =jAj andF A =F(A) . The elements
ofF(A) are called the ﬁnitary subsets ofA .
?For all set A, (A;P (A)) is a ﬁniteness space and (A;P (A)) = (A;P(A)). In particular, eachf f
ﬁnite set A is the web of exactly one space: (A;P (A))=(A;P(A)). We introduce the emptyf
ﬁniteness spaceT =(0/;f0/g) and the ﬁniteness space of ﬂat natural numbersN =(N;P (N)). IfAf
andB are ﬁniteness spaces, we deﬁneA &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 ﬁnite. It is easily seen thatA &B is a
ﬁniteness space, but the same result forA)B is quite technical and the only known proof uses the
axiom of choice [1]. We call ﬁnitary relations the elements ofF(A)B).
Notice thatF(A)B) Rel(jAj;jBj). We write Fin for the category of ﬁniteness spaces with
Fin(A;B)=F(A)B) and composition deﬁned 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 deﬁnitions 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 ﬁxed 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
reﬂexive, symmetric and transitive closure of a contextual relation > on typed terms. We deﬁne > 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 ﬁniteness 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 ﬁrst 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 deﬁned 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, ﬁrst 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 deﬁnes a semantics in Fin: assume a ﬁniteness structureF(X) is
given for all atomic type X, so that X =(JXK;F(X)) is a ﬁniteness 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: ﬁx 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
ﬁxA as the collection of all sets (or a ﬁxed set of sets) andC =P(JAK). Then set s’ t iff JsK =JtK ,A Rel G G
for any suitableG. The point in deﬁning 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
ﬁniteness spaces andC =F(A ), allows to denote conveniently all ﬁnitary 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 deﬁne 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 ﬂy. 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 ﬁnal
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 deﬁne 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 ﬁrst equation: JIOK= Jlylz(IOyz)K= JlylzzK=f([];[a];a); a2 JAKg.
4 A ﬁnitary 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 reﬂects 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 afﬁne: 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 deﬁne 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 afﬁne. Notice thatO2F(N) andS 2F(N)N).l l l l l
Fixpoints. For all ﬁniteness 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 deﬁnition:R t uv=A
O 7! v
match t with . This deﬁnition is recursive, and a natural means to obtain such0 0 0St 7! ut (R t uv)
O 7! z
an operator is as the ﬁxpoint 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 ﬁxpoints at all types: for all set A and f2 Rel(A;A), the least ﬁxpoint of f is f 0,/ which isk0
an increasing union. The least ﬁxpoint operator is itself deﬁnable 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 ﬁnitary:1 n ii=1 i i A
(k) (k)ifA is a ﬁniteness space then, for all k,F ix =F ix 2F((A)A))A). The ﬁxpoint, however,
A jAj
>is not ﬁnitary 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 ﬁrst introduce the ﬁnitary 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 ﬁnitary operatorC ase, intuitively de-
O 7! v
ﬁned as:C aset uv= match t with . More formally:0 0St 7! ut
! + + +Deﬁnition 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 ﬁnitary: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 ﬁnitary, we check the deﬁ-
nition of F() ). For the ﬁrst 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 ﬁnitary subsets is ﬁnitary. 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
0ﬁnite; this is immediate because N has at most one element.
A recursor in Rel. We introduce the relationR as the ﬁxpoint ofS tep.
0 0 0Deﬁnition 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 deﬁneR = R , and ﬁx JRK=R.A k0A A A
Lemma 4.2. For all ﬁniteness 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 ﬁniteness of the approximants follows from Theorem 3.2. The explicit description ofR is
A
a direct application of the deﬁnition 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 ﬁnitary. Following the deﬁnition of () ), we proceed
in two steps: the image of a ﬁnitary subset ofN is ﬁnitary; conversely, the preimage of a singleton isl
“anti-ﬁnitary”.
!Deﬁnition 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
Access to the YouScribe library is required to read this work in full.
Discover the services we offer to suit all your requirements!