Minimal lambda-theories by ultraproducts

A longstanding open problem in lambda calculus is whether there exist continuous models of the untyped lambda calculus whose theory is exactly the $\lambda\beta$ or the least sensible lambda-theory $\cH$ (generated by equating all the unsolvable terms). A related question is whether, given a class of lambda models, there is a minimal lambda-theory represented by it. In this paper, we give a general tool to answer positively to this question and we apply it to a wide class of webbed models: the i-models. The method then applies also to graph models, Krivine models, coherent models and filter models. In particular, we build an i-model whose theory is the set of equations satisfied in all i-models.

Data and Resources

Additional Info

Field Value
Source https://hal.science/hal-00710340
Author Carraro, Alberto, Salibra, Antonino, Bucciarelli, Antonio
Maintainer CCSD
Last Updated May 15, 2026, 15:01 (UTC)
Created May 15, 2026, 15:01 (UTC)
Identifier hal-00710340
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Preuves, Programmes et Systèmes (PPS) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)
creator Carraro, Alberto
date 2012-05-15T00:00:00
harvest_object_id 5c6ff1d0-afdf-4084-9e36-2b0ed3d5624e
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2026-03-13T00:00:00
set_spec type:UNDEFINED