Given an acyclic graph, how can I build a lambda calculus term such that this graph is the term's Böhm tree?

  • If the Böhm tree is a finite tree (so the result is a strongly normalizing term).
  • If the Böhm tree is an acyclic graph, but not necessarily a tree (so the result may not be normalizing).
  • If the Böhm tree is not finite — is there a language of inifinite trees on which the process is decidable and which allows reaching every lambda term?

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.