We illustrate the use of intersection types as a semantic tool for proving easiness result on λ-terms. We single out the notion of simple easiness for λ-terms as a useful semantic property for building filter models with special purpose features. Relying on the notion of easy intersection type theory, given λ-terms M and E, with E simple easy, we successfully build a filter model which equates interpretation of M and E, hence proving that simple easiness implies easiness. We finally prove that a class of λ-terms generated by ω2 ω2 are simple easy, so providing alternative proof of easiness for them. © 2002 Published by Elsevier Science B.V.
Simple Easy Terms
ALESSI, Fabio;
2003-01-01
Abstract
We illustrate the use of intersection types as a semantic tool for proving easiness result on λ-terms. We single out the notion of simple easiness for λ-terms as a useful semantic property for building filter models with special purpose features. Relying on the notion of easy intersection type theory, given λ-terms M and E, with E simple easy, we successfully build a filter model which equates interpretation of M and E, hence proving that simple easiness implies easiness. We finally prove that a class of λ-terms generated by ω2 ω2 are simple easy, so providing alternative proof of easiness for them. © 2002 Published by Elsevier Science B.V.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
