技术笔记

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

Sort and align are useful when do format.

Sorting

Sorting in Emacs works a lot like the command line utility sort. All commands sort lines, except the lone paragraph command.

M-x sort-lines sorts in ascending order, but if you call it with a universal argument it will reverse the sort order.

Aligning

Text alignment in Emacs encompasses both justification and columnated text. In fact, the alignment engine in Emacs is so sophisticated that it is able to automatically align and justify code based on regexp patterns.

Emacs’s align commands are powerful and useful if you often deal with unformatted text or code. The only downside is that you have to wade through the complex mode to repeat the alignment process more than once on a single line.

Sorting and aligning are alway use regex to match, then use rules to do some modify, it is also the main idea of formatting code.