Lambda-calcul et fonctions récursives
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.
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.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
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$ :
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.).
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$
Tu dois être un des seul au monde à en être capable, c'est assez éreintant, il livre de véritables preuves formelles sans sauter d'étape souvent JLK