技术笔记

又过了一个星期，到周末了。这个周末，是一个清明节。 第一天，👩早晨在家给我们洗衣服，👨带我和妹妹下面玩一号🐹和二号🐹的游戏。 到了中午，👩跟我说好要去吃肯德基，吃完肯德基带我看电影。到了中大银泰的肯德基店里，妈妈在座位上点菜，肯德基那边有个小的玩具厂，然后我在里面玩的非常开心。我玩的滑滑梯，过了一会我走出了玩具厂，然后在座位上等了一会，我等得非常饿，洗完手后，👩让我在座位上再等一会，过了一会儿，👩把饮料还有炸鸡翅，薯条都拿了过来。吃完以后，👩给我们又点了一份蛋挞，吃完我们就去看电影了。看完了电影，妈妈告诉我去糖糖姐姐家玩。 到了糖糖姐姐家，糖糖姐姐带我去楼顶上看了兔子，还有乌龟，我还喂了兔子苹果和青菜。然后下了楼，我们一起玩了一个小房子。玩了很长的时间，妈妈说要吃饭了。吃完饭后，糖糖姐姐给我吃了一个棒棒糖。我们两个人又开始一起玩了。 第二天到了，吃完早饭，我们就去爬山了。我们爬城隍山。我跟糖糖姐姐一起爬山。到了山顶，我们又往前继续走，那边又很多的石头，就像一座山，我们一起爬上去又爬下来。👨带着妹妹也一起爬上爬下。 中午到了，我们去西湖银泰吃了莜莜面。吃完面，我们去外面打了会游戏，吃了个冰淇凌。然后我们就回家了。 下午我们再玩了一会一号🐹和二号🐹。 今天早晨，吃完早饭，妈妈去把我们上周的书还掉，爸爸带着我和妹妹又去玩了一号🐹和二号仓鼠。 下午我们在家里休息。 晚上我想再和爸爸去玩一号🐹和二号🐹😂。 这个清明节，虽然没有去成三亚，但是还是非常非常愉快，这个清明节简直是我最喜欢的一个清明节了。

过了一个周末，又到了该上学日子。十点钟，上完课老师准备带我们下去玩。到了下面我和cmh一起玩。我们拿着玩沙工具一起去找贝壳，找好贝壳我们要上去吃饭了。吃完饭，我们有个餐后活动，我还是和cmh一起玩自己带来的玩具，玩的非常开心。 中午老师说收玩具，我们要去睡觉了，午觉起床后，我们下楼要准备吃点心了。吃完点心老师说带我们下去再玩一会。玩好上来我们就马上要放学了。 放学后，我和cmh一起在外面学轮滑。cmh教我怎么练走路，我学的非常高兴，因为我已经学会了她教我的走路方法。 晚上吃完晚饭，妈妈带我和妹妹一起去滑🛴。 第二天，第三天，第四天，第五天，每天cmh都在教我不一样的滑轮方法，我很快就学会了这些方法，然后我就滑得飞快飞快😊。这个滑轮方法，是cmh教会了我，我很高兴她能教会我这么多的滑轮方法，我现在做什么事情都可以用🛼滑过去，然后完成那样事情。不知道下个礼拜二cmh还会教我什么事情可以用🛼做呢?

有一天晚上爷爷说：“明天你起床一定会白茫茫的一片。” 然后我就上床去睡觉了。 第二天我起床，发现爷爷说的一模一样。外面真的是一片白茫茫的。 然后我很快穿好衣服，从床上起来了。刷好牙，洗完脸，吃好饭，看完动画片就赶紧穿好外套，下楼去了。 下面实在太冷了，我跟奶奶准备开始堆雪人。第一步，拿一小块雪，然后把它滚起来，要滚出两个雪球，一个大一点，一个小一点，大的在下，小的在上，然后把它们合起来。 然后摘两片🍂，粘在小的球上，再找两根🌿，插在大球的两侧偏上的位置。再摘四片树叶作为钮扣。再拿个铁桶作为它的🎩，⛄就堆好啦！这次堆雪人真高兴呀！

过年

小孩小孩你别馋，过了腊八就是年。 腊八粥，喝几天，哩哩啦啦二十三。 二十三，糖瓜粘，二十四，扫房子。 二十五，冻豆腐，二十六，去买肉。 二十七，宰公鸡，二十八，把面发。 二十九，蒸馒头，三十晚上熬一宿。 初一初二满街走，满街走！ Happy new year!

第一天我们参加第一个项目喂🦒吃🥕。 喂完长颈鹿总台说可以入住了。 然后我们就坐了一辆车到了我们住的小木屋酒店。 到了酒店后，妈妈说妹妹睡觉，爸爸抱着妹妹去睡了。 然后妈妈就带着我出去，到了儿童乐园去玩滑滑梯。 晚上妈妈带我们去吃自助餐了。 第二天早晨，又吃了一次自助早餐，吃完自助餐后，妈妈说去喂小鸟了。 我们看见了好多动物，有孔雀，我们还喂了小浣熊和小鸟。 然后我们就回酒店去整理行李了。在去回酒店的时候，妈妈非得让我们回去整理行李，而我却要去儿童乐园玩，妈妈没办法只能带着我和妹妹一起去玩了。我自己在儿童乐园里面玩来玩去。然后爸爸带着妹妹玩了一个跷跷板。 我玩了好多次最长的滑梯。然后我们玩玩了最后一次滑滑梯，我还想在玩一次的时候，妈妈叫我们回去吧，然后我们就回到了酒店里面。 然后我们整理完行李，坐着车来到停车场。在回去的路上要一个小时才能到家，因为我们只能回家才能吃饭，我们又饿又累，我和妹妹就睡着了。睡觉起来我们离我们家很近了。妈妈在车上点了个外卖，然后我们就回到了家，妈妈点外卖的时候有点晕，她回到了家就吐了。 我们所有的外卖都到了，妈妈是一碗米线，而我和爸爸是老娘舅的饭。妹妹没有饭吃，钥了几勺我吃不完的饭，到了晚上，我们在外婆家吃了饭。我们还没有从外婆家回来的时候，爷爷奶奶已经回到了家里。爷爷回来的时候给我带了一只鸟笼还有一只机器狗。 第二天我放学回来，爷爷给我带了两只小鸟，我给她们娶了名字，蓝色的叫瑟瑟，绿色的叫小花朵。这次我的旅程非常愉快！上次我和爸爸妈妈去了龙之梦玩，也看到了许多好玩的小动物，下次我还要跟着爸爸妈妈去个更好玩，更有趣的地方！我的妹妹的名字叫可可，我叫俞果。

以前的冬天我和爷爷奶奶一起在小区玩堆雪人和打雪仗的游戏。整个冬天我跟爷爷奶奶每天早晨一起在小区里玩的很开心，很开心。 今天选择javascript作为我的学习编程语言，写了减一函数：

1
2

let 冰雪花=x=>x-1
冰雪花(22)

ref e ↦* ref v ↦ l l location ———–> v !e ↦ !l ↦ v e := e' ↦* l := v ↦()

to implement iarray int ref A

ref(int -> int) index: any int initialized 0 l ↦ v:A

new:unit->iarray

new ()↦*iarray access: iarray-> int-> int index element

a[i]

update: iarray->int-> int->unit index value

new: λ_:unit. ref(λi:int.0) iarray:ref(int->int)

access: λa:iarray. λi:int. !a i int->int

update

correct answer

update: λa:iarray.λi:int.λn:int

let x=e in e' = (λx:A.e') e

• 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

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)

λ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.