advertisement

ynot march 2007

50 %
50 %
advertisement
Information about ynot march 2007
Entertainment

Published on June 17, 2007

Author: Sabatini

Source: authorstream.com

advertisement

Y0 Y-not Y-knot Y-naught?:  Y0 Y-not Y-knot Y-naught? Greg Morrisett with Aleks N., Ryan W., Paul G., Rasmus P., Lars B. ESC, JML, Spec#, …:  ESC, JML, Spec#, … Need a different spec language: 'pure' boolean expressions: length(x)==42 'modeling' types (e.g., pure lists, sets, …) If the implementation is pure, can’t use it in the specs! x.f versus \old(x.f) What if Simplify can’t prove something? Ignore (e.g., arith, modifies clause): unsound Rewrite code? Weaken spec? Not really modular: can’t write 'app' or 'map' DML, ATS, Omega, …:  DML, ATS, Omega, … Introduce different spec language. Again, a separate 'pure' language To capture all properties of lists, you’d have to index them with well, lists. Can’t talk about properties of effectful computations (or limited capacity). ATS can build proofs, but it’s awkward. Coq, PRL, Isabelle, …:  Coq, PRL, Isabelle, … Ynot starts with Coq as the basic language: [co]inductive definitions, h.o. functions, polymorphism, h.o. predicates, proofs, … Strong support for modularity e.g., can package up and abstract over terms, types, predicates, proofs, in a uniform fashion. can prove that, e.g., append is associative and rev(rev(x)) = x, etc. after defining it. But huge drawback: No effects (non-term, IO, state, recursive types, etc.) Not a strong phase separation Quick Coq:  Quick Coq Set : (think * in Haskell) nat, bool, functions from sets to sets, … inductive set definitions (e.g., list) co-inductive set definitions (e.g., stream) Prop : Think of nat-andgt;Prop as a subset of nat. Equality, /\, \/, etc. [co-]inductive definitions (e.g., judgments) Refinement:  Refinement Can form mixed products andamp; sums {n:nat | n andgt;= 42} is a pair of a nat and a proof that this nat is andgt;= 42. Array subscript: forall (A:Set)(n:nat) (v:vector n A) (j:nat), (j andlt; n) -andgt; A Can extract Ocaml or Haskell code. 'erase' Prop objects (really, replace with unit). Purity:  Purity We want to pull the Curry-Howard isomorphism to represent a proof of Prop P as a term with type P. Reduce proof-checking to type-checking. Should be no term with type False. If we added recursive functions, recursive types, exceptions, or refs, we could code up a term of type False. So everyone forgoes these 'features' in their type theory. Coq Demo:  Coq Demo A few examples… Ynot and HTT:  Ynot and HTT We add a new type constructor, IO A As in Haskell, encapsulate effectful computations. We’re not pretending that IO False is a proof of false -- rather, it’s a computation which when run, if it terminates, then it produces a proof of False. Of course, it can’t terminate. Ynot IO: Attempt #1:  Ynot IO: Attempt #1 IO : Set -andgt; Set return: forall (A:Set), A -andgt; IO A bind : forall (A B:Set), IO A -andgt; (A -andgt; IO B) -andgt; IO B ffix : forall (A:Set), (IO A -andgt; IO A) -andgt; IO A Reasoning about IO:  Reasoning about IO steps : IO A -andgt; IO A -andgt; Prop. steps_ret_bnd : forall (A B:Set)(v:A)(f:A-andgt;IO B), steps (bind (ret v) f) (f v). steps_bnd_cong : forall (A B:Set)(c1:IO A)(f:A-andgt;IO B), (steps c1 c2) -andgt; (steps (bind c1 f) (bind c2 f)). steps_ffix : forall (A:Set)(f:IO A-andgt;IO A), steps (ffix f) (f (ffix f)) Problem::  Problem: We have added a way to prove False! Sketch of problem (not quite right): Define diverges(c:IO A):Prop Define stepsn c1 c2 n as c1 steps to c2 in no more than n steps. Define diverges c as there’s no n and v such that stepsn c (ret v) n. Define T := { f : nat -andgt; IO nat | for some n, diverges(f n) } Problem Continued:  Problem Continued Next, define: f(p:T):T = {g;q } where g n = if n = 0 then 0 else (fst p)(n-1) and q argues that for some n, g diverges: (snd p) provides a proof that for some m, (fst p) diverges, so pick n=m+1. Finally, take F := ffix(f) snd(F) proves fst(F) diverges but fst(F) does not! How to Fix?:  How to Fix? One option: restrict IO to admissible types. In essence, we need closure conditions to ensure that fixed-points preserve typing. Comprehensions (subsets of types) are problematic in general. Crary shows some sufficient syntactic criteria for determining admissibility. Another option: don’t expose steps or any other axiom on IO terms. Well, we can expose some (the monad laws.) No Axioms?:  No Axioms? Can interpret IO A := unit. ret v = tt, bind v f = tt, ffix f = tt Without any axioms, can’t tell the difference! Allows us to establish consistency of logic. a trivial model. Aleks is then able to prove preservation and progress for the real operational semantics. But we have limited reasoning about computations within the system. Extending IO:  Extending IO We want to handle the awkward squad: Refs, IO, exceptions, concurrency, … So need to scale IO A. Today: refs, exceptions Tomorrow: IO Quite a ways off: concurrency? Heaps & Refs in Ynot:  Heaps andamp; Refs in Ynot We model heaps in Coq as follows: loc : Set loc_eq:(x y:loc)-andgt;{x=y}+{xandlt;andgt;y} can model locs as nats. dynamic := {T:Set; x:T} heap := loc -andgt; option dynamic NB: heaps aren’t 'Set' w/out impredicative IO Monad:  IO Monad Pre := heap -andgt; Prop Post(A:Set) := A -andgt; heap -andgt; heap -andgt; Prop IO: forall (A:Set), Pre -andgt; Post A -andgt; Post exn -andgt; Set. Implicit Arguments IO [A]. Return & Throw:  Return andamp; Throw ret : forall (A:Set)(x:A), IO (fun h =andgt; True) (fun y old h =andgt; y=x /\ h=old) (fun e old h =andgt; False) Implicit Arguments ret[A]. throw : forall (A:Set)(x:exn), IO (fun h =andgt; True) (fun y old h =andgt; False) (fun e old h =andgt; e=x /\ h=old) Reading a Location:  Reading a Location read : forall (A:Set)(x:loc), IO (fun h =andgt; exists v:A,mapsto h x v) (fun y old h =andgt; old = h /\ mapsto h x v) (fun e old h =andgt; False) where mapsto(A:Set)(h:heap)(x:loc)(v:A) := (h x) = Some(mkDynamic {A;v}} Writing a Location:  Writing a Location write : forall (A:Set)(x:loc)(v:A), IO (fun h =andgt; exists B, exists w:B, mapsto h x w) (fun y old h =andgt; y = tt /\ h = update old x A v) (fun e old h =andgt; False) Implicit Arguments write[A]. where update(h:heap)(x:loc)(A:Set)(v:A):heap := fun y =andgt; if (eq_loc x y) then Some(Dynamic{A,v}) else h y Bind:  Bind bind : forall (A B:Set)(P1:Pre)(Q1:Post A)(E1:Post exn) (P2:A-andgt;Pre)(Q2:A-andgt;Post B)(E2:A-andgt;Post exn), (IO A P1 Q1 E1) -andgt; (A -andgt; IO B P2 Q2 E2) -andgt; IO B (fun h =andgt; P1 h /\ (forall x m,(Q1 x h m) -andgt; P2 m)) (fun y old m =andgt; exists x m, (Q1 x old m) /\ (Q2 y m h)) (fun e old m =andgt; (E1 e old m) \/ (exists x m, (Q1 x old m) /\ (E2 e m h))) Implicit Arguments bind [A B P1 Q1 E1 P2 Q2 E2]. Using Bind:  Using Bind Definition readThen := fun (A B:Set)(x:loc) (p:A-andgt;pre)(q:A-andgt;post B) (e:A-andgt;post exn) (c:forall y:A, IO (p y) (q y) (e y))=andgt; bind (read A x) c. Implicit Arguments readThen [A B p q e]. Example::  Example: Definition swap := fun (A B:Set)(x y:loc) =andgt; (readThen x (fun (xv:A) =andgt; readThen y (fun (yv:B) =andgt; writeThen x yv (writeThen y xv (ret tt))))). Type Inferred for Swap:  Type Inferred for Swap forall (A B : Set) (x y : loc 1), IO (fun i : heap =andgt; (fun i0 : heap =andgt; exists v : A, mapsto i0 x v) i /\ (forall (x0 : A) (m : heap), (fun (y0 : A) (i0 m0 : heap) =andgt; mapsto i0 x y0 /\ m0 = i0) x0 i m -andgt; (fun (xv : A) (i0 : heap) =andgt; (fun i1 : heap =andgt; exists v : B, mapsto i1 y v) i0 /\ (forall (x1 : B) (m0 : heap), (fun (y0 : B) (i1 m1 : heap) =andgt; mapsto i1 y y0 /\ m1 = i1) x1 i0 m0 -andgt; (fun (yv : B) (i1 : heap) =andgt; (fun i2 : heap =andgt; exists B0 : Set, exists z : vector B0 1, mapsto_vec i2 x z) i1 /\ (forall (x2 : unit) (m1 : heap), (fun (_ : unit) (i2 m2 : heap) =andgt; m2 = update i2 x yv) x2 i1 m1 -andgt; (fun (_ : unit) (i2 : heap) =andgt; (fun i3 : heap =andgt; exists B0 : Set, exists z : vector B0 1, mapsto_vec i3 y z) i2 /\ (forall (x3 : unit) (m2 : heap), (fun (_ : unit) (i3 m3 : heap) =andgt; m3 = update i3 y xv) x3 i2 m2 -andgt; (fun _ : unit =andgt; nopre) x3 m2)) x2 m1)) x1 m0)) x0 m)) pre-condition only! Do:  Do do : forall (A:Set)(P1:Pre)(Q1:Post A)(E1:Post exn) (P2:Pre)(Q2:Post A)(E2:Post exn), (IO A P1 Q1 E1) -andgt; (forall h,(P2 h) -andgt; (P1 h)) -andgt; (forall y old m, (p2 old) -andgt; (Q1 y old m) -andgt; (Q2 y old m)) -andgt; (forall e old m, (p2 old) -andgt; (E1 y old m) -andgt; (E2 y old m)) -andgt; IO A P2 Q2 E2. Implicit Arguments do [A P1 Q1 E1]. Essentially, the rule of consequence. Ascribing a Spec to Swap:  Ascribing a Spec to Swap Program Definition swap_precise : forall (A B:Set)(x y:loc 1), IO (fun i =andgt; exists vx:A, exists vy:B, mapsto i x vx /\ mapsto i y vy) (fun (_:unit) i m =andgt; exists vx:A, exists vy:B, m = update (update i x vy) y vx) (fun _ _ _ =andgt; False) := fun A B x y =andgt; do (swap A B x y) _. Followed by a long proof. (can be shortened with combination of key lemmas and tactics.) Another Example::  Another Example: Definition InvIO(A:Set)(I:Pre) := IO I (fun (_:A) _ m =andgt; I m) (fun (_:exn) _ m =andgt; I m). Program Fixpoint mapIO(A B:Set)(I:pre) (f:A -andgt; B -andgt; InvIO B I (acc:B)(x:list A) {struct x} : InvIO B I := match x with | nil =andgt; do (ret acc) _ | cons h t =andgt; do (bind (f h acc) and#x4;and#x4; (fun acc2 =andgt; mapIO A B p q e pf f acc2 t)) _ end. Advantages:  Advantages For pure code: Can use refinements a la DML/ATS Or, can reason after the fact E.g., can prove append associative without having to tie it into the definition. Modeling language is serious e.g., heaps are defined in the model. Abstraction over values, types, specifications, and proofs (i.e., compositional!) If you stick to simple types, no proofs. Key Open Issues:  Key Open Issues Proofs are still painful. Need to adapt automation from ESC Need analogues to object invariants, ownership, etc. for mutable ADTs. Separation logic seems promising (next time). IO and other effects Need pre/post over worlds (heaps are just a part.) Better models? Predicate transformers seem promising Rasmus andamp; Lars working on denotational model

Add a comment

Related presentations

Related pages

YNot Web: Online Marketing, Web Design, Web Development ...

YNot Web specializes in creating complete Web Systems and custom website design and development for small businesses and entrepreneurs. We also offer services
Read more

Y0 Ynot Y-knot Y-naught? - eecs.harvard.edu

Y0 Y-not Y-knot Y-naught? Greg Morrisett with Aleks N., Ryan W., Paul G., Rasmus P., Lars B.
Read more

YNot Blog | YNot Web

YNot Blog; My Account; Sitemap © Copyright 2003 - 2015 YNot Web Inc. All Rights Reserved :::: YNot Web P.O. Box 1963 Fair Oaks, CA 95628 :: ... 2007; 2006 ...
Read more

ABQjournal: Cruces Man Wants To Be 'Ynot Bubba'

Front Page news state. Wednesday, March 14, 2007 Cruces Man Wants To Be 'Ynot Bubba' The Associated Press LAS CRUCES— Justin Brady's friends call him ...
Read more

Ynot

Ynot makes it easy to enhance its automation with support ... As of March 15, 2010, ynot-rdb contains a small tweak to ... July 2007. Ynot: Reasoning with ...
Read more

Ynot Entertainment, Inc. in Newbury Park, CA - Reviews ...

Ynot Entertainment, Inc. in Newbury Park, CA 91320 - Reviews - Lookup its California Secretary of State Registration.
Read more

ynoT_Gaming - Twitch

ynoT_Gaming Jul 8, 2016 10:08 PM Come check out my YouTube by that i mean sub or i will come and get u . 2 1. Share; Report; Are you sure you want to ...
Read more

Time dilation or malfunctioning clock? - International ...

Time dilation or malfunctioning clock? Science, Mathematics, ... Originally Posted by ynot. ... 14th March 2007 at 05:27 PM. 14th March 2007, 05:30 ...
Read more

Y 0 Y-not Y-knot Y-naught? | PPT Directory

http://www.eecs.harvard.edu/~greg/cs250rsp2007/ynot_march_2007.ppt. Preview. Download. Filesize: 5024 KB | Format : .PPT . No related posts.
Read more

Why Not Blog? - Marica Zottino

Gabriel Moreno. Stunning illustrations by Gabriel . Animals by Christopher Meyer. Animals, Moments of the Carters, Travis Latham and some other... is a ...
Read more