Personal tools
You are here: Home Events Abstract Archives 2003 Higher order beta matching

Higher order beta matching

Ralph Loader 4pm Thursday 5 June 2003 Room 2511, JCMB, King's Buildings

In the 1970's, Huet asked if matching equations in the simply typed lambda calculus are decidable.

I give a proof that these matching problems are undecidable, when we use beta equivalence as the equality.

I'll start by illustrating the key proof technique with a slight variant of Huet's undecidability proof for higher order unification, and then explain how to apply the technique to matching.

Document Actions