5 ms·

Interesting. Thank you for sharing that. Gave it a shot on SWI Prolog and got the same error. It seems like a problem that ought to be solvable with static ana

Interesting. Thank you for sharing that. Gave it a shot on SWI Prolog and got the same error. It seems like a problem that ought to be solvable with static analysis or a fuzzer -- solvable in the sense that the error is detected before the question is asked. I imagine if Prolog had wider adoption, somebody would have taken a crack at it.

yorwba 8y ago
The problem is nontermination. Static analysis of arbitrary programs to detect nontermination is the famous Halting Problem and known to be impossible. At its core, Prolog combines term unification with a depth-first search strategy. Implement those two primitives and you get a Prolog. But there are problems where depth-first search is not the best approach (e.g. when the search space is potentially infinite), and being able to code a different strategy is important. Modern languages support limited unification in the form of destructuring assignment. If they could make it bidirectional without also completely confusing everyone used to more traditional programming languages, Prolog wouldn't have many advantages left.
- nickpsecurity 8y ago
  "The problem is nontermination. Static analysis of arbitrary programs to detect nontermination is the famous Halting Problem and known to be impossible." People reading that might think you can never prove termination of programs automatically. Sounds overstated given the results happening in CompSci. There are a few tools that can automatically prove termination of a given program. AProVe was an older example that used rewriting like a lot of them: https://www.researchgate.net/publication/2877806_Automated_Termination_Proofs_with_AProVE https://www.researchgate.net/publication/2877806_Automated_T... Terminator is one for C programs: https://www.microsoft.com/en-us/research/video/automatically-proving-the-termination-of-c-programs/ https://www.microsoft.com/en-us/research/video/automatically... There's also a site where many tool builders competed in lots of categories: http://termination-portal.org/wiki/Termination_Competition http://termination-portal.org/wiki/Termination_Competition Lots of research happens under the "temporal logic" banner where they run it through model checkers, provers, and so on. Anyway, it seems proving termination of useful programs, protocols, or just critical portions is possible in general and doable with current tools for some subset.
  - ahmedalsudani 8y ago
    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...

yorwba 8y ago

The problem is nontermination. Static analysis of arbitrary programs to detect nontermination is the famous Halting Problem and known to be impossible. At its core, Prolog combines term unification with a depth-first search strategy. Implement those two primitives and you get a Prolog. But there are problems where depth-first search is not the best approach (e.g. when the search space is potentially infinite), and being able to code a different strategy is important. Modern languages support limited unification in the form of destructuring assignment. If they could make it bidirectional without also completely confusing everyone used to more traditional programming languages, Prolog wouldn't have many advantages left.

nickpsecurity 8y ago
"The problem is nontermination. Static analysis of arbitrary programs to detect nontermination is the famous Halting Problem and known to be impossible." People reading that might think you can never prove termination of programs automatically. Sounds overstated given the results happening in CompSci. There are a few tools that can automatically prove termination of a given program. AProVe was an older example that used rewriting like a lot of them: https://www.researchgate.net/publication/2877806_Automated_Termination_Proofs_with_AProVE https://www.researchgate.net/publication/2877806_Automated_T... Terminator is one for C programs: https://www.microsoft.com/en-us/research/video/automatically-proving-the-termination-of-c-programs/ https://www.microsoft.com/en-us/research/video/automatically... There's also a site where many tool builders competed in lots of categories: http://termination-portal.org/wiki/Termination_Competition http://termination-portal.org/wiki/Termination_Competition Lots of research happens under the "temporal logic" banner where they run it through model checkers, provers, and so on. Anyway, it seems proving termination of useful programs, protocols, or just critical portions is possible in general and doable with current tools for some subset.
- ahmedalsudani 8y ago
  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...