The Nuprl Proof Development System
The Nuprl Proof Development SystemChristoph KreitzDepartment of Computer Science, Cornell UniversityIthaca, NY 14853http://www.nuprl.org
The Nuprl Project at Computational formal logicsType Theory Proof & program development systems– The Nuprl Logical Programming EnvironmentGUIGUIStructureEditor– Fast inference engines proof search techniquesGUIWebEmacs ModeLibraryEvaluatorTHEORYMaudeTHEORYPRLdefs, thms, tacticsrules, structure, codeMetaPRLEvaluatorSoS (Lisp)– Natural language generation from formal mathematicsEvaluatorTHEORY(HOL)defs, thms, tacticsrules, structure, codeTHEORYTHEORYJava.defs, thms, tacticsrules, structure, code(PVS)defs, thms, tacticsrules, structure, codeTranslatorInferenceEngineNuprl rInferenceEnginePVSInferenceEngineMinLog.defs, thms, tacticsrules, structure, codeEvaluatorTHEORY.defs, thms, tacticsrules, structure, codeTranslatorOCaml– Program extraction automated complexity analysis Application to reliable, high-performance networks– Assigning precise semantics to system software3URJUDPPLQJ/RJLF– Performance Optimizations&RPPXQLFDWLRQ– Assurance for reliability (verification)– Verified System DesignThe Nuprl Proof Development System6HFXU1VRIWZDULQIUDVWUXFWXUHCalculemus, September 2002
Nuprl’s Type Theory Constructive higher-order logic– Reasoning about types, elements, propositions, proofs, functions . . . Functional programming language– Similar to core ML: polymorphic, with partial recursive functions Expressive data type system– Function, product, disjoint union, Π- & Σ-types, atoms, void, top– Integers, lists, inductive types, universes– Propositions as types, equality type, subsets, subtyping, quotient types– (Dependent) intersection, union, records, modules Open-ended– new types can be added if needed User-defined extensions possibleThe Nuprl Proof Development System2Calculemus, September 2002
The Nuprl Proof Development System Beginnings in 1984– Nuprl 1 (Symbolics): proof & program refinement in Type Theory– Book: Implementing Mathematics . . .(1986)– Nuprl 2: Unix Version Nuprl 3: Mathematical problem solving(1987–1994)– Constructive machine proofs for unsolved mathematical problems Nuprl 4: System verification and optimization(1993–2001)– Verification of logic synthesis tools & SCI cache coherency protocol– Optimization/verification of the Ensemble group communication system Nuprl 5: Open distributed architecture(2000–. . . )– Cooperating proof processes centered around persistent knowledge base– Asynchronous, concurrent, and external proof engines; Interactive digital libraries of formal algorithmic knowledgeThe Nuprl Proof Development System3Calculemus, September 2002
Applications: Mathematics & Programming Formalized mathematical theories––––––Elementary number theory, real analysis, group theory(Allen, 1994 –. . . )Discrete mathematicsGeneral algebra(Jackson, 1994)Finite and general automata(Constable, Naumov & Uribe 1997, Bickford, 2001)Basics of Turing machines(Naumov, 1998 . . . )Formal mathematical textbook(Constable, Allen me.html Machine proof for unsolved problems– Girard’s paradox– Higman’s Lemma(Howe 1987)(Murthy 1990) Algorithms and programming languages––––Synthesis of elementary algorithms: square-root, sorting, . . .Simple imperative programming(Naumov, 1997)Programming semantics & complexity analysis(Benzinger, 2000)Type-theoretical semantics of large OCaml fragment(Kreitz 1997/2002)The Nuprl Proof Development System4Calculemus, September 2002
Applications: System Verification and ZDULQIUDVWUXFWXUH Verification of a logic synthesis tool(Aagaard & Leeser 1993) Verification of the SCI cache coherency protocol(Howe 1996) Ensemble group communication toolkit– Optimization of application protocol stacks (by factor 3–10)(Kreitz, Hayden, Hickey, Liu, van Renessee 1999)– Verification of protocol layers– Formal design of new adaptive protocols(Bickford 1999)(Bickford, Kreitz, Liu, van Renessee 2001) MediaNet stream computation network– Validation of real-time schedules wrt. resource limitationsThe Nuprl Proof Development System5(ongoing)Calculemus, September 2002
After more than 15 years . . . Insights– Type theory expressive enough to formalize today’s software systems– Formal optimization can significantly improve practical performance– Formal verification reveals errors even in well-explored designs– Formal design reveals hidden assumptions and limitations for use of software Ingredients for success in applications. . .– Precise semantics for implementation language of a system– Formal models of: application domain, system model, programming language– Knowledge-based formal reasoning tools– Collaboration between systems and formal reasoning groupsThe Nuprl Proof Development System6Calculemus, September 2002
Purpose of this course Understand Nuprl’s theoretical foundation Understand features of the Nuprl proof development system Learn how to formalize mathematics and computer scienceAdditional material can be found at e/kreitz/Abstracts/02calculemus-nuprl.htmlThe Nuprl Proof Development System7Calculemus, September 2002
Overview Introduction1. Nuprl’s Type Theory– Distinguishing Features– Standard Nuprl Types2. The Nuprl Proof Development System– Architecture and Feature Demonstration3. Proof Automation in Nuprl– Tactics & Rewriting– Decision Procedures– External Proof Systems4. Building Formal Theories– (Dependent) Records, Algebra, Abstract Data Types5. Future DirectionsThe Nuprl Proof Development System8Calculemus, September 2002
The Nuprl Proof Development System9I. Type Theory: Distinguishing Features
The NuPRL Type TheoryAn Extension of Martin-Löf Type Theory Foundation for computational mathematics– Higher-order logic programming language data type system– Focus on constructive reasoning– Reasoning about types, elements, and (extensional) equality . . . Open-ended, expressive type system–––––Function, product, disjoint union, Π- & Σ-types, atoms; programmingIntegers, lists, inductive types; inductive definitionPropositions as types, equality type, void, top, universes; logicSubsets, subtyping, quotient types; mathematics(Dependent) intersection, union, records; modules, program compositionNew types can/will be added as needed Self-contained– Based on “formalized intuition”, not on other theoriesThe Nuprl Proof Development System10I. Type Theory: Distinguishing Features
Distinguishing Features of Nuprl’s Type Theory Uniform internal notation– Independent display forms support flexible term display; free syntax Expressions defined independently of their types– No restriction on expressions that can be defined– Expressions in proofs must be typeable; Y combinator; “total” functions Semantics based on values of expressions– Judgments state what is true– Equality is extensional; computational semantics Refinement calculus– Top-down sequent calculus– Proof expressions linked to inference rules– Computation rules; interactive proof development; program extraction; program evaluation User-defined extensions possible– User-defined expressions and inference rulesThe Nuprl Proof Development System11; abstractions & tacticsI. Type Theory: Distinguishing Features
Syntax Issues Uniform notation: opid {pi:Fi}(x11, ., xm11.t1;. . . ;x1n, ., xmnn.tn)––––Operator name opid listed in operator tablesParameters pi:Fi for base terms (variables, numbers, tokens. . . )Sub-terms tj may contain bound variables x1j , ., xmj jNo syntactical distinction between types, members, propositions . . . Display forms describe visual appearance of termsInternal Term Structurevariable{x:v}()function{}(S; x.T )function{}(S; .T ).lambda{}(x.t)apply{}(f ;t).Display Formxx:S TS T.λx.tf t.; conventional notation, information hiding, auto-parenthesizing, aliases, . . .The Nuprl Proof Development System12I. Type Theory: Distinguishing Features
Semantics models proof, not denotation (Lazy) evaluation of expressions– Identify canonical expressions (values)– Identify principal arguments of non-canonical expressions– Define reducible non-canonical expressions (redex)– Define reduction steps in redex–contracta tablecanonical non-canonicalS TRedexContractumλx.tλx.u t βf tu[t/x] Judgments: semantical truths about expressions– 4 categories: Typehood(T Type), Type EqualityMembership (t T ),(S T ),Member equality (s t in T )– Semantics tables define judgments for values of expressionsS1 T1 S2 T2iff S1 S2 and T1 T2λx1.t1 λx2.t2 in S T iff S T Type and t1[s1/x1] t2[s2/x2] in Tfor all s1, s2 with s1 s2 S.The Nuprl Proof Development System13I. Type Theory: Distinguishing Features
Nuprl’s Proof Theory Sequentx1:T1,.,xn:Tn Cbext tc“If xi are variables of type Ti then C has a (yet unknown) member t”– A judgment t T is represented as T bext tc; proof term construction– Equality is represented as type s t T bext Axc; propositions as types– Typehood represented by (cumulative) universes U i bext Tc Refinement calculus– Top-down decomposition of proof goal; interactive proof development– Bottom-up construction of proof terms; program extractionΓ S T bext λx.ec by lambda-formation xΓ, x:S T bext ecΓ S S U i bext Axc– Computation rules; program evaluationAbout 8–10 inference rules for each Nuprl typeThe Nuprl Proof Development System14I. Type Theory: Distinguishing Features
Executing a Formal Proof StepTHM intsqrtTheorem nameStatus position in proof# top 1Hypothesis of main goal1. x:INConclusion y:IN. y2 xInference ruleBY natE 1First subgoal – status, conclusion1# y:IN. y2 0Second subgoal – status,2# 2. n:INnew hypothesesx (y 1)2 0 (y 1)23. 0 n4. v: y:IN. y2 n-1 y:IN. y2 nconclusionThe Nuprl Proof Development System 15 n-1 (y 1)2n (y 1)2I. Type Theory: Distinguishing Features
Methodology for building types Syntax:– Define canonical type– Define canonical members of the type– Define noncanonical expressions corresponding to the type Semantics– Introduce evaluation rules for non-canonical expressions– Define type equality judgment for the typeThe typehood judgment is a special case of type equality– Define member equality judgment for canonical membersThe membership judgment is a special case of member equalityDefine judgments only in terms of the new expressions; consistency Proof Theory– Introduce proof rules that are consistent with the semanticsThe Nuprl Proof Development System16I. Type Theory: Distinguishing Features
Methodology for defining proof rules Type Formation rules:– When are two types equal?(typeEquality)– How to build the type?(typeFormation)Γ S TUjΓ Uj bext Tc Canonical rules:– When are two members equal?(member Equality)– How to build members?(member Formation)Γ s t TΓ T bext tc Noncanonical rules:– When does a term inhabit a type? (noncanonical Equality)– How to use a variable of the type(typeElimination)Γ s t TΓ, x:S, T bext tc Computation rules:– Reduction of redices in an equality (noncanonical Reduce*)Γ redex t Special purpose rulesThe Nuprl Proof Development System17I. Type Theory: Distinguishing Features T
Proof Rules for the Function TypeΓ Uj bext x:S Tcby dependent functionFormation x SΓ S Uj bext AxcΓ x1:S 1 T 1 x2:S 2 T 2Γ λx1.t1 λx2.t2Γ x:S T bext λx0.tcby lambdaFormation j x0Γ, x0:S T [x0/x] bext tcΓ S Uj bext Axcby functionEquality xΓ S 1 S 2 Uj bext AxcΓ, x:S 1 T1 [x/x1 ] T2 [x/x2 ]Γ, x:S Uj bext Tc x:S T bext Axcby lambdaEquality j x0Γ, x0 :S t1 [x0 /x1 ] t2 [x0 /x2 ] T [x0 /x] bext AxcΓ S Uj bext AxcΓ f 1 t1 f 2 t2 T [t1/x] bext Axcby applyEquality x:S TΓ f 1 f 2 x:S T bext AxcΓ t1 t2 S bext AxcΓ (λx.t) s t2by applyReduceΓ t[s/x] t2 Uj bext Axc Uj bext AxcΓ, f : x:S T , C bext t[f s, Ax/y, z]cby dependent functionElimination i s y zΓ, f : x:S T , s S bext AxcΓ, f : x:S T , y:T [s/x], z: y f s T [s/x], C bext tcΓ f 1 f 2 x:S T bext tcby functionExtensionality j x1:S 1 T 1 x2:S 2 T 2 x0Γ, x0:S f 1 x0 f 2 x0 T [x0/x] bext tcΓ S Uj bext AxcT bext AxcT bext AxcΓ f1Γ f2 x1:S 1 T 1 bext Axcx2:S 2 T 2 bext AxcNote: e e T is usually abbreviated by e TThe Nuprl Proof Development System18I. Type Theory: Distinguishing Features
User-defined Extensions Conservative extension of the formal language Abstraction: new-opid {parms}(sub-terms) expr [parms, sub-terms]e.g. exists{}(T ; x.A[x]) x:T A[x] Display Form for newly defined terme.g. x:T .A[x] exists{}(T ; x.A[x])Library contains many standard extensions of Type Theorye.g. Intuitionistic logic, Number Theory, List Theory, Algebra, . . . Tactics: User-defined inference rules– Meta-level programs built using basic inference rules and existing tactics– May include meta-level analysis of the goal to find a proof– Always result in a valid proofLibrary contains many standard tactics and proof search proceduresThe Nuprl Proof Development System19I. Type Theory: Distinguishing Features
Standard Nuprl TypesFunction SpaceProduct SpaceDisjoint UnionUniversesEqualityEmpty TypeAtomsS T , x:S TS T , x:S TS TUjs t TVoidAtomλx.t, f ths,ti, let hx,yi e in uinl(s), inr(t), case e of inl(x) 7 u inr(y) 7 vNumbersZZListsInductive Typesi jS listrectype X T [X]0,1,-1,2,-2,. . . s t, s-t, s*t, s t, s rem t,if a b then s else t, if i j then s else tind(u; x,fx.s; base; y,fy .t)Ax[], t::list, rec-case L of [] 7 base x::l 7 [fl ].tlet f (x) t in f (e), — members defined by T [X] —{x:S P [x]}, x:S.T [x],x:S T [x]Union x:S.T [x]Quotientx,y : S//E[x, y]Very Dep. Functions {f x:S T [f, x]}Squiggle Equalitys tSubsetIntersectionThe Nuprl Proof Development System— types of level j —Axany(x), — no members —"token", if a b then s else t— some members of S —— members that occur in all T [x] —— members x that occur S and T [x] —— members that occur in some T [x], tricky equality—— members of S, new equality —— a “simpler” equality20I. Type Theory: Standard Nuprl types
Functions: Basic Programming ConceptsSyntax:S T , λx.eCanonical:Noncanonical: e1 e2Evaluation:βλx.u t u[t/x]Semantics:· S T is a type if S and T are· λx1.e1 λx2.e2 in S T if S T type ande1[s1/x1] e2[s2/x2] in T for all s1, s2 with s1 s2 SProof System: — see above —The Nuprl Proof Development System21I. Type Theory: Standard Nuprl types
Cartesian Products: Building Data StructuresSyntax:Canonical:S T , he1,e2iNoncanonical: let hx,yi e in uEvaluation:βlet hx,yi he1,e2i in u u[e1, e2 / x, y]Semantics:· S T is a type if S and T are· he1,e2i he1’,e2’i in S T if S T type, e1 e1’ in S, and e2 e2’ in TLibrary Concepts: e.1, e.2The Nuprl Proof Development System22I. Type Theory: Standard Nuprl types
Disjoint Union: Case DistinctionsSyntax:Canonical:S T , inl(e), inr(e)Noncanonical: case e of inl(x) 7 u inr(y) 7 vEvaluation:case inl(e’) of inl(x) 7 u inr(y) 7 vcase inr(e’) of inl(x) 7 u inr(y) 7 vβ u[e0 / x]β v[e0 / y]Semantics:· S T is a type if S and T are· inl(e) inl(e’) in S T if S T type, e e’ in S· inr(e) inr(e’) in S Tif S T type, e e’ in TLibrary Concepts: ——The Nuprl Proof Development System23I. Type Theory: Standard Nuprl types
The Curry-Howard Isomorphism, formallyPropositions are represented as typesPropositionTypeP Q P QP Q P Q x:T P [x]P Q P x:T .P [x] x:T .P [x] P QP Voidx:T P [x]Need an empty type to represent “falsehood”Need dependent types to represent quantifiersThe Nuprl Proof Development System24I. Type Theory: Standard Nuprl types
Empty TypeSyntax:Canonical:Void– no canonical elements –Noncanonical: any(e)Evaluation: – no reduction rules –Semantics:· Void is a type· e e’ in Void never holdsLibrary Concepts: ——Warning: rules for Void allows proving semantical nonsense likex:Void 0 1 2The Nuprl Proof Development Systemor25 Void 2 typeI. Type Theory: Standard Nuprl types
Singleton TypeSyntax:Canonical:Unit, AxNoncanonical: – no noncanonical expressions –Evaluation: – no reduction rules –Semantics:· Unit is a type· Ax Ax in UnitLibrary Concepts: ——Defined type in Nuprl, see the library theory core 1 for further detailsThe Nuprl Proof Development System26I. Type Theory: Standard Nuprl types
Dependent types Allow representing logical quantifiers as type constructs Allow typing functions likeλx. if x 0 then λx.x else λx,y.x Allow expressing mathematical concepts such as finite automata– (Q,Σ,q0,δ,F), where q0 Q, δ:Q Σ Q, F Q. Allow representing dependent structures in programming languages– Record types [f1:T1; .; fn:Tn]– Variant recordstype date January of 1.31 February of 1.28 . Nuprl had them from the beginning. . . as did Coq, Alf, . . .– Other systems have recently adopted them (PVS, SPECWARE, .)The Nuprl Proof Development System27I. Type Theory: Standard Nuprl types
Dependent Functions (Π-Types)Subsumes independent function type generalizes Syntax:x:S T , λx.eCanonical:Noncanonical: e1 e2Evaluation:βλx.u t u[t/x]Semantics:· x:S T is a type if S is a type and T [e/x] is a type for all e in S· λx1.e1 λx2.e2 in x:S T if x:S T type ande1[s1/x1] e2[s2/x2] in T [s1/x] for all s1, s2 with s1 s2 SThe Nuprl Proof Development System28I. Type Theory: Standard Nuprl types
Dependent Products (Σ-Types)Subsumes (independent) cartesian product generalizes Syntax:Canonical:x:S T , he1,e2iNoncanonical: let hx,yi e in uEvaluation:βlet hx,yi he1,e2i in u u[e1, e2 / x, y]Semantics:· x:S T is a type if S is a type and T [e/x] is a type for all e in S· he1,e2i he1’,e2’i in x:S T if x:S T type,e1 e1’ in S, and e2 e2’ in T [e1/x]The Nuprl Proof Development System29I. Type Theory: Standard Nuprl types
Well-formedness Issues Formation rules for dependent type require checkingx0:S T [x0/x] type– T is a function from S to types that could involve complex computations,e.g. T [i] if Mi(i) halts then IN else VoidWell-formedness is undecidablein (extensional) theories with dependent types Programming languages must restrict dependencies– Only allow finite dependencies; decidable typechecking Typechecking in Nuprl cannot be fully automated– Typechecking becomes part of the proof process; heuristic typechecking Additional problem– What is the type of a function from IN to types?The Nuprl Proof Development System30; Girard ParadoxI. Type Theory: Standard Nuprl types
Universes Syntactical representation of typehood– T type expressed as T U — S T expressed as S T U Universes are object-level terms– U is a type and a universe– Girard’s Paradox: a theory with dependent types and U U is inconsistent7 No single universe can capture the notion of typehood– Typehood ˆ cumulative hierarchy of universes U UU1 U2 U3 .Syntax:Canonical:UjNoncanonical: —Semantics:· Uj is a typefor every positive integer j· S T in Ujif . . . mimic semantics for S T· Uj1 Uj2 in Uj if j1 j2 jThe Nuprl Proof Development System31as types. . .I. Type Theory: Standard Nuprl types
Integers: Basic ArithmeticSyntax:Canonical:ZZ , 0, 1, -1, 2, -2, . . . i j, AxNoncanonical: rec-case i of x 0 7 [fx ].s 0 7 b y 0 7 [fy ].t,s t, s-t, s*t, s t, s rem t,if i j then s else t, if i j then s else t,Evaluation:βrec-case 0 of x 0 7 [fx ].s 0 7 b y 0 7 [fy ].t brec-case i of x 0 7 [fx ].s 0 7 b y 0 7 [fy ].twhere i 0β t[i, rec-case i 1 of x 0 7 [fx ].s 0 7 b y 0 7 [fy ].t / x, fx]rec-case i of x 0 7 [fx ].s 0 7 b y 0 7 [fy ].twhere i 0β s[i, rec-case i 1 of x 0 7 [fx ].s 0 7 b y 0 7 [fy ].t / x, fx]other noncanonical expressions evaluate as usualSemantics:· ZZ is a type· i j is a type if i ZZ and j ZZ· i i in ZZfor all integer constants i· Ax Ax in i j if i, j are integers with i jLibrary Concep
The Nuprl Proof Development System 8 Calculemus, September 2002 Overview p Introduction 1.Nuprl’s Type Theory { Distinguishing Features { Standard Nuprl Types 2.The Nuprl Proof Development System { Architecture and Feature Demonstration 3.Proof Automation in Nuprl { Tactics & Rewriting { Decision Procedures { External Proof Systems 4.Building .
May 02, 2018 · D. Program Evaluation ͟The organization has provided a description of the framework for how each program will be evaluated. The framework should include all the elements below: ͟The evaluation methods are cost-effective for the organization ͟Quantitative and qualitative data is being collected (at Basics tier, data collection must have begun)
Silat is a combative art of self-defense and survival rooted from Matay archipelago. It was traced at thé early of Langkasuka Kingdom (2nd century CE) till thé reign of Melaka (Malaysia) Sultanate era (13th century). Silat has now evolved to become part of social culture and tradition with thé appearance of a fine physical and spiritual .
On an exceptional basis, Member States may request UNESCO to provide thé candidates with access to thé platform so they can complète thé form by themselves. Thèse requests must be addressed to esd rize unesco. or by 15 A ril 2021 UNESCO will provide thé nomineewith accessto thé platform via their émail address.
̶The leading indicator of employee engagement is based on the quality of the relationship between employee and supervisor Empower your managers! ̶Help them understand the impact on the organization ̶Share important changes, plan options, tasks, and deadlines ̶Provide key messages and talking points ̶Prepare them to answer employee questions
Dr. Sunita Bharatwal** Dr. Pawan Garga*** Abstract Customer satisfaction is derived from thè functionalities and values, a product or Service can provide. The current study aims to segregate thè dimensions of ordine Service quality and gather insights on its impact on web shopping. The trends of purchases have
since 1950 E. German, Suhl choke-bore barrel mark PROOF MARKS: GERMAN PROOF MARKS, cont. PROOF MARKS: ITALIAN PROOF MARKS, cont. ITALIAN PROOF MARKS PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1951 Brescia provisional proof for all guns since 1951 Gardone provisional proof for all guns
PROOF MARKS: BELGIAN PROOF MARKSPROOF MARKS: BELGIAN PROOF MARKS, cont. BELGIAN PROOF MARKS PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1852 Liege provisional black powder proof for breech loading guns and rifled barrels - Liege- double proof marking for unfurnished barrels - Liege- triple proof provisional marking for
The business architecture maps out a view of banking capabilities and services that will allow for strategic growth. In this it is important to recognize that the nature of banking and the way banking products are delivered has shifted dramatically since the 1980s and early 1990s. In the past products were typically defined by the capabilities of legacy banking systems, with the branch being .
