自动机无限运行的简单类型λ项有限语义

模型检测属性通常通过有限自动机来描述。任何此类特定自动机根据哪个状态具有无限运行，将无限树集合划分为有限多个类。在此基础类型解释之上构建完整的类型层级，可为简单类型λ树提供有限语义。基于此语义的演算被证明是可靠且完备的。特别是，对于正则无限λ树，判定给定自动机是否具有运行是可决定的。由于正则λ树精确对应于递归方案，该可判定性结果适用于任意层级的任意递归方案，且无任何句法限制。