5 ms·

Can you explain what parts of the TLA+ stuff you can express in Prolog and why you think that might be better (or equally good)? It's true that modeling languag

Can you explain what parts of the TLA+ stuff you can express in Prolog and why you think that might be better (or equally good)? It's true that modeling languages all have something in common with Prolog, but do you think that proofs about a similar Prolog version would be nicer than in TLA+?

carapace 7y ago
I don't know if it's better or nicer. "I am but an egg." Here is Lecture 4 of Lamport's course: https://lamport.azurewebsites.net/video/video4.html https://lamport.azurewebsites.net/video/video4.html TLA+ source code: EXTENDS Integers VARIABLES small, big TypeOK == /\ small \in 0..3 /\ big \in 0..5 Init == /\ big = 0 /\ small = 0 FillSmall == /\ small' = 3 /\ big' = big FillBig == /\ big' = 5 /\ small' = small EmptySmall == /\ small' = 0 /\ big' = big EmptyBig == /\ big' = 0 /\ small' = small SmallToBig == IF big + small =< 5 THEN /\ big' = big + small /\ small' = 0 ELSE /\ big' = 5 /\ small' = small - (5 - big) BigToSmall == IF big + small =< 3 THEN /\ big' = 0 /\ small' = big + small ELSE /\ big' = small - (3 - big) /\ small' = 3 Next == \/ FillSmall \/ FillBig \/ EmptySmall \/ EmptyBig \/ SmallToBig \/ BigToSmall This is what I came up with (SWI Prolog). Note that I made some constraints explicit to prune the search, like guarding the empty_FOO steps with constraints that the jugs must not already be empty: :- use_module(library(clpfd)). type_ok(Small, Big) :- Small in 0..3, Big in 0..5. next_dh(Moves) :- next_dh(0, 0, Moves). next_dh(Small, Big, [[Move, Si, Bi]|Moves]) :- type_ok(Small, Big), die_hard(Move, Small, Big, Si, Bi), (Bi = 4 -> Moves = [] ; next_dh(Si, Bi, Moves)). die_hard( fill_small, Small, Big, 3, Big) :- Small #< 3. die_hard( fill_big, Small, Big, Small, 5) :- Big #< 5. die_hard(empty_small, Small, Big, 0, Big) :- Small #> 0. die_hard( empty_big, Small, Big, Small, 0) :- Big #> 0. die_hard(small_to_big, Small, Big, S, B) :- Big #< 5, Small #> 0, small_to_big(Small, Big, S, B). die_hard(big_to_small, Small, Big, S, B) :- Small #< 3, Big #> 0, big_to_small(Small, Big, S, B). big_to_small(Small, Big, S, 0) :- Small + Big #=< 3, S #= Small + Big. big_to_small(Small, Big, 3, B) :- Small + Big #> 3, B #= Big - (3 - Small). small_to_big(Small, Big, 0, B) :- Small + Big #=< 5, B #= Small + Big. small_to_big(Small, Big, S, 5) :- Small + Big #> 5, S #= Small - (5 - Big). And here's a query with depth limit and some manual reflow of the list for presentation... ?- call_with_depth_limit(next_dh(Moves), 11, _). Moves = [ [fill_big, 0, 5], [big_to_small, 3, 2], [empty_small, 0, 2], [big_to_small, 2, 0], [fill_big, 2, 5], [big_to_small, 3, 4] ] ; true.
- tom_mellior 7y ago
  This is very neat. It shows that Prolog is very close to being the holy grail of an executable specification language. But my question was about verification: TLA+ is not just used for modeling but also for proving stuff about the models. Do you have anything similar for Prolog? If yes, I would love to use it :-) If you're only interested in the specification part of TLA+ but in proofs, that's great. But then it's not fair to claim that you can do everything in Prolog that TLA+ does.
  - carapace 7y ago
    > This is very neat. Cheers! > Do you have anything similar for Prolog? Well, what you think of "Formal Methods: A First Introduction using Prolog to specify Programming Language Semantics"? https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf Abstract > An important fundamental idea in formal methods is that programs are mathematical objects one can reason about. Here we introduce students and developers to these ideas in the context of formal programming language semantics. We use first-order Horn clause logic as implemented by Prolog both as a specification and a proof scripting language. A module we have written facilitates using Prolog as a proof assistant and insures that Prolog implements a sound logic. In order to illustrate our approach we specify the semantics of a small functional language and demonstrate various proof approaches and styles. I just found this the other day and it seems promising. > it's not fair to claim that you can do everything in Prolog that TLA+ does. A claim I didn't make. "So far", I said, and, "I'm not to far into it yet" (sic). :-) (Although it's trivially true because of Turing completeness, eh?) I have great respect for Lamport. I would hate to be unfair to him.
    - tom_mellior 7y ago
      Oh, that paper is very interesting, thanks for that. It's not really comparable to a fully formal system, though: The user essentially chooses which trivial things to prove to convince themselves of something. For example, a real proof assistant would tell you what exactly to prove for the inductive proof in the factorial example. In this system you pick an induction principle yourself and hope it's correct. Still, I'd like to see more work along these lines.

carapace 7y ago

I don't know if it's better or nicer. "I am but an egg." Here is Lecture 4 of Lamport's course: https://lamport.azurewebsites.net/video/video4.html https://lamport.azurewebsites.net/video/video4.html TLA+ source code: EXTENDS Integers VARIABLES small, big TypeOK == /\ small \in 0..3 /\ big \in 0..5 Init == /\ big = 0 /\ small = 0 FillSmall == /\ small' = 3 /\ big' = big FillBig == /\ big' = 5 /\ small' = small EmptySmall == /\ small' = 0 /\ big' = big EmptyBig == /\ big' = 0 /\ small' = small SmallToBig == IF big + small =< 5 THEN /\ big' = big + small /\ small' = 0 ELSE /\ big' = 5 /\ small' = small - (5 - big) BigToSmall == IF big + small =< 3 THEN /\ big' = 0 /\ small' = big + small ELSE /\ big' = small - (3 - big) /\ small' = 3 Next == \/ FillSmall \/ FillBig \/ EmptySmall \/ EmptyBig \/ SmallToBig \/ BigToSmall This is what I came up with (SWI Prolog). Note that I made some constraints explicit to prune the search, like guarding the empty_FOO steps with constraints that the jugs must not already be empty: :- use_module(library(clpfd)). type_ok(Small, Big) :- Small in 0..3, Big in 0..5. next_dh(Moves) :- next_dh(0, 0, Moves). next_dh(Small, Big, [[Move, Si, Bi]|Moves]) :- type_ok(Small, Big), die_hard(Move, Small, Big, Si, Bi), (Bi = 4 -> Moves = [] ; next_dh(Si, Bi, Moves)). die_hard( fill_small, Small, Big, 3, Big) :- Small #< 3. die_hard( fill_big, Small, Big, Small, 5) :- Big #< 5. die_hard(empty_small, Small, Big, 0, Big) :- Small #> 0. die_hard( empty_big, Small, Big, Small, 0) :- Big #> 0. die_hard(small_to_big, Small, Big, S, B) :- Big #< 5, Small #> 0, small_to_big(Small, Big, S, B). die_hard(big_to_small, Small, Big, S, B) :- Small #< 3, Big #> 0, big_to_small(Small, Big, S, B). big_to_small(Small, Big, S, 0) :- Small + Big #=< 3, S #= Small + Big. big_to_small(Small, Big, 3, B) :- Small + Big #> 3, B #= Big - (3 - Small). small_to_big(Small, Big, 0, B) :- Small + Big #=< 5, B #= Small + Big. small_to_big(Small, Big, S, 5) :- Small + Big #> 5, S #= Small - (5 - Big). And here's a query with depth limit and some manual reflow of the list for presentation... ?- call_with_depth_limit(next_dh(Moves), 11, _). Moves = [ [fill_big, 0, 5], [big_to_small, 3, 2], [empty_small, 0, 2], [big_to_small, 2, 0], [fill_big, 2, 5], [big_to_small, 3, 4] ] ; true.

tom_mellior 7y ago
This is very neat. It shows that Prolog is very close to being the holy grail of an executable specification language. But my question was about verification: TLA+ is not just used for modeling but also for proving stuff about the models. Do you have anything similar for Prolog? If yes, I would love to use it :-) If you're only interested in the specification part of TLA+ but in proofs, that's great. But then it's not fair to claim that you can do everything in Prolog that TLA+ does.
- carapace 7y ago
  > This is very neat. Cheers! > Do you have anything similar for Prolog? Well, what you think of "Formal Methods: A First Introduction using Prolog to specify Programming Language Semantics"? https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf Abstract > An important fundamental idea in formal methods is that programs are mathematical objects one can reason about. Here we introduce students and developers to these ideas in the context of formal programming language semantics. We use first-order Horn clause logic as implemented by Prolog both as a specification and a proof scripting language. A module we have written facilitates using Prolog as a proof assistant and insures that Prolog implements a sound logic. In order to illustrate our approach we specify the semantics of a small functional language and demonstrate various proof approaches and styles. I just found this the other day and it seems promising. > it's not fair to claim that you can do everything in Prolog that TLA+ does. A claim I didn't make. "So far", I said, and, "I'm not to far into it yet" (sic). :-) (Although it's trivially true because of Turing completeness, eh?) I have great respect for Lamport. I would hate to be unfair to him.
  - tom_mellior 7y ago
    Oh, that paper is very interesting, thanks for that. It's not really comparable to a fully formal system, though: The user essentially chooses which trivial things to prove to convince themselves of something. For example, a real proof assistant would tell you what exactly to prove for the inductive proof in the factorial example. In this system you pick an induction principle yourself and hope it's correct. Still, I'd like to see more work along these lines.