Thomas Ehrhard (Paris, France), Extensional collapse of the relational semantics of Linear Logic, and applications
Schedule
- Feb. 23, 2012, 9:00 - 10:20
Abstract
We present a model of Classical Linear Logic whose objects can be understood as triples made of the relational interpretation of a type, the interpretation of the same type as a prime-algebraic lattice (Scott interpretation) and a realizability predicate between these interpretations. We prove that, in this model, all types with parameters have a least fix-point in some sense, and hence that this model contains many models of the pure lambda-calculus (in CBN and CBV).
In the relational semantics, where the exponential is non-idempotent, proving sensibility results of models (theorems of the kind: if the interpretation of a term is non-empty, then this term normalizes in some sense) by purely combinatorial means is possible. Indeed, such results boil down to normalization in a suitable promotion-free resource lambda-calculus whose term denote derivations of the fact that a given point of the model belong to the interpretation of a term (aka intersection typing).
We show how to use our collapse model for transferring such results to Scott models, where these combinatorial methods are not available, and where such sensibility results are obtained by syntactic reducibility methods only. This approach applies to many situations in a completely uniform way: in some sense, all the realizability structure needed to prove results of this kind has been encapsulated in the construction of the model, once and for all.
Attachments
We present a model of Classical Linear Logic whose objects can be understood as triples made of the relational interpretation of a type, the interpretation of the same type as a prime-algebraic lattice (Scott interpretation) and a realizability predicate between these interpretations. We prove that, in this model, all types with parameters have a least fix-point in some sense, and hence that this model contains many models of the pure lambda-calculus (in CBN and CBV).
In the relational semantics, where the exponential is non-idempotent, proving sensibility results of models (theorems of the kind: if the interpretation of a term is non-empty, then this term normalizes in some sense) by purely combinatorial means is possible. Indeed, such results boil down to normalization in a suitable promotion-free resource lambda-calculus whose term denote derivations of the fact that a given point of the model belong to the interpretation of a term (aka intersection typing).
We show how to use our collapse model for transferring such results to Scott models, where these combinatorial methods are not available, and where such sensibility results are obtained by syntactic reducibility methods only. This approach applies to many situations in a completely uniform way: in some sense, all the realizability structure needed to prove results of this kind has been encapsulated in the construction of the model, once and for all.