Cardinalité du calcul lambda non typé intégré à Haskell

Question

Haskell accepte la définition du type suivant

data Lam = Func (Lam -> Lam)

qui entend représenter Termes lambda non typés . Par exemple, les booléens de Church sont de ce type

trueChurch :: Lam
trueChurch = Func (\x -> Func (\y -> x))
falseChurch :: Lam
falseChurch = Func (\x -> Func (\y -> y))

Le constructeur Func :: (Lam -> Lam) -> Lam a cette fonction inverse

lamUnfold :: Lam -> (Lam -> Lam)
lamUnfold (Func f) = f

et ces deux fonctions définissent un isomorphisme de type entre Lam -> Lam y Lam . Ceci est surprenant lorsque l'on regarde les cardinaux (les tailles) de ces types. À cause des booléens de Church ci-dessus, le cardinal de Lam est d'au moins 2, donc il y a plus d'éléments dans Lam -> Lam que dans Lam -> Bool . Ce dernier est le type de sous-types de Lam c'est-à-dire l'ensemble des puissances de Lam et par Le théorème de Cantor il a déjà beaucoup plus d'éléments que Lam fait. Comment l'existence du type Lam ne viole pas le théorème de Cantor ?

Une partie de la réponse pourrait se trouver dans théorie des domaines . Si je comprends bien, les éléments de Lam -> Lam ne serait pas l'ensemble des fonctions de la théorie des ensembles (qui sont plus grandes que Lam par le théorème de Cantor), mais seulement des fonctions continues. Si c'est le cas, quelle est la topologie qui définit cette continuité, et pourquoi les termes Haskell de type Lam -> Lam continue pour elle ?

Answer 1

La façon la plus simple de résoudre le paradoxe est probablement d'observer que toutes les fonctions (de la théorie des ensembles) ne sont pas représentables comme un terme lambda.

Chaque terme lambda valide peut être obtenu en choisissant un nombre fini de productions grammaticales dans un ensemble au plus dénombrable et en les appliquant au plus un nombre fini de fois. En tant que tel, l'ensemble de tous les termes lambda est une union dénombrable d'ensembles dénombrables, et donc il est lui-même dénombrable. 0 L'argument s'applique de manière transparente au type Haskell : la seule façon d'obtenir des termes de type Lam est d'invoquer le constructeur, et à tout moment, même si votre programme ne se termine pas, le constructeur ne peut avoir été invoqué qu'un nombre fini de fois. Ainsi, pendant toute son exécution, le programme peut rencontrer au maximum un nombre infini de différents types d'objets. Lam valeurs. En pratique, étant donné que la mémoire des ordinateurs est finie, le nombre de termes que vos programmes pourront effectivement manipuler sera un peu plus petit.

En théorie des ensembles, rien n'empêche de considérer une chaîne de bits obtenue en lançant une pièce de monnaie un nombre infini de fois comme une fonction valide : elle satisfait à la définition d'une fonction en théorie des ensembles, puisqu'elle attribue exactement un élément du codomaine (le résultat du lancer de la pièce) à chaque élément du domaine (la position dans la chaîne de bits). Mais étant donné que la construction d'une telle fonction nécessite de faire un nombre infini de choix arbitraires 1 il n'a pas de terme lambda correspondant.

(Plus formellement : ajouter un symbole f au langage de ZFC, et pour chaque nombre naturel n choisissez aléatoirement l'un des éléments suivants f ( n ) = 0' ou ' f ( n ) = 1' comme un axiome. Si nous choisissons un sous-ensemble fini d'axiomes définissant f il est évidemment cohérent avec ZFC qu'une fonction satisfaisant ce sous-ensemble fini existe. Par le théorème de compacité il est cohérent avec ZFC qu'une fonction f satisfaisant tous les axiomes existe.)

Il n'est pas nécessaire d'invoquer des concepts compliqués comme la continuité. Tout ce qui précède découle simplement de considérations sur la cardinalité elle-même tout en faisant attention à l'origine des termes lambda (et des termes de type en Haskell).

---

0 Ceci est techniquement faux si vous commencez avec un ensemble indénombrable de symboles pour les variables. Mais même dans ce cas, vous pouvez choisir un sous-ensemble infini de termes lambda auquel chaque terme lambda de l'ensemble complet sera -équivalent. Le problème disparaît également si vous utilisez les indices de Brun au lieu des symboles de variables.

1 En supposant que les tirages à pile ou face soient vraiment non déterministes et indépendants, bien sûr.

Answer 2

Si je comprends bien, les éléments de Lam -> Lam ne serait pas l'ensemble des fonctions de la théorie des ensembles (qui sont plus grandes que Lam par le théorème de Cantor), mais seulement des fonctions continues.

Oui, c'est une réponse courante au paradoxe apparent.

Plus généralement, les types sont des types, avec leur théorie logique (théorie des types), tandis que les ensembles sont des ensembles (fonctionnant comme dans la théorie des ensembles).

On est tenté d'interpréter les types comme des ensembles, c'est-à-dire de construire des modèles du lambda calculus dans des ensembles.

Je vous suggère de lire le document important "Polymorphism is not set theoretic" de Reynolds. Il montre que si vous avez des types "forall" comme dans le Système F, et que vous interprétez les fonctions comme des ensembles de la manière "évidente", vous obtenez une contradiction, par un argument similaire à celui que vous avez utilisé (celui de Cantor, en gros). En effet, Reynolds construit T ~= (T -> Bool) -> Bool .

Reynolds suggère en effet que l'une des options consiste à interpréter les types de fonctions comme un "sous-ensemble" de fonctions sur des ensembles, par exemple les fonctions continues que vous avez mentionnées.

Si oui, quelle est la topologie qui définit cette continuité ?

La topologie de Scott.

et pourquoi les termes Haskell de type Lam -> Lam continue pour elle ?

En gros, parce que toutes les opérations de base (abstractions lambda, applications, ...) sont continues, on obtient donc une composition d'opérateurs continus qui doit être continue.

Notez que la définition d'une sémantique formelle appropriée de Haskell est une tâche ardue. Même en se concentrant uniquement sur le système F, qui est beaucoup plus simple en comparaison, les modèles sont déjà assez complexes.

Vous pourriez commencer par le lambda calculus simplement typé et apprendre leurs modèles catégoriques : les catégories cartésiennes fermées (CCC). Travailler, par exemple, dans la catégorie des fonctions continues de Scott est un cas particulier de CCC. La structure générale des CCC vous fait comprendre qu'une fois que vous avez une structure de base (essentiellement du currying et peu d'autres choses), vous pouvez l'utiliser pour créer un modèle complet, interprétant n'importe quel terme lambda (typé).

Answer 3

Je ne suis pas convaincu qu'il y ait beaucoup d'intérêt à résoudre ce problème avec des notions de continuité de Scott. Haskell ne possède pas le type de sémantique formelle qui serait nécessaire pour ces arguments mathématiques. Il y a un peu de guerre philosophique sur le fait que cela signifie Haskell est cassé ou plutôt les théoriciens ne cessent de penser à des choses excessives pour le dire avec humour. JE NE SAIS PAS.

Certains problèmes montrent que l'argument de Cantor ne tient pas ici :

• On peut en douter, Lam n'a en fait que cardinalité 1 car il n'y a aucun moyen de distinguer deux valeurs. La seule chose que vous pouvez faire avec x :: Lam est d'appliquer la fonction contenue à une autre y :: Lam pour obtenir... encore un autre z :: Lam . Bien sûr, elles peuvent toutes avoir un code et un temps d'exécution différents, etc., mais elles sont toutes équivalentes en ce sens que vous n'obtiendrez jamais de valeurs Haskell qui auraient un WHNF différent de manière observable ou quelque chose comme ça.
  Cela ne règle pas exactement la discussion, car vous pourriez facilement ajouter un autre constructeur et avancer un argument similaire, mais ce ne serait pas aussi simple.

• Les fonctions Haskell ne sont pas en fait des fonctions, en particulier elles ne sont pas totales. Je pourrais aussi écrire un "isomorphisme"

  f :: Bool -> Maybe Bool
  f False = Just True
  f True = Just False
  
  f' :: Maybe Bool -> Bool
  f' (Just False) = True
  f' (Just True) = False
  f' Nothing = f' Nothing

  Bonne chance pour trouver un x tal que f (f' x) se termine par une valeur non égale à x . (Bien sûr, il n'y aura pas de fin. du tout para x = Nothing mais maintenant bonne chance pour résoudre le problème de halte...)