Cours 13: Théorème de Friedman: correction

Nouveau professeur pour cette seconde partie : Michele Pagani

Rappels

En λ-calcul simplement typé:

Types:
A,BσAB
Termes:
MxλxA.MMN
x1:A1,,xn:AnΓM:B x1:A1,,xn:Anxi:AiΓ,x:AM:BΓλxA.M:ABΓM:ABΓN:AΓ(MN):B

Sémantique dénotationnelle dans Set:

  • σX=XSet
  • ABχ=BXAX
  • x1:A1,,xn:AnM:BX=x1:A1X××xn:AnXBX

Exponentielle dans une CCC:

BA×AevBC×AΛ(f)×idf

Pour le λ-calcul simplement typé: on a besoin d’un objet réflexif dans une CCC

DDD

i.e.

tout élément de DD est aussi un élément de D.

NB: Set n’a pas d’objet réflexif, ce qui a poussé Dana Scott à définir ses domaines de Scott.

Modèles du λ-calcul

  • Set pour le simplement typé
  • Scott (CPOs et fonction Scott-continues): pour le λ-calcul typé et non typé
  • Stab (espaces cohérents et fonctions stables)

NB: sématnique dénotationnelle: pourquoi?

  1. Pour étudier la théorie équationnelle entre les termes:

    MNΓM=ΓN

    et parler “d’équivalences de programmes”, et de leurs propriétés partagées

  2. on peut introduire de nouvelles primitives dans le calcul:

    AB=!AB

    Exemples:

    • primitives probabilistes
    • computation quantique ⟶ on a besoin de la linéarité (non duplication, etc…)
  3. Compilation dans le langage haut-niveau vers un langage bas-niveau: Ex: Categorical Abstract Machine (a donné naissance à CamL) basée sur les catégories cartésiennes closes.

    Ex:

    (λx.x)y=evΛ(π22),π22

NB: dans cette seconde partie du cours, on se concentrera surtout sur 1 et 2.


Théorème de Friedman (1973)

Chap. 4 de AMADIO-CURIEN: “Domains and λ-calculi” ⟶ théorème 4.5.8

Th (Friedman, 1973): Let X be an infinite set and ⟦_⟧_X be the interpretation of the simply typed λ-calculus in the CCC Set associating X with the ground type. For any terms ΓM:A and ΓN:A, we have:

M=βηNMX=NX

NB:

  • on peut alors profiter du fait que travailler avec MX et NX est beaucoup plus agréable !

  • pas vrai pour n’importe quelle CCC

βη-equivalence

Congruence:
  • symetric
  • reflexive
  • transitive
  • and:

    M=βηNλx.M=βηλx.NM=βηNP=βηQMP=βηNQ
=βη:

is the smallest congruence over Λ s.t.

(λx.M)N=βηM{N/x}λx.Mx=βηM if xfv(M)

Definition de ⟦_⟧_X

x1:A1,,xn:AnM:Bx1:A1××xn:AnB
  • Variables ⟶ projections:

    x1:A1,,xn:Anxi:Ai=πi
  • λ-abstractions ⟶ use the adjonction:

    ΓλxA.M:AB=Λ(Γ,x:AM:B)=g(aM(g,a))
  • Application ⟶ pairing:

    ΓMN:B=evΓM:AB,ΓN:A=gM(g,N(g))

NB: on a fait un effacement dans le premier point, une duplication dans le dernier point.

Démonstration du théorème de Friedman

M=βηNcorrectionMX=NX M=βηNcomplétudeMX=NX

Correction

M=βηNcorrectionMX=NX

par induction sur la taille de la dérivation de =βη

Trois actions possibles :

(λx.M)N=βηM{N/x}xfv(M)λx.Mx=βηMM=βηM

Le plus délicat: premier cas: (λx.M)N=M{N/x}

Substitution lemma: Let Γ,x:AM:B and ΓN:A, then

ΓM{N/x}:B=gM(g,N(g))

Proof: By induction on M.


Attention: il y a une difficulté pour λx.Mx=M (contextes et types omis): on a besoin de montrer que (aΓ,x:AM:B(g,a)a)=(aΓM:AB(g,a)), via

Weakening lemma: si xfv(M):

Γ,x:AM:B(g,a)=ΓM:B(g)

Complétude

M=βηNcomplétudeMX=NX

Preuve de Friedman: définit

  • un modèle syntaxique S
  • une famille de relations {RA}ATypes

    • RAAXSet×AS
    • pour tout M: M:ASetRAM:AS
    • RA est fonctionnelle:

      dAXSet,N,NASdRANS et dRANSNS=NS
    • MS=NSM=βηN

NB: RA est un cas particulier de relation logique (logical relation) ⟶ ex: les candidats de réductibilité (on s’intéressait aux termes fortement normalisables au lieu de la relation de βη-équivalence) étaient des cas particuliers de relation logique unaire.

Leave a comment