Lévy-Longo tree

Lévy-Longo trees are a device used in the semantic analysis of the untyped \lambda-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.

Definition

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

If M has no WHNF, then we define its Lévy-Longo tree to be the 'empty tree'
```
LLT(M) = \bot
```
If M has a WHNF, then we look at its structure.
- If the WHNF is of the form y N_1 \ldots N_m, then we define LLT(M) to be

<mxfile host="embed.diagrams.net" modified="2023-04-25T22:45:15.403Z" 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="CkTwAHiYS1cl23zUjxJG" version="21.2.2" type="embed"><diagram id="HNxQAf7u1rnelHc1t8eG" name="Page-1">7ZjNjpswFIWfBqldTAQYSFgm6XS6mJEqpVLXHnDAqsHUMQnp09dgO/yFJJrSdCS6SfDBvrbPd4ELBlgnxRODWfxCQ0QM2wwLA3wybHvuO+K3FI5ScMBCChHDoZSsWtjgX0iJplJzHKJdqyOnlHCctcWApikKeEuDjNFDu9uWkvasGYxQT9gEkPTV7zjksVQX9rzWvyAcxXpmy/PlmQTqzmonuxiG9NCQwKMB1oxSLo+SYo1I6Z32RY77PHD2tDCGUn7LAFsO2EOSq72pdfGj3ixKw2XpmWilNBXiKuYJES1LHDKapyEqg5mi1Z9dLQiFLUPVWp4QTRBnR9HhUNvoKmvihoNaY4hAjvdtDFDRjE7hTjN8pVisxDZV4gFfxdF555jtEDuaswCpUU3bOoFOA4+dwDoQhyxCvBdIHDS2XUsVlfOEwKQIOWAsQvO7EXImRci1xyLk342QOy1C7kiEuqj/IiGvR+jYQ8RRIYxa7TijP9CaEspqWJDgKBXNQDBBQl9tMSGdPg2ge8Q4Fs/zpRqW4DAsp1kdYszRJoNBOedBFC+30y9jouIif535HUDAVeVBIz+8M/kBzOFUaHl/weh5z+jn528fXgzbI5W5+WvLdO9nXpYiqy1N+cOuKsSWooOfFZUV+rQ4isp/S8cRy6hCSfnjO2VZ7kpVl/44aIE3cO1dufTtEdAurqDNYPonbEdKEft8ijTVaqFTyxzH+neZ499wU5A8ksv03kmOPQzch/4n2dAL0JUnzxhJpvP77Vk2HU6DJdw9OFk9TrPZbDLWd4uzu1p/7nNM7+rQ0is7d19r9nuXyMZgpMvYCwX03B2lgBbN+mucfLGpP2mCx98=</diagram></mxfile>

If the WHNF is of the form \lambda x. N, then we define LLT(M) to be

<mxfile host="embed.diagrams.net" modified="2023-04-25T22:46:08.545Z" 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="tgprqWdMS3Vq44mvLbZB" version="21.2.2" type="embed"><diagram id="HNxQAf7u1rnelHc1t8eG" name="Page-1">zVXLjtsgFP0aS+2ikWP8SJZjJ50uptVIqdTOkjE3Nio2EcGx068vDvhBaKKONItmEXEP98G954A9lFXdo8CH8isnwLzAJ52HNl4QJOtQ/ffAWQMhWmmgEJRoaDkBO/obDOgbtKEEjpaj5JxJerDBnNc15NLCsBC8td32nNlVD7gAB9jlmLnoD0pkqdFVkEz4F6BFOVRexmu9U+HB2XRyLDHh7QxCWw9lgnOpV1WXAetnN8xFx32+sTseTEAt/yUA6YATZo3pzZxLnodmoSYP/cyUVfNagWkpK6aspVoK3tQE+mS+sqCj8me/XizD0Ngvyv6kAIQMsOlm3pvzzHgGQSuQIAzmNmP6A2LxY1p7BK6ixVk5tBMrkZl0OSNkwAQwLOnJZhUbcRRjurHCM6fqJIFvdBxGq0Uc+uPPJBhFnSzQbNdHdv4jb0QOJuWcousqsW/lRWvfTiSxKEA6idRiNpMJuijghnx8Rw5PT98/fPvoiEJCp2aZHqXgvyDjjItJHpjRolZmrmjruUz3lLErn5mETiAkVXfrwYRVlJC+TNqWVMLugPO+ZqseEkdve15L8zqs7+mlLwHdXcUMww6SRWTTOIhlpqn4L5oK/NvysSi5N//AvY7Z1kvTzgtidhl486qWhbx0q6FXcY2oMpbff8ndu5B1dTOitUNVErlUobdTpczpUdY3a/qyoe0f</diagram></mxfile>

Notice the following things:

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

LLT(\Omega) = \bot
LLT(\lambda x. x) = \lambda x. x
LLT(\lambda x. x\Omega) = \lambda x. x\bot
LLT(\lambda x. \Omega) = \lambda x. \bot

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 \bot.

Induced theory

The theory induced by stipulating that M = N whenever LLT(M) = LLT(N) coincides with the theory of Plotkin-Scott-Engeler models Longo 1983.

References

It seems that Levy-Longo trees were introduced (as just "trees") in

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}
}

Lévy-Longo tree

Definition

Examples

Induced theory

See also

References