Higher-Order Unification with Definition by Cases

Abstrakt

We discuss unification within the simply-typed λ-calculus extended by a definition by cases operator (denoted by d) slightly differing from similar operators introduced by earlier investigations. Such operators may be thought of as restrictions of Hilbert’s choice operator. We provide several non-trivial examples which illustrate the benefits of introducing such an operator.