Comment le calcul lambda capture-t-il exactement la notion intuitive de calculabilité?

J'ai essayé d'enrouler ma tête autour du quoi, pourquoi et comment du -calculus mais je ne suis pas parvenu à comprendre "pourquoi ça marche"? $\lambda$

«Intuitivement», j'obtiens le modèle de calculabilité de Turing Machines (TM). Mais cette -abstraction me laisse juste perplexe. $\lambda$

Supposons que les MT n'existent pas - alors comment peut-on être convaincu "intuitivement" de la capacité de -calculus à saisir cette notion de calculabilité. Comment le fait d'avoir un tas de fonctions pour tout et leur composobilité implique-t-il la calculabilité? Qu'est-ce que j'oublie ici? J'ai lu le document d'Alonzo Church à ce sujet mais je suis toujours confus et je cherche une compréhension plus "fictive" de la même chose. $\lambda$

soft-question computability lambda-calculus ho.history-overview intuition Doctorat
la source

Avez-vous le même problème avec les systèmes de réécriture et les grammaires? Dans le calcul lambda, les opérations de base sont assez simples: abstraction de fonction, application de fonction par substitution et le calcul est la normalisation bêta. En d'autres termes, je ne vois pas quel est votre problème avec le fait qu'il s'agisse d'un modèle de calcul raisonnable.

Kaveh

Je n'ai vu personne douter que les fonctions définissables du calcul lambda sont calculables. Historiquement, la question était de savoir si ce sont les seules fonctions intuitivement calculables, ce qui est un problème complètement différent de ce que vous semblez demander.

Kaveh

Une chose que j'ai trouvée utile était le livre de Raymond M Smullyan, "To Mock a Mockingbird" qui remplace les fonctions avec des oiseaux dans une forêt magique (et est une bonne lecture)

dspyz

Le livre de Smullyans traite de la logique combinatoire

Trismegistos

Réponses:

$\lambda$

$\lambda$ $\lambda$

Andrej Bauer
la source

Si le firewalking est aussi amusant que vous le dites, alors je dois l' essayer.

Radu GRIGore

Andrej, connaissez-vous une référence pour ceux-ci? Godel n'a pas accepté le modèle de Chruch comme capturant toutes les fonctions commutables, mais je ne me souviens pas avoir vu nulle part où il a critiqué le modèle beaucoup plus loin que cela. Pour autant que je sache, sa critique du modèle de calcul lambada de Church était comparable à sa critique de ses propres fonctions récursives générales de Godel-Herbrand.

Kaveh

Je pense que vous voulez K. Godel: "Quelques remarques sur les résultats de l'indécidabilité", dans Solomon Feferman, John Dawson & Stephen Kleene (éd.), Kurt Gödel: Collected Works Vol. Ii. Oxford University Press. 305-306 (1972). Voir books.google.si/…

Andrej Bauer

Vous programmez dedans! Jetez un œil aux encodages d'église . Vous pouvez voir à quel point toute l'arithmétique peut être effectuée, ce qui devrait probablement vous convaincre qu'elle est extrêmement puissante. J'aime cependant regarder les opérations sur les listes. Vous pouvez définir la plupart des structures de données en fonction d'une fonction qui effectue l'opération la plus importante.

Par exemple, un encodage d'une liste est la fonction de pliage qui se replie sur elle. Notez que ce n'est pas le codage de Church mais celui que j'ai obtenu des types et des langages de programmation de Percie. Les codages de paires de Church ne nous donnent pas de récursivité, nous devons l'ajouter en nous-mêmes avec une sorte de combinateur de récursivité.

donc une liste prend deux arguments, une fonction pour faire le pliage, et une valeur initiale pour se connecter au pli à un moment donné.

cons x xs = lam f. lam a. f x (xs f a)
nil       = lam f. lam a. a

maintenant nous pouvons définir une sommation avec une fonction d'ajout (voir les encodages d'église ci-dessus)

sum xs = xs add 0

nous pouvons faire plus et définir une fonction de carte

consApply f x xs = cons (f x) xs
map f xs = xs (consApply f) nil

si vous n'êtes toujours pas convaincu qu'il y a un calcul en cours ici et que vous voulez vous assurer que vous pouvez effectuer n'importe quel calcul, consultez le combinateur à virgule fixe . Cela me fait un peu mal à la tête de penser parfois, donc je ne suis pas sûr que je l'appellerais intuitif, mais si vous l'évaluez manuellement avec quelques arguments, vous pouvez voir ce qui se passe.

Jake
la source