The denotation of λs.λz.s(sz) in the geometry of interaction.
(letrec ((＊ (λ (c) (cons π1 c)))
(π23
(λ (c)
(π21
(λ (n)
(cond
((< n 2) (c n))
(else (c (add1 n))))))))
(π22
(λ (c)
(π24
(λ (n)
(cond
((< n 2) (c n))
((= n 2) 'z)
(else (c (sub1 n))))))))
(π25
(λ (c)
(π23
(λ (n)
(cond
((< n 1) (c n))
((= n 1) (car (c 1)))
((= n (add1 1)) (cdr (c 1)))
(else (c (sub1 n))))))))
(π24
(λ (c)
(π26
(λ (n)
(cond
((< n 1) (c n))
((= n 1) (cons (c 1) (c (add1 1))))
(else (c (add1 n))))))))
(π27
(λ (c)
(π25
(λ (n)
(cond
((< n 0) (c n))
((= n 0) (car (c 0)))
((= n (add1 0)) (cdr (c 0)))
(else (c (sub1 n))))))))
(π26
(λ (c)
(π6
(λ (n)
(cond
((< n 0) (c n))
((= n 0) (cons (c 0) (c (add1 0))))
(else (c (add1 n))))))))
(π15
(λ (c)
(π17
(λ (n)
(cond
((< n 0) (c n))
((= n 0) (car (c 0)))
((= n (add1 0)) (cdr (c 0)))
(else (c (sub1 n))))))))
(π16
(λ (c)
(π14
(λ (n)
(cond
((< n 0) (c n))
((= n 0) (cons (c 0) (c (add1 0))))
(else (c (add1 n))))))))
(π17
(λ (c)
(π19
(λ (n)
(cond
((< n 1) (c n))
(else (c (add1 n))))))))
(π18
(λ (c)
(π16
(λ (n)
(cond
((< n 1) (c n))
((= n 1) 's)
(else (c (sub1 n))))))))
(π11
(λ (c)
(π9
(λ (n)
(cond
((< n 0) (c n))
(else (c (add1 n))))))))
(π10
(λ (c)
(π12
(λ (n)
(cond
((< n 0) (c n))
((= n 0) 's)
(else (c (sub1 n))))))))
(π13
(λ (c)
((if (eq? 'L (car (c 0))) π11 π15)
(λ (n) (if (= n 0) (cdr (c n)) (c n))))))
(π12
(λ (c)
(π3
(λ (n) (if (= n 0) (cons 'L (c 0)) (c n))))))
(π14
(λ (c)
(π3
(λ (n) (if (= n 0) (cons 'R (c 0)) (c n))))))
(π19
(λ (c)
((if (eq? '○ (car (c 1))) π8 π22)
(λ (n) (if (= n 1) (cdr (c n)) (c n))))))
(π20
(λ (c)
(π18
(λ (n) (if (= n 1) (cons '○ (c 1)) (c n))))))
(π21
(λ (c)
(π18
(λ (n) (if (= n 1) (cons '● (c 1)) (c n))))))
(π9
(λ (c)
((if (eq? '○ (car (c 0))) π5 π20)
(λ (n) (if (= n 0) (cdr (c n)) (c n))))))
(π7
(λ (c)
(π10
(λ (n) (if (= n 0) (cons '○ (c 0)) (c n))))))
(π8
(λ (c)
(π10
(λ (n) (if (= n 0) (cons '● (c 0)) (c n))))))
(π4
(λ (c)
((if (eq? '○ (car (c 0))) π7 π27)
(λ (n) (if (= n 0) (cdr (c n)) (c n))))))
(π5
(λ (c)
(π2
(λ (n) (if (= n 0) (cons '○ (c 0)) (c n))))))
(π6
(λ (c)
(π2
(λ (n) (if (= n 0) (cons '● (c 0)) (c n))))))
(π1
(λ (c)
((if (eq? '○ (car (c 0))) π4 π13)
(λ (n) (if (= n 0) (cdr (c n)) (c n))))))
(π2
(λ (c)
(＊
(λ (n) (if (= n 0) (cons '○ (c 0)) (c n))))))
(π3
(λ (c)
(＊
(λ (n)
(if (= n 0) (cons '● (c 0)) (c n)))))))
(λ (π)
(case π ((＊) π1) (else (error "unknown port" π)))))
One Trackback/Pingback
[...] macro use expands into the code given here. Notice that links are implemented as recursive functions. Traveling along a link in the graph [...]
Post a Comment