3 ms·

> The invariant for `K+D` is the identity function. So if we had a `D` with holes, we could use a prover to verify the identity invariant and “solve for D” simu

> The invariant for `K+D` is the identity function. So if we had a `D` with holes, we could use a prover to verify the identity invariant and “solve for D” simultaneously. This was pretty mind-blowing for me. (I haven't really looked into program synthesis so I may be slightly more susceptible ;) There was one part of it that seemed problematic from my (perhaps flawed) understanding, though. So I guess the idea is we have K+D = I (and this is roughly equivalent to 'D(K(s)) = I(s)' where 's' is a string to compress), so if we come up with a proof of 'I'—which would be a path through theorem space starting from I'm not sure what axioms—and we know 'I' is equivalent to 'K+D', and we already know the value of 'K,' then the value of 'D' is implied. My question is what is the equivalent here to the subtraction operation that would allow us to say D = I - K? It seems very surprising to me that K and D would be structured in such a way that their own proofs would necessarily have any relationship to the proof we derived for I, so that such a subtraction would work so cleanly...

saurabh20n 8y ago
Your `D(K(..))` notation is better than mine. Email me, and I will send you a gift card. What you do is solve `\exists D: \forall arr: D(K(arr)) = arr` where `arr` is an arbitrary length array/bitstream. See paper [1]. There is also really old code you can browse at the bottom of my personal page linked in profile (doesn't compile anymore coz of deprecated dependencies.) The arithmetic analogy break down when solving. So you're not explicitly computing `I - K`, but instead letting the constraint solver pick values that satisfy the equation (hence SMT solving.) Also, you are absolutely right that there is no reason to have their structure be related to identity: But, the "damage" done by `K` is encoded in the state at the interface to `D` and `D` better undo that state to get to identity, which is what the solver would exploit. [1] Path-based Inductive Synthesis for Program Inversion http://saurabh-srivastava.com/pubs/pldi11-pins.pdf http://saurabh-srivastava.com/pubs/pldi11-pins.pdf
- westoncb 8y ago
  > So you're not explicitly computing `I - K`, but instead letting the constraint solver pick values that satisfy the equation Ah—makes sense. I wonder if attempts at going in the other direction have been made, and initially constraining the structures of the known parts so that you could do something like a subtraction to get the unknown (probably a crazy dead-end idea I realize :). > But, the "damage" done by `K` is encoded in the state at the interface to `D` and `D` better undo that state to get to identity, which is what the solver would exploit. Interesting. So because we know it's an inversion scenario beforehand we can modify the solver to not be so general, and only bother considering solutions which modify the state in an inverse manner to our original program... Cool. I'll be keeping this at the back of my mind to see if any ideas come up. Thanks and good luck!
  - saurabh20n 8y ago
    Look up Nate's work [1], specifically Boomerang [2] that aims for bidirectional programming. Be crazy :) [1] Nate Foster: http://www.cs.cornell.edu/~jnfoster/ http://www.cs.cornell.edu/~jnfoster/ [2] Boomerang http://www.seas.upenn.edu/~harmony/ http://www.seas.upenn.edu/~harmony/

saurabh20n 8y ago

Your `D(K(..))` notation is better than mine. Email me, and I will send you a gift card. What you do is solve `\exists D: \forall arr: D(K(arr)) = arr` where `arr` is an arbitrary length array/bitstream. See paper [1]. There is also really old code you can browse at the bottom of my personal page linked in profile (doesn't compile anymore coz of deprecated dependencies.) The arithmetic analogy break down when solving. So you're not explicitly computing `I - K`, but instead letting the constraint solver pick values that satisfy the equation (hence SMT solving.) Also, you are absolutely right that there is no reason to have their structure be related to identity: But, the "damage" done by `K` is encoded in the state at the interface to `D` and `D` better undo that state to get to identity, which is what the solver would exploit. [1] Path-based Inductive Synthesis for Program Inversion http://saurabh-srivastava.com/pubs/pldi11-pins.pdf http://saurabh-srivastava.com/pubs/pldi11-pins.pdf

westoncb 8y ago
> So you're not explicitly computing `I - K`, but instead letting the constraint solver pick values that satisfy the equation Ah—makes sense. I wonder if attempts at going in the other direction have been made, and initially constraining the structures of the known parts so that you could do something like a subtraction to get the unknown (probably a crazy dead-end idea I realize :). > But, the "damage" done by `K` is encoded in the state at the interface to `D` and `D` better undo that state to get to identity, which is what the solver would exploit. Interesting. So because we know it's an inversion scenario beforehand we can modify the solver to not be so general, and only bother considering solutions which modify the state in an inverse manner to our original program... Cool. I'll be keeping this at the back of my mind to see if any ideas come up. Thanks and good luck!
- saurabh20n 8y ago
  Look up Nate's work [1], specifically Boomerang [2] that aims for bidirectional programming. Be crazy :) [1] Nate Foster: http://www.cs.cornell.edu/~jnfoster/ http://www.cs.cornell.edu/~jnfoster/ [2] Boomerang http://www.seas.upenn.edu/~harmony/ http://www.seas.upenn.edu/~harmony/