Discriminating Lambda-Terms Using Clocked Boehm Trees

As observed by Intrigila, there are hardly techniques available in the lambda-calculus to prove that two lambda-terms are not beta-convertible. Techniques employing the usual Boehm Trees are inadequate when we deal with terms having the same Boehm Tree (BT). This is the case in particular for fixed...

Full description

Bibliographic Details
Main Authors: Joerg Endrullis, Dimitri Hendriks, Jan Willem Klop, Andrew Polonsky
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2014-05-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/880/pdf