Inverse Limit Models as Filter Models

Natural intersection type preorders are the type structures which agree with the plain intuition of intersection type constructor as set-theoretic intersection operation and arrow type constructor as set-theoretic function space constructor. In this paper we study the relation between natural intersection type preorders and natural #-structures, i.e. #-algebraic lattices D with Galois connections given by F : D # [D # D] and G : [D # D] # D. We prove on one hand that natural intersection type preorders induces natural #-structures, on the other hand that natural #-structures admits presentations through intersection type preorders. Moreover we give a concise presentations of classical D# #-models of untyped #-calculus through suitable natural intersection type preorders and prove that filter #-models induced by them are isomorphic to D# .