For most of history, Japan has been existed as a small island next to the mighty kingdom of China. Even its name, "Land of the Rising Sun," refers to its relation as a nation east of Chinaa.
Then along came the industrial revolution. Soon Japan was out conquering China, despite China having a much larger army.
AI will be much faster, and much, much more powerful than the Industrial Revolution.
If Switzerland is the first to human-level AI, it will not become the world leader in oil production, or shipping, or agriculture. But everything else will be Swiss.
And then when the AI becomes superhuman, everything else will be gone.
GPT-4 speaks every human language, knows every programming language, and can answer introductory and sometimes even advanced questions in history, law, biology, and mathematics. In what way is it not more knowledgable than us?
Yes, everything there is already known by someone. But look at medicine. Specialists who are able to recognize conditions and recommend treatments better than others make fortunes, sometimes just for briefly looking at patients and answering other doctors' questions. Look at cybersecurity. A lot of exploits come from knowing something the victim didn't about a lot of different pieces of software or processes, chained together. Being able to think through the whole of human knowledge, or even the whole of a single field like biology, is something no human can do.
Also, GPT-4 is an existing system, one inconceivable a couple of years ago.
An important concept behind this is Omohundro's Basic Drives. Any maximizing agent with a goal will try to acquire more resources, resist being shut off, resist having its goal changed, create copies of itself, and improve its algorithm. If it is possible to maximize its goal in a way that will not guarantee humanity's flourishing, then we all die, guaranteed.
Aren't humans/biological life a counterexample? Simple bacteria are clearly maximizing agents, and cyanobacteria did infact almost destroy all life on earth by filling the entire planet with toxic oxygen.
We've known how to improve ourselves via selective breeding yet vanishingly few humans are proponents. We and other intelligent animals have a wide variety of goals, and even share food across species.
The evidence just doesn't seem to support this concept of Basic Drives. If anything, the evidence (and common sense) seems to suggest that the more intelligent the organism, the more easily and more often it ignores its basic drives.
I have not published any papers on parsing, but I've read a large chunk of the Handbook on Parsing, am buddies with Terrence Parr and have given a lecture on the ALL() parsing algorithm, and worked for a company that has perhaps the most extensive collection of GLR parsers around. (Whereas langcc boasts automatically-generated parsers for the easy-to-parse Python and Go, my old employer has automatically-generated parsers for Ruby, C++, COBOL, and about 100 others.) I would not consider myself an expert on parsing in comparison to the few who research it, but I would consider myself expert by the standards of most professional compiler engineers, and certainly by the standards of the average software engineer.
When I see a library like this, I ask "What new things does this thing bring to the table?" For that, before I even get into trying to understand what it does, I want to see how well the author understands what's already been done and how it compares to prior work.
My very blunt assessment: I don't see any reason to take this library seriously.
I looked at the 40 page paper. I can tell just from the citations that it takes a very 70's few of parsing. And when it does discuss other work, it mostly gets it wrong. A few examples:
Page 8: He writes about the "ETL family, also called GLR parsing." "ETL family" seems to be a term of his own coinage, and he's writing about GLR parsing and Earley parsing as if they're the same. Now that I think about it, I see some resemblance, but they're usually considered quite different. See e.g.: https://cstheory.stackexchange.com/questions/30903/why-tomit...
* Page 9
> There has also been significant development of the top-down family of parser generators, including tools such as ANTLR [PQ95] which support a superset of LL(k) grammars, as well as their
parallel counterparts, referred to as Generalized LL (GLL). For the reasons described above, we
believe that while top-down parsers are theoretically interesting, the grammars they support are
not sufficiently general to capture full programming languages.6 Notably, they are significantly
more restrictive than LR(k), and we argue that even the latter is not sufficiently general in its
standard formulation.
This has not been true since ANTLR 2, released 25 years ago. The LL() algorithm of ANTLR 3, described in a 2011 publication, is capable of parsing even some context-sensitive grammars.
Page 9:
> The tree automata of Adams and Might [AM17] are similar to our
implementation of monotonic attributes; they differ in that they impose left-to-right sequencing on the attribute constraints (whereas attributes can refer to arbitrary constituents of a grammar rule), and require productions to be duplicated (whereas attributes are boolean or integer values
layered independently on top of the standard context-free grammar rules)."
This is one of my favorite papers of the last 5 years, and this is totally inaccurate. The user writes down a normal grammar and syntactic regular expressions for forbidden subterms. From that, it automatically generates a new grammar that e.g.: breaks symmetries.
In short, I think the author has the knowledge to claim that his solution beats the best that the 70's and 80's has to offer. I am not motivated to look at this any further because I've been given no reason to believe it's had a fair comparison to what the 2010's has to offer. I continue to recommend ANTLR 4 for your parser-generator needs. Its ALL(*) algorithm truly is magic. tree-sitter is also good and has a lot of momentum.
Joe Zimmerman: If you're reading this, please don't take it too personally. I'm reacting to the claims of the work more than the work itself. If you'd like, I'll gladly discuss this with you. Either I'll learn something new, you'll get better at clarifying your ideas, or both.
I ran into a couple issues using ANTLR 4. The first is that it mostly required my build pipeline to have a JVM, which wasn't super convenient. The second is that the generated Python parsers are super slow, like too slow for even just iterating while developing.
I almost wish ANTLR 5 wouldn't be about any new parsing stuff, but just a refocusing of the project on implementing its compiler-generator in the popular languages. It basically is that already, but it's pretty clearly not first class.
Someone has done something awesome and good, why not start from that perspective of supporting and recognising someone else's talent.
From my understanding of your undertone of your message you are telling them they don't know what they're talking about when I don't think that's true.
Satirical answer: Because I'm a crusty old scientist who needs to defend his turf.
Self-serving answer: I'm doing the author a favor as perhaps the first person with my level of knowledge of the field putting effort into giving feedback on the work.
Serious answer: Because it's presenting itself as an artifact of scientific novelty rather than as an engineering accomplishment. It is making major claims not only about itself but also about the entire state-of-the-art. (You could say that the langcc papers put down the entire field of parsing.) Its contributions and scholarship therefore need to be evaluated like any other scientific work.
> Whereas langcc boasts automatically-generated parsers for the easy-to-parse Python and Go, my old employer has automatically-generated parsers for Ruby, C++, COBOL, and about 100 others.
Python may be (comparatively) easy to parse, but Golang is not - it is _barely_ LR(1) with the extensions described in https://arxiv.org/pdf/2209.08383.pdf (notably, semantic attributes and the CPS transformation).
> my old employer has automatically-generated parsers for Ruby, C++, COBOL, and about 100 others
GLR parsing, as I note in the paper, is very different from pure LR(k) parsing. Are the automatically-generated parsers you mention guaranteed to run in linear time? Are they more efficient than hand-written recursive-descent for the same languages?
Not to mention that full C++ parsing, as I also note in the paper, is undecidable, due to simple ambiguities such as "x * y;" (whose parse depends on whether x names a value or a type, which may depend on template computations). So it should be impossible to fully automatically generate a parser for C++ from a declarative BNF spec, without some significant ad-hoc machinery on top.
> he's writing about GLR parsing and Earley parsing as if they're the same. Now that I think about it, I see some resemblance, but they're usually considered quite different.
I'm not calling them "the same"; I'm grouping them together into the same family, as they share some particular characteristics relevant to the paper (polynomial but not necessarily linear time, left-to-right, dynamic-programming-style).
> This has not been true since ANTLR 2, released 25 years ago. The LL() algorithm of ANTLR 3, described in a 2011 publication, is capable of parsing even some context-sensitive grammars.
Again, the implicit claim here is "generated from a declarative BNF spec, efficiently, with guaranteed linear time, parsing full industrial languages...". Of course one can parse many languages with backtracking. Do you have examples of full industrial languages parsed with ANTLR 3 that satisfy the relevant criteria?
> This is one of my favorite papers of the last 5 years, and this is totally inaccurate.
Could you say what, specifically, is inaccurate about it?
> In short, I think the author has the knowledge to claim that his solution beats the best that the 70's and 80's has to offer. I am not motivated to look at this any further because I've been given no reason to believe it's had a fair comparison to what the 2010's has to offer.
Again, I would ask you to exhibit concrete results here. Show me an existing tool that is already capable of generating a parser for Golang 1.17.8, from a declarative BNF spec, with guaranteed linear-time parsing, and that matches or exceeds the hand-written parser in speed.
Hello Joe! Always good to see an author responding to criticism.
> Again, the implicit claim here is "generated from a declarative BNF spec, efficiently, with guaranteed linear time, parsing full industrial languages...". Of course one can parse many languages with backtracking. Do you have examples of full industrial languages parsed with ANTLR 3 that satisfy the relevant criteria?
I would suggest you lead with this and make the implicit claim explicit. The main interesting part of the claim is guaranteed linear time, something which is interesting and (to my knowledge) novel (although not what's important to me personally in parsing). I did not gather from my level of inspection that guaranteed linear-time was a claim of this work. What I gathered instead is the claim that it can improve on 70's LALR parser generators and that it attacks a consensus that handwritten parsers are necessary for industrial languages.
Both of these claims that I actually gathered decreased my motivation to read more about this work. In particular, I'd say the "consensus" that hand-written parsers are necessary is old hat, and, in the circles of people who are actually interested in better ways of constructing tools, the consensus is more the opposite. I can't say I've done an explicit poll of the software language engineering community, but everyone in the community who's brought this up has said something along the lines of "the days of handwritten parsers are over." The last time I heard this opinion was last week at ICFP (I believe said by Michael Adams, in fact).
I've now learned a (to me) new claim, that a key part is the guaranteed linear-time parse. This is great on its own even as a pure theory result. But I'll need to read a lot of highly-technical development to evaluate this claim, and the other claims discourage me from investing the effort.
Speaking of which, I highly encourage you to submit your work to SLE ( https://2022.splashcon.org/home/sle-2022 ), or, if you're feeling more ambitious, OOPSLA. These are the main venues I know of where parsing results are still published. (SLE in some years has had an entire parsing-focused sub-conference.) If the claims you're making are true, then this is work that needs to get the stamp-of-approval of peer review from people more expert than I, and for everyone to know about. There's an early-submission process for OOPSLA to get feedback far in advance of the conference; the deadline is in just over a month.
> I'm not calling them "the same"; I'm grouping them together into the same family, as they share some particular characteristics relevant to the paper (polynomial but not necessarily linear time, left-to-right, dynamic-programming-style).
Cool! I agree. This will be a great way to revise your description in the next draft of the paper if you're inclined to make one.
> Could you say what, specifically, is inaccurate about it?
I believe I did in my last comment. The main thing being the duplication of productions. The only interpretation of this that makes sense to me as a claim about the paper (as opposed to a claim about CFGs in general) is that it somehow requires the user to write a production or variants thereof twice, which is false. "Left-to-right sequencing on the attribute constraints" is also nonsense to me. I think it's requiring me to reinterpret the results of that paper in terms of the algorithm of XLR, which I don't like as a way to evaluate a competing work. Read on its own, I again can't think of anything in the Adams paper which involves "left-to-right sequencing" of anything.
> Again, I would ask you to exhibit concrete results here. Show me an existing tool that is already capable of generating a parser for Golang 1.17.8, from a declarative BNF spec, with guaranteed linear-time parsing, and that matches or exceeds the hand-written parser in speed.
I have to congratulate you for having this benchmark that I cannot name a work that matches it.
This raises the question of why this should be a benchmark of concern. Declarative BNF spec, sure. Guaranteed linear-time, you don't even need a benchmark to claim significance if the proof is accurate. But why Golang, and why comparison to the handwritten parser? E.g.: I'm not aware of Semantic Designs (the company with GLR parsers for Ruby, COBOL, and C++) even having a Golang parser, as they mostly deal with legacy systems. I am not prepared right now to say how significant the perf comparison is. I don't know how the result was achieved (like whether it's been achieved by well-understood perf engineering techniques that could be replicated in competitors), nor how strong the baseline is. I've done paid work in 30+ languages and studied many more, but Golang is not one of them.
I can say that I misremembered the ALL(*) paper showing spectacular performance results compared to all other parser generators. In fact, they only gave the comparison for the Java parser. So I was probably overconfident in its performance
Anyway, if you want to discuss this more, or you want an intro to a real parsing expert, I'm happy to; my contact information is in my profile. Now you have at least one datapoint about how someone versed in modern parsing is reacting to this work.
> everyone in the community who's brought this up has said something along the lines of "the days of handwritten parsers are over."
I am aware of this "consensus", but I believe it is largely wishful thinking. Prior to langcc, the community had yet to propose an alternative that is general and efficient enough (esp., linear-time) to replace hand-written recursive-descent parsers for industrial languages such as Golang. lex and yacc are not sufficient for this. It is only with the advances of the langcc paper (improved optimization procedures, CPS transformation, semantic attributes, etc.) that this has become possible.
> I believe I did in my last comment. The main thing being the duplication of productions. The only interpretation of this that makes sense to me as a claim about the paper (as opposed to a claim about CFGs in general) is that it somehow requires the user to write a production or variants thereof twice, which is false.
My comments were referring to the compilation of tree automata to CFGs, which seems to be necessary in order to use them with standard LR parsing techniques. The alternative seems to be to use the automata to filter sets of possible parses after-the-fact, which does not by itself lead to an efficient parsing algorithm.
> But why Golang, and why comparison to the handwritten parser?
Golang is a representative example of the formidable complexity, and near-ambiguity, of constructs that are commonly used in industrial languages - and which people often take as a justification that handwritten parsers are necessary. In order to be competitive with hand-written parsers (and thus support the "consensus" that hand-written parsers are no longer necessary), a generated parser should at least be guaranteed linear-time, and should be comparable in terms of concrete efficiency benchmarks.
Okay, we seem to be whittling down on the points where we disagree.
Initial disagreement:
* langcc/XLR is a major breakthrough in the ability to generate parsers for industrial languages
---- Positions:
----------- Joe: Yes
----------- Me: Unclear. Several other works in the past 20 years have similar claims. Benchmark selected by langcc is of unclear significance. langcc paper is lacking indicia of reliability to investigate its linear time claim.
Current crux:
* Linear time guarantee is a bright-line barrier between parser generators suited for tool or compiler development on industrial languages and parser generators not so suited.
------ Positions:
---------- Joe: Yes
---------- Me: No
Is this a fair summary of the discussion so far?
I can say that this is a crux for me because, if you convince me that the linear-time guarantee is this important and that langcc has it, I will be much more likely to crow about / evangelize langcc in the future.
> My comments were referring to the compilation of tree automata to CFGs, which seems to be necessary in order to use them with standard LR parsing techniques. The alternative seems to be to use the automata to filter sets of possible parses after-the-fact, which does not by itself lead to an efficient parsing algorithm.
Cool! So, the distinguishment is more about its use of CFGs as a compilation target than about the main meat of the work. I find this a much clearer description of how you intend to compare Michael Adams's paper than the one I quoted.
* "In order to be competitive with hand-written parser [...] a generated parser should at least be guaranteed linear-time, and should be comparable in terms of concrete efficiency benchmarks. "
* "the community had yet to propose an alternative that is general and efficient enough (esp., linear-time) to replace hand-written recursive-descent parsers for industrial languages such as Golang"
This is an interesting set of claims because all the arguments I've heard in the past in favor of handwritten parsers were about error messages, not perf. I know langcc has an idea for that as well, but you seem to be focusing on performance as the real breakthrough.
So, question:
Would you accept a generated parser for Ruby, C++, Haskell, Delphi, or Verilog that is empirically within 3x the parsing speed of the handwritten alternative as sufficient evidence that some existing work is already competitive on this front?
> I can say that this is a crux for me because, if you convince me that the linear-time guarantee is this important and that langcc has it
The fact that langcc has the linear-time guarantee follows from the fact that it generates shift/reduce parsers that take steps according to an LR DFA. If you are not already convinced that this property is important, I am not sure that I can convince you, except to ask whether you would be comfortable running, e.g., a worst-case-O(n^3) parser for a real industrial language in production. (Or, for that matter, running a parser such as GLR which may fail with an ambiguity at parse time. langcc parsers, of course, will report potential ambiguity as an LR conflict at _parser generation time_; once langcc produces the LR DFA, its behavior at parse time is unambiguous.)
There are also many other important theoretical innovations in the langcc paper, e.g., the LR NFA optimization procedures, the conflict tracing algorithm, and XLR.
> This is an interesting set of claims because all the arguments I've heard in the past in favor of handwritten parsers were about error messages, not perf. I know langcc has an idea for that as well, but you seem to be focusing on performance as the real breakthrough.
Yes, langcc also features a novel LR conflict tracing algorithm, which makes conflicts very easy to debug at parser generation time. I am not sure if I would call performance the "breakthrough"; more so that linear-time performance is a _prerequisite_, and the theoretical breakthroughs of the langcc paper are what allow us to satisfy that prerequisite.
> Would you accept a generated parser for Ruby, C++, Haskell, Delphi, or Verilog that is empirically within 3x the parsing speed of the handwritten alternative as sufficient evidence that some existing work is already competitive on this front?
I have not studied Ruby, Delphi, or Verilog extensively, so could not comment on those languages at the moment. I know that Golang 1.17.8 is sufficiently difficult to parse as to be a good benchmark. I am not sure whether Haskell is sufficiently difficult to parse, but would at least be _interested_ in results for it. C++ parsing is undecidable, so that would seem to rule it out as a candidate for a fully automatically generated parser.
> If you are not already convinced that this property is important, I am not sure that I can convince you, except to ask whether you would be comfortable running, e.g., a worst-case-O(n^3) parser for a real industrial language in production. (Or, for that matter, running a parser such as GLR which may fail with an ambiguity at parse time.
Looks like it stops here. Yes, I am comfortable running such algorithms in production. Github code-nav uses GLR parsing (via tree-sitter) on a large fraction of the code in existence.
I saw a private demo of Mutable.ai last month. It was extremely impressive, and even more impressive was the pace of development. This is a clear must for anyone doing Jupyter.
In what ways program synthesis different than code generation taught in compiler and/or PLT courses? Is the goal here get ad high level ss possible, or be able to create as much code as possible?
One word: search. Most of the traditional compilation pipeline can be expressed using deterministic rewrite rules. Synthesizers of all families generate and consider a large number of possibilities.
Flipping it around, there's an old joke that "a synthesizer is just a compiler that sometimes doesn't work."
But the first thing to learn is that, the deeper you go, the blurrier the lines get. There certainly exists a compiler out there that does more search than a good chunk of things done under the name of synthesis. (Especially because "synthesis" has become a bit of a buzzword in PL circles, and often gets slapped where it doesn't really belong.) I've discussed this briefly before in my blog: http://www.pathsensitive.com/2021/03/why-programmers-shouldn...
Not so much a question as a complaint: I can't find anything about Inductive Logic Programming in the course material. ILP is the field that studies the inductive synthesis of logic programs, it should fit right in with the rest of the material, particulary in the parts about constraint based synthesis and verification.
If ILP is discussed and I missed it, apologies- I've only read through very quickly to get a general idea of the curriculum and bookmarked the top level for reference.
I'm barely familiar with Inductive Logic Programming and never hear anyone talk about it. I came in prepared to dismiss the field's relevance to synthesis, but decided to do a bunch of reading first so that I could do so from an informed perspective. I knew ILP to be "constructing a classifier from a conjunction of literals," which is very much not synthesis. It turns out there's a lot more done under the name of ILP.
I think the real answer is largely that logic programming as a whole fell out of favor in the US sometime in the 90's, whereas the program synthesis renaissance started in the 2000's -- and is still US-dominated. Not to say there still aren't tons of people doing logic programming, but, personal anecdote: I encountered a ton of logic programming papers during the lit review for one of my other project, which has some overlap in the symbolic techniques used, and....they're all from the period 1988-1995.
Mukund's work is the most relevant from a synthesis perspective that I know of, as one of the only people doing synthesis of a logic language (unless you count SQL). (Note: This is distinct from people like William Byrd doing synthesis using a logic programming language.) Have a look at the bottom of page 23 of "Provenance-Guided Synthesis of Datalog Programs" https://dl.acm.org/doi/pdf/10.1145/3371130 . It does a good job explaining the distinction between the goals of ILP things done under the umbrella of synthesis. But note that this work is still considered niche in the synthesis world.
There's also the question about what techniques belong to what field; I expect that, were I to dig into thy synthesis-relevant parts of ILP further, I'd find a lot of techniques that are familiar and that I learned with no connection to ILP. Paul Graham has said that philosophy is not useful because everything useful it discovers was spun out into a different field. ( http://www.paulgraham.com/philosophy.html ) The philosophy of computer science in that perspective is AI. 40 years ago, garbage collection, term rewriting, logic programming, and programming assistants were all AI. Even just 20 years ago, Tessa Lau's work on inductive synthesis was AI. Today, all of those are things likely to be rejected from a top AI conference, but welcome at a PL conference. Thus, you might find in the synthesis world techniques that would be familiar to an old-school ILP researcher, but without shared context.
(Two recent exceptions are neural synthesis and probabilistic programming, where you do see a lot of crossover between PL and ML. This is very recent. [Insert harsh judgments here about the attempts from 2016 and earlier to learn programs.])
Thank you for your thoughtful and kowledgeable comment and many apologies for my
belated reply. I was crossing an ocean on an unseaworthy vessel ("with slight
abuse of terminology").
My intuition is the same as yours: US institutions don't really take notice of
what's going on in Europe. It's a little strange in this day and age were we
don't have to wait for correspondence to be delivered by wind clipper, say, but
oh well, it's the way it is.
ILP is a small field with hubs in Europe and in Japan, and those also tend to be
the hubs for logic programming (for obvious reasons). The overlap with a
slightly arcane programming paradigm that, like you say, is more well-known in
Programming Language circles is not really helping ILP's popularity, I guess.
>> I came in prepared to dismiss the field's relevance to synthesis, but decided
to do a bunch of reading first so that I could do so from an informed
perspective
Well, respect!
Regarding Mukund Raghothaman's work that you linked. First of all, thanks for
making me aware of yet another interesting approach to learning datalog programs
that I had missed because I myself don't keep as watchful an eye on the wider
program synthesis literature as I wish others kept on ILP. Guilty! Second, I so
disagree with the characterisation of the work in Muggleton et al. 2015 :) I
guess that's typical, Stephen (Muggleton) is my thesis advisor and my work is a
few steps down the path from the 2015 work so obviously I have a different
perspective. Still, by January 2020 there were more recent results to cite and
more advanced systems to compare against. Exciting things are happening in ILP
right now, long-term thorny problems (predicate invention, learning recursion,
learning in languages other than Prolog, efficiency) are falling one by one and
it's a bit of a shame that it's all being missed by everyone outside our tiny
little field.
Regarding what techniques belong to what field, I think you're probably right,
ILP is traditionally based on search, specifically searching the space of logic
programs that are sets of clauses constructible from examples and background
knowledge (both also logic programs) and some kind of typically extra-logical
language bias. The big problem has always been the size of the resulting
hypothesis spaces. Of course I would think so because my work has been mainly
about this big problem. Anyway as far as I know, wider program synthesis
approaches also work essentially the same way, by searching a program space, and
so have the same problems wih searching large spaces so definitely there will be
much overlap. The difference is in the perspective: like you say, ILP sometimes
has a bit of a strongly theoretical flavour because many of the experts in the
field have a deep background in logic programming and expect the same from
published papers. Btw, while there's few of us, the main venues for ILP work
still include IJCAI and AAAI and special issues of the MLJ, and you can even
find work in the machine learning conferences (although usually it's the
Statistical Relational Learning branch that publishes there).
>> I knew ILP to be "constructing a classifier from a conjunction of literals,"
which is very much not synthesis.
Yes, I know this interpretation of ILP. The idea is that examples in ILP are
typically labelled positive/negative so you can see a correct program that
accepts positives and rejects negatives as a discriminator. Another way to see
it is that examples are logical atoms assigned true/false values by a logical
interpretation (literally an assignment of truth values to atoms) so again
correctly recognising true from false can be seen as a classification.
This notion of "classification" has come from inside the field, I think as part
of an effort to make ILP more approachable to the mainstream of machine
learning. I know the people it came from and the goal was of course noble, but I
think the result is that it sells short what is a much more interesting
discipline. I mean, sure, the task of recognising _and generating_
sorted/unsorted lists can be shoehorned into a classification problem but that's
missing the point that the task is to learn a program that has some kind of
expected behaviour. Which is the essence of program synthesis of course.
For me the magical thing about ILP considered as program synthesis from
incomplete specifications is that the specifications are logic programs, so
learning a program that explains the examples with respect to the background
knowledg is essentially completing a specification. And while the
specicification is a program, a program-learning approach can learn its own
specifications: what is called "predicate invention" in the literature.
But it might be worth to connect with the other side of the pond and all that. Like we just did :)
Edit: btw, I thought I had met Armando so I just checked and we were both at the Dagstuhl conference on Inductive Programming (yet another byword for program synthesis) in 2018. I don't think we talked much but we were introduced and he gave a short talk. Small world!
It's possible, but if you have a lot of knowledge, I think he'd welcome the connection. It's also incredibly flattering if you can ask intelligent questions or give intelligent appreciation about their papers. How else do you know your stiff is being read?
> Edit: btw, I thought I had met Armando so I just checked and we were both at the Dagstuhl conference on Inductive Programming (yet another byword for program synthesis) in 2018. I don't think we talked much but we were introduced and he gave a short talk. Small world!
> Would knowledge in automated theorem proving (e.g. knowing how coq works) be somehow transferable to research in this field?
Possibly.
First, Coq is not an automated theorem proving tool; it's an interactive theorem prover.
If by automated theorem proving, you're thinking of a tool like Z3 or CVC4 which find models of statements in a decidable theory (which are pretty much always mathematically uninteresting), then...absolutely! SAT/SMT are at the core of constraint-based synthesis. Heck, CVC4 has a SyGuS mode that won the synthesis competition one year.
If you're referring to actually searching for interesting theorems, as done by tools like Vampire and Otter, then probably not.
Last month, I was discussing the matching algorithm used in the paper "egg: Fast and Flexible Equality Saturation" with a collaborator. It uses code trees, which I read about a few months earlier in the Handbook of Automated Reasoning. It stands out because I had pretty much never encountered a mention of any of that stuff in the preceding several years.
It's a very lively field. Lots of groups working on it. Last year, the big 3 PL conferences (PLDI, POPL, OOPSLA) all had tracks dedicated to it. A few years ago, Armando (my advisor and the professor of this course) taught a weekend seminar on the nitty-gritty internals of how his tool, Sketch, works ---- and had commercial users flying in.
Fun fact:
My elder brother was Armando's TA in TAMU. Armanda probably was the brightest and most fun guy to work with. There were extra credit for building a fully functional software CPU and its vector pipeline supporting VLIW (mid 90s duh). Your advisor guy did it in a breeze. The instructor privately confided to my brother he was a legend in the making.
Ask him about Sid in Lawrence Rawschberger's class for good old anecdotes! :)
And it's noteably slow due to it; c.p.s. made sense at that time, but modern hardware takes advantage of the existence of a stack much more aggressively.
Chicken Scheme also uses it with a novel approach that allows the C stack to become the garbage collector which is still relatively fast as far as I heard.
For those chiming in about statistics and causal inference: This paper is about causal event ordering in distributed systems. While both might benefit from some common philosophy, this subject has almost nothing to do with causal inference as studied by Pearl, Spirtes, Robins, and friends. See https://en.m.wikipedia.org/wiki/Causal_consistency
Hash tables are bounded below by the speed of arithmetic. A trillion-bit number takes a while to multiply. You may have never touched a trillion-bit number, but it's called "asymptotic" for a reason.
You only get O(1) if you use a model of computation in which arithmetic is constant time. It's simple to work with, even though it's not realistic, and opens up scenarios where you can encode a really complex operation into adding/multiplying some huge numbers, and then claim the overall computation is still fast.
Some theorists use a model of computation in which, if your input size n, then multiplying a log-n bit number is O(1), but multiplying an n-bit number is O(n). I have no idea how this is well-defined.
Constant-time arithmetic is realistic in most normal situations, like evaluating the performance of a hash table implementation. Perhaps your implementation uses 32 bits for the hash function, and can only scale to 4 billion slots. Maybe your implementation of a vector has the same limitation. In general, the reason you'll have trouble trying to store 2^trillion items is not because you chose a data structure with worse asymptotic performance than you expected, it's because you run out of space in the universe in which to store them.
So saying such a structure has O(1) asymptotic access time is not perfectly true in a mathematical sense, for unrealistic numbers. But it's certainly realistic.
Yes, it is, but the question is how do you make this notion of "realistic" formal and rigorous. The usual model for complexity analyses, the TM, can't do constant-time arithmetic. So we're interested in a more powerful model.
I'd proposed a model in a sibling comment that seems to be the one most people use for analyzing algorithms.
A Turing machine can do constant-time arithmetric (or more simply, constant-time bound arithmetic) for operands of bounded size, as was suggested above.
Indeed, in the TM model hash table lookups are necessarily Omega(n) in the length of data stored.
The model of computation used in these analyses and interview questions I'd say is a random-access infinite register machine of infinite size (and constant arithmetic), which is more powerful than a TM (and siblings) in complexity analyses.
Of course, they are useless for analyzing complexity classes of computational problems, but you can use them to talk about the complexity of computer algorithms.
That's not what big O notation is about. It represents the growth rate. In a the case of a hash table, the size of the thing you are hashing is not affected by the number of items present in the hash table. Putting a trillion bit integer into a hash table of other integers is still O(1); it's a constant.
>In a the case of a hash table, the size of the thing you are hashing is not affected by the number of items present in the hash table.
But it is, and that's precisely the reason why hash tables are not O(1) but rather O(log(n)). By the pigeon hole principle, it is impossible to store N items in a hash table using a key whose representation is less than log(N) bits without a collision. This means that there is a relationship between the the size of the key being hashed and the number of elements being inserted in the hash map, specifically the relationship is an element of O(log(n)).
> But it is, and that's precisely the reason why hash tables are not O(1) but rather O(log(n))
I'm sorry, but as a reader it is quite amusing that various posters are claiming (all without citing any sources) hashtables are O(1), O(n) and O(log(n))
I've been studying program transformations for 7 years. Cosmin has a technique, context rewriting, which makes it easy to build refactorings that were hard to do previously. This tool can move is out of the Stone Age for making mass changes.
Then along came the industrial revolution. Soon Japan was out conquering China, despite China having a much larger army.
AI will be much faster, and much, much more powerful than the Industrial Revolution.
If Switzerland is the first to human-level AI, it will not become the world leader in oil production, or shipping, or agriculture. But everything else will be Swiss.
And then when the AI becomes superhuman, everything else will be gone.