In this paper retractions existing in all models of simply typed lambda-calculus are studied relating them to other relations among types as isomorphisms, surjections and injections. A formal system to deduce the existence of such retractions is shown to be sound and complete with respect to retractions definable by linear lambda-terms and results aiming to a system complete w.r.t. the "provable retractions" tout court are established.
Retracts in simply typed λ-βη calculus
DE' LIGUORO, Ugo;
1992-01-01
Abstract
In this paper retractions existing in all models of simply typed lambda-calculus are studied relating them to other relations among types as isomorphisms, surjections and injections. A formal system to deduce the existence of such retractions is shown to be sound and complete with respect to retractions definable by linear lambda-terms and results aiming to a system complete w.r.t. the "provable retractions" tout court are established.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
