[Prev][Next][Index][Thread]
Re: semantics for F_{sub,rec} ??
Dear Thomas,
First some comments on details, which may however matter:
> 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.
It seems to me that your question is about F_{omega, sub, rec}, since you
want a lambda calculus of kinds, rather than about F_{sub, rec}. I agree that
F_{omega, sub, rec} is harder. For F_{sub, rec}, however, one can find
fixpoints even when T is not contractive, by analyzing those special cases.
T is typically the identity. This is (in my opinion) inelegant, but works.
> 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).
1xA is in fact contractive in A---curiously perhaps! If 1xA and 1xA' differ at
some rank n+1, it must be because A and A' differ at rank n (much as
in Theorem 7 of the paper by MacQueen, Plotkin, and Sethi on the ideal model).
As for your main 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
>
Since your "FULL F_{sub,rec}" seems to be a system with a kind level
(what I would much rather call F_{omega, sub, rec}, perhaps), then I don't
have a very good answer, and leave the (interesting) question to others.
Best,
Martin
Follow-Ups: