¿Cuál es la menor función del cálculo de la lambda que genera todas las funciones de cálculo de la lambda?

Question

Sospecho que hay una buena probabilidad de que la respuesta a esto es desconocido y difícil (o al menos extremadamente tedioso), pero pensé que valdría la pena preguntar.

Es bien sabido que una de las funciones $K:=\lambda x.\lambda y.x$ y $S:=\lambda x.\lambda y.\lambda z.xz(yz)$ generar todas las funciones de cálculo lambda.

También es posible hacerlo con una sola función, como se ha mencionado aquí: Si definimos $U=\lambda x.xSK$, entonces podemos obtener la $K=U(U(UU))$, e $S=U(U(U(UU))$, y así todo.

También es posible hacer esto con $V:=\lambda x.xKS$, ya que el $S=VVV$, e $K=V(VVVVV)$.

Lo que quiero saber es, elegir un razonable noción de "longitud", ¿hay alguna manera que es más corto de $U$ o $V$? Digamos por ahora que la longitud es el número de apariciones de una variable, incluso cuando se les presenta, así, por ejemplo, $K$ tiene una longitud de 3, $S$ tiene una longitud de 7, y $U$ $V$ tienen cada una longitud de 12. (O es que hay una noción usual de "longitud", que ha sido estudiado?) Es posible hacer mejor que 12, y cuál es el camino más corto?

Lo que si permitimos que más de un generador y el total de las longitudes? A continuación, el conjunto habitual $\{S,K\}$ lo hace con 10. (Debemos agregar una penalización por el uso de más de uno? Bueno, supongo que podría, pero no lo voy a definir de esa manera aquí. Quiero decir, a menos que las personas han estudiado este problema y ya haciendo de esa manera...). Puede esta variante se realiza en menos de 10, y lo que es el más corto?

No creo que hay ninguna manera fácil de responder al "¿cuál es el más corto" la pregunta, pero estoy esperando tal vez que al menos si hay un camino más corto que alguien va a saber o encontrar.

Answer 1

Creo que esto está relacionado con encontrar un solo axioma de base para intuitionistic cálculo proposicional. Hay una página web por Ted Ulrich sobre el tema, que explica muchos de esos axiomas. Sin embargo, tratando de encontrar el menor solo axioma corresponde tratando de encontrar un combinador con el menor tipo (que se opone a su meta encontrar un combinador con el menor λ-cálculo de la expresión).

Edit: Se pueden tomar esos solo los axiomas y pedir Djinn (Haskell teorema de armario) para encontrar las funciones con sus correspondientes tipos. Por ejemplo, tomando uno de los primeros axiomas en Ted Ulrich página web, usted puede pedir Djinn:

Djinn> ? x :: ((p -> q) -> r) -> (s -> ((q -> (r ->  t)) -> (q -> t)))

y respuestas

x :: ((p -> q) -> r) -> s -> (q -> r -> t) -> q -> t
x a _ b c = b c (a (\ _ -> c))

Así que la expresión λazbc.bc(un(λy.c)) tiene el tipo, y es un candidato para un solo combinador de que usted está buscando.

(No es obvio cómo expresar S y K a partir de un combinador, pero puede ser recuperado de la prueba de que forumlas (p→(q→r))→((p→q)→(p→r)) y p→(q→p) puede ser derivada a partir de la única axioma.)

De esta manera, se podría generar muchas posibles combinadores y ver por cuánto tiempo. Más probable es que usted no encontrará la más corta, pero es posible encontrar algunos que son más cortos que los que usted describe. Si usted, háganoslo saber!

Answer 2

Me gusta $W = \lambda x.x K S K$ puesto que hace $K = W W W$ y $S = W (W W)$, aunque es más largo que sea $U$ o $V$.