4 ms·

Most examples I tried didn't work very well, but when it did work it was truly neat. The performance makes sense from a quick glance into the paper. The model r

by fmap 8y ago

Most examples I tried didn't work very well, but when it did work it was truly neat. The performance makes sense from a quick glance into the paper. The model represents programs as paths in the AST, which is not sufficient to reconstruct the semantics, but is a good "fingerprint" of a program for fuzzy retrieval tasks. That's the domain which the authors wanted to target. I wonder if there is really so much low hanging fruit still lying around, or if everybody who tried injecting some more domain knowledge into tools like this had quietly failed. For example, the obvious way of building a distributed representation of, e.g., the simply-typed lambda-calculus (STLC) is by building a model. There are four local constraints that the model has to satisfy and the payoff is a representation that is invariant under program equivalence. There are some complexity theoretic reasons why this cannot really work all the time (conversion in STLC is nonelementary), but even something that works in simple cases would be more robust than a statistical fingerprint that gets confused by the names of local variables...

0xBABAD00C 8y ago
> representation that is invariant under program equivalence is this even computable at all (leaving aside the complexity theoretic issues)?
- DannyBee 8y ago
  No, it isn't. It's clearly undecidable. Herbrand equivalence is the best you can do (in general) if you are trying to say whether two variables have the same values at the same program points. If you are willing to be probablistically correct you can do better, but you will get wrong answers (and not know they are wrong) That is likely okay for this application.
- fmap 8y ago
  That was a poor choice of words. Models of lambda calculus are invariant under beta-eta conversion, which is what I meant by program equivalence, but which is not the same thing as contextual equivalence. Thus you get a representation invariant under computation. This remains decidable when you consider only normalizing programs as in STLC or related subsystems.

by fmap 8y ago

0xBABAD00C 8y ago

> representation that is invariant under program equivalence is this even computable at all (leaving aside the complexity theoretic issues)?

DannyBee 8y ago
No, it isn't. It's clearly undecidable. Herbrand equivalence is the best you can do (in general) if you are trying to say whether two variables have the same values at the same program points. If you are willing to be probablistically correct you can do better, but you will get wrong answers (and not know they are wrong) That is likely okay for this application.
fmap 8y ago
That was a poor choice of words. Models of lambda calculus are invariant under beta-eta conversion, which is what I meant by program equivalence, but which is not the same thing as contextual equivalence. Thus you get a representation invariant under computation. This remains decidable when you consider only normalizing programs as in STLC or related subsystems.