To remedy this problem one can instead construct a realizability model whereby one starts with a set of realizers. One can here follow Kleene’s numerical realizability closely where functions are realized by codes for Turing machines. Or alternatively, one can let realizers be terms in a lambda calculus or combinatory logic possibly extended with appropriate constants. Types are then represented by sets of realizers, or often as partial equivalence relations on the set of realizers. A partial equivalence relation is a convenient way to represent a type with a notion of “equality” on it.