Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

Le lambda‑calcul, purement et en général
Auteur Message
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17727
Mar 26 Mar 2019 08:44
Message Re: Le lambda‑calcul, purement et en général
Copie du message Re: Les logiques : notes en vrac.

--------------- %< ---------- >% ---------------

La notation de la substitution de a par b (substituting b for a, in English) dans e, varie selon les auteurs, de ces différentes manières :

  • E[b/a]
  • [b/a]E
  • E[a := b]
  • E[a ↦ b]
  • [a ↦ b]E

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17727
Mar 17 Sep 2019 23:48
Message Re: Le lambda‑calcul, purement et en général
Hibou a écrit : 
[…]

Il complète en ajoutant une production pour les constantes, dont on pourra supposée qu’il en est des prédéfinies.

Code : 

<Exp> ::=
<identifier> |
<constant> |
(<Exp>) |
<Exp><Exp> | -- application
λ<identifier>.<Exp> -- abstraction


Il ajoute deux commentaires, qui introduisent aussitôt deux […]

En fait, les constantes sont un OVNI dans le lambda calcul, je ne vois même pas quel sens elles peuvent y avoir quand elles ne valent que pour elles‑mêmes.

Quand elles sont des noms pour des lambda‑expressions, alors elles sont simplement des variables liées et je ne comprend alors pas pourquoi un terme spécifique est introduit pour en parler.

Ces constantes, je crois ne pas les comprendre. Elles n’existaient pas dans la définition d’origine par Church.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17727
Mar 17 Sep 2019 23:50
Message Re: Le lambda‑calcul, purement et en général
Les langages fonctionnels sont inspirés du Lambda Calcul. Ils ne permettent pas les substitutions autrement que par effet de bord, c’est à dire qu’ils ne le permettent que d’une manière non‑fonctionnelle. C’est surprenant quand on sait l’importance de la substitution dans le Lambda Calcul.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17727
Jeu 19 Sep 2019 14:22
Message Re: Le lambda‑calcul, purement et en général
Un combinateur, c’est une lambda‑expression fermée, c’est à dire qui n’a pas de variable libre. Je reviendrai sur ce point des variables libres.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17727
Jeu 19 Sep 2019 14:25
Message Re: Le lambda‑calcul, purement et en général
L’alpha‑conversion et l’eta‑conversion, sont parfois aussi nommées alpha‑réduction et eta‑réduction.

Je préfère parler d’alpha‑conversion et d’eta‑réduction. Quoique parler d’eta‑réduction peut prêter à confusion si on pense à l’évaluation par beta‑réduction … c’est cependant quand‑même plus une réduction qu’une conversion. L’alpha‑conversion n’a rien d’une réduction, je ne vois pas de bonne raison de l’appeler alpha‑réduction.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17727
Ven 20 Sep 2019 12:42
Message Re: Le lambda‑calcul, purement et en général
C’est Turing qui en 1936, a démontré que sa machine de Turing et le lambda‑calcul de Church, permettent d’exprimer les mêmes calculs : ils ont la même expressivité. Les deux ont été présentés environ en même temps, la même année.

Un certain Schönfinkel avait introduit la notion de curryfication des fonctions, en 1924 (ça ne s’appelait alors pas encore « curryfication »), avant que Curry ne l’introduise indépendamment plus tard.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
cron