Thanks for the link to the video. I have actually thought about some of the things that he talked about but I never put it all together and saw it the way they see agda. I am skeptical about some of Sankel's claims but that is not really relevant. For example I have two problems with Agda that I did not get from the presentation. One is continuous spaces vs discreet sets and the other is the possibility of using improper subsets vs using iterated sets. But maybe those examples are trivial. Even if those examples are trivial I still have other problems with the claims.)
But that video really made me think. I think that the issue of types is really central to AGI and it would be important to an implementation of a 'programming language' like I am thinking about. (A semantic 'programming language' that doesn't actually compile a real program could be used to analyze an actual program - although it might not be as tight as AGDA or an implementation of an actual program.) Here is my thing about types. Let's say that an AGI program is a program that is enabled to learn and to use that learning to deal with situations. Then it is a program that is able to create its own programming. (The programming does not have to have the same features of a good programming language. It could be made so that it is doesn't crash (badly).) If the program is creating its own (high-level) programs then it really has to be typing the objects in those programs. This means that the AGI program will need to be able to treat types as values in some cases and then treat them as types in others. This is something that is important to me so I will use it in my programming language (even I only develop a light analytical tool). The thing with types is that there can be variations amongst types and interrelations. So even if I don't develop a pseudo programming language to work with pure logic problems I do want to develop one to work with AGI problems. So the video really got me thinking. Jim Bromer On Sat, May 24, 2014 at 12:54 PM, Jim Bromer <jimbro...@gmail.com> wrote: > Thanks for the link to the video. I have actually thought about some of > the things that he talked about but I never put it all together and saw it > the way they see agda. I am skeptical about some of Sankel's claims but > that is not really relevant. For example I have two problems with Agda that > I did not get from the presentation. One is continuous spaces vs discreet > sets and the other is the possibility of using improper subsets vs using > iterated sets. But maybe those examples are trivial. Even if those examples > are trivial I still have other problems with the claims.) > > But that video really made me think. I think that the issue of types is > really central to AGI and it would be important to an implementation of > a 'programming language' like I am thinking about. (A semantic 'programming > language' that doesn't actually compile a real program could be used to > analyze an actual program - although it might not be as tight as AGDA or an > implementation of an actual program.) Here is my thing about types. Let's > say that an AGI program is a program that is enabled to learn and to use > that learning to deal with situations. Then it is a program that is able to > create its own programming. (The programming does not have to have the same > features of a good programming language. It could be made so that it is > doesn't crash (badly).) If the program is creating its own (high-level) > programs then it really has to be typing the objects in those programs. > This means that the AGI program will need to be able to treat types as > values in some cases and then treat them as types in others. This is > something that is important to me so I will use it in my programming > language (even I only develop a light analytical tool). The thing with > types is that there can be variations amongst types and interrelations. So > even if I don't develop a pseudo programming language to work with pure > logic problems I do want to develop one to work with AGI problems. So the > video really got me thinking. > > Jim Bromer > > > On Fri, May 23, 2014 at 7:04 PM, Nil Geisweiller > <ngeis...@googlemail.com>wrote: > >> Hi Jim, >> >> you might be interested in functional languages that supports dependent >> types, like Agda or Idris. >> >> That talk is an excellent introduction to dependent type, you don't need >> to know Haskell, though it helps, to follow it >> >> https://www.youtube.com/watch?v=vy5C-mlUQ1w >> >> Nil >> >> On 05/23/2014 08:44 PM, Jim Bromer via AGI wrote: >> > That is interesting. I don't think a purely functional language is quite >> > right for me, but I want to look at the idea more closely. >> > >> > I realized that there are cases where you want to be able to study an >> > operation that does not perform properly (like a network call that >> fails) >> > and there are times when you want to study a problem with the >> presumption >> > that the operations will succeed. And you want to be able to study the >> > cases where there is a reasonable possibility that it will fail more >> often >> > than other cases where there isn't that expectation. >> > >> > I guess that the results of a study like this would not be general >> enough >> > to be of much interest to most people in this group. However, I would >> like >> > to try to find a basic text book on applying mathematical logic to the >> > analysis of algorithms and programs - if I have the time. >> > >> > Jim Bromer >> > >> > >> > On Fri, May 23, 2014 at 5:22 AM, Ben Goertzel <b...@goertzel.org> wrote: >> > >> >> >> >> Jim, >> >> >> >> Any purely functional language, such as Haskell e.g., can be >> >> straightforwardly analyzed using mathematical logic, and there are >> loads of >> >> research papers on this... >> >> >> >> -- Ben >> >> >> >> >> >> On Fri, May 23, 2014 at 5:01 AM, Jim Bromer via AGI <a...@listbox.com >> >wrote: >> >> >> >>> I am starting to think it might be useful to begin studying a logical >> >>> programming where a formal statement of program can be analyzed in >> the way >> >>> that statements in pure traditional logic can be. >> >>> It has to be kept simple, so I am thinking of a purely abstract >> logical >> >>> programming model. So all other applications would be avoided. >> >>> >> >>> A statement can be pure traditional logic or a combination of pure >> >>> traditional logic and program instructions. >> >>> A traditional logical statement can only be executed by a program. >> >>> A traditional logical statement is analyzable. >> >>> A program statement can be executable or analyzable. >> >>> There could be more than one logical statement to be worked on by the >> >>> program. I mean that the logic of the program does not necessarily >> return a >> >>> single true or false. >> >>> >> >>> To start to explain why I think it might be of value to be able to >> >>> analyze a program in a way similar to the methods that we use with >> >>> traditional logic here is an example. If an IF-THEN statement in a >> program >> >>> is executable and the condition is true, then the THEN part is >> executed. >> >>> But in traditional logic, the IF-THEN operation may be false. The >> reason I >> >>> would want to be able to analyze a programmed IF-THEN operation is >> because >> >>> we need to think of programs in simplistic ways so, for example, we >> might >> >>> want to keep track of a (pseudo) program operation that might fail >> even >> >>> though the conditional seemed to have been met. And it might be >> useful to >> >>> also consider program operations that operated that way. >> >>> >> >>> It is necessary to simplify this as much as possible while retaining >> >>> the significant characteristics of an algorithm (that is working with >> a >> >>> traditional logical statement). >> >>> >> >>> An initial effort might only consist of the analysis of a single >> layer of >> >>> executable program instructions which can only call pure traditional >> >>> logical statements. >> >>> >> >>> I know that a lot of the guys in the group have been interested in >> >>> something along these lines. The only way you are going to make any >> >>> progress is by starting out with something less ambitious and less >> >>> confounding. >> >>> >> >>> Jim Bromer >> >>> *AGI* | Archives <https://www.listbox.com/member/archive/303/=now >> > >> >>> <https://www.listbox.com/member/archive/rss/303/212726-deec6279> | >> Modify<https://www.listbox.com/member/?&;>Your Subscription >> >>> <http://www.listbox.com> >> >>> >> >> >> >> >> >> >> >> -- >> >> Ben Goertzel, PhD >> >> http://goertzel.org >> >> >> >> "In an insane world, the sane man must appear to be insane". -- Capt. >> >> James T. Kirk >> >> >> >> "Emancipate yourself from mental slavery / None but ourselves can free >> our >> >> minds" -- Robert Nesta Marley >> >> >> > >> > >> > >> > ------------------------------------------- >> > AGI >> > Archives: https://www.listbox.com/member/archive/303/=now >> > RSS Feed: >> https://www.listbox.com/member/archive/rss/303/13870055-4c6c634a >> > Modify Your Subscription: >> https://www.listbox.com/member/?&; >> > Powered by Listbox: http://www.listbox.com >> > >> >> > ------------------------------------------- AGI Archives: https://www.listbox.com/member/archive/303/=now RSS Feed: https://www.listbox.com/member/archive/rss/303/21088071-f452e424 Modify Your Subscription: https://www.listbox.com/member/?member_id=21088071&id_secret=21088071-58d57657 Powered by Listbox: http://www.listbox.com
