技术笔记

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

随便打打

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

When new programming languages appear, a major mode for Emacs that does basic syntax highlighting and indenta- tion appears almost immediately. But i think auto format is more important, no matter what indent you write, code always tobe same format, that means you don't need care about indent at all.

TAB: Indenting the Current Line

Disabling tab characters

If you dislike the use of tab characters and if you prefer whitespace, customize the variable indent-tabs-mode.

Changing the amount of indentation

The variable tab-width controls how many characters of spacing each tab uses. It also controls the amount of whitespace to use if you disabled indent-tabs-mode.

Indenting Regions

In an ideal world, pressing TAB with an active region is all you need to re-indent it. Unfortunately, Emacs might not support that, or in some programming languages it is not physically possible to determine the correct indentation. Pressing TAB follows most of the same rules as line indentation: Emacs attempts to indent according to the indent-line-function and it falls back on simply inserting TAB characters (or whitespace, if you disabled indent-tabs-mode).

Typing C-M- explicitly indents the region; for some modes it works identically to TAB and in others it doesn’t. If you give the command a numeric argument, it will indent the region to that column (i.e., the number of characters) and Emacs will also use your fill prefix (if you have one) and fill the text accordingly. C-M- is occasionally useful as it respects your fill prefix. However, if you want to indent a fixed number of columns, you should use C-x TAB.

C-x TAB explicitly indents the region a certain number of columns. It also takes negative and numeric arguments. However, if you don’t pass an argument, Emacs will en- ter an arrow-key-driven indentation mode that lets you interactively indent the region with S-<left> and S-<right>.

There are several built-in tools – and just as many third-party ones – in Emacs that expand text. All of them serve a slightly different purpose, but the goal is to minimize typing and maximize automation.

• Abbrev
• DAbbrev
• Hippie expand
• Skeletons
• Tempo
• YASnippet
• Autoinsert

Abbrev

DAbbrev and Hippie Expand

DAbbrev is not smart. It looks at other words in your buffer and it attempts to complete the word at the point to one of those. That does not make it useless – it is still useful – it’s just that Hippie Expand is so much better.

To use Hippie Expand effectively, you should replace DAb- brev as the two – though it’s possible to use both – really don’t complement one another at all. Add this to your init file to switch to Hippie Expand:

(global-set-key [remap dabbrev-expand] 'hippie-expand)

Hippie Expand expands more than just words. The variable hippie-expand-try-functions-list is an ordered list of expan- sion functions Hippie Expand will call with the text at the point when you call M-/.

What I like most about Hippie Expand is the file name com- pletion. It works exactly like your shell’s TAB-completion: you type M-/ and Hippie Expand will try to complete the filename or directory at the point. If you ever find yourself inserting absolute paths or relative file names in code, config- uration files or documentation — Hippie Expand will make your life much easier.

Another great feature is its ability to complete whole lines. It will fall back to word completion if it runs out of ideas, and if you regularly write elisp, then Hippie Expand will guess if the text at the point is a potential elisp symbol and automatically complete it for you also.