Lambda-calcul et fonctions récursives

marco · July 2020

Bonjour,

Soit $t$ un terme du lambda-calcul, qui n'a pas de variable libre. Soit $k$ un entier naturel fixé, on suppose que pour un $k$-uplet d'entiers (du lambda-calcul) $e_1, \dots, e_k$, le terme $(\dots ((t)e_1)e_2)\dots e_k$ se réduit par $\beta$-réductions en un terme $t_2$ auquel on ne peut plus appliquer de $\beta$-réduction. Est-ce que $t_2$ est alors nécessairement un entier (du lambda-calcul) ?

Si $t_2$ est un entier (qui dépend de $e_1,\dots, e_k$) pour tout $e_1, \dots,e_k$, alors est-ce que la fonction qui à $e_1,\dots, e_k$ associe $t_2$ est récursive primitive (ou alors seulement récursive) ?

Merci.

Foys · July 2020

Soit $\pi_0 := \lambda x_0 \lambda x_1 ... \lambda x_k .x_0$ et soit $u$ un lambda terme en forme normale qui n'est pas un entier (exemple: $u:=\lambda x \lambda y .x$; on a pour tous entiers de Church $n$ et tous termes $a$, $((n)I)a >a$ mais $((u)I)a>I$ avec $I:= \lambda x .x$, "$>$" désignant la cloture transitive de la beta-réduction). Alors $t:=(\pi_0) u$ fournit un contre-exemple à ta première question.

Foys · July 2020

Pour la deuxième question, c'est seulement "récursive" (le lambda-calcul est Turing-complet et il y a un terme réalisant la fonction d'Ackermann).

marco · July 2020

Merci Foys.

christophe c · July 2020

Salut marco,
ta première question revient exactement à demander si une application de $\N^k$ dans $E$ "programmable" va faire qu'obligatoirement $\N\subset E$. Et évidemment la réponse est non.

Pour ta deuxième question, sache que pour toute fonction récursive $f$, il existe un terme $t$ du $LC$ tel que pour tous entiers $n,p$ :

$f(n) =p$ si et seulement si $t*(n') $ se beta-réduit à quelque chose et, en plus, c'est à $p'$

en notant $x'$ l'entier du LC associé à $x$ et en notant $*$ l'unique opération binaire "appliqué à" du LC

À noter aussi que si tu t'intéresses à ce sujet, il y a tout un tas de petites nuances (entre la réduction gauche, la droite, la "comme on veut", la confluence" (qui dit que ça revient souvent au même mais pas toujours, etc, sans compter la beteEta réduction qui applique une sorte d'extensionalité, etc.).

christophe c · July 2020

Pour les gens qui ça intéresse, je rappelle ce qu'est le lambda calcul:

1/ on a une infinité de lettres (qui jouent toutes le même rôle)

2/ on a une opération binaire que l'on note espace (ou on colle) appelée "application de .. à .."

3/ On a un signe abstracteur $\lambda$, qui ne peut que se placer à gauche d'une lettre (ie pas d'un mot) pour la lier.

Pour la suite sachez que c'est par économie typographique: $[\lambda x u]$ est juste une manière plus courte d'écrire $x\mapsto u$.

Le règles d'exécution "one-step" sont:

1/ renommer les variables liées pour ne pas subir de capture indue

2/ $[\lambda x (uv)] t $ peut passer à $([\lambda x u] t)([\lambda x v] t)$

3/ $[\lambda xy] t$ peut passer à $y$ quand $y$ est une lettre AUTRE QUE $x$

4/ $ [\lambda x x] t$ peut passer à $t$

5/ $[\lambda x[ \lambda yu] \ ] t$ peut passer à $[\lambda y ([\lambda xu]t) \ ] $

Bref, ça représente ce que vous attendez tous de la réécriture de $[x\mapsto MOT] (argument)$ obtenue en remplaçant toutes les occurrences libres de $x$ de MOT par $argument$

L'entier de Church $n$ est la fonction qui compose $n$ fois son argument.

Par exemple $3f = (f\circ f\circ f)$

où $a\circ b$ est "évidemment" défini comme étant $[\lambda x[\lambda y[\lambda z (x(yz))] ] ]$

A remarquer qu'un entier appliqué à un autre est l'opération usuellement appelée "puissance": $n(p) = p^n$

marco · July 2020

Merci Christophe. En fait, j'ai lu les 3/4 (ou les 2/3) du livre de Krivine. Mais sans me poser de questions (en vérifiant seulement les démonstrations). Donc, j'ai oublié. :-D