An easy lambda term must be equatable consistently with every closed lambda term. Choose the proposed equation . Applying it to gives . Applying that equation to an arbitrary closed gives . In particular the two Church Booleans become equal; then applying them to arbitrary gives . The extended equational theory is trivial, hence inconsistent in the required sense. Therefore is not easy.
Articles by others on the same topic
There are currently no matching articles.