4 ms·

a dependent typing engine is exactly how I was thinking of representing this - i.e "x: int => x + 1" would have a type signature of "x: int => x + 1". Further c

a dependent typing engine is exactly how I was thinking of representing this - i.e "x: int => x + 1" would have a type signature of "x: int => x + 1". Further compositions would stack. If I e.g. converted the Collatz conjecture to a function I would get the following signatures: - collatz(x: 1) => halt - collatz(x: int where x > 0 && x % 2 = 0) => collatz(x / 2) - collatz(x: int where x > 0 && x % 2 = 1) => collatz(x * 3 + 1) I figure that if I extract out recursion like this (as recursion seems to be the only thing that makes a computation potentially undecidable) and bubble the branching up to the signature as a form of pattern matching, then the signature becomes something you could potentially use to figure out if it is decidable. The issue I'm stuck on is what approach to take to build a deduction system for calculating whether continuing such a sequence from any value in the allowed input space would halt - obviously at this point in time the collatz conjecture is an open question but we can also construct functions using the same notation that we can intuitively determine will either always halt or only sometimes halt, so there is surely room for the existence of such a deductive system. I just don't want to spend a year learning about e.g. category theory or natural deductive logic just to find out that this problem cannot be effectively expressed in such a system.

chriswarbo 8y ago
A dependently typed system (or presumably anything else) which allows non-halting definitions is unsound. The classic example is an infinite loop: loop = loop What is the type of `loop`? We can infer it by starting with a completely generic type variable, e.g. `forall t. t`: loop : forall t. t loop = loop Then we can look at the type of the body to see which constraints it must satisfy, and perform unification with that and the `t` we have so far. In this case the body is `loop` which has type `forall t. t` (i.e. which is completely unconstrained). Unifying `forall t. t` with `forall t. t` gives (unsurprisingly) `forall t. t`. Hence that is the type of `loop`. Yet this claims to hold for all types `t`, which must include empty types like `Empty`, which should have no values! data Empty where -- This page intentionally left blank loop : forall t. t loop = loop myEmptyValue : Empty myEmptyValue = loop In particular, this lets us "prove" (in an invalid way) things like the Collatz conjecture. Here's a quick definition of the Collatz sequence, in Agda/Idris notation (untested): -- Peano arithmetic data Natural where Zero : Natural Succ : Natural -> Natural one = Succ Zero halve : Natural -> Natural halve Zero = Zero halve (Succ Zero) = Succ Zero -- Should never reach this; included for completeness halve (Succ (Succ n)) = Succ (halve n) threeTimes : Natural -> Natural threeTimes Zero = Zero threeTimes (Succ n) = Succ (Succ (Succ (threeTimes n))) data Boolean where True : Boolean False : Boolean not : Boolean -> Boolean not True = False not False = True ifThenElseNat : Boolean -> Natural -> Natural -> Natural ifThenElseNat True x y = x ifThenElseNat False x y = y isEven : Natural -> Boolean isEven Zero = True isEven (Succ n) = not (isEven n) collatzStep : Natural -> Natural collatzStep Zero = one -- Again, only for completeness collatzStep (Succ n) = ifThenElseNat (isEven (Succ n)) (halve (Succ n)) (Succ (threeTimes (Succ n))) -- This won't be allowed by Agda/Idris since it may or may not halt ;) collatzLoop : Natual -> Natural collatzLoop Zero = collatzLoop (collatzStep Zero) -- For completeness collatzLoop (Succ Zero) = Succ Zero -- Halt collatzLoop (Succ (Succ n)) = collatzLoop (collatzStep (Succ (Succ n))) We can then define the Collatz conjecture, using a standard encoding of equality: data Equal : Natural -> Natural -> Type where reflexivity : (n : Natural) -> Equal n n CollatzConjecture : Type CollatzConjecture = (n : Natural) -> Equal (collatzLoop n) one proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = ? disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture purportedProof = ? The disproof basicallys says "if you give me a proof of `CollatzConjecture`, I can give you a value which doesn't exist"; since that's absurd, the only way it can hold is if there are no proofs of `CollatzConjecture` to give it (this is a form of proof by contradiction: give me a supposed proof, and I'll show you why it must be wrong). The problem with allowing non-terminating recursion is that we can use `loop` to fill in either of these proofs, or even both of them! proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = loop disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture purportedProof = loop The type of `loop` is `forall t. t`, which can unify with either of these types, so the language/logic will allow us to use it in these definitions (or anywhere else, for that matter). For this reason, we have to make sure our language isn't Turing-complete, which we can do using a "totality checker" (a static analyser which checks if our definitions halt: if they definitely do, they're permitted; if they don't or we can't tell, they're forbidden). That stops us from writing things like `loop`, but unfortunately it stops us from writing `collatzLoop` as well. One way to get around this is to use "corecursion". This lets an infinite loop pass the totality checker, as long as it's definitely producing output data as it goes (e.g. like a stream which is forbidden from getting "stuck"). We can use this to make a `Delayed` type, which is just a stream of dummy data which might or might not end (a polymorphic version of this is described in more detail at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html ): data Delayed : Type where Now : Natural -> Delayed Later : Delayed -> Delayed collatzLoop : Natural -> Delayed collatzLoop Zero = Later (collatzLoop (collatzStep Zero)) -- For completeness collatzLoop (Succ Zero) = Now (Succ Zero) -- Halt collatzLoop (Succ (Succ n)) = Later (collatzLoop (collatzStep (Succ (Succ n)))) This will pass the totality checker since each step is guaranteed to produce some data (either the `Now` symbol or the `Later` symbol); even though the contents of a `Later` value may be infinite! If we run this version of `collatzLoop` on, say, 6 (ignoring the `Zero`/`Succ` notation for brevity), we get: collatzLoop 6 Later (collatzLoop 3) Later (Later (collatzLoop 10)) Later (Later (Later (collatzLoop 5))) Later (Later (Later (Later (collatzLoop 16)))) Later (Later (Later (Later (Later (collatzLoop 8))))) Later (Later (Later (Later (Later (Later (collatzLoop 4)))))) Later (Later (Later (Later (Later (Later (Later (collatzLoop 2))))))) Later (Later (Later (Later (Later (Later (Later (Later (collatzLoop 1)))))))) Later (Later (Later (Later (Later (Later (Later (Later (Now 1)))))))) We can rephrase the Collatz conjecture as saying that the return value of `collatzLoop` will always, eventually, end with `Now one`. This is an existence proof: there exists an `n : Natural` such that after `n` layers of `Later` wrappers there will be a `Now one` value. Since we're dealing with constructive logic, to prove this existence we must construct the number `n` (e.g. using some function, which I'll call `boundFinder`): unwrap : Natural -> Delayed -> Delayed wrap Zero x = x wrap (Succ n) (Now y) = Now y wrap (Succ n) (Later y) = unwrap n y data DelayEqual : Delayed -> Delayed -> Type where delayedReflexivity : (d : Delayed) -> DelayEqual d d -- The notation `(x : y *** z)` is a dependent pair, where the first element has -- type `y` and the second element has type `z` which may refer to the first -- value as `x` CollatzConjecture : Type CollatzConjecture = (boundFinder : Natural -> Natural *** (n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = ? disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture (boundFinder, purportedProof) = ? With this definition, a value of type `CollatzConjecture` will be a proof of the Collatz conjecture. Since we can't use tricks like `loop`, we're forced to actually construct a value of the required type. This value will be a pair: the first element of the pair is a function of type `Natural -> Natural`, which we call `boundFinder`. The second element of the pair is also a function, but it has type: (n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) This says that given any `n : Natural`, we can return a proof that: DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) This says that `unwrap (boundFinder n) (collatzLoop n)`, i.e. removing `boundFinder n` layers of `Later` wrappers from `collatzLoop n`, is equal to the value `Now one`. To disprove this form of the Collatz conjecture, we're given a supposed proof: i.e. we're given some `boundFinder` function and a value supposedly proving the equation described above. We need to find a contradiction to that supposed proof, which might be an `n : Natural` which reduces to `Now x` where `x` is not 1; or which we can show doesn't reduce at all. Either way this would contradict the claim made by `purportedProof`, and we could use that contradiction to prove anything ("ex falso quodlibet") including the `Empty` return value we need (just as if we had `loop`!). The thing is, even if we set up all of this machinery, there is an unfortunate fact staring us in the face: compare the definition of `Natural` to the definition of `Delayed`. They're almost identical! The only difference is that `Now` takes an argument but `Zero` doesn't. If we think about what `Succ` is doing, it's just adding a wrapper around a `Natural` to represent "one more than" (e.g. `Succ Zero` is 1, `Succ (Succ Zero)` is 2, etc.). If we think about what `Later` is doing, it's just adding a wrapper around a `Delayed` to represent "one more step". In essence we've just traded one form of counting for another! It doesn't actually get us any closer to solving the Collatz conjecture, other than giving us something to plug a proof attempt into, such that it will be verified automatically. It's like setting up a Wordpress blog: it lets us say anything we like to the world, but doesn't help us figure what we want to say ;)
- lisper 8y ago
  That is quite possibly one of the best comments ever posted to HN!
- beaconstudios 8y ago
  hey, just so you're aware I am working my way through your answer. I appreciate the depth of your comment and will be coming back to reply once I've fully understood your answer. I don't know how long it takes for HN to lock a thread for replies, but if you want to discuss this further would you mind dropping me an email (my address is in my profile)? It might take a couple more days for me to formulate a response.
- beaconstudios 8y ago
  hey Chris, I've read through your argument a few times and completely see your point - I've encountered this kind of second-system loop myself while trying to whiteboard a way to map a function to a representation that can be treated more like an algebra. Now my angle of approach is - I would be delighted for my system to not permit the collatzLoop function to be declared without constraining the range of natural numbers allowed! From the sounds of it a totality checker may be what I'm actually wanting to write, rather than a type system - to be honest, I wanted to avoid explicit type notation within this language anyway, I'd much rather treat the functions included as a mapping where the output type inherently contains the relationship it shares with the inputs. I see two approaches I could proceed with: one fairly simple but not ideal, and one that is more optimal but that I do not know how to approach. Scenario 1: What I'm imagining is a checker that, given a specific recursive function, can determine the exact input type that is required in order to terminate in 1 execution, 2 executions, and so on up until a defined limit. So for the collatz conjecture, it could determine that only the input `1` would halt on a single execution, `2` on two executions, etc but then would open up to either `32` or `5` after five executions. That seems simple enough to implement by converting branches into multiple function signatures and "solving for x" with substitution. However, I would love to be able to ensure that a function halts after an unrestricted number of recursions, and it seems as though it would be possible - because we can intuitively know that, for example, a function `f(n: Nat) => n is even ? f(n / 2) : f(n + 1)` will always halt on valid input. Scenario 2: If we can intuitively know the fact noted above then surely that intuition could be encoded into a program? It seems like more of a meta concept in that I don't believe it would be possible to show such a fact using simple algorithmic substitutions (although I would welcome being wrong on this, makes my life easier!). From reading about the history of various mathematical fields over the past couple of weeks it seems like this pattern has shown up in maths on numerous occasions and appears to be basically a fundamental trait of logic - that any closed system that is permitted to contain references to the whole system suddenly gains a whole new set of behaviours that cannot be understood from the "meta-level" of the system itself. I mean, that's what GEB seems to be partially about too. A set containing sets that does not contain itself, the proof of the halting problem including an oracle that can call itself with itself as input, that kind of thing. And there's often a new system "on top of" the self-referential system that basically takes the self-reference out and provides a new meta-level for reasoning about the lower system, but with extra added self-reference. I guess what I'm trying to get to is - this scenario #2 seems like it must match up to some theory or another that is perhaps one of these meta-theories atop something like category theory or deductive logic - not looking at the relationships between input and output directly, but the relationship between the relationships, to determine whether it eventually resolves down. Something that could tell that the above-mentioned function halts, from base principles. I've found something that seems comparable in axioms and axiom schemata, but being able to build an axiomatic system seems pretty deep down the logic rabbit-hole and I don't want to dive in head-first without knowing I'm at least looking in the right direction, y'know? Anyways, whether you respond to this comment or not, I want to thank you for your comment. You've described in a much more comprehensive way, something that I've been bumping into while researching this topic and that helps a great deal to verify to me that going down the lower meta-level route (damn you, lack of relevant terminology!) of trying to convert the logic into a different representation and solve that way is a fruitless exercise - though I still don't know if it is possible to move to a higher meta-level and make some progress from there; I guess that's why I'm asking :)

chriswarbo 8y ago

A dependently typed system (or presumably anything else) which allows non-halting definitions is unsound. The classic example is an infinite loop: loop = loop What is the type of `loop`? We can infer it by starting with a completely generic type variable, e.g. `forall t. t`: loop : forall t. t loop = loop Then we can look at the type of the body to see which constraints it must satisfy, and perform unification with that and the `t` we have so far. In this case the body is `loop` which has type `forall t. t` (i.e. which is completely unconstrained). Unifying `forall t. t` with `forall t. t` gives (unsurprisingly) `forall t. t`. Hence that is the type of `loop`. Yet this claims to hold for all types `t`, which must include empty types like `Empty`, which should have no values! data Empty where -- This page intentionally left blank loop : forall t. t loop = loop myEmptyValue : Empty myEmptyValue = loop In particular, this lets us "prove" (in an invalid way) things like the Collatz conjecture. Here's a quick definition of the Collatz sequence, in Agda/Idris notation (untested): -- Peano arithmetic data Natural where Zero : Natural Succ : Natural -> Natural one = Succ Zero halve : Natural -> Natural halve Zero = Zero halve (Succ Zero) = Succ Zero -- Should never reach this; included for completeness halve (Succ (Succ n)) = Succ (halve n) threeTimes : Natural -> Natural threeTimes Zero = Zero threeTimes (Succ n) = Succ (Succ (Succ (threeTimes n))) data Boolean where True : Boolean False : Boolean not : Boolean -> Boolean not True = False not False = True ifThenElseNat : Boolean -> Natural -> Natural -> Natural ifThenElseNat True x y = x ifThenElseNat False x y = y isEven : Natural -> Boolean isEven Zero = True isEven (Succ n) = not (isEven n) collatzStep : Natural -> Natural collatzStep Zero = one -- Again, only for completeness collatzStep (Succ n) = ifThenElseNat (isEven (Succ n)) (halve (Succ n)) (Succ (threeTimes (Succ n))) -- This won't be allowed by Agda/Idris since it may or may not halt ;) collatzLoop : Natual -> Natural collatzLoop Zero = collatzLoop (collatzStep Zero) -- For completeness collatzLoop (Succ Zero) = Succ Zero -- Halt collatzLoop (Succ (Succ n)) = collatzLoop (collatzStep (Succ (Succ n))) We can then define the Collatz conjecture, using a standard encoding of equality: data Equal : Natural -> Natural -> Type where reflexivity : (n : Natural) -> Equal n n CollatzConjecture : Type CollatzConjecture = (n : Natural) -> Equal (collatzLoop n) one proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = ? disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture purportedProof = ? The disproof basicallys says "if you give me a proof of `CollatzConjecture`, I can give you a value which doesn't exist"; since that's absurd, the only way it can hold is if there are no proofs of `CollatzConjecture` to give it (this is a form of proof by contradiction: give me a supposed proof, and I'll show you why it must be wrong). The problem with allowing non-terminating recursion is that we can use `loop` to fill in either of these proofs, or even both of them! proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = loop disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture purportedProof = loop The type of `loop` is `forall t. t`, which can unify with either of these types, so the language/logic will allow us to use it in these definitions (or anywhere else, for that matter). For this reason, we have to make sure our language isn't Turing-complete, which we can do using a "totality checker" (a static analyser which checks if our definitions halt: if they definitely do, they're permitted; if they don't or we can't tell, they're forbidden). That stops us from writing things like `loop`, but unfortunately it stops us from writing `collatzLoop` as well. One way to get around this is to use "corecursion". This lets an infinite loop pass the totality checker, as long as it's definitely producing output data as it goes (e.g. like a stream which is forbidden from getting "stuck"). We can use this to make a `Delayed` type, which is just a stream of dummy data which might or might not end (a polymorphic version of this is described in more detail at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html ): data Delayed : Type where Now : Natural -> Delayed Later : Delayed -> Delayed collatzLoop : Natural -> Delayed collatzLoop Zero = Later (collatzLoop (collatzStep Zero)) -- For completeness collatzLoop (Succ Zero) = Now (Succ Zero) -- Halt collatzLoop (Succ (Succ n)) = Later (collatzLoop (collatzStep (Succ (Succ n)))) This will pass the totality checker since each step is guaranteed to produce some data (either the `Now` symbol or the `Later` symbol); even though the contents of a `Later` value may be infinite! If we run this version of `collatzLoop` on, say, 6 (ignoring the `Zero`/`Succ` notation for brevity), we get: collatzLoop 6 Later (collatzLoop 3) Later (Later (collatzLoop 10)) Later (Later (Later (collatzLoop 5))) Later (Later (Later (Later (collatzLoop 16)))) Later (Later (Later (Later (Later (collatzLoop 8))))) Later (Later (Later (Later (Later (Later (collatzLoop 4)))))) Later (Later (Later (Later (Later (Later (Later (collatzLoop 2))))))) Later (Later (Later (Later (Later (Later (Later (Later (collatzLoop 1)))))))) Later (Later (Later (Later (Later (Later (Later (Later (Now 1)))))))) We can rephrase the Collatz conjecture as saying that the return value of `collatzLoop` will always, eventually, end with `Now one`. This is an existence proof: there exists an `n : Natural` such that after `n` layers of `Later` wrappers there will be a `Now one` value. Since we're dealing with constructive logic, to prove this existence we must construct the number `n` (e.g. using some function, which I'll call `boundFinder`): unwrap : Natural -> Delayed -> Delayed wrap Zero x = x wrap (Succ n) (Now y) = Now y wrap (Succ n) (Later y) = unwrap n y data DelayEqual : Delayed -> Delayed -> Type where delayedReflexivity : (d : Delayed) -> DelayEqual d d -- The notation `(x : y *** z)` is a dependent pair, where the first element has -- type `y` and the second element has type `z` which may refer to the first -- value as `x` CollatzConjecture : Type CollatzConjecture = (boundFinder : Natural -> Natural *** (n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) proofOfCollatzConjecture : CollatzConjecture proofOfCollatzConjecture = ? disproofOfCollatzConjecture : CollatzConjecture -> Empty disproofOfCollatzConjecture (boundFinder, purportedProof) = ? With this definition, a value of type `CollatzConjecture` will be a proof of the Collatz conjecture. Since we can't use tricks like `loop`, we're forced to actually construct a value of the required type. This value will be a pair: the first element of the pair is a function of type `Natural -> Natural`, which we call `boundFinder`. The second element of the pair is also a function, but it has type: (n : Natural) -> DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) This says that given any `n : Natural`, we can return a proof that: DelayEqual (unwrap (boundFinder n) (collatzLoop n)) (Now one)) This says that `unwrap (boundFinder n) (collatzLoop n)`, i.e. removing `boundFinder n` layers of `Later` wrappers from `collatzLoop n`, is equal to the value `Now one`. To disprove this form of the Collatz conjecture, we're given a supposed proof: i.e. we're given some `boundFinder` function and a value supposedly proving the equation described above. We need to find a contradiction to that supposed proof, which might be an `n : Natural` which reduces to `Now x` where `x` is not 1; or which we can show doesn't reduce at all. Either way this would contradict the claim made by `purportedProof`, and we could use that contradiction to prove anything ("ex falso quodlibet") including the `Empty` return value we need (just as if we had `loop`!). The thing is, even if we set up all of this machinery, there is an unfortunate fact staring us in the face: compare the definition of `Natural` to the definition of `Delayed`. They're almost identical! The only difference is that `Now` takes an argument but `Zero` doesn't. If we think about what `Succ` is doing, it's just adding a wrapper around a `Natural` to represent "one more than" (e.g. `Succ Zero` is 1, `Succ (Succ Zero)` is 2, etc.). If we think about what `Later` is doing, it's just adding a wrapper around a `Delayed` to represent "one more step". In essence we've just traded one form of counting for another! It doesn't actually get us any closer to solving the Collatz conjecture, other than giving us something to plug a proof attempt into, such that it will be verified automatically. It's like setting up a Wordpress blog: it lets us say anything we like to the world, but doesn't help us figure what we want to say ;)

lisper 8y ago
That is quite possibly one of the best comments ever posted to HN!
beaconstudios 8y ago
hey, just so you're aware I am working my way through your answer. I appreciate the depth of your comment and will be coming back to reply once I've fully understood your answer. I don't know how long it takes for HN to lock a thread for replies, but if you want to discuss this further would you mind dropping me an email (my address is in my profile)? It might take a couple more days for me to formulate a response.
beaconstudios 8y ago
hey Chris, I've read through your argument a few times and completely see your point - I've encountered this kind of second-system loop myself while trying to whiteboard a way to map a function to a representation that can be treated more like an algebra. Now my angle of approach is - I would be delighted for my system to not permit the collatzLoop function to be declared without constraining the range of natural numbers allowed! From the sounds of it a totality checker may be what I'm actually wanting to write, rather than a type system - to be honest, I wanted to avoid explicit type notation within this language anyway, I'd much rather treat the functions included as a mapping where the output type inherently contains the relationship it shares with the inputs. I see two approaches I could proceed with: one fairly simple but not ideal, and one that is more optimal but that I do not know how to approach. Scenario 1: What I'm imagining is a checker that, given a specific recursive function, can determine the exact input type that is required in order to terminate in 1 execution, 2 executions, and so on up until a defined limit. So for the collatz conjecture, it could determine that only the input `1` would halt on a single execution, `2` on two executions, etc but then would open up to either `32` or `5` after five executions. That seems simple enough to implement by converting branches into multiple function signatures and "solving for x" with substitution. However, I would love to be able to ensure that a function halts after an unrestricted number of recursions, and it seems as though it would be possible - because we can intuitively know that, for example, a function `f(n: Nat) => n is even ? f(n / 2) : f(n + 1)` will always halt on valid input. Scenario 2: If we can intuitively know the fact noted above then surely that intuition could be encoded into a program? It seems like more of a meta concept in that I don't believe it would be possible to show such a fact using simple algorithmic substitutions (although I would welcome being wrong on this, makes my life easier!). From reading about the history of various mathematical fields over the past couple of weeks it seems like this pattern has shown up in maths on numerous occasions and appears to be basically a fundamental trait of logic - that any closed system that is permitted to contain references to the whole system suddenly gains a whole new set of behaviours that cannot be understood from the "meta-level" of the system itself. I mean, that's what GEB seems to be partially about too. A set containing sets that does not contain itself, the proof of the halting problem including an oracle that can call itself with itself as input, that kind of thing. And there's often a new system "on top of" the self-referential system that basically takes the self-reference out and provides a new meta-level for reasoning about the lower system, but with extra added self-reference. I guess what I'm trying to get to is - this scenario #2 seems like it must match up to some theory or another that is perhaps one of these meta-theories atop something like category theory or deductive logic - not looking at the relationships between input and output directly, but the relationship between the relationships, to determine whether it eventually resolves down. Something that could tell that the above-mentioned function halts, from base principles. I've found something that seems comparable in axioms and axiom schemata, but being able to build an axiomatic system seems pretty deep down the logic rabbit-hole and I don't want to dive in head-first without knowing I'm at least looking in the right direction, y'know? Anyways, whether you respond to this comment or not, I want to thank you for your comment. You've described in a much more comprehensive way, something that I've been bumping into while researching this topic and that helps a great deal to verify to me that going down the lower meta-level route (damn you, lack of relevant terminology!) of trying to convert the logic into a different representation and solve that way is a fruitless exercise - though I still don't know if it is possible to move to a higher meta-level and make some progress from there; I guess that's why I'm asking :)