Böhm tree

Böhm trees are a device used in the semantic analysis of the untyped \lambda-calculus.

There is an entire chapter about Böhm trees in Barendregt's book Barendregt 1984, ch. 10.

Definition

Let M be an untyped term. We consider its behaviour under head reduction.

• If M has no head normal form, then we define its Böhm tree to be the 'empty tree'

  BT(M) = \bot
  

• If M has a head normal form \lambda x_1, \ldots, x_n. y M_1 \ldots M_m, we define its Böhm tree BT(M) to be

<mxfile host="embed.diagrams.net" modified="2023-04-25T18:10:10.176Z" agent="Mozilla/5.0 (Windows NT 10.0; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/112.0.0.0 Safari/537.36 Edg/112.0.1722.58" etag="r-YX92RSx6wkGS_BQ9Hs" version="21.2.2" type="embed"><diagram id="HNxQAf7u1rnelHc1t8eG" name="Page-1">7VjLjpswFP0apHYxEe+EZUjT6WakSqnUtQc7YNVg6piE9OtrwA4QII+WZkai2cQ+2NfX5xwbG81axfkzA2n0QiEimqnDXLM+aaZp2JYt/grkWCFzb1EBIcNQNqqBDf6FJKhLNMMQ7VoNOaWE47QNBjRJUMBbGGCMHtrNtpS0R01BiDrAJgCki37HkEcVujDnNf4F4TBSIxuuVz2JgWosZ7KLAKSHBmStNWvFKOVVKc5XiBTkKV6qfp8Hnp4SYyjht3Qwqw57QDI5N5kXP6rJogQuC85ELaGJAP2Ix0TUDFFkNEsgKoLpotYdXSaEYItQmcszojHi7CgaHGoaHUlN1GBQYQwRwPG+LQOQaoancKcRvlIsMjF16TzLk3Gk72xbb4fY0YwFSPZq0nYW6NTxeBZYBeKAhYh3AolCY9o1VKrSr5A1KYVsayyF5g9TyJ6UQo45lkLewxRypqWQM5JC51L/Q4XcjkLHjkQc5YIof8cZ/YFWlFBWiwUIDhNRDYQmSOD+FhNy1qYh6B4xjsX7fCm7xRjCYhj/EGGONikIijEP4vRyu/pFTJRf1H9ob3JlveEPt8cflj5shRb3F4ied4j2v3140UyXlNxmry3O3Z9ZcRLxtzThT7vyHLYUDbw0L5lQj0UpLP4NFUdkUYaq4I/vVMpiVvJw6Y2j7EnJ86V3ZeWbIyi7uKxsCpK/kXYkh5j9DmmiZaJTM45tvJ1xvOtbQiVHfFm8d2Kxp4Fd6L/Hhm4/V147Y3hM2fuPTTYdmRz7DWUyOjLNZrPJUG8PnZwfQX3Pp5jVWvP9vGeRDGxx+b1bsaHfshdffHWX/ujdWe9NZjGzit9ARn00JLO7tvqeCAp6ZX19m+3e5RIYw/PqSqAuI47X8fzcGeUyIqr1l83qklh/H7bWvwE=</diagram></mxfile>

Notice the following things, especially about the nontrivial case.

• It may be infinitely deep (but not wide). In fact, this is a definition by coinduction.
• It may also be written in a term-like notation (see examples below).

Examples

• BT(\Omega) = \bot
• BT(\lambda x. x) = \lambda x. x.
• BT(\lambda x. x\Omega) = \lambda x. x\bot

Induced theory

Böhm trees induce an equational theory \mathcal{B} of the untyped \lambda-calculus, in which all terms with the same Böhm tree are equated Barendregt 1984, § 16.4:

 \mathcal{B} \vdash M = N  \quad\triangleq\quad  BT(M) = BT(N)

This theory contains \lambda\beta.

It also has a close relationship with various classical models:

• it is the theory induced by the graph model Barendregt 1984, § 19.1
• it is the theory induced by the Engeler model
• it is contained in the theory induced by D_\infty

See also

• Lévy-Longo trees

References

• According to Sangiorgi & Walker 2003, p. 493, Böhm trees were introduced by Barendregt in his seminal book, and named after a theorem of Corrado Böhm.