On Tue, May 20, 2008 at 10:05 AM, Lukasz Stafiniak <[EMAIL PROTECTED]> wrote: > On Tue, May 20, 2008 at 5:16 AM, Stephen Reed <[EMAIL PROTECTED]> wrote: >> >> Code synthesis, according to my plan, should avoid the need for type >> inference. The AGI would know in advance the type(s) of the variable. >> >> Do you see a use for type inference in my work that I have overlooked? >> > How would it know in advance what type of the variable does it need? > Perhaps to compute some result it would need some other or more > specific arguments than initially conceived? > > In my opinion, planning and program synthesis are closely related, and > type inference is just a way of looking at some issues involved. > (I repeat some of my message below, for the group.)
You can avoid type inference (or something equivalent) only if you use propositional logic (in a specific sense), a logic where you cannot specify properties of objects piece-by-piece. If you can, you need to track what properties exactly a variable (a parameter, a result of some computation/action) has to have having already occurred in contexts it has occurred in, to know where it can be applied / what can be done with it further on. I call this type inference. You can't guess the program at once and then typecheck it, you need do type inference as you go. Oh, a P.S.: you use incremental parsing, interpreting a sentence word-by-word. Type inference is a (usually limited and static) form of program interpretation. It needs to be done incrementally to accompany program synthesis. And this is sometimes difficult! I don't do it incrementally yet (in the system I currently work on). The relation between type inference and program synthesis can be seen from the parallels between algorithm W (the classical type inference for the core of ML languages) and my algorithm C (for program synthesis in the same type system) [http://www.ii.uni.wroc.pl/~lukstafi/pmwiki/uploads/Main/DM_generation.pdf]. Interested people can look at the translated beginning of [http://www.ii.uni.wroc.pl/~lukstafi/pmwiki/uploads/Main/dyplom_en.pdf]. My ideas have evolved since back then. Currently I work on type inference (yeah) in a bit more expressive context. The page of my system: http://www.ii.uni.wroc.pl/~lukstafi/pmwiki/index.php?n=Infer.Infer Using weak constraints would add it more AGIsh flavor, but my work is in programming languages theory context and I needed the simplest thing possible. Currently (in addition to the "glue" type-trees) I have linear inequalities. I plan to add Datalog as a sublogic, then it should at least start looking a bit more like AI... Here two examples with linear arithmetic: >>>>>>> input: newtype Bar newtype List : nat newcons LNil : List 0 newcons LCons : for all (n) : Bar * List(n) --> List(n+1) let rec split = function LNil -> LNil, LNil | LCons (x, LNil) as y -> y, LNil | LCons (x, LCons (y, z)) -> match split z with (l1, l2) -> LCons (x, l1), LCons (y, l2) <<<<<<< output: split1 : [?gen10 <= ?gen9; ?gen9 <= ?gen10 + 1;] List (?gen10 + ?gen9) -> List ?gen9, List ?gen10 -------------- what this means: "split" (the first thing defined by this name) is a function that takes a list of length "a + b" and returns a pair of lists, one of length "a" and the other of length "b", where "b <= a" and "a <= b+1", that is they are of roughly the same length. >>>>>>> input: newtype Binary : nat newtype Carry : nat newcons Zero : Binary 0 newcons PZero : for all (n) : Binary(n) --> Binary(n+n) newcons POne : for all (n) : Binary(n) --> Binary(n+n+1) newcons CZero : Carry 0 newcons COne : Carry 1 let rec plus = function CZero -> (function Zero -> (fun b -> b) | PZero a1 as a -> (function Zero -> a | PZero b1 -> PZero (plus CZero a1 b1) | POne b1 -> POne (plus CZero a1 b1)) | POne a1 as a -> (function Zero -> a | PZero b1 -> POne (plus CZero a1 b1) | POne b1 -> PZero (plus COne a1 b1))) | COne -> (function Zero -> (function Zero -> POne(Zero) | PZero b1 -> POne b1 | POne b1 -> PZero (plus COne Zero b1)) | PZero a1 as a -> (function Zero -> POne a1 | PZero b1 -> POne (plus CZero a1 b1) | POne b1 -> PZero (plus COne a1 b1)) | POne a1 as a -> (function Zero -> PZero (plus COne a1 Zero) | PZero b1 -> PZero (plus COne a1 b1) | POne b1 -> POne (plus COne a1 b1))) <<<<<<<<< output: plus1 : [?vCarry_n_12 <= 1;] Carry ?vCarry_n_12 -> Binary ?gen10 -> Binary ?gen11 -> Binary (?gen10 + ?gen11 + ?vCarry_n_12) ----------------- what this means: "plus" is a function that takes a value of type "Carry c" and binary numbers "Binary a" and "Binary b", and returns a binary number "Binary (a+b+c)" where the carry token "c <= 1" (numbers in types are natural numbers). ------------------------------------------- agi Archives: http://www.listbox.com/member/archive/303/=now RSS Feed: http://www.listbox.com/member/archive/rss/303/ Modify Your Subscription: http://www.listbox.com/member/?member_id=8660244&id_secret=103754539-40ed26 Powered by Listbox: http://www.listbox.com
