HNHacker News
TopNewBestAskShowJobs

LaPrometheus

25 karma · joined September 19, 2014

[ my public key: https://keybase.io/xerophyte; my proof: https://keybase.io/xerophyte/sigs/blSwerdSLbxDSRNiR9KleKxzoUerD0i-FIqZMKk8Azg ]
submissionscomments
LaPrometheus··on Impala: Scalable Distributed Deep Reinforcement Learning
This is typical Google/DeepMind ignorance. The rest of the world is non-exist.
LaPrometheus··on Behind the fall and rise of China's Xiaomi
I don't see any of the commenters here understand why Xiaomi rise again, and ironically the author of this article.

Xiaomi is like Amazon in China's smart home market, except with a much stronger mobile department that Amazon would dream to get.

LaPrometheus··on Optimize Deep Learning GPU Operators with TVM: A Depthwise Convolution Example
This is super cool. Any comparison with Weld? https://weld-project.github.io/
LaPrometheus··on Introducing Cosette – a SQL solver for checking semantic equivalences of queries
Please try again now :)
LaPrometheus··on Introducing Cosette – a SQL solver for checking semantic equivalences of queries
CURRENT_TIMESTAMP is truly random. One thing we can do is to over approximate. For example, let CURRENT_TIMESTAMP be a symbolic variable, which essentially can be any value. If we still can prove the equivalence, then the equivalence is sound. But there might be some false negative.

ROWNUM is interesting. You can actually declare ROWNUM as an extra attribute of the table and then assert it is a key (We will add support of key constraints very soon). Then many cases will be covered.

LaPrometheus··on Introducing Cosette – a SQL solver for checking semantic equivalences of queries
Exactly, SQL minimization is a real problem. While there is no canonical form of all SQL in general, it is still possible to reduce Query.

There is some existing work. You might want to look at this one: https://pdfs.semanticscholar.org/c243/25d76c3ba91388e16085c1...

One problem is that bag semantic chase is very complicated to implement. We are actually working on a new chase algorithm on our SQL formalization right now.

LaPrometheus··on Introducing Cosette – a SQL solver for checking semantic equivalences of queries
Thanks for trying out. The parser error report is not great now. The real error actually, it should be "union all" rather than "union".

I changed your query:

/* define schema s1, here s1 can contain any number of attributes, but it has to at least contain integer attributes x and y */ schema s1(x:int, ya:int, ??);

    schema s2(yb:int, ??);        -- define schema s2
    
    table a(s1);            -- define table a using schema s1
    table b(s2);            -- define table b using schema s1
    
    query q1                -- define query q1 on tables a and b
    `select distinct x.x as ax 
    from a x, b y
     where x.ya = y.yb`;
    
    query q2                -- define query q2 likewise
    `(select x.x as ax 
     from a x, a y, b z 
     where x.x = y.x and x.ya = z.yb)
     union all (select 1 as ax from a x where 1 = 0)`;
    
    verify q1 q2;           -- does q1 equal to q2?
The Rosette execution indeed returns a counterexample (since they are not equal). There is an error in Coq code generation part, we are fixing that now.
LaPrometheus··on Introducing Cosette – a SQL solver for checking semantic equivalences of queries
Author here. Happy to answer questions.
LaPrometheus··on CS294: Program Synthesis for Everyone
A list of applications built on top of Rosette:

http://emina.github.io/rosette/apps.html

LaPrometheus··on CS294: Program Synthesis for Everyone
An advanced version of this course, by one of the teachers of CS294.

https://courses.cs.washington.edu/courses/cse507/16sp/

LaPrometheus··on Why Ruby is an acceptable Lisp (2005)
No, It is not acceptable.
LaPrometheus··on HaxeDevelop: A Haxe IDE on Windows
How to play your game?
LaPrometheus··on I Was the Most Wanted Man in China
I am a Chinese. Obviously I don't think Dr Fang is an enemy.
LaPrometheus··on Structure and Interpretation of Computer Programs: Interactive Version
That's awesome! Make the learning more joyful.