[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: