順便釐清看看
前言一下
list A ::= [] | list A : a.
且, 用 list 表示 context: Γ.
首先,來看幾個case
λ.0 : [] ; a -> a
λλ.0 : [] ; a -> b -> b
λλ.1 : [] ; a -> b -> a
λλλ.2 : [] ; a -> b -> c -> a
然後根據某條rule
λ_ : Term (G,T) T' -> Term G (T -> T')
就變成了
0 : [a] ; a
λ.0 : [a] ; b -> b
λ.1 : [a] ; b -> a
λλ.2 : [a] ; b -> c -> a
後三個case可以再來一次
0 : [a,b] ; b
1 : [a,b] ; a
λ.2 : [a,b] ; c -> a
最後一個case還可以更進一步
2 : [a,b,c] ; a
結論
確實,不管有幾層λ-binder
如果是取 zero
那就是直接取出context最後進來的
如果是取 suc zero
就是往後數一個
取 suc suc zero
則再往後取一個
--
明白以後..
突然覺得這兩三天的時間...
實在是花得很浪費= =
