The invariance of the meaning of a lambda term under reduction/expansion w.r.t. the considered computational rules is one the minimal requirements for a lambda model. Being the intersection type systems a general framework for the study of semantic domains for the lambda calculus, the present paper provides a characterisation of meaning invariance in terms of characterisation results for intersection types systems enabling typing invariance of terms w.r.t. various notions of reduction/expansion, like beta, eta and a number of relevant restrictions of theirs.
[ bib | http ]