首页 | 本学科首页   官方微博 | 高级检索  
     检索      


Strong stability and the incompleteness of stable models for λ-calculus
Authors:Olivier Bastonero  Xavier Gouy
Abstract:We prove that the class of stable models is incomplete with respect to pure λ-calculus. More precisely, we show that no stable model has the same theory as the strongly stable version of Park's model. This incompleteness proof can be adapted to the continuous case, giving an incompleteness proof for this case which is much simpler than the original proof by Honsell and Ronchi della Rocca. Moreover, we isolate a very simple finite set, , of equations and inequations, which has neither a stable nor a continuous model, and which is included in and in , the contextual theory induced by the set of essentially λI-closed terms. Finally, using an approximation theorem suitable for a large class of models (in particular stable and strongly stable non-sensible models like and ), we prove that and are included in , giving an operational meaning to the equality in these models.
Keywords:Lambda calculus  Denotational semantics  Continuity  Stability  Strong stability
本文献已被 ScienceDirect 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号