TD4 : Modèles du 𝜆-calcul

Énoncé

EX 1

1.

Supposons que $u ≝ (𝜆x. s)t ⟶_𝛽 v ≝ s[x:=t]$.

• $⟦u⟧ = i(r(V \mapsto ⟦s⟧𝜌[x:=V]))⟦t⟧ = ⟦s⟧𝜌[x:=⟦t⟧]$

• $⟦v⟧ = ⟦s[x:=t]⟧ = ⟦s⟧𝜌[x:=t]$ à démontrer

Par induction structurelle sur $s$ :

• $s = y∈Var$ :

  $⟦u⟧ = ⟦s⟧𝜌[x:=⟦t⟧] = 𝜌x:=⟦t⟧ = \begin{cases} ⟦t⟧ \text{ si } y=x
  𝜌(s) \text{ sinon} \end{cases}$

Sinon : on procède de la même manière.

2.

Supposons que $u ≝ (𝜆x. vx) ⟶_𝜂 v$ avec x∉fv(V).

\[⟦u⟧𝜌 = ⟦𝜆x. vx⟧𝜌 \\ = r(V \mapsto ⟦vx⟧𝜌[x:=V]) \\ = r(V \mapsto i(⟦v⟧𝜌[x:=V])(V)) \\ = r(i(⟦v⟧𝜌)) \quad \text{ car } x∉fv(V) \\ = ⟦v⟧𝜌\]

EX 2

1.

\[⟦𝜆x. x⟧ = r(V \mapsto ⟦x⟧𝜌[x:=V]) \\ = r(V \mapsto V) \\ = \lbrace (𝛽, b)∈D \mid b∈𝛽 \rbrace\]

---

\[⟦𝜆x, y. x⟧ = r(V \mapsto ⟦𝜆y. x⟧𝜌[x:=V]) \\ = r(V \mapsto r(V' \mapsto ⟦x⟧𝜌[x:=V, y:=V'])) \\ = r(V \mapsto \lbrace (𝛽, b)∈D \mid b∈V \rbrace) \\ = \Big\lbrace (𝛽', b')∈D \mid b'∈\lbrace (𝛽, b)∈D \mid b∈𝛽' \rbrace \Big\rbrace \\ = \Big\lbrace (𝛽, (𝛽',b))∈D \mid b∈𝛽\rbrace\]

---

\[⟦𝜆x. x x⟧ = r(V \mapsto ⟦xx⟧𝜌[x:=V]) \\ = r(V \mapsto i(⟦x⟧𝜌[x:=V])⟦x⟧𝜌[x:=V]) \\ = r(V \mapsto i(V)(V)) \\ = \lbrace (𝛽, b)∈D \mid b∈i(𝛽)(𝛽) \rbrace \\ = \Big\lbrace (𝛽', b')∈D \mid b'∈\lbrace b \mid ∃𝛽 ⊆_{fin} 𝛽'; (𝛽,b)∈𝛽' \rbrace \Big\rbrace \\\]

2.

CPO : immédiat.

On vérifie que $i \circ r = id_{[D ⟶ D]}

Mais $r \circ i ≠ id$ :

Contre-ex :

\[A = \lbrace 0, 1 \rbrace \\ x = \lbrace (\lbrace 0 \rbrace, 0) \rbrace\]

Alors

$(\lbrace 0, 1 \rbrace, 0)∈r\circ i (x)$, d’où $r\circ i (x) ≠ x$

EX 3

1.

\[𝔹 ≝ \lbrace tt, ff \rbrace\] \[C(𝔹) = \lbrace \lbrace tt \rbracett, \lbrace ff \rbrace\rbrace\]

$C(𝔹&𝔹)$ :

  graph {
    tt1 -- tt1;
    tt1 -- tt2;
    tt2 -- tt2;
    ff1 -- ff2;
    ff1 -- ff1;
    ff2 -- ff2;
    tt1 -- ff2;
    tt2 -- ff1;
  }

1.

Si $(𝛼,b)∈ \vert B_∞ ⟹ B_∞ \vert$,

il existe $N$ tq

\[\begin{cases} 𝛼 ∈ C_{fin}(B_N) \\ b∈ \vert B_N \vert \end{cases}\]

alors

$(𝛼,b)∈ \vert B_N ⟹ B_N \vert ⊆ \vert B_{N+1} \vert ⊆ \vert B_∞ \vert$

Inclusion :

On prend le max des indices $n, m, p$ qui interviennent dans la déf de la première relation binaire.