λ 演算與型別 (Lambda Calculus and Types)

• 講者: 陳亮廷 Liang-Ting Chen

Practical introduction to lambda calculus (thus excluding, e.g., computability theory). May be interleaved with FP.

Outline

• Untyped lambda calculus (1 unit)
  • Syntax, alpha-conversion, beta-reduction
  • Reduction strategies & Church-Rosser Theorem
  • Programming in lambda calculus
    • Church numerals
    • Fixed-point combinator
• Simply typed lambda calculus (1 unit)
  • Typing rules (à la Curry)
  • Simply typed lambda calculus à la Church
  • Type safety
    • Subject reduction and strong normalisation
  • Programming with simply typed lambda calculus
• Polymorphic lambda calculus (1 unit)
  • Typing rules
  • Church numerals and folds revisited
  • Parametricity overview

Course Materials

• slides 1
• slides 2
• slides 3
• handout 0
• handout 1
• handout 2
• handout 3

[註] handout 1 中有些許變更如下：

1. (Def. 1.1) 加註 \(\Lambda\) 指的是所有 \(\lambda\)-term 所成的集合
2. (Def. 1.2) 修正 bound variable 的定義（出現在 \(\lambda\) x. M 裡頭的 x 即為 bound occurrence）
3. (Def. 1.6) \(\beta\)-conversion 的定義中由 (\(\lambda\) x. M) 跟 (\(\lambda\) x’. M) 為 \(\alpha\)-equivalent 改為 M 跟 M’ 為 \(\alpha\)-equivalent。兩者皆正確，但後者較為精簡。
4. \(\lambda\)-logical theory 改為 \(\beta\)-convertibility。
5. Church numerals 中的 \(f^n\) 定義稍有改進。
6. Successor 中原本寫 succ \(\bar{n} \xrightarrow{\beta*} \bar{n+1}\) 中的 \(\bar{n}\) 修正為 \(c_n\)，\(\bar{n+1}\) 亦然。
7. Conditional 的定義修正。
8. (Example 3.4 & 3.6) 的 G 定義修正（原始定義漏了 “add n”）。