1David Evanshttp://www.cs.virginia.edu/evansCS150: Computer ScienceUniversity of VirginiaComputer ScienceLecture 40: Lecture 40: Computing Computing with Glue and with Glue and PhotonsPhotonsThe Tinkertoy Computer and Other Machinationsby A. K. Dewdney http:// www.amazon. com/exec/o bidos/tg/deta il/-/071672491X/ 103-4408705-53 67831?v=g lance2Lecture 40: Computing with Glue and PhotonsEquivalent Computers?z z zz z z z1StartHALT), X, L2: look for (#, 1, -¬), #, R¬(, #, L(, X, R#, 0, -Finite State Machine...Turing Machine≡term = variable | term term| (term)| λλλλ variable . termλy. M ⇒αλv. (M [y v])where v does not occur in M.(λx. M)N ⇒βM [ x N ]ααLambda Calculus3Lecture 40: Computing with Glue and PhotonsLambda Calculus is a Universal Computer?z z z z z z z z z z z z z z z zz z z z1StartHALT), X, L2: look for (#, 1, -¬), #, R¬(, #, L(, X, R#, 0, -Finite State Machine• Read/Write Infinite TapeMutable Lists• Finite State MachineNumbers• ProcessingWay to make decisions (if)Way to keep going4Lecture 40: Computing with Glue and PhotonsWhat is 42?42forty-twoXLIIcuarenta y dos5Lecture 40: Computing with Glue and PhotonsMeaning of Numbers• “42-ness” is something who’s successor is “43-ness”• “42-ness” is something who’s predecessor is “41-ness”• “Zero” is special. It has a successor“one-ness”, but no predecessor.6Lecture 40: Computing with Glue and PhotonsMeaning of Numberspred (succ N) → Nsucc (pred N) → Nsucc (pred (succ N)) → succ Nzero? zero → Tzero? (succ zero) → F27Lecture 40: Computing with Glue and PhotonsIs this enough?Can we define add with pred, succ, zero? and zero?add ≡ λxy.if (zero? x) y (add (pred x) (succ y))8Lecture 40: Computing with Glue and PhotonsCan we define lambda terms that behave likezero, zero?, pred and succ?Hint: what if we had cons, car and cdr?9Lecture 40: Computing with Glue and PhotonsNumbers are Lists...zero? ≡ null?pred ≡ cdrsucc ≡ λ x . cons F xThe length of the list corresponds to the number value.10Lecture 40: Computing with Glue and PhotonsMaking Pairs(define (make-pair x y) (lambda (selector) (if selector x y))) (define (car-of-pair p) (p #t)) (define (cdr-of-pair p) (p #f)) 11Lecture 40: Computing with Glue and Photonscons and carcons ≡ λx.λy.λz.zxycons M N = (λx.λy.λz.zxy) M N→β(λy.λz.zMy) N→βλz.zMNcar ≡ λp.p Tcar (cons M N) ≡ car (λz.zMN) ≡ (λp.p T) (λz.zMN)→β(λz.zMN) T →βTMN →β(λxy. x) MN →β(λy. M)N →βMT ≡ λxy. x12Lecture 40: Computing with Glue and Photonscdr too!cons ≡ λxyz.zxy car ≡ λp.p Tcdr ≡ λp.p Fcdr cons M Ncdr λz.zMN = (λp.p F) λz.zMN→β(λz.zMN) F→βFMN →βN313Lecture 40: Computing with Glue and PhotonsNull and null?null ≡ λx.Tnull? ≡ λx.(x λy.λz.F)null? null → λx.(x λy.λz.F) (λx. T)→β(λx. T)(λy.λz.F)→βT14Lecture 40: Computing with Glue and PhotonsNull and null?null ≡ λx.Tnull? ≡ λx.(x λy.λz.F)null? (cons M N) → λx.(x λy.λz.F) λz.zMN→β(λz.z MN)(λy.λz.F)→β(λy.λz.F) MN→βF15Lecture 40: Computing with Glue and PhotonsCounting0 ≡ null1 ≡ cons F 02 ≡ cons F 13 ≡ cons F 2...succ ≡ λx.cons F xpred ≡ λx.cdr x16Lecture 40: Computing with Glue and Photons42 = λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. y λxy.(λz.z xy) λxy. yλxy.(λz.z xy) λxy. y λx.T17Lecture 40: Computing with Glue and PhotonsLambda Calculus is a Universal Computerz z z z z z z z z z z z z z z zz z z z1StartHALT), X, L2: look for (#, 1, -¬), #, R¬(, #, L(, X, R#, 0, -Finite State Machine• Read/Write Infinite Tape Mutable Lists• Finite State Machine Numbers to keep track of state• Processing Way of making decisions (if)☯ Way to keep goingWe have this, butwe cheated using ≡to make recursive definitions!18Lecture 40: Computing with Glue and PhotonsWay to Keep Going(λ f. ((λ x.f (xx)) (λ x. f (xx)))) (λz.z)→β(λx.(λz.z)(xx)) (λ x. (λz.z)(xx))→β(λz.z) (λ x.(λz.z)(xx)) (λ x.(λz.z)(xx))→β(λx.(λz.z)(xx)) (λ x.(λz.z)(xx))→β(λz.z) (λ x.(λz.z)(xx)) (λ x.(λz.z)(xx))→β(λx.(λz.z)(xx)) (λ x.(λz.z)(xx))→β...This should give you some belief that we might be able to do it. We won’t cover the details of why this works in this class.419Lecture 40: Computing with Glue and PhotonsLambda Calculus is a Universal Computerz z z z z z z z z z z z z z z zz z z z1StartHALT), X, L2: look for (#, 1, -¬), #, R¬(, #, L(, X, R#, 0, -Finite State Machine• Read/Write Infinite Tape Mutable Lists• Finite State Machine Numbers to keep track of state• Processing Way of making decisions (if) Way to keep going20Lecture 40: Computing with Glue and PhotonsEquivalent Computers!z z zz z z z1StartHALT), X, L2: look for (#, 1, -¬), #, R¬(, #, L(, X, R#, 0, -Finite State Machine...Turing Machineterm = variable | term term| (term)| λλλλ variable . termλy. M ⇒αλv. (M [y v])where v does not occur in M.(λx. M)N ⇒βM [ x N ]ααLambda Calculuscan simulatecan simulate21Lecture 40: Computing with Glue and PhotonsUniversal Computer• Lambda Calculus can simulate a Turing Machine– Everything a Turing Machine can compute, Lambda Calculus can compute also• Turing Machine can simulate Lambda Calculus (we didn’t prove this)– Everything Lambda Calculus can compute, a Turing Machine can compute also• Church-Turing Thesis: this is true for any other mechanical computer also22Lecture 40: Computing with Glue and PhotonsNormal Steps• Turing machine:– Read one square on tape, follow one FSM transition rule, write