Navigation

Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter

Discussion: Types de fonction

  1. #1
    Membre à l'essai Avatar de tissebaos
    Homme Profil pro
    Développeur Web
    Inscrit en
    décembre 2017
    Messages
    9
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : Cameroun

    Informations professionnelles :
    Activité : Développeur Web
    Secteur : High Tech - Éditeur de logiciels

    Informations forums :
    Inscription : décembre 2017
    Messages : 9
    Points : 10
    Points
    10

    Par défaut Types de fonction

    Salut a tous

    je suis novice en programmation fonctionnelle et pour l'exercice ci-dessous
    J'ai essayer le 1. en écrivant ceci 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).

  2. #2
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 692
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 692
    Points : 2 957
    Points
    2 957

    Par défaut

    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.
    Du même auteur: le cours OCaml, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

  3. #3
    Membre à l'essai Avatar de tissebaos
    Homme Profil pro
    Développeur Web
    Inscrit en
    décembre 2017
    Messages
    9
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : Cameroun

    Informations professionnelles :
    Activité : Développeur Web
    Secteur : High Tech - Éditeur de logiciels

    Informations forums :
    Inscription : décembre 2017
    Messages : 9
    Points : 10
    Points
    10

    Par défaut

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

  4. #4
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 692
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 692
    Points : 2 957
    Points
    2 957

    Par défaut Difficile de donner une réponse universelle

    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
    Du même auteur: le cours OCaml, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

  5. #5
    Membre à l'essai Avatar de tissebaos
    Homme Profil pro
    Développeur Web
    Inscrit en
    décembre 2017
    Messages
    9
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : Cameroun

    Informations professionnelles :
    Activité : Développeur Web
    Secteur : High Tech - Éditeur de logiciels

    Informations forums :
    Inscription : décembre 2017
    Messages : 9
    Points : 10
    Points
    10

    Par défaut

    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.

  6. #6
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 692
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 692
    Points : 2 957
    Points
    2 957

    Par défaut

    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.
    Du même auteur: le cours OCaml, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

  7. #7
    Membre à l'essai Avatar de tissebaos
    Homme Profil pro
    Développeur Web
    Inscrit en
    décembre 2017
    Messages
    9
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : Cameroun

    Informations professionnelles :
    Activité : Développeur Web
    Secteur : High Tech - Éditeur de logiciels

    Informations forums :
    Inscription : décembre 2017
    Messages : 9
    Points : 10
    Points
    10

    Par défaut

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

  8. #8
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 692
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 692
    Points : 2 957
    Points
    2 957

    Par défaut erratum

    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.
    Du même auteur: le cours OCaml, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

  9. #9
    Expert éminent
    Avatar de Jedai
    Homme Profil pro
    Enseignant
    Inscrit en
    avril 2003
    Messages
    6 243
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Côte d'Or (Bourgogne)

    Informations professionnelles :
    Activité : Enseignant

    Informations forums :
    Inscription : avril 2003
    Messages : 6 243
    Points : 8 539
    Points
    8 539

    Par défaut

    Citation Envoyé par SpiceGuid Voir le message
    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 ?

  10. #10
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 692
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 692
    Points : 2 957
    Points
    2 957

    Par défaut

    Citation Envoyé par Jedai
    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
    Du même auteur: le cours OCaml, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

  11. #11
    Expert éminent
    Avatar de Jedai
    Homme Profil pro
    Enseignant
    Inscrit en
    avril 2003
    Messages
    6 243
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Côte d'Or (Bourgogne)

    Informations professionnelles :
    Activité : Enseignant

    Informations forums :
    Inscription : avril 2003
    Messages : 6 243
    Points : 8 539
    Points
    8 539

    Par défaut

    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.
    A moins que tu veuille dire que 2-Church est la plus petite solution qui ne puisse pas avoir un type différent ?

  12. #12
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 692
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 692
    Points : 2 957
    Points
    2 957

    Par défaut

    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.
    Du même auteur: le cours OCaml, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

+ Répondre à la discussion
Cette discussion est résolue.

Discussions similaires

  1. [OpenOffice][Tableur] macro "moyenne,minimun,ecart type" et fonction sous totaux
    Par karlakir dans le forum OpenOffice & LibreOffice
    Réponses: 0
    Dernier message: 21/03/2009, 18h04
  2. Conflicting types dans fonction déclarée
    Par Spikeuh dans le forum C
    Réponses: 8
    Dernier message: 22/06/2008, 17h49
  3. type et fonction return
    Par acacia dans le forum Débuter
    Réponses: 11
    Dernier message: 23/01/2008, 12h09
  4. Probleme sur un ensemble de type dans fonction
    Par jetgirl dans le forum Oracle
    Réponses: 4
    Dernier message: 19/02/2007, 13h04
  5. type de fonction
    Par sidahmed dans le forum C
    Réponses: 4
    Dernier message: 20/03/2006, 13h50

Partager

Partager
  • Envoyer la discussion sur Viadeo
  • Envoyer la discussion sur Twitter
  • Envoyer la discussion sur Google
  • Envoyer la discussion sur Facebook
  • Envoyer la discussion sur Digg
  • Envoyer la discussion sur Delicious
  • Envoyer la discussion sur MySpace
  • Envoyer la discussion sur Yahoo