Discussion:Lambda-calcul simplement typé

Normalisation forte ou forte normalisation

Il me semble que mettre l'adjectif « forte » avant le substantif « normalisation » est un anglicisme (même s'il m’est arrivé de l’employer ). On dit bien la manière forte, le sexe fort etc. Il me semble donc que nous devrions employer normalisation forte dans notre encyclopédie francophone. Pierre Lescanne (discuter) 21 juin 2024 à 12:15 (CEST)

J'ai consulté mon Grevisse aux sections §397 et §398. Il est assez clairement favorable à l’utilisation de l'expression normalisation forte. --Pierre Lescanne (discuter) 21 juin 2024 à 12:27 (CEST)

Effectivement, j'utilise souvent des anglicismes (surtout quand les ressources en français sont peu nombreuses) et je ne me rends pas forcément compte, merci. J'ai corrigé. JeanCASPAR (discuter) 21 juin 2024 à 12:37 (CEST)

Merci pour la correction.

Cette source francophone utilise la terminologie « normalisation forte ».

N. B. On dit cependant « fortement normalisable ». --Pierre Lescanne (discuter) 21 juin 2024 à 18:20 (CEST)

Un cours que j'ai suivi utilisait « fortement normalisant ». JeanCASPAR (discuter) 22 juin 2024 à 12:22 (CEST)

Produit de types

Le lambda calcul simplement typé (stricto sensu) correspond à la logique implicative minimale. C'est ainsi, à mon avis qu'il faudrait l'introduire et citer Howard, W., The formulas--as--types notion of construction, in Essays on Combinatory Logic, Lambda Calculus, and Formalism, Seldin, J. P. and Hindley, J. R. ed., Academic Press (1980), pp. 479--490.

Le type produit ne devrait venir qu'après l'introduction de l’extension du lambda-calcul et doanc après y avoir ajouté les opérateurs $\langle \_,\_\rangle$, $\pi _{1}$ et $\pi _{2}$ Pierre Lescanne (discuter) 29 juin 2024 à 12:25 (CEST)

Merci pour l'article, étant donné qu'il est fondateur, il vaudrait sans doute mieux le citer. Pour la multiplication, j'ai beaucoup hésité. Les livres centrés sur le lambda-calcul typé (donc pas le Barendregt, dont je ne suis pas sûr de la pertinence par rapport aux autres, ni, dans une moindre mesure, le Krivine, qui parle aussi beaucoup du lambda-calcul non typé) avaient l'air divisées entre présenter le fragment implicatif uniquement, ou présenter le fragment implicatif/multiplicatif d'abord et le fragment additif ensuite. J'avais 3 idées :

1. D'abord présenter le fragment implicatif et la réduction, puis une section sur le fragment multiplicatif et une sur le fragment additif.
2. Faire comme dans l'article actuellement : présenter le fragment implicatif et multiplicatif ensemble, puis la réduction, et après le fragment additif.
3. Présenter tout le lambda-calcul d'un coup, puis la réduction.

Et dans tous les cas, faire Curry-Howard après, d'une traite.

J'ai écarté l'option 3 parce que le fragment additif nécessite les conversions commutatives qui embrouillent un peu les idées, même si je trouve que la section correspondante dans la présentation actuelle n'est pas forcément très bien.

Entre l'option 1 et l'option 2, je me suis dit que ça faisait un peu lourd de faire une présentation complète du fragment implicatif, puis de revenir dessus et de tout redéfinir deux fois de suite. Je pense qu'il est néanmoins pertinent de séparer les fragments multiplcatifs et additifs.

Qu'en penses-tu ? JeanCASPAR (discuter) 2 juillet 2024 à 00:10 (CEST)