Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 1. T[x] => x
- 2. T[(E₁ E₂)] => (T[E₁] T[E₂])
- 3. T[λx.E] => (K T[E]) (if x is not free in E)
- 4. T[λx.x] => I
- 5. T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E)
- 6. T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])
- T : Lambda -> Comb U Lambda lr lol
Add Comment
Please, Sign In to add comment