Logic in the Lambda Calculus, Part 2

Return to List of Lectures

Previous Lecture

• Misc
  • Joe’s Presentation
    • Wang tiles and undecidability
    • First thing in class Monday
    • Donuts
  • Final
    • Tuesday, May 10, 8:00 AM
    • In our classroom
    • Comprehensive, but emphasizing material since 2nd hour exam (e.g., diagonalization, reduction, Rice’s theorem, computation histories, PCP, recursion theorem, lambda calculus, etc.)
    • Designed for 2 hours, you’ll have 2 1/2 +
    • Rules and format otherwise similar to hour exams
    • Donuts and cider
  • SOFIs
    • Helpful to me in planning future offerings of this course
    • 2 filled out so far
    • Please fill out more
• Questions?
• Logic in Lambda Calculus
  • Examples
    • Z 1 = (λn.nF~F) (λfs.fs)
      • → (λfs.fs)F~F
      • → (F~) F
      • = ((λxy.y)~) F
      • = ((λx.(λy.y))~) F
      • → (λy.y) F
      • → F
    • Z 0 = (λn.nF~F) (λfs.s)
      • → (λfs.s)F~F
      • =(λf.(λs.s))F~F
      • → (λs.s)~F
      • → ~ F
      • → T
    • Predecessor
      • Next pair combinator H = λp.(λz.z(S(pT))(pT)))
      • Predecessor combinator P = λn.((nH(λz.z00)) F)
      • P 2 = (λn.(nH(λz.z00)) F) (λfy.f(f(y)))
        • → ( (λfy.f(f(y))) H (λz.z00) ) F
        • → (H(H(λz.z00))) F
        • … → (λz.z21) F
        • … → 1
    • Greater than or equal
      • Is x ≥ y?
      • G = λxy.(Z(xPy))
      • Is the xth predecessor of y = 0?
  • Try devising your own strictly greater
    • Is x > y?
    • GREATER = λxy.(AND (Gxy)(~Exy))
• Next
  • Recursion in Lambda Calculus
  • Read section 4 of Rojas

Next Lecture