笔记 《被讨厌的勇气》

引言

• 世界是简单的，人生也是简单的
  • 人住在主观世界里
  • 摘掉墨镜是勇气的问题

第一夜 我们的不幸是谁的错？

• 心理学“第三巨头”阿德勒
  • 20世纪初阿德勒心理学
  • 与希腊哲学一脉相承
  • 个体心理学

Read More

Haskell

with UPenn CIS 194: Introduction to Haskell (Spring 2013)

and with Algebra of Programming (Richard Bird & Oege de Moor)

基本语法

• 操作符
  • == 等于
  • /= 不等于
  • ++ 两个列表相加
  • ： 向列表前加入一个元素
  • -- 或 {- ... -} 注释
  • $ apply 分隔函数和参数（类似于括号）
  • where 在alternatives中用于定义重复使用的变量

Read More

Software Foundations

Online Textbook

Michael Clarkson's Open Online Course (on Youtube) Michael Charkson's Course (on Bilibili)

Xiong Yingfei's Course Webpage (2023 Spring)

This note is used as a brief summary and supplementofr the textbook and courses.

Tactics

The apply tactic with symmetry and transitivity

apply

When encountering situations where the goal to be proved is exactly the same as some hypothesis in the context or some previously proved lemma, we can use apply tactic instead of the rewrite & reflexivity we previously used.

1
2
3
4
5
6
7
8
9
10
11

Theorem silly1 : forall (n m : nat),
  n = m ->
  n = m.
Proof.
  intros n m eq.
(** n, m : nat
    eq : n = m
    ______________________________________(1/1)
    n = m
*)
  apply eq.  Qed.

Read More

Software Foundations

Online Textbook

Michael Clarkson's Open Online Course (on Youtube) Michael Charkson's Course (on Bilibili)

Xiong Yingfei's Course Webpage (2023 Spring)

This note is used as a brief summary and supplementofr the textbook and courses.

Poly

Polymorphism

Omit Type Argument

1
2
3

Inductive list (X:Type) : Type :=
  | nil
  | cons (x : X) (l : list X).

The type list is thus parameterized on another type X.

Read More

Software Foundations

Online Textbook

Michael Clarkson's Open Online Course (on Youtube) Michael Charkson's Course (on Bilibili)

Xiong Yingfei's Course Webpage (2023 Spring)

This note is used as a brief summary and supplementofr the textbook and courses.

Lists

Pairs

We define the pair of natural numbers. (Cartesian product)

1
2
3
4
5
6
7
8
9
10
11
12
13
14

Inductive natprod : Type :=
  | pair (n1 n2 : nat).

Definition fst (p : natprod) : nat :=
  match p with
  | pair x y => x
  end.

Definition snd (p : natprod) : nat :=
  match p with
  | pair x y => y
  end.

Notation "( x , y )" := (pair x y).

Read More

Introduction to the Theory of Computation Michael Sipser

with MIT 18.404 Theory of Computation 2020 Fall PPT

Part One: Automata and Languages

Lecture 1

Automata, computability and complexity

Finite Automaton 1. a model of computer with limited capacity 2. state diagram of finite automaton

Read More