lambda calcul en prolog

[blili]

Salut a tous,

Je suis nouvelle ici et j'aimerai bien avoir une aide sur l'implémentation du lambda calcul d'ordre supérieur en prolog.

Je suis débutante en Prolog et je commence a connaitre le lambda calcul, j'aimerai bien faire une implémentation du lambda calcul en prolog.

Je voudrais avoir de l'aide juste pour commencer, j'aimerai bien voir un exemple qui marche et puis je pourrais faire la suite après.

Merci a tous.

[Trap D]

Voici un lien intéressant je pense :
http://www.complang.tuwien.ac.at/ulr...edit/ISO-Hiord
Il y a tout dedans.

[blili]

Merci Pour votre réponse.

Mais ce que je cherche vraiment est comment implémenter les types du lambda calcul du second ordre en prolog?

Comment représenter les lambda terme en prolog ainsi que la bêta-réduction et la alpha-conversion?

[Trap D]

Tout de même je pense que l'étude attentive de ce module prolog peut être très intéressante.

[blili]

Merci votre réponse.

Peut être je dois donner plus de précision sur ce que je cherche exactement:

comment représenter les types du lambda calcul du second ordre en prolog?

comment représenter les termes du lambda calcul du second ordre en prolog?

[gorgonite]

question intéressante... as-tu déjà commencé ? histoire qu'on t'aide dans ta réflexion


aussi passage, un petit lien qui devrait te donner un début de piste
http://www.sfs.uni-tuebingen.de/~fr/...ris-lambda.pdf

[blili]

Justement, je veux de l'aide pour commencer.

Merci pour le document, mais ce que je cherche exactement est l’implémentation du lambda calcul du "second ordre" en prolog.

Merci d'avance.

[gorgonite]

que veux-tu exactement, avec une telle implantation ?

vérifier le type d'une expression ?
afficher l'arbre de décomposition permettant d'atteindre ce type ?
juste faire la ré-écriture (alpha et beta conversion) ?
tenter d'inférer le type via des contraintes ? (sachant que le cas général est indécidable)

as-tu au moins chercher une définition formelle du lambda-calcul du second ordre ? sais-tu le comparer avec SystemF ?


telle quelle, ta question ressemble plus à "Pouvez-vous faire mon devoir ?", et la réponse sera "Non, mais on peut t'aider à le finir..."

[blili]

Ce que je veux exactement est:

1)avoir une représentation des types du lambda calcul du second ordre en prolog.

2)donner le type d'une expression(si on a un lambda terme en entrée, afficher en sortie le lambda terme typé correspondant).

3)programme qui permet de calculer l'alpha conversion.

Merci d'avance.

[blili]

Bonjour à tous,

peut être je dois donner plus de précision concernant ce que je cherche:

Quelle structure de données il faut utiliser pour représenter les lambda terme en entrée pour calculer le type d'une expression? si on choisit les listes, alors comment on peut le faire?

Quelle structure de données il faut utiliser pour représenter les différents types du lambda calcul du second ordre (système F)?

et enfin, quelles étapes à suivre pour appliquer la substitution (toujours dans le système F)?

Merci à tous.

[gorgonite]

un petit exemple qui devrait t'aider...
http://www.ling.gu.se/~sl/typechecker.ps


essaies de nous montrer quelque chose, si tu veux plus que des liens informatifs


au passage, si jamais tu veux t'investir plus loin dans ce sujet, regardes ceci :
http://www.cs.cmu.edu/~rvirga/work/thesis.pdf

[blili]

Je vous remercie pour votre réponse.

En fait ce que je veux exactement est:

1)A partir d'un lambda terme (contenant des sous termes typés) pouvoir calculer le type général du lambda terme( çàd calcul des types des termes complexes).

2)Comment représenter la substitution du système F en prolog, càd, comment traduire ceci en prolog:

-si t est une variable,
alors t[x/u]=u si x=t et t sinon

-si t est une application (vw)alors
t[x/u]=v[x/u]->w[x/u]

-si t est une abstraction (lambda y.v) alors
t[x/u]=lambda y.(v[x/u]) si x est différent de y
t sinon