[Prev][Next][Index][Thread]

Re: semantics for F_{sub,rec} ??

Dear Martin,

thanks for your reply to my question. I am not principally against an 
approach via metric spaces. I do see that it allows one to guarantee the
existence of some fixpoint for PARTICULAR type equations without parameters.
But these are fixpoints of FUNCTIONS from Type to Type and not of FUNCTORS. 
What I do not see is to which extent this appraoch leads to an interpretation
of full F_{sub,rec}. This approach only guaranatees the existence of fixpoints
A = T(A) for PARTICULAR T, namely the contractive ones. I don't see how to
restrict F_{sub,rec} to a closed subsystem where one can write down only such
T(A) where T is contractive as this would mean for example that we don't have 
a lambda calculus of kinds. I can't imagine any syntax which for example 
excludes All X. X which certainly is not contractive. Another problem is that
of parameters : consider T(B,A)  where  T(B,-) is contractive only for 
particular choices of B (e.g. T(B,A) = B x A which is not contractive for 
B = 1).

One could now say that the metric approach or that via ranked sets guarantees
the existence of fixpoints for particular type equations and that this 
suffices. I agree with that if one develops a semantically based logic of, 
say, object calculi where one works with an untyped model (as in your book 
with Luca or in my recent work with B.Reus (LICS'02, for a slightly revised 
version see http://www.cogs.susx.ac.uk/users/bernhard/lics02.ps). Then pers
over the untyped model (O = Rec[O->O] where -> stands for partial continuous
functions) are a useful tool for reasoning about untyped programs and one
could use e.g. the metric approach to establish the existence of particular
pers satisfying some requirements formulated as recursive type equations
e.g. A = T(A) = Exists X <: A. X -> T(X) where T is some contravariant functor
though in this case T(-) is simply a monotonic endo function on the lattice of
pers and we may take its greatest fixpoint.

BUT in Bruce's book for example (and some other papers in this vein) the FULL 
F_{sub,rec} is used and not a restriction to a "contractive fragment"
(where I wouldn't know how to formulate it). And I feel a bit uneasy about
using a target language where we have a "semantics for the interesting part
only". To make my point even more precise I have the following to questions

  (1) can one give a semantics for FULL  F_{sub,rec}  in a realizability
      or domain model ?
      I think NO, because I don't see how to dela with non-contractive
      recursive type equations

  (2) can one define a reasonable fragment of F_{sub,rec} restricting to,
      say, guarded type expressions which can be interpreted using the
      already established techniques only

So my (posibly somewhat pedantic) problem is that I don't see how to work with
a "calculus for which only the meaningful part can be interpreted". 

Thomas
References: