CS 421 Lecture 20: Proof systems Lecture outline Defining proof systems Judgments Axioms Rules of inferenceProofsProofs Tsimp: Simple proof system for types in Ocaml OSsimp: Simple proof system for operational semantics of OCaml7/20/20091Motivation Understanding and reasoning about programs and programming languages How does OCaml type inference work? Can we provethat a program is correct?I.e., that the result of the computation is always what we would expect.7/20/20092Proof systems Proof system: formalized representation of mathematical proofs based on axiomsand rules of inference. Can be used to formalize deductions for many purposes Type-checking axioms and rules of inference allow proofs of assertions (a.k.a. “judgments”) of the form “expression e has assertions (a.k.a. “judgments”) of the form “expression e has type τ”. Operational semantics rules allow proofs of judgments of the form “eevaluates to v”. Axiomatic semantics rules allow proofs of judgments of the form “If the variables in a program initially satisfy some conditions C, then after executing statement S, they will satisfy conditions C’ ”.7/20/20093Proof systemsTo define a proof system, we need to define three things: Judgments: A judgment J is an assertion whose truth is subject to proof. Axioms: Judgments that are assumed to be true without proof. There are usually an infinite number of axioms, so proof. There are usually an infinite number of axioms, so they can’t all be listed, but they need to be described in some way. Written: Rules of inference: Rules that allow you to infer a judgment from one or more previously-inferred judgments. Written:7/20/20094JJJJn...1Proofs Given a proof system, a proof is a tree labeled with judgments, such that: Every judgment labeling a leaf node is an axiom Every judgment labeling an internal node can be inferred from its children by a rule of inference. Notational notes:1. Axioms and rules of inference are usually given names, and these names are placed in the proof tree2. Proof trees are written with the root – the main judgment being proved at the bottom.7/20/20095Tsimp– simplified OCaml type system Types: int | τ→τ’ (for any types τ and τ’) Type environments Γ: mapping from variables to typesJudgments:τ:e−Γ├Judgments: Expressions: constants, variables, abstractions, application7/20/20096τ:e−Γ├Tsimp– simplified OCaml type systemAxioms(Const)int:0−Γint:1−Γ├├(and many more)(Var)7/20/20097intintint:→→+−Γxx Γ−Γ:├├Tsimp– simplified OCaml type systemRules of inference:(Application)'::':2121ττττeeee−Γ−Γ→−Γ├ ├├(Abstraction)7/20/20098':fun ':]:[ττττ→→−Γ−Γexex├Examplefun x -> fun y -> (+ x) y : int → int → int7/20/20099Examplefun g -> g(fun x-> x+1) : ((int → int) → int) → int 7/20/200910Notes on Tsimp Given Γ, e, and τ: The structure of the proof tree is completely determined by e – it is the same as the abstract syntax. The content of the proof tree is almost completely determined by e and τ; however, in the application rule, even given Γ, e1, e2, and τ’, τis not uniquely determined.and τ’, τis not uniquely determined.Proving is called type checking.Findingτ such that can be proved is called type inference.7/20/200911τ:Ø e−├τ:Ø e−├OSsimp– simplified OCaml operational semantics The operational semantics of a language says, in an abstract way, how programs in a language are executed. For a functional language like Ocaml, the operational semantics should say how expressions are evaluated. We will take the view that the evaluation of an expression involves transforming it to another, simpler expression.E.g., “(fun x -> x*x) 4” evaluates to “16”.7/20/200912OSsimp– simplified OCaml operational semantics We give the operational semantics of a very simplified OCaml as a proof system. We need to define the judgments of the system, and then give the axioms and rules of inference. Expressions (simplified Ocaml): constants, variables, fun x -> e, e1 e2, e1 e2⊕e, e1 e2, e1 e2 Values: constants, closed abstractions (i.e., fun x -> e, where e has no free variables other than x) Judgments: e ⇓ v (where e is closed)7/20/200913⊕OSsimp– simplified OCaml operational semantics Axioms(Const) for constants kkk⇓(Abstr) (fun x -> e closed)7/20/200914exex→⇓→fun funOSsimp– simplified OCaml operational semanticsRules of inference:(Application)veevxveveexe⇓⇓⇓→⇓21]/'['fun (δ rules)where is any built-in function7/20/200915vee⇓21⊕veevvvveve⇓⊕⊕=⇓⇓21212211Example+ (+ 3 4) 5 ⇓ 127/20/200916Example(fun x -> + x x) (+ 3 4) ⇓ 147/20/200917Example(fun f -> f(fun x -> x)) (fun y -> y) 4 ⇓ 47/20/200918Notes on OSsimp The structure of the proof tree for e ⇓ v is similarto thestructure of e, but not the same. It would be less similar if our simple language had recursion. However, the proof tree – structure and content – are completely, unambiguously determined by the expression completely, unambiguously determined by the expression e. There is no intelligence or insight required; building the proof tree is completely mechanical.7/20/200919Next two lectures Will present more complex and realistic proof systems for type-checking and operational semantics of OCaml. Type system Polymorphism and the special role of “let”. Type-checking of references (i.e., assignable variables) Operational semantics Handling
View Full Document
Unlocking...