Lambda model
= Lambda model
A lambda model interprets variables, <lambda application> and <lambda abstraction> so that <capture-avoiding substitution> agrees with environments and all <beta equivalence> equations hold. A <reflexive domain> gives such an interpretation. Validity of <eta conversion> requires an extra inverse law and does not follow merely from a retraction.