技术笔记

λ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

Hang out with mom and sister. I shared a lot of delicious food with my sister Tangtang and brother Lele.

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

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

随便打打

• moon
• midautumn
• mooncake

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

my first sentence

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

abc practice

abcde

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

words practice

Apple :apple:

Red :red_car:

Flower :white_flower:

House house

follow me

asdf

asadfg

teach my kids to learn abc

Today is really cool, Song Zhang teach me to use magnet to manage windows in mac pro when use the mateview, now i use emacs to write this article and typora to preview at right hand side.

Dev env are ready

• hhkb
• mateview
• mac pro
• tmux
• doom emacs
• typora

To learn some statistics

• prove of central limit theorem
• inference

What is the first class to teach guoguo

• some color words
• fruit words
• numbers

and record what she write, cool, maybe some years later, it will be meaningful.

minimu

My daught call me 'minimu', who is a little horse in the 'Princess Sofia' picture. So it's really a very cute name, i use it as the name of the dev toolbox.

the begin point

We want reach the auto coding state, first we need setup the begin point, it can go to the stable state. So what is the conditions of the begin point:

1. a tool for developers to quick learning
2. a lightweight, versatile, universal tool for developers

with the tool, we can learning all knowledge, and develop the automate coding tools, and the tools then can auto coding.

basic functions

• reading the source code of major programming languages
• writing the source code of major programming languages

emacs init

helm is the init plugin for emacs

1
2

M-x package-refresh-contents
M-x package-install-selected-packages