# HG changeset patch # User Christian Urban # Date 1384250242 0 # Node ID 10526c967679f39d0196ae582b65fa2a01b53c69 # Parent 4e108563716c55ba8a5be13fa54b323e4a28ebef added slides diff -r 4e108563716c -r 10526c967679 programs/prove1.scala --- a/programs/prove1.scala Tue Nov 12 08:03:16 2013 +0000 +++ b/programs/prove1.scala Tue Nov 12 09:57:22 2013 +0000 @@ -31,17 +31,18 @@ val goal = Judgement(Gamma, Del) // request: provable or not? +def partitions[A](ls: List[A]): List[(A, List[A])] = + ls.map (s => (s, ls diff List(s))) + + def prove(j: Judgement, sc: () => Unit) : Unit = { if (j.lhs.contains(j.rhs)) sc() // Axiom rule else prove1(j.lhs, j.rhs, sc) } -def partitions[A](ls: List[A]): List[(A, List[A])] = - ls.map (s => (s, ls diff List(s))) - def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = rhs match { - case True => sc() + case True => sc () case False => () case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) case Says(p, f1) => prove(Judgement(lhs, f1), sc) diff -r 4e108563716c -r 10526c967679 programs/prove2.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/programs/prove2.scala Tue Nov 12 09:57:22 2013 +0000 @@ -0,0 +1,130 @@ +import scala.language.implicitConversions +import scala.language.reflectiveCalls + +abstract class Term +case class Var(s: String) extends Term +case class Const(s: String) extends Term +case class Fun(s: String, ts: List[Term]) extends Term + +abstract class Form +case object True extends Form +case object False extends Form +case class Pred(s: String, ts: List[Term]) extends Form +case class Imp(f1: Form, f2: Form) extends Form +case class Says(p: String, f: Form) extends Form +case class And(f1: Form, f2: Form) extends Form +case class Or(f1: Form, f2: Form) extends Form + +case class Judgement(gamma: Set[Form], f: Form) { + def lhs = gamma + def rhs = f +} + +// some syntactic sugar +implicit def FormOps(f1: Form) = new { + def -> (f2: Form) = Imp(f1, f2) +} +implicit def StringOps(p: String) = new { + def says (f: Form) = Says(p, f) +} +implicit def SetFormOps(gamma: Set[Form]) = new { + def |- (f: Form) : Judgement = Judgement(gamma, f) +} + +val Admin = "Admin" +val Bob = "Bob" +val Del = Pred("del_file", Nil) + +val Gamma: Set[Form] = + Set( (Admin says Del) -> Del, + (Admin says ((Bob says Del) -> Del)), + (Bob says Del) ) + +val goal = Gamma |- Del // request: provable or not? + +def partitions[A](s: Set[A]): Set[(A, Set[A])] = + s.map (e => (e, s - e)) + + +def prove(j: Judgement, sc: () => Unit) : Unit = { + if (j.lhs.contains(j.rhs)) sc () // Axiom rule + else prove1(j.lhs, j.rhs, sc) +} + +def prove1(lhs: Set[Form], rhs: Form, sc: () => Unit) : Unit = + rhs match { + case True => sc () + case False => () + case Imp(f1, f2) => prove(lhs + f1 |- f2, sc) + case Says(p, f1) => prove(lhs |- f1, sc) + case Or(f1, f2) => + { prove(lhs |- f1, sc); + prove(lhs |- f2, sc) } + case And(f1, f2) => + prove(lhs |- f1, + () => prove(lhs |- f2, sc)) + case _ => { for ((f, lhs_rest) <- partitions(lhs)) + prove2(f, lhs_rest, rhs, sc) } + } + +def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = + f match { + case True => prove(lhs_rest |- rhs, sc) + case False => sc () + case And(f1, f2) => + prove(lhs_rest + f1 + f2 |- rhs, sc) + case Imp(f1, f2) => + prove(lhs_rest |- f1, + () => prove(lhs_rest + f2 |- rhs, sc)) + case Or(f1, f2) => + prove(lhs_rest + f1 |- rhs, + () => prove(lhs_rest + f2 |- rhs, sc)) + case Says(p, Imp(f1, f2)) => + prove(lhs_rest |- Says(p, f1), + () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) + case _ => () + } + + + +// function that calls prove and returns immediately once a proof is found +def run (j : Judgement) : Unit = { + try { + def sc () = { println ("Yes!"); throw new Exception } + prove(j, sc) + } + catch { case e: Exception => () } +} + +run (Set[Form]() |- False -> Del) +run (Set[Form]() |- True -> Del) +run (Set[Form]() |- Del -> True) + +run (goal) + +val Gamma1 : Set[Form] = + Set( Admin says ((Bob says Del) -> Del), + Bob says Del ) + +val goal1 = Gamma1 |- Del // not provable + +run (goal1) + +run (Set[Form]() |- (Del -> Del)) + +run (Set[Form]() |- (Del -> Or(False, Del))) + + +val Chr = "Christian" +val HoD = "Peter" +val Email = Pred("may_btain_email", List(Const(Chr))) +val AtLib = Pred("is_at_library", List(Const(Chr))) +val Chr_Staff = Pred("is_staff", List(Const(Chr))) + +val Policy_HoD = (HoD says Chr_Staff) -> Chr_Staff +val Policy_Lib = And(Chr_Staff, AtLib) -> Email +val HoD_says = HoD says Chr_Staff + +run (Set[Form](AtLib, Policy_HoD, Policy_Lib, HoD_says) |- Email) + + diff -r 4e108563716c -r 10526c967679 slides/slides06.pdf Binary file slides/slides06.pdf has changed diff -r 4e108563716c -r 10526c967679 slides/slides06.tex --- a/slides/slides06.tex Tue Nov 12 08:03:16 2013 +0000 +++ b/slides/slides06.tex Tue Nov 12 09:57:22 2013 +0000 @@ -704,12 +704,12 @@ \end{tabular} \end{center} -We are better be able to prove: +We better be able to prove: \begin{center} \begin{tabular}{@{}ll@{}} -(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\ -(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\ +(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\ +(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\ \end{tabular} \end{center} @@ -729,6 +729,38 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[t] + +I want to prove + +\begin{center} +\bl{$\Gamma \vdash \text{del\_file}$} +\end{center}\pause + +There is an inference rule + +\begin{center} +\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} +\end{center}\pause + +So I can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause + +\bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\ +So I can use the rule + +\begin{center} +\bl{\infer{\Gamma, F \vdash F}{}} +\end{center} + +\onslide<5>{\bf\alert{What is wrong with this?}} +\hfill{\bf Done. Qed.} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] \frametitle{}