技术笔记

Posted on In

  • extensions to the simple typed λ-calculus

  • product types

  • sum types

  • fixed point

  • product types A×B = tuples, pairs, records, unit

  • sum types A+B = disjoint unions

  • fixed point construct = recursion

syntax, typing rules, reduction rules

  • product types

A₁×A₂ pair (e₁, e₂): A₁×A₂ projections fst e snd e

type A::= ⋯ | A×A expr e::= ⋯ | (e₁, e₂) | fst e | snd e value v::= ⋯ | (v₁, v₂)

typing rules

Γ ⊢ e₁:A₁ Γ ⊢ e₂:A₂ ----------------------------×I Γ ⊢ (e₁, e₂): A₁×A₂

Γ ⊢ e: A₁×A₂ ----------------------------×E₁ Γ ⊢ fst e:A₁

Γ ⊢ e: A₁×A₂ ----------------------------×E₂ Γ ⊢ snd e:A₂

reduction rules for (e₁, e₂) fst e snd e 1) "eager" (e₁, e₂)≠ a value 2) "lazy" (e₁, e₂) = a value

rule1 e₁ ↦ e₁' ----------------------------fst (e₁, e₂) ↦ (e₁', e₂)

e₁ -> -> -> v₁

rule2 e₂ ↦ e₂' ----------------------------snd (v₁, e₂) ↦ (v₁, e₂')

e₂ -> -> -> v₂

(v₁, v₂)

rule3 e ↦ e' ----------------------------fst fst e ↦ fst e'

e -> -> -> v

----------------------------fst' fst (v₁ v₂) ↦ v₁

----------------------------snd' snd (v₁ v₂) ↦ v₂

"lazy strategy"

(e₁, e₂) a value

rule4 e ↦ e' ----------------------------fst fst e ↦ fst e'

rule5 e ↦ e' ----------------------------snd fst (e₁, e₂) ↦ e₁

e₁ -> -> -> v₁

  • generalized product types

type A::= ⋯ | A₁ × A₂ × ⋯ × Aₙ|unit expr e::= ⋯ | (e₁, e₂, ⋯ eₙ) | projᵢ e | () value v::= ⋯ | (v₁, v₂)

Γ ⊢ eᵢ:Aᵢ 1≤i≤n ----------------------------————-×I Γ ⊢ (e₁, e₂, ⋯ eₙ): A₁×A₂× ⋯ × Aₙ

Γ ⊢ e: A₁×A₂× ⋯ × Aₙ ----------------------------×E Γ ⊢ projᵢ e:Aᵢ

n = 0 <- null-ary case

()

  • sum types a value of A₁ + A₂ => contains a value of A₁ or a value of A₂ not both.

e:A₁ e:A₂ :A₁+A₂ :A₁+A₂

inl_A₂ e:A₁+A₂ inr_A₁ e:A₁+A₂

inleft: injection left inright: injection right

e:A₁+A₂ e:A₁ or e:A₂

λx:A₁+A₂ e

=> case analysis e=>inl_A₂ v e=>inr_A₁ v

case e of inl x₁ e₁ | inr x₂ e₂

type A::= ⋯ | A₁+A₂ expr e::= ⋯ | inl_A e | inr_A e | case e of inl x e | inr x e

Γ ⊢ e:A₁ --------------------------- +Iₗ Γ ⊢ inl_A₂ e: A₁ + A₂

Γ ⊢ e:A₂ --------------------------- +Iᵣ Γ ⊢ inr_A₁ e: A₁ + A₂

Γ ⊢ e: A₁ + A₂ Γ, x₁:A₁ ⊢ e₁:C Γ, x₂:A₂ ⊢ e₂:C --------------------------------------------- case Γ ⊢ case e of inl x₁ e₁ | inr x₂ e₂ : C

if e then e₁ else e₂

  • reduction rules

inl e inl v value v::= ⋯ | inl_A v | inr_A v

e ↦ e' --------------------inl inl_A e ↦ inl_A e'

e ↦ e' --------------------inr inr_A e ↦ inr_A e'

e ↦ e' ----------------------------------------case case e of inl x₁ e₁ | inr x₂ e₂ ↦ case e' of inl x₁ e₁ | inr x₂ e₂

--------------------------------------------------case' case inl_A v of inl x₁ e₁ | inr x₂ e₂ ↦ [v|x₁]e₁ inr_A v ↦ [v|x₂]e₂

A::= ⋯|A×A|uint|A+A bool = unit + unit true = inl_unit () false = inr_unit ()

if e then e₁ else e₂ = case e of inl x₁ e₁ | inr x₂ e₂ — x₁ x₂ unit dummy variable

A::= ⋯|A₁+A₂+ ⋯ + Aₙ n ≥ 2 n = 0 A::= ⋯|void expr::=⋯|abort e

  • extension fixed point

  • fixed point construct (for recursive func) ≠ fixed point combinator in untyped λ = primitive construct

expr e::= ⋯|fix x:A.e

fix x:A.e = fixed point of λx:A.e A→A

f(x) = 2 - x: int -> int f(1) = 1

Γ, x:A ⊢ e:A -------------------------fix Γ ⊢ fix x:A.e

λx:A.e (fix x:A.e) = fix x:A.e

↦ [fix x:A.e | x]e

------------------------------fix fix x:A.e ↦ [fix x:A.e | x]e

fix x:A.e under CB-value

fix f:A→B. λx:A.e ↦ [fix f:A→B. λx:A.e | f] λx:A.e ↦ λx:A[fix f:A→B. λx:A.e | f] e

Posted on In

recursive function construct

fun f x. e = valid expr in λ-calculus syntatic sugar

eq m n = true or false

fac = fun f n. if eq n 0 then 1 else mult n (f (pred n))

FAC = λf.λn. if eq n 0 then 1 else mult n (f (pred n))

f: partial impl of factorial 3×2×1 f(3) f(2) f(1)

FAC: improved impl of factorial

give me f(3)

n = 4 f (pred 4) = f(3) f(4)

FAC f(3) -> f(4)

FAC = λf.λn. if eq n 0 then 1 else mult n (f (pred n)) fac₀ = FAC (λn. omega) ——- 1 fac₁ = FAC (FAC (λn. omega)) ——- 2 × 1 fac₂ = FAC³ λn. omega ——- 3 × 2 × 1 ... facₙ = FAC n+1 λn. omega

suppose fac = correct impl of factorial fac ~= FAC fac = correct impl of factorial

    fac is a fixed point of FAC

    f(x) = x
    f(x) = 2 - x  f(1) = 2 - 1 = 1

fixed point combinator: fix takes F, returns a fixed point of F.

fac = fix(FAC) FAC(fix(FAC)) = fix(FAC)

Posted on In

λx.x ≡ₐ λy.y => without names λx.x = λ.0 λx.λy.x y ≡ λ.λ.1 0 λx.x(λy.x y) λ.0(λ.1 0)

de bruijn expression

M ::= n n ::= 0 | 1 | 2 | ... e ≡ M

λx e₁ e₂ λx /
e₁ e₂

λx(x(λy x y)) (λz x z)

λ(0(λ 1 0)) (λ 1 0)

substitutions using de bruijn expr

λ-calculus → operational sematic → substitutions

(λx e)e' ↦ [e'|x]e (λ M) N ↦ σ(M, N) - find 0 in M - replace it with N

λλ(λ 2 1 0) (λ 0) - redex ↦ λλσ(2 1 0, λ 0) ↦ λλ1 0 λ 0

λλ (λ λ3 2 1 0) (λ 0) ——– M: λ 3 2 1 0 ↦ λλ λ2 1 (λ 0) 0

e₁: (x(λy x y)) e₂: (λz x z)

σ₀(M, N) 0->N σ₀(λM, N) = λσ₁(M, N) - find 1 in M - replace it with N

σᵢ(M,N)

σᵢ(M₁ M₂, N) = σᵢ(M₁,N) σᵢ(M₂,N) σᵢ(λM,N) = λσ_i+1(M,N) σᵢ(i, N) = N σᵢ(j, N) = j j < i σᵢ(j, N) = j - 1 j > i

σᵢ(i, N) = N closed N has free varibles σᵢ(j, N) = j j < i

de bruijin shifting

σᵢ(i,N) = N -> has free vars failed

σ₀(λλ...λi,N) = λλ...λσᵢ(i,N)

N - local var - same free variables λλ...λ σᵢ(i,N) = N - free variables in N - shift by i

λλ(λ 0)(λ 2 1 0) 21 0 ↦λλ(λ2 1 0) 21

λλ(λ(λ 1) 0)(λ 2 1 0) λλ( λ (λ 2 1 0)) (λ 2 1 0)

λλ( λ (λ 3 2 0)) (λ 2 1 0)

σᵢ(i,N) = τ₀ⁱ(N) - find free vars in N - shift by i

      >= 0 => free

τ₀ⁱ(λ N) = λτ₁ⁱ(N) free var >= 0 free var >= 1 τ₁ⁱ(λ N) = λτ₂ⁱ(N)

τⱼⁱ(N) = find free vars in N free vars ≥ j shift by i

τⱼⁱ(N₁ N₂) = τⱼⁱ(N₁) τⱼⁱ(N₂) τⱼⁱ(λ N) = λτⱼ₊₁ⁱ(N) τⱼⁱ(k) = k + i k = free var k≥j τⱼⁱ(k) = k k ≠ free var k<j

Posted on In

There are two kinds of semantics for a programming language.

  • dynamic semantic, which is opeartional semantic
  • static semantic, which is type system

Type safety

  • progress if ∅ Γ e:A then either e:value, or e ↦ e'
  • preservation if Γ ⊢ e:A, e ↦ e' then Γ ⊢ e':A

"well typed expr can not go wrong"

e:A e:value e ↦ e' e':A

Prove of type preservation

If Γ ⊢ e:C and e ↦ e', then Γ ⊢ e':C If e ↦ e', then Γ ⊢ e:C implies Γ ⊢ e':C Proof By rule induction on e ↦ e'

case)

case)

...

case) λx:A.e v ↦ [v|x]e Γ ⊢ (λx:A.e)v:C Γ ⊢ [v|x]e:C

We consider the most challenge case to prove. 

1
2
3
4
5
Γ, x:A ⊢ e:C
----------------
Γ ⊢ λx:A.e:A→C  Γ ⊢ v:A
--------------------
      Γ ⊢ (λx:A.e)v:C

Γ ⊢[v|x]e:C - NTS

recursive to prove: If e ↦ e', then Γ ⊢ e:C implies Γ ⊢ e':C

so we introduce substitution lemma

If Γ ⊢ e:A and Γ,x:A ⊢ e':C, then Γ ⊢ [e|x]e':C Proof By rule induction on Γ, x:A ⊢ e':C By Curry-Howard isomorphism, it's equal to prove If Γ,x:A ⊢ e':C then (Γ ⊢ e:A implies Γ ⊢ [e|x]e':C)

case 

1
2
3
4
5
6
7
8
9
10
--------------------Var  e'=x, C=A
Γ, x:A ⊢ e':C

Γ ⊢ e:A                        assumption

Γ ⊢ [e|x]e':C
  = [e|x]x
  = e:C


case 

1
2
3
4
5
6
7
8
9
10
11
    y:C ∈ Γ
--------------------Var  e'=y≠x
Γ, x:A ⊢ e':C
         y:C
Γ ⊢ e:A                        assumption



Γ ⊢ [e|x]e':C
  = [e|x]y:C
  = y:C

If Γ,x:A ⊢ e':C then (Γ ⊢ e:A implies Γ ⊢ [e|x]e':C)

case 

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

Γ, x:A, y:C₁ ⊢ e'':C₂
-------------------- → I where C=C₁→C₂
Γ, x:A ⊢ e':C
         λy:C₁.e'':C


Γ ⊢ e:A                        assumption
Γ, y:C₁ ⊢ e:A                  by weakening
Γ, y:C₁ ⊢ [e|x]e'':C₂          by IH on the premise


Γ, λy:C₁ ⊢ [e|x]e'':C₂     <- NTS
Γ ⊢ λy:C₁[e|x]e'':C₁→C₂     <- NTS
Γ ⊢ [e|x]λy:C₁.e'':C        <- NTS
Γ ⊢ [e|x]e':C                <- NTS

Posted on In

什么圆圆，什么圆圆，挂天边。 月儿圆，月儿圆，挂天边。 什么圆圆，什么圆圆，甜又甜。 饼儿圆，饼儿圆，甜又甜。 什么圆圆，什么圆圆，甜又甜。 什么圆圆，什么圆圆，笑开颜。 脸儿圆，脸儿圆，笑开颜。

随便打打

  • moon
  • midautumn
  • mooncake

Posted on In

Yesterday my father took me to Maojiabu to play. I ran into many uncles there, and I ran into my grandfather there. Grandpa played cards nearby. Uncle Youzhi also played the violin and gave me a thumb piano. I had a great time playing with sister Maomao.

keyword practise

  • violin
  • youzhi
  • great

Posted on In

my first sentence

I played on the trampoline yesterday and I was very happy!

abc practice

abcde

Posted on Edited on In

The syntax is

1
e ::= x | λx.e | e e

free variables

FV(e) - Free variables of expression e. 

1
2
3
FV(x) = {x}
FV(e₁ e₂) = FV(e₁) ∪ FV(e₂)
FV(λx.e) = FV(e) - {x}

examples 

1
2
3
FV(λx.x) = {}
FV(x y) = FV(x) ∪ FV(y) = {x, y}
FV(λy.λx. x y) = {}

free variables just like global varibles in C programming language.

substitution

λx.e e₁ - when β reduction

[e₁|x]e - means locate x in e, and then substitute x with e₁ 1. e=x [e₁|x]x=e₁ 2. e=y y≠x [e₁|x]y=y 3. [e|x]e₁ e₂ = [e|x]e₁ [e|x]e₂ 4. [e|x]λy.e = ???

case 1, 2, 3 is easy

The last case

1st property of bound variable

λx. ... "rename" "x" name of this bound variable

λx.x ≡ₐ λy.y λx.λy.x y ≡ₐ λy.λx.y x ≡ₐ - α equivalance or α conversion

[e'|x]λx.e = λx.e - we can rename x to other variable, the substitution has no effects.

2nd property of bound variable [e'|x]e = (_) if z ∈ FV(e'), z will be still free after substitution. [e'|x]λy.e = where x≠y λy.[e'|x]e if y∈FV(e'), after substitution, something bad happens, y has been bound.

example: (λx.(λy.x)) y [y|x]λy.x = λy.[y|x]x = λy.y - y been bound!

we should rename y, maybe z. (λx.(λz.x)) y = [y|z]λz.x = λz.y - y still free.

this is called variable capture

we need capture avoiding substitution

[e'|x]λy.e = λz.[e'|x] e

"rename y to z"

if z∈FV(e), suppose we have e=z, FV(e) = {z} λy.z -> λz.z - z is bound

1
[e'|x]λy.e = λz.[e'|x][y⟷z]e

Posted on Edited on In

words practice

Apple :apple:

Red :red_car:

Flower :white_flower:

House house

follow me

asdf

asadfg

0%