Google's Plop is implemented in Lisp
code.google.com
code.google.com
I don't think that makes it a Google product/project. It just means Google paid a student to work on an open source project.
That student appears to have written some of that code in Lisp. Why is that interesting?
surely...
(if (search "lisp" (submission-title submission)) (incf (submission-score submission)))
if(strpos(strtolower($title.$body), 'lisp') !== false) ++$votes;
Oh wait, this is Hacker news. Apologies.
I think that the idea of a Lisp system that learns Lisp programs via probabilistic modeling is intrinsically interesting regardless of who funds it, but that could be personal bias ;->.
Yes, I distrust all language zealots and I avoid them. Committment to a language is a lack of integrity.
I know that when I work with other developers, I want them to use what they will do best with, because I know that I and others are more than smart enough to make minor changes without breaking the thing. Now, it better be well documented, but that's another matter...
Edit: And dammit, why does this topic title tempt me so much to say "your mom is implemented in Lisp"? That's gotta mean something, and I'll bet it's cold as ice.
I see a bunch of AI buzzwords.
Input: (learn 'fib '(x) '(((1) 1) ((2) 1) ((3) 2) ((4) 3))) Output (defun fib (n) (if (< n 3) 1 (+ (fib (1- n)) (fib (- n 2)))))
as well as standard machine-learning tasks such as supervised classification.
For what it does right now, see the examples at the bottom of the quick start guide:
http://code.google.com/p/plop/wiki/QuickStart
For more technical background see e.g. http://metacog.org/main.pdf (my dissertation). I will also add a list of relevant publications to the wiki...
http://www.cs.utexas.edu/~jderick/thesis.pdf
I'll have to look at it more closely when I get a chance.
I was working on learning proofs, rather than programs, but I think there are a lot of similarities.
I'm just a mathematician, and my mind has obviously been warped by continua and the Axiom of Choice but aren't they the same thing?
http://en.wikipedia.org/wiki/Curry-Howard_correspondence
Actually, I've gotten interested in learning more about theoretical CS lately, but my everyone in my department is too old/applied/Russian to care, and my university's CS people only seem to care about operating systems and e-commerce. Can you recommend a logical starting place?
I refer to the article on wikipedia which states: "A converse direction is to use a program to extract a proof, given its correctness. This is only feasible if the programming language the program is written for is very richly typed: the development of such type systems has been partly motivated by the wish to make the Curry-Howard correspondence practically relevant."
Now that more processing power than ever is available, I'm sure this will gradually change. But a lot of theorem proving technology is very old (dates to the 70s) so it may take some time.
The main technique I came up with looks at a particular finite case of a conjecture and generates a proof for that case using simple rewriting. You then look for patterns in that proof and use them to create a generalization. As a simple example, imagine your trying to prove a theorem about lists. First, I consider the case where a list is only 4 elements. Since this is a finite case, I can prove this easily with rewriting. Now I look at that proof and notice that rule X was applied 4 times. If I do the same thing when the list has 5 elements, that rule is applied 5 times. So in the general case, apply the rule n times.
One novel thing about that I came across in this work is something I called "Hybrid proof terms". I found that it is very difficult to find patterns in sequences of terms (the typical way of representing a rewrite based proof). So I used this representation that factors out the things that do not change from one line of the proof to the next.
Feel free to email me if you would like to discuss any more details. I'm not really working on this project anymore but I still find it a fascinating area of study.
Also, for your friend who is thinking about working with ACL2, he should know that the acl2-help mailing list is quite friendly and helpful.
Perhaps a generalisation of this could be used as an intelligence test for AI programs. (for criteria for such a test, see http://www.overcomingbias.com/2008/10/economic-defini.html )
Intelligence is general and is capable of coping with novel problems. AI therefore invovles building machines which have that level of generality. To say this isn't interesting is to say AI isn't interesting.
If you published exactly the problems that were going to be in the test, programs would be written that would solve those problems but would be very poor at doing anything else.
Anyway here are some input-output pairs that I think would be suitable for a learning program:
(i) append 'x' to the end of the string:
r => rx 123 => 123x
Similarly other insertions, deletions, copies of characters or groups of characters.
(ii) learning Roman or Arabic numerals or other number-coding schemes:
/ => i // => ii /// => iii ///////// => ix
3 => xxx 7 => xxxxxxx 9 => xxxxxxxxx 11 => xxxxxxxxxxx
Ideally, once the program has learnt the above two functions it should have an understanding of the underlying concepts and therefore find it easier to learn functions such as:
iii => 3 xii => 12 xvi => 16
r => rx
123 => 123x
and: / => i
// => ii
/// => iii
///////// => ix
3 => xxx
7 => xxxxxxx
9 => xxxxxxxxx
11 => xxxxxxxxxxx
iii => 3
xii => 12
xvi => 16To do AI you have to realize that in the sentences: "Humans have general intelligence and can solve problems in many domains" and "Breadth-first search is a problem-general technique that will always find a solution if one exists" the word "general" does not mean the same thing at all! (cf. the huge literature on inductive bias in human cognition).
For a nice list of program induction problems solvable by search (with a system called ADATE), see http://www-ia.hiof.no/~rolando/Examples/index.html .
I am not suggesting doing that. What I am suggesting is that the problems-to-solve be generated by humans.
Incidently what I am suggesting isn't quite inductive programming but something slightly more general, in that the job of the problem-solver isn't to generate a program that solves the input/output pairs, but to guess what the next output will be depending on its input. (The problem-solver may or may not do this by internally creating a program that solves the problem).
Anyway I've done a quick write-up of what I propose: http://www.includipedia.com/wiki/User:Cabalamat/Function_pre...
See http://research.google.com/. Another way you can tell that this is an official Google project is the 'Google' label on the right-hand side of http://code.google.com/p/plop/, which is only added to code developed at Google that has been open-sourced.
Cheers!
I don't know about these guys, but I've always been under the impression that if you're at Google, you're using one of their "Big 4" languages.... Heck, even Norvig is using Python! (I know, he was using it before he went there... but still).
The research divisions of large companies are generally different than the production side. Researchers generally have the freedom to choose how to implement something.
Also, I don't have a PhD :-)
Neat, that's nice to know.
Does this mean, if you ever wanted your research to go "live" in a Google product, you would first have to rewrite in C++, Java, Python, or Javascript?