Hi Ben, I don't quite see where you are going with this. Let me re-iterate some random unstructured thoughts that I've said before, and see where they might fit in. Like riffing on a melody.
* First, I'd rather not have human being program in atomese -- I kind of wish it really was a knowledge-representation substrate, and some kind of learning algorithms would generate and manipulate atomese. * I do admit that, when human beings do code in atomese, a nicer syntax, or something would be nice. Earlier today, I explained to David DeMaris that one can create timelines in atomese just fine (using ParallelLink, JoinLink and SleepLink) but if you want it to pause (sleep) for random amounts of time (e.g. using RandomLink) then programming gets awkward. Doable but awkard. * But what's the point of hand-written snippets of atomese, anyway? The goal was to have automated learning algos manipulating the graphs and the automated algo might have a really hard time understanding some complicated RandomLink with math in it. ... so why are we doing this? * The nice thing about types and type theory is that type-checking programs are gauranteed to terminate in finite time, always. This is a useful property that we currently do not leverage in atomese. * Type-checking terminates because, in the theory of term rewriting, type checking is .. I forget... strongly confluent, or something like that. * Term re-writing is exactly what we want to do, when converting EvaluationLinks into PredicateNodes, or converting between various forms in the EquivalenceLink. We don't have any architected way of doing this. The chainer and threign beaste pln rules seem to do this in some ad-hoc ways. I think you call them "rules" in PLN, but there's no C++ code or API that I can call to answer the question "here's a graph, do we already have an equivalent graph somewhere in the atomspace?" (for example, by tracing through EquivalenceLink) * I am concerned by the excessive obsession with lambda calculus and the already heavy over-use of LambdaLink. Down that way leads madness. We need to spend a lot more time thinking "term re-writing" and a whole lot less thinking "lambda" -- and this does seem to fit with some sort of AGDA-vision, because proofs are kind-of-ish about term re-writing, and about termination. * Which brings me back to Kripke Semantics and possible worlds. I have no clue how AGDA does it's stuff, but, in the "real world", with probabilistic reasoning, I just don't see any way at all of avoiding the need for possible worlds during the exploration of a proof. * And so, creating a system for managing possible worlds during proof exploration seems to be an important, neglected task. (I'm not sure, I sometimes suspect that what you used to call "inference trails" is a similar-but-different idea). * So, the thing that we really need, is not so much a nice surface syntax for atomese, but a nice surface syntax for inference control. Let me explain: right now, PLN goes off and explores in some random direction, and promptly hits a combinatorial explosion and all is lost, and so you invent ECAN to place some reins on this beast. But ECAN is this opaque automated system, and we can guess at what it might be doing, but its hard to visualize, and maybe its doing the right thing, and maybe its not. So I'm thinking -- lets make inference paths -- the sequence of steps taken during a search for a proof -- lets make that explicitly visible, a first-class object that can be seen and manipulated and explored. Something that can be pruned, or allow to grow, like a good gardener tending a plant: Lets watch the many shoots of inference, and see which seem good and which bad, and then design an automated system to rein in, to control the directions in which inference goes. * The problem that I see with agda, and with haskell, is that they go off and pursue proofs on their own, with no visibility to the programmer about what they are doing. Trust the system. haskell is infamous for having performance that is hard to predict: you look at haskell code, and you can't tell quite how long it might take. So, I'd like to have "visible inference" (in PLN, using kripke semantics) so that we can have ECAN or its follow-ons can "watch PLN think" -- stay focused, stay on track, not get overwhelmed by combinatoric explosion. --linas On Mon, Aug 29, 2016 at 6:12 PM, Ben Goertzel <[email protected]> wrote: > OK -- I see the light now ... > > What we need to do is > > 1) make a surface syntax for Atomese that is effectively like Agda, > but a good bit prettier > > 2) make an ultra-fast type checker that encompasses moderately complex > dependent types > > 3) then instead of using slow Agda, and incurring the overhead of > going Agda ==> Haskell ==> C++ ... we just go straight NewAtomese ==> > C++, and everything is fast as well as elegant (well everything except > the slow things actually happening inside OpenCog...) > > ... in line with the general principle that integrating others' ideas > sometimes ends up working better than integrating their code... > > But ... well ... not this month I guess ;) > > ben > > -- > Ben Goertzel, PhD > http://goertzel.org > > Super-benevolent super-intelligence is the thought the Global Brain is > currently struggling to form... > > -- > You received this message because you are subscribed to the Google Groups > "opencog" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To post to this group, send email to [email protected]. > Visit this group at https://groups.google.com/group/opencog. > To view this discussion on the web visit https://groups.google.com/d/ > msgid/opencog/CACYTDBdDBfi%3DSSnvRpixtsL_AqRu75AxZbX% > 2BAN9UkdLZAZHX2A%40mail.gmail.com. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "opencog" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/opencog. To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CAHrUA37FfTWoq7nh3wu3TmOYTd9rH30qP1ZAs5wZPABJJs-yow%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
