| Date |
Synopsis |
Materials |
| Dec 11 (Mon) |
- Introduction
- I would like to emphasize that one can do formal proof in a DIY fashion.
- We will implement two algorithms (for type inference and verification)
- Notation
- Variables：alphabets（total : 52）
- *：*
- sort：@
- Application：%(M)(N)
- Lambda：$x:(M).(N)
- Type：?x:(M).(N)
- Constants：c[(M),...,(N)]（c[], if no arguments）, where c should contain more than one letter.
- Homework: write a code, whose interface "./test_read def_file" I explained.
|
- pdf
- Derivation rule : Appendix D
- Lambda expressions : Definition 9.1.1
- Example and result
|
| Dec 14 (Thur) |
- I distributed my binaries.
- Inferencer : ./test_automake3 def_file implies log
- Verifier : ./test_book3 def_file log
- I explained in detail how to copy-and-paste the formal proofs in the textbook to your def_file.
- x1:A1, ..., xn:An |> c(\bar{x}) = M : N is written as follows（if it is an axiom, then we write as M=#）.
- def2
- n
- x1
- A1
- ...
- xn
- An
- c
- M
- N
- edef2
- Homework: copy-and-paste the following:
implies,
implies_in,
implies_el,
contra,
contra_in,
contra_el,
not,
not_in,
not_el,
a1_fig11.8,
a2_fig11.8,
a3_fig11.8
|
|
| Dec 18 (Mon) |
- I explained the alpha equivalence on lambda expressions.
- Which lambda expressions are alpha equivalent (if possible, answer by your program)?
- $x:*.($x:x.x)
- $x:*.($x:y.x)
- $x:*.($y:x.y)
- In the expression $x:M.N (or ?x:M.N), the scope of x is N, not M. (If N = $x:A.B, the original x scopes only A).
- I mentioned the De Bruijn index.
- Every variable is classified into one of the following three:
- is a free variable,
- is in the scope of a variable,
- is a variable for abstraction (i.e., $ or ?).
- $x:M.N \equiv $y:A.B iff M\equiv A and N[x:=z]\equiv B[y:=z],
- z is fresh,
- N[x:=z] means the replacement of x in N with z scoped by $x.
- c.f.) See [C.1. Definition in Appendix C in The Lambda Calculus: Its Syntax and Semantics by Barendregt]. ($x:(A).(B))[p:=q] can be calculated as follows (the credit is attributed to Curry (1958)):
- if x=p, then $x:(A[p:=q]).(B)（note that $x:(A).(B) seems OK).
- if x=q, then ($z:(A).(B[x:=z]))[p:=q], where z is fresh.
- otherwise, $x:(A[p:=q]).(B[p:=q]).
- Anyway, it seems there are subtleties around the definition (of course, I do not intend to claim that it is difficult). Is it easy to define briefly and at the same time rigorously?
In a mathematian's view, it is desirable to define it from a wider perspective (e.g., for a context-free grammer with suitale contraints).
- We will implement sort, var, weak, form in the derivation rule in order to duplicate this result for this script.
- sort
- var n x
- weak m n x
- form m n
- Book = vector⟨Judgement⟩
- Judgement = tuple⟨Definitions,Context,Epsilon,Epsilon⟩
- Definitions = vector⟨(descriptive or primitive) Definition⟩
- (descriptive) Definition = tuple⟨Context,string,Epsilon,Epsilon⟩ (primitive definitions are defined later)
- Context = vector⟨pair⟨char,Epsilon⟩⟩
- Homework: copy-and-paste the following:
and,
and_in,
and_el1,
and_el2,
or,
or_in1,
or_in2,
or_el,
equiv,
equiv_in,
equiv_el1,
equiv_el2,
a1_fig11.13,
a2_fig11.13,
a3_fig11.13,
a4_fig11.13,
a5_fig11.13,
a6_fig11.13,,
a7_fig11.13,
a1_fig11.14,
a2_fig11.14,
a3_fig11.14,
sym_or
|
- Chapter 11.5
- Chapter 11.6
|
| Dec 21 (Thur) |
- I will explain the substitution and the beta-delta conversion.
- We will implement appl, abst, conv in the derivation rule.
- Homework: copy-and-paste the following:
exc_thrd,
a2_fig11.16,
a3_fig11.16,
a4_fig11.16,
a5_fig11.16,
a6_fig11.16,
doub_neg,
notnot_in,
notnot_el,
a1_fig11.18,
a2_fig11.18,
a3_fig11.18,
a4_fig11.18,
a5_fig11.18,
a6_fig11.18,
a7_fig11.18,
a8_fig11.18,
a9_fig11.18,
a10_fig11.18,
a11_fig11.18,
or_in_alt1,
a2_fig11.19,
or_in_alt2,
or_el_alt1,
or_el_alt2,
a1_fig11.20,
a2_fig11.20,
a3_fig11.20,
a4_fig11.20,
a5_fig11.20,
a1_fig11.21,
a2_fig11.21,
a3_fig11.21,
a4_fig11.21,
a5_fig11.21,
a6_fig11.21
|
- Chapter 11.8
- Chapter 11.9
|
| Dec 25 (Mon) |
- We will implement def, def-prim, inst, inst-prim in the derivation rule.
- I explained primitive definition
- x1:A1, ..., xn:An |> a(x) = # : N
- formally, tuple⟨Context,string,Epsilon⟩
- beta reduction: ($x:M.N)A --> N[x:=A]
- Substitution: If N=$z:P.Q, then N[x:=A] = $w:P[x:=A].Q[z:=w][x:=A], where w is fresh
- delta reduction: a(U1,...,Us) --> M[x1=U1, ..., xs=Us], where we have a descriptive definition x1:A1, ..., xn:An |> a(x)=M : N
- M[x1:=U1, ..., xs:=Us] = M[x1:=z1]...[xn:=zn][z1:=U1]...[zn:=Un], where z1, ..., zn are fresh
- What is AB[A:=B,B:=C]?
- Unfold implies[(B),implies[(B),(C)]], where A:*, B:* |> implies[(A),(B)] = ?x:A:B : *.
- appl m n
- abst m n
- conv m n
- def m n a
- defpr m n a
- inst m n k1 ... kn p
- p means that we use the p-th defintion in \Delta
- n is the arity of the definition
- Let p-th definition is given by x1:A1, ..., xn:An |> c(x)=M : N.
- For a=1,...,n, if ka-th judgement is \Delta : \Gamma |- Ua : Va, we need to check Va \equiv Aa[x1:=U1,...,x(a-1):=U(a-1)].
- Relation between a descriptive definition x1:A1, ..., xn:An |> a(x)=M : N and a lambda expression $x1:A1.($x2:A2.(...M)) + beta reduction is unclear to me (Disclaimer: I am a math researcher, not a computer scientist). If we can keep the kernel small, it is good for our purpose.
- I mentioned Pure type systems with definitions by Severi and Poll.
- Homework: copy-and-paste the following:
forall,
forall_in,
forall_el,
exists,
exists_in,
exists_el,
a1_fig11.25,
a2_fig11.25,
a3_fig11.25,
a1_fig11.26,
a2_fig11.26,
a3_fig11.26,
a4_fig11.26,
a5_fig11.26,
a1_fig11.27,
a2_fig11.27,
a3_fig11.27,
a4_fig11.27,
a5_fig11.27,
exists_in_alt,
exists_el_alt,
a1_fig11.29,
a2_fig11.29,
a3_fig11.29,
a4_fig11.29,
a5_fig11.29,
a6_fig11.29,
a7_fig11.29,
a1_fig11.24,
a2_fig11.24,
a3_fig11.24,
a4_fig11.24,
a5_fig11.24,
a6_fig11.24
|
- Chapter 11.10
- Chapter 11.11
- Definition 9.5.1, see also ERRATA (page 51) by the authors）
- Remark 9.4.1
|
| Jan 4 (Thur) |
- From now on, we will implement a type inferencer.
- I explained how to implement get_type(M; (\Delta,\Gamma)).
- In the rest, NF(M; \Delta) stands for the beta-delta normal form of M.
- (see sort) If M = *, then return @
- If M = @ or #, then halt (Strictly speaking, # is not a lambda expression).
- (see var) If M = x, then find x:A in \Gamma and return NF(A; \Delta) (otherwise, halt).
- (see appl) If M = %(M)(N), then:
- If L = get_type(M; (\Delta,\Gamma)) is not a form of ?z:(A).(B), then halt.
- Otherwise, return NF(B[z:=N]; \Delta).
- (see inst) If M = c(U1,...,Un) with respect to a definition x1:A1, ..., xn:An |> c(\bar{x}) = M : N, then return NF(N[x1:=U1,...,xn:=Un]; \Delta).
- (see abst) If M = $x:(A).(B), then modify M to an appropriate $z:(A).(B') and return NF(?z:(A).(get_type(B'; (\Delta,\Gamma'))); \Delta), where \Gamma' = \Gamma + z:A.
- (see form) If M = ?x:(A).(B), then modify M to an appropriate ?z:(A).(B') and return get_type(B'; (\Delta,\Gamma')). (If it is not * or @, then you can halt the execution)
- I will explain how to implement get_script(M; (\Delta,\Gamma)) next week.
- I explained two syntax sugars cp and sp, but I encourage you to do without them.
- Homework: copy-and-paste the following (you are required to do some puzzles):
eq,
eq_alt,
a2_fig12.2,
eq_refl,
a1_fig12.4,
a2_fig12.4,
eq_subs,
a1_fig12.5,
a2_fig12.5,
a3_fig12.5,
eq_cong,
Q1_fig12.6,
eq_cong2,
Q2_fig12.10,
a2_fig12.10,
eq_sym,
a4_fig12.10,
eq_sym2,
Q3_fig12.12,
eq_trans,
a3_fig12.12
|
- Chapter 12
- Lemma 10.4.7 (1)
|
| Jan 11 (Thur) |
- I explained how to implement get_script(M; (\Delta,\Gamma)) for M=%(M)(N).
- get_script spells out a script from "\Delta,\Gamma |- *:@" to "\Delta,\Gamma |- M:something".
- Call recursively get_script for M, N, A:=get_type(M; (\Delta,\Gamma)), B:=get_type(N; (\Delta,\Gamma)).
- Get "\Delta;\Gamma |- M:A" by "\Delta,\Gamma |- M:something", "\Delta;\Gamma |- A:s" and conv.
- Similar for "\Delta;\Gamma |- N:B"
- Apply appl for 3 and 4.
- Note that you may halt the execution based on results of suitable checks (such as "whether A is of the form ?z:(P).(Q) or not" or P\equiv B）.
- The verifier checks 6 anyway.
- Homework: copy-and-paste the following (you are required to do some puzzles):
refl,
trans,
pre_ord,
antisymm,
part_ord,
Least,
exists_at_least,
exists_at_most,
exists1,
iota,
iota_prop,
a1_fig12.9,
a2_fig12.9,
a3_fig12.9,
a4_fig12.9,
a6_fig12.9,
a7_fig12.9,
a8_fig12.9,
a9_fig12.9,
a10_fig12.9,
a11_fig12.9,
a1_fig12.17,
a2_fig12.17,
a3_fig12.17,
a4_fig12.17,
a5_fig12.17,
Min,
a2_fig12.18,
|
|
| Jan 15 (Mon) |
- Homework: copy-and-paste the following (you are required to do some puzzles):
ps,
element,
subseteq,
cup,
IS,
cap,
setminus,
complement,
element_in,
element_el,
a1_fig13.4,
a2_fig13.4,
a3_fig13.4,
a4_fig13.4,
a5_fig13.4,
a6_fig13.4,
a7_fig13.4,
a8_fig13.4,
a9_fig13.4,
a10_fig13.4,
a11_fig13.4,
a12_fig13.4,
eq_subset,
IS_prop
|
|
| Jan 18 (Thur) |
- Tips for copy-and-paste: When proving "assumption => conclusion", try to write
- def2
- ...
- u
- assumption
- name_of_auxiliary_Prop
- complicated
- conclusion
- edef2
and mechanically obtain the following (do not unfold implies[(assumption),(conclusion)] because it violates readability).
- def2
- ...
- name_of_Theorem
- $u:(assumption).(name_of_auxiliary_Prop[(...),(u)])
- implies[(assumption),(conclusion)]
- edef2
- Homework: copy-and-paste the following (you are required to do some puzzles):
emptyset,
full_set,
a3_fig13.7,
a4_fig13.7,
a5_fig13.7,
a6_fig13.7,
a7_fig13.7,
a8_fig13.7,
a1_fig13.8,
a2_fig13.8,
a3_fig13.8,
a4_fig13.8,
a5_fig13.8,
a6_fig13.8,
a7_fig13.8,
a8_fig13.8,
a9_fig13.8,
a10_fig13.8,
a11_fig13.8,
a12_fig13.8,
a13_fig13.8,
a14_fig13.8,
reflexive,
symmetric,
transitive,
equivalence_relation,
class
|
|
| Jan 22 (Mon) |
- Homework: copy-and-paste the following (you are required to do some puzzles):
a1_fig13.11,
a2_fig13.11,
a3_fig13.11,,
a4_fig13.11,
a5_fig13.11,
a6_fig13.11,
a7_fig13.11,
a8_fig13.11,
a9_fig13.11,
a10_fig13.11,
a11_fig13.11,
a12_fig13.11,
R_fig13.12,
a2_fig13.12,
F_fig13.12,
injective,
surjective,
bijective,
inj_subset,
image,
origin,
a1_fig13.16,
a2_fig13.16,
a3_fig13.16,
a4_fig13.16,
a5_fig13.16,
a6_fig13.16,
a4_fig13.13,
inv,
Exer13.14
|
|
| Feb 1 (Thur) |
- Q and A session
- Final presentations
|
|
| Feb 5 (Mon) |
- Special lecture
- Submit your def2 and implementations with explanations by slack. The deadline is 15 Feb.
|
|