Cours 15: PCF

Expressivité

  • Pouvoir expressif du $λ$-calcul simplement typé sur les entiers de Church = polynômes + quelques fonctions (max, min, etc…) ⟶ pas très expressif

  • Expressivité du Système F = fonctions récursives totales dans l’artihmétique du second ordre (correspond à $PA_2$)

  • $λ$-calcul pur = Turing-complet (toutes les fonctions récursives)

Programming with Computable Functions (PCF)

(ch. 6 du Amadio-Curien)

Pour étendre le $λ$-calcul simplement typé:

  • soit on étend les types ⟶ Système F
  • soit on garde les types et on étend les règles de construction de termes + opérateur de point fixe ⟶ PCF

Introduit par Dana Scott et Plotkin dans les années 90 (pères de la sémantique dénotationnelle)

On utilise ce langage pour tester des choses (sémantique, etc…) avant de l’appliquer à de vrais langages de programmation

Présentation

\[Terms ≝ x \mid λx. M \mid MN\\ Types ≝ \underbrace{\omicron: bool \mid ι: int}_{\text{ground types}} \mid A ⇒ B\]

Pour un contexte $Γ$:

\[\cfrac{}{Γ ⊢ t: \omicron}\\ \cfrac{}{Γ ⊢ f: \omicron}\\ \cfrac{n ∈ ℕ}{Γ ⊢ n: ι}\\ \cfrac{Γ ⊢ M: \omicron \quad Γ ⊢ P, Q: \overbrace{g}^{\text{ground type: } ι \text{ or } \omicron}}{Γ ⊢ \texttt{if } M \texttt{ then } P \texttt{ else } Q: g}\]

Ex: Dans la règle, le fait de se restreindre aux types de base $g$ n’est pas une vraie restriction (c’est du sucre syntaxique), car tous les types sont de la forme $A_1 ⇒ ⋯ ⇒ A_n ⇒ g$, et:

\[λx_1^{A_1}, ⋯, x_n^{A_n}. \texttt{if } M \texttt{ then } P \, x_1 \, ⋯ \, x_n \texttt{ else } Q \, x_1 \, ⋯ \, x_n\] \[\cfrac{Γ ⊢ M: ι}{Γ ⊢ succ(M): ι}\\ \cfrac{Γ ⊢ M: ι}{Γ ⊢ pred(M): ι}\\ \cfrac{Γ ⊢ M: ι \quad Γ ⊢ N:ι}{Γ ⊢ M=N: \omicron}\]

Il ne reste qu’une chose pour être Turing-complet: la récursion.

Pour ce faire, on va utiliser un opérateur de point fixe:

\[\cfrac{Γ ⊢ M: A ⇒ A}{Γ ⊢ (Y_A \, M): A}\\ Y_A \, M ⟶ M \, (Y_A \, M)\]

Ex: l’addition

\[add \, x \, y = \begin{cases} y \text{ si } x=0 \\ add \, (x-1) \, (y+1) \text{ si } x > 0 \end{cases}\\ ⟹ add ≝ \underbrace{Y}_{A} \, \underbrace{(λf^{ι ⇒ ι ⇒ ι} \, x^ι \, y^ι. \texttt{if } x=0 \texttt{ then } y \texttt{ else } f \, (pred \, x) \, (succ \, y))}_{\underbrace{(ι ⇒ ι ⇒ ι) }_{≝ A}⇒ \underbrace{ι ⇒ ι ⇒ ι}_{A}}\]

NB: La sémantique vient de Scott et de Strachey ⟶ la programmation correspond à résoudre des équations mathématiques, avec des expressions qui décrivent des primitives de programmation. $λ$-calcul différentiel ⟶ équations différentielles.

Sémantique opérationnelle

On a de nouvelles règles de réduction, comme on a de nouveaux constructeurs.

\[Y_A \, M ⟶ M \, (Y_A \, M)\\ \texttt{if } true \texttt{ then } P \texttt{ else } Q ⟶ P\\ \texttt{if } false \texttt{ then } P \texttt{ else } Q ⟶ Q\\ pred \, (n+1) ⟶ n\\ pred \, 0 ⟶ 0 \\ succ \, n ⟶ n+1\\ n = n ⟶ true\\ n = m ⟶ false \text{ si } n≠m\]

Comme PCF est utilisé comme un langage de programmation, on donne une stratégie de réduction (même si on a la propriété de Church-Rosser).

Sémantique opérationnelle: weak call-by-name

Evaluation context:
\[E[] ≝ [] \mid (E \, []) \, M \mid \texttt{if } E [] \texttt{ then } P \texttt{ else } Q\\ succ \, (E []) \mid pred \, (E []) \mid E[] = M \mid n = E []\]
A program:

a closed term of ground type (it represents either a boolean or an integer).

Lemma: Let $M$ be a closed term of ground type. If $M$ has a redex, then there exists a unique evaluation context $E[]$ and redex $R$ s.t.

\[M = E[R]\]

Proof: Induction on $M$.

Beware: if $M = \underbrace{N_0 N_1}_{\text{of type } ι}$, then $N_0: A ⇒ ι$ and $N_1: A$, and we can’t use the IH, since it’s not a ground type.

Cette sémantique est weak parce qu’elle n’évalue pas en dessous des $λ$: si on a une fonction $λx^ι. (λg^ι. g^ι) \, 0$, on s’arrête, parce qu’on est face à une $λ$-abstraction.

Ex: Si

\[\underbrace{N_0}_{A_1 ⇒ ⋯ ⇒ A_n ⇒ ι} \, N_1 \, ⋯ \, N_n\]

alors si $n>0$, $N_0$ est une $λ$-abstraction (par les règles de typage).

Let $M$ be a program.

We define $M ⟶ N$ iff

\[M = E[R]\]

and

\[N = E[C]\]

where $R ⟶ C$

Lemma (Subject Reduction): If $Γ ⊢ \underbrace{M}_{\text{the subject}}:A$ and $M ⟶ N$, then $Γ ⊢ N:A$

Maintenant, on a un langage Turing-complet: une $M: ι → ι$ peut être n’importe quelle fonction récursive partielle.

Certains termes ne sont pas normalisables:

\[Y \, (λx^ι. succ \, (x^ι)) ⟶^2 succ \, Y \, (λx^ι. succ \, (x^ι)) ⟶ ⋯\\ Ω_A ≝ Y \, (λx^A. x^A) ⟶ (λx^A. x^A) Ω_A ⟶ Ω_A ⟶ ⋯\]

Autre exemple de fonction, définie sur les nombres pairs et divergeant sur les impairs:

\[Y \, (λf \, x. \texttt{if } x=0 \texttt{ then } 0 \texttt{ else if } x=1 \texttt{ then } Ω_i \text{ else } f \, (pred \, (pred x))\]

Catégorie des Complete Partial Orders (CPOs)

Pas de sémantique dans $Set$:

  • on a besoin d’une sémantique où toutes les fonctions ont des points fixes
  • comment interpréter les fonctions qui divergent dans $Set$?

On va introduire un ordre sur les fonctions: $f ≤ g$ ssi sur toute entrée, quand $f$ renvoie une valeur, $g$ renvoie la même.

$A$ is a CPO:

iff $A$ is a set with a partial order $≤$ s.t.

  • $⊥_A ∈ A$ is the bottom element
  • any monotonous non-decreasing chain $\lbrace x_i \rbrace ⊆ A$ has the supremum $∨_i \, x_i$

NB: on travaille avec des chaînes seulement et pas des ensembles dirigés, car pour les sémantiques probabilistes, seuls les sup de chaînes de fonctions mesurables sont assurés de rester mesurables.

$f: A ⟶ A$ is Scott-continuous:

iff

  • $f$ is monotonous and non-decreasing:

    \[\text{if } x ≤ y, \text{ then } f(x) ≤ f(y)\]

  • $f$ preserves the chain suprema:

    \[f(∨_i \, x_i) = ∨_i f(x_i)\]

Th (Tarski): Let $A$ be a CPO and $f: A ⟶ A$ a Scott-continuous function. Then

\[\bigvee_{n} f^n(⊥) \text{ is the smallest fixed point of } f\]

Catégorie des CPOs: $CPO$

  • Objects: CPOs

  • Morphisms: Scott-continuous functions

Proposition: $CPO$ is a CCC

Proof:

  • There are finite products (check that the projections are Scott-continuous)

  • Terminal object: $⊤$

  • Right adjoint of $A × _$: $A ⇒ _$

    • the order in $A ⇒ B$ is the pointwise order

Interprétation

$⟦ι⟧_{CPO} ≝$

  digraph {
    rankdir=BT;
    ⊥ -> 1, 2, 3, ⋯;
  }

NB: on l’appelle le “flat domain of $ι$”

La chaine des entiers ne convient pas, car on pourrait construire des fonctions non croissantes de $⟦ι⟧{CPO}$ and $⟦ι⟧{CPO}$

Lazy integers:

  digraph {
    rankdir=BT;
    ⊥ -> 0, "1*";
    "1*" -> 1, "2*";
    "2*" -> 2, "3*";
    "3*" -> 3, ⋯;
  }

mais n’est pas un CPO: la chaîne des entiers étoilés n’a pas de sup ⟶ ajouter $ω$, plus grand que tous les étoilés.

$⟦\omicron⟧_{CPO} ≝$

  digraph {
    rankdir=BT;
    ⊥ -> true, false;
  }
\[⟦A ⇒ B⟧_{CPO} ≝ \lbrace f:A ⟶ B \mid f \text{ Scott-continue} \rbrace\] \[⟦x_1: A_1, ⋯, x_n: A_n ⊢ M:B⟧: \underbrace{A_1 × ⋯ × A_n}_{\text{the product of CPOs, ordered componentwise}} ⟶ B\]

NB: au niveau du $λ$-calcul, l’interprétation n’a rien changé. On a juste l’information supplémentaire que les fonctions sont particulières : elles sont Scott-continues.

\[⟦Γ ⊢ succ(M): ι⟧ \, \vec{g} ≝ \begin{cases} n+1 &&\text{ si } ⟦Γ ⊢ M⟧ \, \vec{g} = n \\ ⊥ &&\text{ sinon} \end{cases}\] \[⟦Γ ⊢ \texttt{if } M \texttt{ then } P \texttt{ else } Q⟧ \, \vec{g} ≝ \begin{cases} ⟦Γ ⊢ P⟧ \, \vec{g} &&\text{ si } ⟦Γ ⊢ M⟧ \, \vec{g} = true \\ ⟦Γ ⊢ Q⟧ \, \vec{g} &&\text{ si } ⟦Γ ⊢ M⟧ \, \vec{g} = false \\ ⊥ &&\text{ sinon} \end{cases}\] \[⟦Γ ⊢ Y_A \, (M)⟧ \, \vec{g} = \bigvee_n (⟦Γ ⊢ M⟧ \, \vec{g})^n (⊥)\]

NB:

  • La $λ$-abstraction permet de construire des fonctions non linéaires (qui n’envoient donc pas $⊥$ sur $⊥$): $λx^ι. 1$
  • les contextes d’évaluation envoient $⊥$ sur $⊥$ ⟶ $⟦λx^ι. E[x^ι]⟧ \, ⊥$ (correspondent aux fonctions linénaires dans la sémantique de la logique linéaire).

Leave a comment