CS611 Lecture 30 Propositions as Types Continued 17 Novemb er 2006Lecturer: Dexter Kozen1 A Digression on Heyting AlgebraAs discussed last time, there are fewer formulas that are considered intuitionistically valid than classicallyvalid. The law of double negation (¬¬ϕ → ϕ), the law of excluded middle (ϕ∨¬ϕ), and proof by contradictionor reductio ad absurdum are no longer accepted.Bo olean algebra is to classical logic as Heyting algebra is to intuitionistic logic. A Heyting algebra isan algebraic structure of the same signature as Boolean algebra, but satisfying only those equations thatare provable intuitionistically. Whereas the free Boolean algebra on n generators has 22nelements, the freeHeyting algebra on one generator has infinitely many elements.ssss@@@@ ⊥P ¬PFree Boolean algebra on one generatorsssssssssssssssss@@@@@@@@@@@@@@@@@@@@@@ @@⊥P¬P¬¬PP∨¬P¬¬P → P¬P ∨¬¬P...Free Heyting algebra on one generatorThe picture on the right is sometimes called the Rieger–Nishimura ladder.2 Extracting Computational ContentMany automated deduction systems, such as NuPrl and Co q, are based on constructive logic. Automaticprogramming was a significant research direction that motivated the development of these systems. The ideawas that a constructive proof of the existence of a function would automatically yield a program to computeit: the statement asserting the existence of the function is a type, and a constructive proof yields a λ-terminhabiting that type. For example, to obtain a program computing square roots, one merely has to give aconstructive proof of the statement ∀x ≥ 0 ∃yy2= x.3 Other DirectionsMany fruitful correspondences have been found between constructive logic and types. Other logics have beenused to give intuition about typing systems and vice versa.For example, linear lo gic is a logic that keeps track of resources. One may only use an assumption inthe application of a rule once; the assumption is consumed and may not be reused. This corresponds tofunctions that consume their arguments, and hence is a possible model for systems with bounded resources.14KATDemoThe remainder of the lecture was a demo of the KAT interactive proof assistant. This system is based onconstructive equational logic of universal Horn formulas (formulas of the form ∀¯xs1= t1→ ··· → sn= tn→s = t). In the demo, we illustrated how proofs are represented as λ-terms that are extracted automaticallyas rules are applied.The system is available for downloading from
View Full Document
Unlocking...