Esto está inspirado en esta pregunta. Sea la colección de todos los combinadores que solo tienen dos variables ligadas. ¿ C es combinatoriamente completa?
Creo que la respuesta es negativa, sin embargo, no pude encontrar una referencia para esto. También me interesarían las referencias para pruebas de incompletitud combinatoria de conjuntos de combinadores (puedo ver por qué el conjunto consiste en combinadores con una sola variable enlazada es incompleto, por lo que estos conjuntos deberían contener más que solo elementos de D ).
Respuestas:
[Expandiendo el comentario en una respuesta.]
Primero, solo una aclaración sobre el conteo de variables ligadas en un combinador (= término cerrado) . Interpreto la pregunta como preguntando sobre el número total de nombres de variables enlazadas distintas en t de modo que, por ejemplo, el término t = ( λ x . X ( λ y . Y ) ) ( λ x . Λ y . Y x ) cuenta como tener dos variables ligadas, a pesar de tener cuatro ligantes (es decir, abstracciones lambda). Esta forma de contar fue inicialmente un poco extraña para mí, ya que no es invariable bajot
Entonces, que sea la colección de todos los combinadores que se pueden escribir utilizando como máximo dos variables ligadas distintas, o de manera equivalente la colección de todos los combinadores cuyos subterms tienen como máximo dos variables libres.C
Teorema (Statman) : no está combinatoriamente completo.C
Parece que la prueba original de esto está contenida en un informe técnico de Rick Statman:
Statman define una colección de combinadores esencialmente isomórficos que él llama "HOT", por "hereditariamente de orden dos". El informe técnico en realidad muestra que el problema de la palabra (es decir, la igualdad ) para HOT aún no se puede decidir, a pesar del hecho de que no es combinatoriamente completo. Más tarde, Statman escribió un breve documento autónomo con la prueba de que HOT no se completa combinatoriamente en:β
fuente