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 : 17495
Lun 21 Juil 2014 18:50
Message Le lambda‑calcul, purement et en général
Ce sujet parlera du λ‑calcul en général, et c’est pourquoi il ne réutilise pas le sujet des références sur SML.

L’écriture et les règles de réécritures sont autant importantes dans le λ‑calcul qu’elles le sont dans la logique en général, et il existe justement une très étroite relation entre logique et λ‑calcul. La première chose présentée, sera alors la syntaxe.

λ Calculus (allisons.org)

Il donne cette syntaxe pour le pure lambda calcul, celui des mathématicien(ne)s :

Code : 

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


On peut définir une chose dont les éléments font référence à d’autres choses préalablement définies (la syntaxe pour associer un symbole à une expression, n’est pas donnée), mais on a pas de point d’entrée, puisque pour définir un nouveau symbole, il faut bien qu’il y ait des symboles préexistants.

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 notions : l’application et l’abstraction. Les opérations sur les expressions du λ‑calcul, seront présentées plus tard.
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17495
Mer 23 Juil 2014 07:47
Message Re: Le lambda‑calcul, purement et en général
Deux très bons liens et un troisième lien plus inattendu, moins généraliste que les deux premiers, mais important, car concernant les opérations que j’ai promis d’aborder plus tard. Le premier lien est vers un PDF, les deux suivants sont vers des pages web classiques.

Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17495
Mer 17 Sep 2014 14:33
Message Re: Le lambda‑calcul, purement et en général
Je recopie ici un message posté dans Les logiques : notes en vrac (page 6), et ajoute une référence plus bas.

‑‑‑‑‑‑‑‑‑‑ %< ‑‑‑‑‑‑‑‑‑‑‑‑‑‑‑ >% ‑‑‑‑‑‑‑‑‑‑

Les axiomes du lambda‑calcul dans un diaporama présentant les grandes lignes de l’inférence de types. C’est de troisième main, ces axiomes sont repris et repris… une source parmi d’autres.

An Introduction to Type Inference (cs.columbia.edu) [PDF], Alfred V. Aho, Novembre 2011.

À la diapositive № 5.

Citation : 
Axioms of lambda calculus
  • α‑equivalence: change of bound variable name, e.g., λx.E = λ y.E[y/x]
  • β‑equivalence: application of function to arguments, e.g., (λx.E)y = E[y/x]
  • η‑equivalence: elimination of redundant lambda‑abstractions, e.g., if x is bound in E, λx.(Ex) = E

Traduction a écrit : 
Axiomes du lambda‑calcul
  • α‑équivalence : renommage de variable liée, ex. λx.E = λ y.E[y/x]
  • β‑équivalence: application de fonction à des arguments, ex. (λx.E)y = E[y/x]
  • η‑équivalence: élimination de lambda‑abstractions redondantes, ex. si x est liée dans E, λx.(Ex) = E


C’est simplifié, au moins pour le premier axiome, qui nécessite de s’assurer qu’une variable liée n’est pas renommée avec le nom d’un variable pré‑existante dans l’expression. […]

‑‑‑‑‑‑‑‑‑‑ %< ‑‑‑‑‑‑‑‑‑‑‑‑‑‑‑ >% ‑‑‑‑‑‑‑‑‑‑

À la fin du message d’origine, je parlais de la nécessité d’approfondir. Voici justement un article d’une encyclopédie de philosophie en ligne, qui le fait : Lambda Calculi (iep.utm.edu). Ou la version imprimable [1], plus agréable à lire à mes yeux : Lambda Calculi (version imprimable).


[1]: Pas sur papier hein, plutôt en PDF Oops, n’a fait une bêtise . Rien ne vaut jamais un gaspillage inutile.

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 : 17495
Lun 15 Fév 2016 00:43
Message Re: Le lambda‑calcul, purement et en général
L’application d’une fonction, est parfois nommée « combinaison » en français ou “combination” en Anglais. C’est au moins le cas pour HOL4, qui a une primitive nommée mk_comb, pour créer un terme qui est l’application d’une fonction à un paramètre.

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 : 17495
Lun 15 Fév 2016 03:36
Message Re: Le lambda‑calcul, purement et en général
Notez qu’une instanciation (terme pas encore introduit ici jusque maintenant), n’est rien d’autre qu’une substitution. Dans son sens le plus courant dans les langages informatiques en général, c’est une substitution d’une valeur à une variable (substitutions multiple, si nécessaire). En particulier, on parle d’instanciation dans le lambda‑calcul typé, quand on substitue un type à une variable de type. L’instanciation a un sens plus général par ailleurs.

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 : 17495
Jeu 30 Mar 2017 01:55
Message Re: Le lambda‑calcul, purement et en général
Une valeur monadique, est une valeur accompagnée d’un état ou d’annotations (prenez l’expression qui vous parle le plus), et d’une fonction ou d’un opérateur (prenez le mot que vous préférez) interprétant cette valeur dans cet état ou cette valeur annotée.

Deux fonctions primitives s’appliquent aux monades : bind — souvent notée >>= — et return — parfois notée unit. Plus à ce sujet, peu après.

Les fonctions bind et return, doivent vérifier trois règles :

  • Identité à droite : return x >>= f ≡ fx
  • Identité à gauche : x >>= return ≡ x
  • Associativité : (x >>= f) >>= g ≡ x >>= (f >>= g)

Bind, prend une valeur annotée pour en tirer une valeur non‑annotée, quand c’est possible, car ça ne l’est pas toujours. Si on note la valeur annotée, [x], et la valeur non‑annotée, x, alors bind permet de relier une fonction f: x -> [y] et une fonction g: y -> [z] pour obtenir [z]. Elle permet de prendre [y] venant de f et de passer le y qu’elle en tire, pour le passer à g pour finir avec [z], le résultat de l’expression.

Imaginons un cas en particulier, ou [y] est renvoyé par une fonction de division, et que l’annotation que peut porter [y], et de savoir si oui ou non, [y] est le résultat d’une division par zéro. Si c’est le résultat d’une division par zéro, alors il n’existe pas de y qui puisse être passé en argument, de par exemple une fonction d’addition. C’est pour cette raison que bind est nécessaire et qu’il n’en existe pas de définition unique. Pour rester concis, je ne dis pas ce que bind peut renvoyer quand il n’est pas possible d’extraire un y de [y].

Bind ne doit pas être confondue avec la composition de deux fonctions. Il n’existe en effet qu’une seule définition mathématique de la composition de deux fonctions, tandis qu’il n’existe pas de définition unique de bind, il y en a une pour chaque type monadique défini (les deux sont définis ensemble). Et bind ne renvoi pas une fonction, mais une valeur monadique, ce qui la ferait plutôt qualifier de fonction d’application.

Attention à ne pas confondre le type unit de SML avec unit, l’alias du return monadique. Le return monadique, est également différent du return des langages les plus courants. Attention à ne pas confondre le bind monadique avec le bind de JavaScript, même si on peut leur trouver des similitudes sémantiques.

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 : 17495
Jeu 30 Mar 2017 11:44
Message Re: Le lambda‑calcul, purement et en général
Les monades, un terme mathématique, sont parfois appelées “computation expression” ou “computation builder”.

Une définition de l’interface abstraite des monades, en SML :

Source SML : 

signature MONAD = sig
type 'a monad
val return: 'a -> 'a monad
val bind: 'a monad -> ('a -> 'b monad) -> 'b monad
end


La fonction return, permet de définir une fonction monadique. Une fonction monadique, est une fonction retournant une valeur monadique, mais dont le paramètre est une valeur « normale ». La fonction bind, permet de lier deux fonctions monadiques, d’où son nom. Mais comme dit précédemment, attention à ne pas prendre bind pour une fonction de composition générale.

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 : 17495
Ven 27 Oct 2017 05:41
Message Re: Le lambda‑calcul, purement et en général
Pour un définition de alpha‑équivalence, voir : Re: Les logiques : notes en vrac.

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 : 17495
Mar 26 Mar 2019 07:33
Message Re: Le lambda‑calcul, purement et en général
Voir aussi le message « Re: Les logiques : notes en vrac », pour la mention d’un livre important.

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 : 17495
Mar 26 Mar 2019 08:33
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 me semble que les constantes pourraient être définies comme les paramètres d’une expression englobante, ou plutôt de plusieurs expressions englobantes, comme les paramètres multiples sont exprimés par curryfication.

Image
Hibou57

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