Galculator: Functional Prototype of a Galois-connection Based Proof Assistant
?
0 likes?349 views
This document describes a proof assistant called Galculator that is based on Galois connections. Galois connections allow algebraic reasoning about proofs by "abstracting" the underlying logic. The document motivates this approach using an example proof about whole number division. It then outlines the objectives of Galculator, which is to build a proof assistant that utilizes the algebra of Galois connections and associated tactics. Background information is provided on Galois connections and the pointfree transform, which abstracts variables from definitions for more compact symbolic manipulation.
![Galculator
Representation
Type representation
data Type a where
Bool :: Type Bool
Char :: Type Char
Int
:: Type Int
List
:: Type a ¡ú Type [a]
Set
:: Type a ¡ú Type (Set a)
Maybe :: Type a ¡ú Type (Maybe a)
¡¤ ¡Á ¡¤ :: Type a ¡ú Type b ¡ú Type (a, b)
Fun
Rel
GC
:: Type a ¡ú Type b ¡ú Type (a ¡û b)
:: Type a ¡ú Type b ¡ú Type (a ? b)
:: Type a ¡ú Type b ¡ú Type (GC a b)
LogoDI2
Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho)
Galculator
PPDP¡¯08
22 / 27](https://image.slidesharecdn.com/ppdp08-131120142222-phpapp02/85/Galculator-Functional-Prototype-of-a-Galois-connection-Based-Proof-Assistant-32-320.jpg)
Galculator: Functional Prototype of a Galois-connection Based Proof Assistant
- 1. Galculator Functional Prototype of a Galois-connection Based Proof Assistant Paulo Silva Jos¨¦ Nuno Oliveira Departamento de Inform¨¢tica Universidade do Minho Braga, Portugal Principles and Practice of Declarative Programming July 15 ¨C 17, 2008 Valencia LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 1 / 27
- 2. Outline Outline 1 Introduction Motivation Objectives 2 Theoretical background Galois connections Pointfree transform 3 Galculator Principles Representation 4 Conclusion Conclusion Future work LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 2 / 27
- 3. Introduction Outline 1 Introduction Motivation Objectives 2 Theoretical background Galois connections Pointfree transform 3 Galculator Principles Representation 4 Conclusion Conclusion Future work LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 3 / 27
- 4. Introduction Motivation Software correctness Current approaches Software correctness is an ambitious challenge Logic based approaches bene?t from the help of theorem provers Sometimes proofs are hindered by the theory It is not always easy to devise the correct strategy Alternatives Sometimes algebraic approaches are possible Algebras ¡°abstract¡± the underlying logic Proofs become more syntactic Galois connections can play an important role Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator LogoDI2 PPDP¡¯08 4 / 27
- 5. Introduction Motivation Whole division implementation Haskell code x ¡®div ¡® y | x < y = 0 | x y = (x ? y ) ¡®div ¡® y + 1 for non-negative x and positive y . This is the code. Where is the speci?cation? LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 5 / 27
- 6. Introduction Motivation Whole division speci?cation Implicit de?nition c =x ¡Ây ? ?r : 0 r <y : x =c¡Áy +r Explicit de?nition x ¡Ây = z :: z ¡Á y x Galois connection z ¡Áy x ? z x ¡Ây (y > 0) LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 6 / 27
- 7. Introduction Motivation Whole division Speci?cation vs. Implementation We can verify if the implementation meets the speci?cation. We can calculate the implementation from the speci?cation. De?nition (Indirect equality) a=b ? ? x :: x a?x b a=b ? ? x :: a x ?b x Another useful Galois connection a?b Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) c ? a Galculator c+b LogoDI2 PPDP¡¯08 7 / 27
- 8. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Â y assuming x x { cancellation, thanks to a ? b z ¡Áy ?y ? 0, y > 0 } c?a c+b } x ?y { distributivity } (z ? 1) ¡Á y ? { z ¡Áy z ?1 ? x ? z x ¡Â y assuming x y} (x ? y ) ¡Â y { a?b z x ?y c?a c+b } (x ? y ) ¡Â y + 1 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 8 / 27
- 9. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Â y assuming x x { cancellation, thanks to a ? b z ¡Áy ?y ? 0, y > 0 } c?a c+b } x ?y { distributivity } (z ? 1) ¡Á y ? { z ¡Áy z ?1 ? x ? z x ¡Â y assuming x y} (x ? y ) ¡Â y { a?b z x ?y c?a c+b } (x ? y ) ¡Â y + 1 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 8 / 27
- 10. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Â y assuming x x { cancellation, thanks to a ? b z ¡Áy ?y ? 0, y > 0 } c?a c+b } x ?y { distributivity } (z ? 1) ¡Á y ? { z ¡Áy z ?1 ? x ? z x ¡Â y assuming x y} (x ? y ) ¡Â y { a?b z x ?y c?a c+b } (x ? y ) ¡Â y + 1 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 8 / 27
- 11. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Â y assuming x x { cancellation, thanks to a ? b z ¡Áy ?y ? 0, y > 0 } c?a c+b } x ?y { distributivity } (z ? 1) ¡Á y ? { z ¡Áy z ?1 ? x ? z x ¡Â y assuming x y} (x ? y ) ¡Â y { a?b z x ?y c?a c+b } (x ? y ) ¡Â y + 1 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 8 / 27
- 12. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Â y assuming x x { cancellation, thanks to a ? b z ¡Áy ?y ? 0, y > 0 } c?a c+b } x ?y { distributivity } (z ? 1) ¡Á y ? { z ¡Áy z ?1 ? x ? z x ¡Â y assuming x y} (x ? y ) ¡Â y { a?b z x ?y c?a c+b } (x ? y ) ¡Â y + 1 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 8 / 27
- 13. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Â y assuming x x { cancellation, thanks to a ? b z ¡Áy ?y ? 0, y > 0 } c?a c+b } x ?y { distributivity } (z ? 1) ¡Á y ? { z ¡Áy z ?1 ? x ? z x ¡Â y assuming x y} (x ? y ) ¡Â y { a?b z x ?y c?a c+b } (x ? y ) ¡Â y + 1 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 8 / 27
- 14. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Ây } x { transitivity, since x < y } z ¡Áy ? x ¡Ä z ¡Áy <y { since y = 0 } z ¡Áy ? { z z x ¡Ä z 0 0 entails z ¡Á y x, since 0 x } 0 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 9 / 27
- 15. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Ây } x { transitivity, since x < y } z ¡Áy ? x ¡Ä z ¡Áy <y { since y = 0 } z ¡Áy ? { z z x ¡Ä z 0 0 entails z ¡Á y x, since 0 x } 0 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 9 / 27
- 16. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Ây } x { transitivity, since x < y } z ¡Áy ? x ¡Ä z ¡Áy <y { since y = 0 } z ¡Áy ? { z z x ¡Ä z 0 0 entails z ¡Á y x, since 0 x } 0 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 9 / 27
- 17. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Ây } x { transitivity, since x < y } z ¡Áy ? x ¡Ä z ¡Áy <y { since y = 0 } z ¡Áy ? { z z x ¡Ä z 0 0 entails z ¡Á y x, since 0 x } 0 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 9 / 27
- 18. Introduction Motivation Proof. z ? x ¡Ây { z ¡Áy z ¡Áy ? x ? z x ¡Ây } x { transitivity, since x < y } z ¡Áy ? x ¡Ä z ¡Áy <y { since y = 0 } z ¡Áy ? { z z x ¡Ä z 0 0 entails z ¡Á y x, since 0 x } 0 LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 9 / 27
- 19. Introduction Objectives Objectives Galculator Build a proof assistant based on Galois connections, their algebra and associated tactics LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 10 / 27
- 20. Theoretical background Outline 1 Introduction Motivation Objectives 2 Theoretical background Galois connections Pointfree transform 3 Galculator Principles Representation 4 Conclusion Conclusion Future work LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 11 / 27
- 21. Theoretical background Galois connections Galois connections De?nition (Galois connection) Given two preordered sets (A, A ) and (B, B ) and two functions g f Bo A and A o B , the pair (f , g) is a Galois connection if and only if, for all a ¡Ê A and b ¡Ê B: f a B b ? a A gb Graphical notation A Al f , g
- 22. B B or (A, A) o (f ,g) (B, B) LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 12 / 27
- 23. Theoretical background Galois connections Properties Property f a Bb?a Agb g (b B b ) = g b A g b f (a A a ) = f a B f a a A g (f a) f (g b) B b a A a ?f a B f a b B b ?g b A g b g B= A f ¡ÍA = ¡ÍB Description ¡°Shunting rule¡± Distributivity (UA over meet) Distributivity (LA over join) Lower cancellation Upper cancellation Monotonicity (LA) Monotonicity (UA) Top-preservation (UA) Bottom-preservation (LA) LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 13 / 27
- 24. Theoretical background Galois connections Galois connections ¡ª Algebra Identity connection (A, A) o (id,id) (A, A) Composition if (A, ) o (f ,g) (B, ) and (B, ) o (h,k ) (h?f ,g ?k ) (C, ) then (A, ) o (C, ) Composition is associative and the identity is its unit. Galois connections form a category. LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 14 / 27
- 25. Theoretical background Galois connections Galois connections ¡ª Algebra Converse if (A, ) o (f ,g) (B, ) then (B, ) o (g,f ) (A, ) Relator For every relator F that distributes through binary intersections, if (A, ) o (f ,g) (B, ) then (FA, F (F f ,F g) )o (FB, F ) LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 15 / 27
- 26. Theoretical background Pointfree transform Pointfree transform Based on the formalization of set theory without variables proposed by Tarski Abstracts points from de?nitions More compact and cryptic More amenable for syntactical manipulation LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 16 / 27
- 27. Theoretical background Pointfree transform Pointfree transform summary Pointwise ? c :: bRc ¡Ä cSa ? x :: xRb ? xSa ? x :: bRx ? aSx bRa ¡Ä cSa bRa ¡Ä dSc bRa ¡Ä bSa bSa ¡Å bSa (f b)R(g a) b=a True False ? a, b :: bRa ? bSa ? a, b :: bRa ? bSa ? a :: aRa Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator Pointfree b(R ? S)a b(R S)a b(S/R)a (b, c) R, S a (b, d)(R ¡Á S)(a, c) b(R ¡É S)a b(R ¡È S)a b(f ? ? R ? g)a b id a b a b¡Ía R?S R=S id ? R LogoDI2 PPDP¡¯08 17 / 27
- 28. Theoretical background Pointfree transform Pointfree de?nitions De?nition (Galois connection) f? ? B = A ? g De?nition (Indirect equality) f =g f =g ? ? ? f ? f = ? =g ? ? g ? LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 18 / 27
- 29. Galculator Outline 1 Introduction Motivation Objectives 2 Theoretical background Galois connections Pointfree transform 3 Galculator Principles Representation 4 Conclusion Conclusion Future work LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 19 / 27
- 30. Galculator Principles Design Principles Combine GC Derive Laws Relation algebra Derive Properties Derive Theory domain Derive Rules TRS Strategies Combine Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator LogoDI2 PPDP¡¯08 20 / 27
- 31. Galculator Representation Algebraic data types List de?nition ¡ª Algebraic data type data List a = Nil | Cons a (List a) List de?nition ¡ª Generalized algebraic data type data List a where Nil :: List a Cons :: a ¡ú List a ¡ú List a LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 21 / 27
- 32. Galculator Representation Type representation data Type a where Bool :: Type Bool Char :: Type Char Int :: Type Int List :: Type a ¡ú Type [a] Set :: Type a ¡ú Type (Set a) Maybe :: Type a ¡ú Type (Maybe a) ¡¤ ¡Á ¡¤ :: Type a ¡ú Type b ¡ú Type (a, b) Fun Rel GC :: Type a ¡ú Type b ¡ú Type (a ¡û b) :: Type a ¡ú Type b ¡ú Type (a ? b) :: Type a ¡ú Type b ¡ú Type (GC a b) LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 22 / 27
- 33. Galculator Representation Relational representation Representation Relation Functions Orders Galois connections Combinators data R ¡¤? ¡¤ ?¡¤ ¡¤ ¡¤¡Á¡¤ ... r where :: R (b ? a) ¡ú R (a ? b) :: Type b ¡ú R (c ? b) ¡ú R (b ? a) ¡ú R (c ? a) :: R (b ? a) ¡ú R (d ? c) ¡ú R ((b, d) ? (a, c)) LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 23 / 27
- 34. Conclusion Outline 1 Introduction Motivation Objectives 2 Theoretical background Galois connections Pointfree transform 3 Galculator Principles Representation 4 Conclusion Conclusion Future work LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 24 / 27
- 35. Conclusion Conclusion Conclusion Proof assistant prototype based on Galois connections Innovative approach Combination of Galois connections and pointfree calculus Non-trivial example of the application of distinctive features of functional languages Generalized algebraic data types Existential data types Combinatorial approaches (parsing, rewriting) Support for embedded domain speci?c languages Computations as monads Higher-order functions New: Polymorphic type representation with uni?cation ... LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 25 / 27
- 36. Conclusion Future work Future work User-friendly syntax Automated proofs Free-theorems Integration with host theorem provers LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 26 / 27
- 37. The End Download Source code and documentation available from www.di.uminho.pt/research/galculator Contact Questions to paufil@di.uminho.pt LogoDI2 Paulo Silva, Jos¨¦ Nuno Oliveira (UMinho) Galculator PPDP¡¯08 27 / 27