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