Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!know!zaphod.mps.ohio-state.edu!sdd.hp.com!hplabs!hplabsz!kirshenb From: kirshenb@hplabsz.HPL.HP.COM (Evan Kirshenbaum) Newsgroups: comp.lang.prolog Subject: Re: Lists (was Arrays) in Prolog Message-ID: <6015@hplabsz.HPL.HP.COM> Date: 5 Oct 90 00:09:19 GMT References: <1238@ecrc.de> <1990Sep19.075314.14372@irisa.fr> <1403@ecrc.de> <34487@cup.portal.com> <6009@hplabsz.HPL.HP.COM> Reply-To: kirshenb@hplabsz.UUCP (Evan Kirshenbaum) Organization: Hewlett-Packard Laboratories Lines: 33 >This is not exactly a novel idea. Never claimed it was new. The original poster asked for a notation. > The problem with segment >variables is that unification not only may have several solutions, but >occasionally infinitely many of them. Consider: > > [..X foo] to be unified with [foo ..Y] > >The set of unifiers for this example is: > > { X = Y = [] } > { X = Y = [foo] } > { X = Y = [foo foo] } > { X = Y = [foo foo foo] } > ... Actually, [..X, foo] unified with [foo, ..Y] would yield X = Y = [] and X = [foo, ..A], Y = [..A, foo] I don't remember the proof offhand, but if neither sequence is circular, there is always a finite number of unifiers. The problem occurs when you try to unify X:[a,..X] with [...,E,...] (infinitely many unifiers) or [...,L] (no unifiers, but it's hard to prove that). Evan Kirshenbaum HP Laboratories 3500 Deer Creek Road, Building 26U Palo Alto, CA 94304 kirshenbaum@hplabs.hp.com (415)857-7572