Title :
Retracts in simply type λβη-calculus
Author :
de´Liguoro, U. ; Piperno, A. ; Statman, R.
Author_Institution :
Dipartimento di Sci. dell´´Informazione, Roma Univ., Italy
Abstract :
Retractions existing in all models of simply typed λ-calculus are studied and related to other relations among types, such 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 λ-terms. Results aiming at a system complete with respect to the provable retractions tout court are established
Keywords :
data structures; formal logic; formal system; injections; isomorphisms; lambda -calculus; lambda calculus; linear lambda -terms; surjections; type lambda beta eta -calculus; Ear; Mathematical model; Mathematics; Remuneration; Time of arrival estimation; Virtual manufacturing;
Conference_Titel :
Logic in Computer Science, 1992. LICS '92., Proceedings of the Seventh Annual IEEE Symposium on
Conference_Location :
Santa Cruz, CA
Print_ISBN :
0-8186-2735-2
DOI :
10.1109/LICS.1992.185557
