4 ms·

Thank you. I wanted to write something along the same vein (albeit much less eloquently!) but didn't get the chance.

by ahmedalsudani 8y ago

sgt101 8y ago
You can prove termination in many cases. But there are infinite cases where you can't prove it, and it will terminate.
- nickpsecurity 8y ago
  I'm still learning about how much of a problem that is in practice. I have less data on analyzing infinite-state systems. What both real-time and functional developers said to do was this: 1. Design the main computation or loop to operate on a fixed chunk of data in a way that can be verified in isolation. 2. Design a component that either streams in new data or says there is none. Verify it in isolation. 3. Compose the two. The result will take X proven timing multiplied by Y amount of streamed data for as long as it runs or do nothing if stream is empty. Shouldn't this handle what you describe in the general case or does that simple strategy fall apart even on common stuff with event loops?
  - carapace 8y ago
    FWIW in the limited time I've been using Prolog that pattern has worked fine for me. A factor to consider: Prolog is old. It's very unlikely to encounter some problem or issue that ahs not already been addressed, often by a team of researchers. For example, when I was exploring Prolog I tried a simple transformation on syllogisms. I found some code online that had them in this form: syll(all(M,P), all(S,M), all(S,P)). % This is barbara in the 1st figure. syll(no(M,P), all(S,M), no(S,P)). % This is celarent in the 1st figure. Etc... I transformed them using term_expansion/2 [1] with this rule: term_expansion(syll(A, B, C), (C :- B, A)). To generate rules like these: all(A, C) :- all(A, B), all(B, C). no(A, B) :- all(A, C), no(B, C). Etc... However, these rules (plus a few facts: all(dogs, canines). all(canines, mammals). ) led to huge open-ended search. ?- all(A, B). ERROR: Out of local stack It turns out I can just use call_with_depth_limit/3 [2] to bound the search depth: ?- call_with_depth_limit(all(A, B), 10, R). A = dogs, B = mammals, R = 11 ; A = dogs, B = canines, R = 11 ; A = canines, B = mammals, R = 1. It finds some solutions. Not all Prologs have call_with_depth_limit/3 built-in but it's easy to write a meta-interpreter that does the same thing.[3] From the POV of security, the trick I want to explore is writing Prolog code to generate provably-correct machine code. [1] http://www.swi-prolog.org/pldoc/doc_for?object=term_expansion/2 http://www.swi-prolog.org/pldoc/doc_for?object=term_expansio... [2] http://www.swi-prolog.org/pldoc/doc_for?object=call_with_depth_limit/3 http://www.swi-prolog.org/pldoc/doc_for?object=call_with_dep... [3] https://en.wikipedia.org/wiki/Iterative_deepening_depth-first_search https://en.wikipedia.org/wiki/Iterative_deepening_depth-firs...
    - sgt101 8y ago
      Did you try using answer sets?

Thank you. I wanted to write something along the same vein (albeit much less eloquently!) but didn't get the chance.

sgt101 8y ago

You can prove termination in many cases. But there are infinite cases where you can't prove it, and it will terminate.

nickpsecurity 8y ago
I'm still learning about how much of a problem that is in practice. I have less data on analyzing infinite-state systems. What both real-time and functional developers said to do was this: 1. Design the main computation or loop to operate on a fixed chunk of data in a way that can be verified in isolation. 2. Design a component that either streams in new data or says there is none. Verify it in isolation. 3. Compose the two. The result will take X proven timing multiplied by Y amount of streamed data for as long as it runs or do nothing if stream is empty. Shouldn't this handle what you describe in the general case or does that simple strategy fall apart even on common stuff with event loops?
- carapace 8y ago
  FWIW in the limited time I've been using Prolog that pattern has worked fine for me. A factor to consider: Prolog is old. It's very unlikely to encounter some problem or issue that ahs not already been addressed, often by a team of researchers. For example, when I was exploring Prolog I tried a simple transformation on syllogisms. I found some code online that had them in this form: syll(all(M,P), all(S,M), all(S,P)). % This is barbara in the 1st figure. syll(no(M,P), all(S,M), no(S,P)). % This is celarent in the 1st figure. Etc... I transformed them using term_expansion/2 [1] with this rule: term_expansion(syll(A, B, C), (C :- B, A)). To generate rules like these: all(A, C) :- all(A, B), all(B, C). no(A, B) :- all(A, C), no(B, C). Etc... However, these rules (plus a few facts: all(dogs, canines). all(canines, mammals). ) led to huge open-ended search. ?- all(A, B). ERROR: Out of local stack It turns out I can just use call_with_depth_limit/3 [2] to bound the search depth: ?- call_with_depth_limit(all(A, B), 10, R). A = dogs, B = mammals, R = 11 ; A = dogs, B = canines, R = 11 ; A = canines, B = mammals, R = 1. It finds some solutions. Not all Prologs have call_with_depth_limit/3 built-in but it's easy to write a meta-interpreter that does the same thing.[3] From the POV of security, the trick I want to explore is writing Prolog code to generate provably-correct machine code. [1] http://www.swi-prolog.org/pldoc/doc_for?object=term_expansion/2 http://www.swi-prolog.org/pldoc/doc_for?object=term_expansio... [2] http://www.swi-prolog.org/pldoc/doc_for?object=call_with_depth_limit/3 http://www.swi-prolog.org/pldoc/doc_for?object=call_with_dep... [3] https://en.wikipedia.org/wiki/Iterative_deepening_depth-first_search https://en.wikipedia.org/wiki/Iterative_deepening_depth-firs...
  - sgt101 8y ago
    Did you try using answer sets?