Decidability of behavioural equivalence in unary PCF

摘要

Unary PCF is a fragment of the simply typed lambda-calculus PCF. We present a short proof that behavioral equivalence in unary PCF is decidable. An algorithm is described that enumerates all behaviorally equivalent expressions by increasing types, where types are ordered by a nested multiset ordering.