技术笔记

上上周我去朱家尖玩。我们10点出发，直到下午3点才到。我们到酒店了以后，换上游泳衣，去东沙的沙滩玩。我跟妹妹先玩了一会沙子，然后爸爸带我去游泳。我去玩大浪，我都吃了好几口咸的海水。 玩好了以后，我又到了妈妈那边和妹妹一起玩沙子。

回到家洗好澡以后，妈妈带我们去吃海鲜。我们吃了海鲜炒饭，虾，海螺，扇贝。吃完饭妈妈带我和妹妹去买了两桶水。等爸爸吃完了以后，我和妹妹已经很累了，我们就回到了酒店。我和妹妹刷好牙就一起睡觉了。

我们第二天吃好早饭以后，就去大清山玩。我们到了大清山很高的地方，看下去的风景很美。我们在上山的地方，还看到了一个沙滩，我们下去玩了一会会。在下山的路上，我在车上看到下面的海是五颜六色的。有墨绿色，深蓝色，淡蓝色，还有黄色。我们下山了以后，就去了另外一个酒店。到酒店了以后，过了一会，阿姨给我们吃了西瓜，吃完后，我们放下行李，去吃海鲜面条。回到酒店，我们上楼。我们的房间打开窗户就能看到沙滩。

下午妹妹起床，我们换好泳衣，到楼下小沙滩去玩堆沙堡。在玩沙之前，我最近想出了一个很好玩的游戏，叫小猫露露。我是小猫露露，妹妹是白兔糖糖，爸爸是乌龟皮皮。我想到一个好主意，我们用干沙和湿沙围了一个圆圈。👨说把这个当做一个城堡。然后我们又用干沙和湿沙一起搭了一个很坚固的城堡。那时候快涨潮了，👨突然想到了一个好主意，👨说我们可以挖一条护城河。我们在挖护城河的时候，我看到那边有人也造了一个沙堡，他们因为没有护城河，很快就被潮水淹没了。潮水越涨越高，再过10分钟就要到达我们的地方了，我说我们必须得挖快一点啦！果真过了10分钟之后，海水真的到达我们的目的地了。看起来护城河跟大浪像在打仗一样，感觉很多大浪快被护城河运走了。最后实在更多大浪过来了，在没有淹之前，妈妈帮我们拍了我们自己造的城堡，我们拿上工具，摆了一个造型。城堡被淹没后，我们回酒店了。

第三天早上，我们到一楼，吃了好吃的。我们的饭都是一样的，我感觉超级好吃，里面有鸡蛋、西瓜、花生和咸菜，还有泡饭、馒头。吃完早饭后，我们收拾好行李，去观音法界。我看到了千手观音。还看到了很多的观音的雕像。我还看了一会电影。然后我们就回家了。

到家了以后，爷爷烧了香喷喷的饭菜，我吃了很多。真是一个愉快的暑假开始的第一个周末！

端午节的上午爸爸带我和妹妹去篮球场玩。我跟妹妹玩，爸爸投篮。玩好之后爸爸带我们走回家。

我们吃西瓜，吃完中饭妹妹睡午觉。

下午在家玩树莓派。爸爸先教我灯闪烁，又教我了声音传感器。我们一起录了视频，我扮了小猫露露，可可在外面玩。

吃晚饭，睡觉。

起床，今天早晨起来，我带爷爷去昨天那个篮球场，我自己玩，爷爷投篮。爷爷骑自行车带我回到家。吃早饭。妹妹起床有点生病。过了一会妈妈说带我去看琴。吃饭。回来。妹妹已经睡着了。妹妹起来后我们一起玩小猫露露的游戏。我扮演小猫露露，妹妹扮演白兔糖糖。妈妈跟我讲，明天要和糖糖姐姐一起去森泊水上乐园。

我很开心，马上要到我的生日了。这个端午节是我最爱的端午节！

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

过了一个周末，又到了该上学日子。十点钟，上完课老师准备带我们下去玩。到了下面我和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)