logical relation

A relation R satisfying

f R g = For all a, b, a R b =@# f a R g b

This definition, by Plotkin, can be used to extend the

definition of a relation on the types of a and b to a relation

on functions.