Discussion :

[tissebaos]

Salut a tous

je suis novice en programmation fonctionnelle et pour l'exercice ci-dessous
J'ai essayer le 1. en écrivant ceci

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

λx.x

comme exemple de termes clos mais apparemment je suis complètement a coté alors j’espère si on peut m'aider pour cet exercice

merci !!!

Pour chacun des types suivants, donner un terme clos (sans variable libre) de ce type.
1. A → A
2. (A → A) → (A → A)
3. A → ((A → B) → B).

[SpiceGuid]

Bienvenue sur les forums de developpez.net

Bravo, la fonction identité (fun x -> x en OCaml par exemple) est la bonne réponse à la question n°1.
Pour la question n°3 pense à la règle de typage d'une application de fonction.
Pour la question n°2 ça ressemble à une spécialisation de la fonction identité donc tu serais bien inspiré d'appliquer la fonction identité au terme qui va bien.

[tissebaos]

merci pour ton aide SpiceGuid et pourrait tu m'indiquer un document de cours et exercice sur le sujet ?

[SpiceGuid]

C'est le lambda-calcul qui t'intéresse ?
Ou bien c'est la programmation fonctionnelle ?
Et surtout, vu du point de vue d'un développeur web, ça peut vite paraître ésotérique dans le sens où tu n'en n'auras jamais l'utilité au quotidien.

Je te proposes ceci (en français, pas d'exercices), mais ça n'est pas forcément ce que tu attends :
Gabriel.scherer.pdf

[tissebaos]

Merci beaucoup pour le lien de PDF c'est exactement ce que je recherchais. C'est le lambda calcul qui m’intéresse. En fait je suis aussi étudiant en informatique et je fait des cours sur le lambda calcul et le langage Haskell.

[SpiceGuid]

Alors dans ce cas Comprehensive Encoding of Data Types devrait t'intéresser aussi.
Ce papier utilise l'encodage de Scott pour représenter les types inductifs. Dans ce cas le typage ne permet pas de garantir la terminaison. Le langage est Turing-complet.
Alors que le précédent papier de Gabriel Scherer utilise l'encodage de Church pour représenter ces mêmes types inductifs. Dans ce cas le typage permet de garantir la terminaison. Mais le langage n'est plus Turing-complet.

[tissebaos]

Grand merci a toi pour cet aide je pouvait pas espéré mieux

[SpiceGuid]

Désolé, pour la question n°2, je n'ai pas tilté sur le coup.
Le type (A → A) → (A → A) est le type des entiers naturels ℕ en encodage de Church.
Du coup il y a une infinité de réponses possibles, la plus petite étant l'entier 2-Church.

[Jedai]

Désolé, pour la question n°2, je n'ai pas tilté sur le coup.
Le type (A → A) → (A → A) est le type des entiers naturels ℕ en encodage de Church.
Du coup il y a une infinité de réponses possibles, la plus petite étant l'entier 2-Church.

Pourquoi 2-Church ? Est-ce une notation particulière qui ne veux pas dire l'entier 2 dans l'encodage de Church ?
Parce qu'a priori 0 est encodé par 2 abstractions et une expression élémentaire alors que 2 est encodé par 2 abstractions, une expression élémentaire et 2 applications, non ?

[SpiceGuid]

Pourquoi 2-Church ?

C'est une notation particulière pour dire que ce n'est pas 2 dans un autre encodage (par exemple l'encodage de Scott).
Et oui c'est bien λf.λx.f(f x) ou alors fun f x -> f (f x) en ocaml.

Tandis que 2-Scott ça serait λλ.1(λλ.1(λλ.2)) où j'ai remplacé les variables par leur indice de De Bruijn.
Voir scott-encoding.pdf

[Jedai]

Ok, c'est bien ce que j'avais compris. L'encodage de Scott est intéressant, merci pour la référence, mais ma question était plutôt de pourquoi tu disais que 2-Church était la plus petite solution ayant ce type, a priori 0-Church est plus petit.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

λf.λx.x

A moins que tu veuille dire que 2-Church est la plus petite solution qui ne puisse pas avoir un type différent ?

[SpiceGuid]

C'est ce que je voulais dire, bien que zero-Church et un-Church soient aussi du type nat-Church, un générateur de type automatique les étiquette avec un type plus général :

Code ocaml :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
# fun f x -> x;;
- : 'a -> 'b -> 'b = <fun>
# fun f x -> f x;;
- : ('a -> 'b) -> 'a -> 'b = <fun>
# fun f x -> f (f x);;
- : ('a -> 'a) -> 'a -> 'a = <fun>
# fun f x -> f (f (f x));;
- : ('a -> 'a) -> 'a -> 'a = <fun>

@tissebaos: le type (A → A) → A → A est le même que (A → A) → (A → A) puisque l'opérateur de type → est associatif à droite.