技术笔记

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.

Keyboard Macros

You can record keystrokes and commands in Emacs and save them for later playback as a keyboard macro. A keyboard macro in Emacs is very different from a lisp macro and you should not confuse the two.

Basic Commands

You can also pass the universal argument and digit arguments to the macro commands:

Appending to the last macro (C-u F3) is occasionally useful, but passing a numeric argument to F4 is very useful since replaying the macro a set number of times is a frequent thing indeed; so much so that passing digit 0 (C-0 F4 or C-u 0 F4, for instance) will run the macro over and over again until it terminates with an error, such as reaching the end of a buffer or when a command in the macro triggers an error.

Advanced Commands

There is an entire prefix key group, C-x C-k, dedicated to Emacs’s macro functionality. There are many commands and you are unlikely to ever use most of them.

Interactive Macro Playback

Let’s start out with the counters. When you start recording, Emacs will automatically initialize an internal counter to zero, and every time you press F3 during the recording, Emacs will insert the counter and then increment the internal counter by 1. There are, of course, many creative uses for the counter: creating numbered lists is the most obvious.

The standout command is C-x C-k q. When you call it, Emacs will tag that step in the macro recording and ask the user for advice – in effect stopping the macro temporarily to prompt the user – before continuing.

Saving and Recalling

Macros in Emacs are stored in a macro ring, a concept that you should recognize from other parts of Emacs (like the kill ring and undo ring.) Creating a new macro automatically stores old macros in the macro ring without you having to do anything. The commands below let you save and recall from the macro ring, edit and bind macros to keys, and more.

Text manialations is one aspect Emacs is especially good at, and it has a variety of tools to help you. Massaging text files for further processing or extracting pertinent information from log files are both common things to do in Emacs.

Editable Occur

I introduced M-x occur in Occur(M-s o in helm): Print lines matching an expression as a way of collating all lines that match a certain pattern.

You can typing e begin to edit, and after you finish, C-c C-c to commit the changes to their original lines, it is especially great for keyboard macros and search & replace.

Deleting Duplicates

By default, M-x delete-duplicate-lines deletes the first dupli- cate line it encounters, starting from the top. With a single universal argument, it starts from the bottom and therefore deletes the last.

Flushing and Keeping Lines

Sometimes you want to filter lines in a region by a pattern; whether that is to flush lines that match a pattern, or keep the ones that do.

Both commands act on the active region so it is common – if you want to do this on a whole buffer - to call C-x h to select the entire buffer first.

Keeping lines that match a pattern is useful for large log files then you want to.

Joining and Splitting Lines

Unlike the kill commands that act on lines (C-M-<backspace> and C-k), these commands won’t alter your kill ring. They are also more specialized, as they insert or remove lines with- out moving your point.

Whitespace Commands

Managing whitespace is an issue that recurs often when you yank text from elsewhere or if you work with languages where whitespace is significant.

M-SPC is useful as it trims all whitespace, to the left or right of the point, to a single whitespace character. ving none. M-x cycle-spacing cycles between leaving one, leaving none, and restoring the original spacing.