技术笔记

上幼儿园真开心

Posted on 2022-03-13 In guo

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

堆雪人

Posted on 2022-01-31 Edited on 2022-03-06 In guo

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

过年

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

去长颈鹿庄园玩

Posted on 2022-01-08 Edited on 2022-01-09 In guo

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

冰雪花朵

Posted on 2021-12-12 In guo

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

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

references

Posted on 2021-11-21 In tapl

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

simple extensions

Posted on 2021-11-21 In tapl

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

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

Γ ⊢ 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₂

Γ ⊢ 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

fixpoint

Posted on 2021-11-21 In tapl

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)

de bruijn index

Posted on 2021-11-21 In tapl

λ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

Hilton Garden Inn Hangzhou Lu'niao travel

Posted on 2021-10-16 In guoguo

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

type safety

Posted on 2021-10-01 In tapl

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) λx:A.e v ↦ [v|x]e Γ ⊢ (λx:A.e)v:C Γ ⊢ [v|x]e:C

We consider the most challenge case to prove.

Γ, 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

--------------------Var  e'=x, C=A
Γ, x:A ⊢ e':C

Γ ⊢ e:A                        assumption

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

case

    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


Γ, 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