Skip to content

Instantly share code, notes, and snippets.

@danking

danking/gist:a888afa58333735dbd0c

Created March 5, 2015 22:03
Show Gist options
  • Save danking/a888afa58333735dbd0c to your computer and use it in GitHub Desktop.
Save danking/a888afa58333735dbd0c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
T[[#1 e]] = T[[e]] (λ x. λ y. x)
T[[(e₁, e₂)]] = λ f. f T[[e₁]] T[[e₂]]
T[[(e₁, e₂)]] = (λ x. λ y. λ f. f x y) T[[e₁]] T[[e₂]]
T[[Ω]] = (λ x . (x •) (x •)) (λ_. λ x. (x •) (x •))
p = (λx.x, Ω)
* CBN w/ pairs
#1 p → λx.x
terminates
* CBV a
T[[#1 p]] = T[[p]] (λ x. λ y. (x •))
= (λ f. f T[[λx.x]] T[[Ω]]) (λ x. λ y. (x •))
→ (λ x. λ y. x)) T[[λx.x]] T[[Ω]]
= (λ x. λ y. x)) (λx.(x •)) T[[Ω]]
→ (λ y. (λx.(x •))) T[[Ω]]
= (λ y. (λx.(x •))) ((λ x. (x •) (λ_.(x •)))
(λ_. λ x. (x •) (λ_.(x •))))
→ (λ y. (λx.(x •))) (((λ_. λ x. (x •) (λ_.(x •))) •)
(λ_.((λ_. λ x. (x •) (λ_.(x •))) •)))
→ (λ y. (λx.(x •))) ((λ x. (x •) (λ_.(x •)))
(λ_.((λ_. λ x. (x •) (λ_.(x •))) •))
→ (λ y. (λx.(x •))) ((λ x. (x •) (λ_.(x •)))
(λ_.((λ_. λ x. (x •) (λ_.(x •))) •))
→ (λ y. (λx.(x •))) (((λ_.((λ_. λ x. (x •) (λ_.(x •))) •)) •)
(λ_.((λ_.((λ_. λ x. (x •) (λ_.(x •))) •)) •)))
→ (λ y. (λx.(x •))) (((λ_. λ x. (x •) (λ_.(x •))) •)
(λ_.((λ_.((λ_. λ x. (x •) (λ_.(x •))) •)) •)))
→ (λ y. (λx.(x •))) ((λ x. (x •) (λ_.(x •)))
(λ_.((λ_.((λ_. λ x. (x •) (λ_.(x •))) •)) •)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment