В монографии "Ламбда-исчисление. Его синтаксис и семантика", Барендрегт Х., 1985 (перевод с английского Г. Е. Минца под редакцией А. С. Кузичева), в параграфе 16.4 рассматривается эквациональная теория B = {M = N | M, N ∈ Λ0, BT(M) = BT(N)}, где BT(M) - дерево Бема для терма M (см. "Краткое изложение λ-исчисления"). Иными словами, в этой теории отождествяются термы, имеющие одни и те же деревья Бема. Теория B непротиворечива, так как является собственным подмножеством ее экстенсионального расширения Bη, которое, в свою очередь, совпадает с единственной HP-полной λ-теорией H*.
Все комбинаторы неподвижной точки имеют одно и то же дерево Бема, поэтому они отождествляются в теории B. Более того, существуют термы, которые формально не подпадают под определение комбинаторов неподвижной точки, но имеют то же самое дерево Бема. Термы, которым соответствует дерево Бема комбинаторов неподвижной точки, обобщенно называются нестандартными комбинаторами неподвижной точки, а термы из этого множества, не являющиеся комбинаторами неподвижной точки, в свою очередь, называют существенно нестандартными. В следующей статье показывается, что множество нестандартных комбинаторов неподвижной точки не является рекурсивно перечислимым, в отличие от множества обычных комбинаторов неподвижной точки.
On the Recursive Enumerability of Fixed-Point Combinators
Mayer Goldberg
We show that the set of fixed-point combinators forms a recursively-enumerable subset of a larger set of terms we call non-standard fixed-point combinators. These terms are observationally equivalent to fixed-point combinators in any computable context, but the set of non-standard fixed-point combinators is not recursively enumerable.
http://www.brics.dk/RS/05/1/BRICS-RS-05-1.pdf
Все комбинаторы неподвижной точки имеют одно и то же дерево Бема, поэтому они отождествляются в теории B. Более того, существуют термы, которые формально не подпадают под определение комбинаторов неподвижной точки, но имеют то же самое дерево Бема. Термы, которым соответствует дерево Бема комбинаторов неподвижной точки, обобщенно называются нестандартными комбинаторами неподвижной точки, а термы из этого множества, не являющиеся комбинаторами неподвижной точки, в свою очередь, называют существенно нестандартными. В следующей статье показывается, что множество нестандартных комбинаторов неподвижной точки не является рекурсивно перечислимым, в отличие от множества обычных комбинаторов неподвижной точки.
On the Recursive Enumerability of Fixed-Point Combinators
Mayer Goldberg
We show that the set of fixed-point combinators forms a recursively-enumerable subset of a larger set of terms we call non-standard fixed-point combinators. These terms are observationally equivalent to fixed-point combinators in any computable context, but the set of non-standard fixed-point combinators is not recursively enumerable.
http://www.brics.dk/RS/05/1/BRICS-RS-05-1.pdf
