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.