Lévy-Longo trees are a device used in the semantic analysis of the untyped -calculus.
They are similar to the better-known Böhm trees. But while Böhm trees are closely related to head normal forms, Lévy-Longo are closely related with weak head normal forms.
Let be an untyped term. We consider its behaviour under weak head reduction.
If has no WHNF, then we define its Lévy-Longo tree to be the 'empty tree'
If has a WHNF, then we look at its structure.
Notice the following things:
For the first three, these are the same as their respective Böhm trees; however, as Böhm trees require head normal forms, the Böhm tree for the last is simply .
The theory induced by stipulating that whenever coincides with the theory of Plotkin-Scott-Engeler models [Longo 1983].
Longo, Giuseppe. 1983. ‘Set-Theoretical Models of λ-Calculus: Theories, Expansions, Isomorphisms’. Annals of Pure and Applied Logic 24 (2): 153–88. https://doi.org/10.1016/0168-0072(83)90030-1.
@article{longo_1983,
title = {Set-theoretical models of λ-calculus: theories, expansions, isomorphisms},
volume = {24},
doi = {10.1016/0168-0072(83)90030-1},
number = {2},
journal = {Annals of Pure and Applied Logic},
author = {Longo, Giuseppe},
year = {1983},
pages = {153--188}
}