 In  Section 1.3  we have already defined a very general notion of (equational) full abstraction, based on synonymy, i.e., equality of interpretation of terms. In the case PCF, whose intended models are partially ordered at all types, we can define a stronger property: