<\body> <\doc-data| w j¦zykach typizowanych>||<\author-address> Politechnika WrocŖawska, WPPT |>||>|> \; <\table-of-contents|toc> |.>>>>|> Wprowadzenie> |.>>>>|> 1.1Wst¦p. |.>>>>|> 1.2Zagadnienia. |.>>>>|> GP i geny. |.>>>>|> > Zalety wprowadzenia typizacji: programowanie dedukcyjne. |.>>>>|> > Automatyczne programowanie -- synteza programów: synteza dedukcyjna i synteza indukcyjna. |.>>>>|> > Operatory genetyczne i generowanie termów. |.>>>>|> > Generowanie termów i ``answer substitution''. |.>>>>|> > Zacie±nianie odpowiednio±ci mi¦dzy ci”giem wyborów a poprawnie typowanymi termami; przeszukiwanie. |.>>>>|> > Generowanie termów jako przeszukiwanie przestrzeni programów. |.>>>>|> > O potrzebie inferencji typu. |.>>>>|> > Algorytm ``head-driven''. |.>>>>|> > Rozstrzygalno±¢ problemu niepusto±ci typu w ML. |.>>>>|> > Definicje rekurencyjne i definicje lokalne. |.>>>>|> > Rekombinacja i homomorfizm typizowa«. |.>>>>|> > Rekombinacja przez anty-unifikacj¦. |.>>>>|> > Generalizacja i GP. |.>>>>|> > Rekombinacja zgodna z mutacj” i anty-unifikacja drugiego rz¦du. |.>>>>|> > Systemy typów z wi¦zami. |.>>>>|> > Nierozstrzygalno±¢ inferencji typu dla rekurencji polimorficznej. |.>>>>|> > WŖasno±¢ stopu zapewniona przez system typów. |.>>>>|> > Dalej w pracy. |.>>>>|> > RozdziaŖ 2 -- Generowanie termów. |.>>>>|> > RozdziaŖ 3 -- Generalizacja. |.>>>>|> > RozdziaŖ 4 -- Zako«czenie. |.>>>>|> > Generowanie termów.> |.>>>>|> 2.1System typów prostych a intuicjonistyczny rachunek zda«. |.>>>>|> System dedukcji naturalnej i typizowany >-rachunek. |.>>>>|> > |.>>>>|> > >-termu. |.>>>>|> > |.>>>>|> > Dowody w postaci normalnej. |.>>>>|> > |.>>>>|> > |.>>>>|> > Poszukiwanie dowodów. |.>>>>|> > >>. |.>>>>|> > |.>>>>|> > Algorytm generuj”cy >-termy. |.>>>>|> > 2.2System Damasa-Milnera: inferencja typu i generowanie termu. |.>>>>|> Algorytm inferencji typu > i algorytm generowania termu >. |.>>>>|> > Poprawno±¢. |.>>>>|> > PeŖno±¢. |.>>>>|> > Rozszerzenie j¦zyka o konstrukcj¦ . |.>>>>|> > Poprawno±¢ z . |.>>>>|> > PeŖno±¢ z . |.>>>>|> > Zagadnienia praktyczne: CASE sterowane u»yciem. |.>>>>|> > 2.3Monotoniczno±¢ i wŖasno±¢ stopu. |.>>>>|> System typów i algorytm >. |.>>>>|> > Unifikacja z podtypowaniem >>. |.>>>>|> > 2.4Generowanie: mechanizmy do zastosowania. |.>>>>|> System typów z typami indukcyjnymi z wi¦zami unifikacyjnymi. |.>>>>|> > Generowanie >-dŖugich >-normalnych polimorficznych >-termów: Prolog. |.>>>>|> > W stron¦ peŖnego . |.>>>>|> > Programy bez nieu»ytecznych definicji lokalnych. |.>>>>|> > Rekombinacja i generalizacja> |.>>>>|> 3.1Rekombinacja swobodna. |.>>>>|> 3.2Anty-unifikacja drugiego rz¦du -- prosty przypadek. |.>>>>|> Definicja. |.>>>>|> > WŖasno±¢: maksymalnie specyficzna generalizacja. |.>>>>|> > Zgodno±¢ rekombinacji z systemem typów. |.>>>>|> > Zwi”zek z algorytmami z prac [] i []. |.>>>>|> > 3.3Generalizacja drugiego rz¦du i ogólne struktury. |.>>>>|> Generalizacje rekombinatorowe z pracy []. |.>>>>|> > Definicje ogólne i algorytm dla termów monadycznych. |.>>>>|> > Relewantne kombinatory i algorytm dla termów poliadycznych. |.>>>>|> > Praktyczny algorytm uwzgl¦dniaj”cy rozmiar generalizacji. |.>>>>|> > Algorytm rekonstrukcji generalizacji z relewantnymi >-abstrakcjami. |.>>>>|> > Generalizacja przez znajdowanie maksymalnych wspólnych podstruktur. |.>>>>|> > |.>>>>|> > |.>>>>|> > Znajdowanie maksymalnych izomorficznych podsystemów. |.>>>>|> > Rozszerzanie generalizacji na >-termy z definicjami lokalnymi i rekurencyjnymi. |.>>>>|> > Zgodno±¢ z systemem typów. |.>>>>|> > Zako«czenie> |.>>>>|> 4.1WkŖad pracy. |.>>>>|> 4.2Postawione zadania. |.>>>>|> |.>>>>|> Praca bada mo»liwo±ci stosowania bogatszych systemów typów dla programów generowanych przez programowanie genetyczne (ang. genetic programming, GP). GP jest zastosowaniem programowania ewolucyjnego (algorytmów genetycznych w szerokim sensie) do przeszukiwania przestrzeni programów. Wymaga to opracowania operatorów genetycznych dla programów: 0-argumentowego operatora kreacji (generowanie przypadkowego programu), 1-argumentowego operatora mutacji (drobna przypadkowa modyfikacja programu), 2-argumentowego operatora rekombinacji (wymiana fragmentów mi¦dzy dwoma programami). Generowanie termu obejmuje inferencj¦ typu. Praca uzasadnia stosowanie systemów polimorficznych (implicit polymorphism), oraz oparcie rekombinacji na anty-unifikacji. Wybór pada na systemy z wi¦zami ze wzgl¦du na Ŗatwo±¢ wyra»ania w nich wŖasno±ci programów. Opracowanie operatorów genetycznych sprowadza si¦ do zada« generowania termu dla zadanego typu oraz znajdowania podtermów o typizacjach ''homomorficznych''. Praca ilustruje kluczowe wŖasno±ci rozwi”za«: poprawno±¢ i peŖno±¢ algorytmu generowania termów, poprawno±¢ algorytmu rekombinacji termów, dowodami dla mo»liwie najprostszych przypadków. Przedstawione jest nowe spojrzenie na anty-unifikacj¦ drugiego rz¦du. Opracowanie praktycznych algorytmów dla systemów typów z wi¦zami wymaga dalszych bada«, które niniejsza praca jedynie zapocz”tkowuje. \; Programowanie genetyczne (ang. genetic programming, GP) to metaheurystyka (czyli metoda) rozwi”zywania problemów poprzez automatyczn” konstrukcj¦ programów, wykorzystuj”ca wiedz¦ o dziedzinie problemu poprzez funkcj¦ oceniaj”c”, jak dobrze dany program radzi sobie z problemem (funkcj¦ dostosowania, ang. fitness function). Ogólno±¢ metody GP polega na tym, »e nie jest potrzebna analiza semantyczna programów, a w wyniku nie jest potrzebna dogŖ¦bna analiza problemu, poniewa» programy zazwyczaj ocenia si¦ uruchamiaj”c je (np. w symulowanym ±rodowisku). GP jest przykŖadem programowania ewolucyjnego czy te» szeroko rozumianych algorytmów genetycznych, czyli metaheurystyk stochastycznych przetwarzaj”cych zbiór rozwi”za« (populacj¦), konstruuj”cych nowe rozwi”zania z jednego lub wi¦cej starych, wybranych z uwzgl¦dnieniem funkcji dostosowania (lepsze rozwi”zania maj” wi¦ksz” szans¦ wyboru). Wprowadzenie do metod ewolucyjnych zawiera . Termin ``Programowanie genetyczne'' i zapocz”tkowanie dziedziny zawdzi¦czamy Johnowi Kozie . Wyró»nikiem GP w±ród innych zastosowa« programowania ewolucyjnego jest (istotna) niesko«czono±¢ zbioru rozwi”za«; nie mo»na nawet w przybli»eniu reprezentowa¢ programów przez wektory cech o ustalonej dŖugo±ci. Je±li mamy tak” reprezentacj¦, cechy te nazywa si¦ genami. Odpowiednikiem hipotezy bloków buduj”cych jest w przypadku GP hipoteza, »e GP prowadzi do automatycznej identyfikacji przydatnych, funkcjonalnych podprogramów, które rozprzestrzeniaj” si¦ w populacji i s” doskonalone w ró»nych kontekstach. Odpowiednikiem tej hipotezy w dziedzinie ewolucji naturalnej (biologicznej) jest wprowadzona przez Dawkinsa koncepcja jednostki selekcji . Sugeruje to my±lenie o puli genów w przypadku GP jako o bycie zmiennym, który sam podlega ewolucji. Geny to fragmenty programów, które maj” du»” szans¦ by¢ przekazane w caŖo±ci w wielokrotnym zastosowaniu rekombinacji. Opisuje to np. . Bogatsze systemy typów s” inn” (ni» funkcja dostosowania) metod” uwzgl¦dnienia wiedzy o problemie, dost¦pn” gdy wiedz¦ t” mo»na wyrazi¢ w postaci reguŖ logicznych. Ograniczaj” one przestrze« rozpatrywanych programów, eliminuj”c konstrukcje nierozs”dne (nietypizowalne) oraz pozwalaj”c na zadanie specyfikacji, wymaganych od rozwi”za«. Szczególnie istotne jest uwzgl¦dnienie jak najwi¦kszej wiedzy na etapie konstrukcji rozwi”zania, gdy ocena rozwi”zania jest kosztowna (np. funkcj¦ nale»y sprawdzi¢ na wielu przypadkach, albo potrzeba symulowa¢ skomplikowane ±rodowisko dla programu steruj”cego robotem). Cel, który speŖni¢ ma rozwi”zanie, okre±la si¦ jako typ zadany (generowane b¦d” programy tego typu), warunki lokalne zadaje si¦ jako typy konstrukcji pierwotnych (np. funkcji wbudowanych). HasŖo ``automatyczne programowanie'' obejmuje ró»ne techniki komputerowego wspierania programowania. Przegl”d zagadnie« zawiera np. . Synteza programów oznacza automatyczne (lub póŖautomatyczne, interaktywne) generowanie programów. Synteza dedukcyjna oznacza syntez¦ programu na podstawie jego peŖnej specyfikacji w pewnym systemie formalnym. Systemy syntezy dedukcyjnej dzielimy na teorio-dowodowe i transformacyjne. W tych pierwszych specyfikacja jest pewn” formuŖ” logiczn”, dowód której odpowiada znalezieniu programu: w logikach konstruktywnych dowód istnienia oznacza podanie odpowiedniego obiektu, specyfikacja stwierdza istnienie szukanych obiektów. Systemy transformacyjne przeksztaŖcaj” specyfikacj¦ przy pomocy zbioru reguŖ, i gdy nie ma ju» reguŖ do zastosowania, wynik transformacji jest szukanym programem. Systemy teorio-dowodowe podzieliŖbym dalej na systemy reguŖowe i systemy teorio-typowe. Pierwsze przeksztaŖcaj” formuŖ¦ przy pomocy zbioru reguŖ logicznych, otrzymuj”c w wyniku formuŖ¦ (formuŖy) wyra»aj”c” odpowied¹; fragment tej formuŖy jest szukanym programem. Np. formuŖ” wej±ciow” jest tautologia P(?x)>, gdzie jest zmienn” egzystencjaln”, jest specyfikacj”; reguŖy logiczne zachowuj” prawdziwo±¢; formuŖ” wynikow” jest , gdzie jest szukanym programem. Drugie konstruuj” dowód w postaci drzewa (w¦zŖy drzewa identyfikuj” stosowane reguŖy); na mocy izomorfizmu Curry'ego-Howarda, dowód jest szukanym programem. Synteza indukcyjna oznacza generowanie programu na podstawie niepeŖnej wiedzy wyra»aj”cej nasze oczekiwania; wiedzy ``sŖabo ustrukturowanej'', tzn. nie daj”cej wskazówek co do struktury programu. Mamy do dyspozycji mi¦dzy innymi: albo ustalone pary wej±cie-wyj±cie (uczenie si¦ z nauczycielem, program dla zadanych wej±¢ ma zwraca¢ okre±lone wyj±cia), albo metod¦ zwracaj”c” poprawne wyj±cia dla danych wej±¢ (uczenie si¦ z wyroczni”, program ma by¢ prostsz” metod” aproksymuj”c” wyroczni¦), albo metod¦ okre±laj”c” jako±¢ danego wyj±cia dla danego wej±cia (uczenie si¦ ze wzmocnieniem przez eksperymentowanie), albo sposób oceny jako±ci caŖego programu (uczenie si¦ ze wzmocnieniem; nazwa pochodzi st”d, »e mo»emy oceni¢, czy modyfikacja rozwi”zania polepsza go czy pogarsza). Uczenie si¦ ze wzmocnieniem daje u»ytkownikowi najwi¦ksz” swobod¦ co do informacji u»ytej w ocenie programów, ale najmniej wskazówek systemowi co do struktury programu. Z kolei mo»emy podzieli¢ systemy indukcyjnego uczenia si¦ na lokalne i globalne (nielokalne). Metody lokalne rozpatruj” atrakcyjno±¢ pojedynczego rozwi”zania (np. metody optymalizacji gradientowej). Metody globalne (nielokalne) rozpatruj” hipotez¦ opisuj”c” atrakcyjne obszary przestrzeni rozwi”za« (np. metody optymalizacji dziel-i-rz”d¹). Programowanie genetyczne to metoda syntezy indukcyjnej programów b¦d”ca nielokalnym uczeniem si¦ ze wzmocnieniem. Generowanie programów w j¦zykach typizowanych to teorio-dowodowa, teorio-typowa metoda syntezy dedukcjyjnej. Podsumowuj”c: <\enumerate> Synteza dedukcyjna <\enumerate> transformacyjna teorio-dowodowa <\enumerate> reguŖowa Synteza indukcyjna <\enumerate> uczenie si¦ z nauczycielem uczenie si¦ z wyroczni” uczenie si¦ ze wzmocnieniem przez eksperymentowanie uczenie si¦ ze wzmocnieniem <\enumerate> lokalne Praca proponuje poŖ”czenie metod syntezy dedukcyjnej i indukcyjnej, aby najpeŖniej wykorzysta¢ wiedz¦ o problemie. T” cz¦±¢ specyfikacji, która ma charakter ``logiczny`` i jest na tyle prosta, »e pozwala na efektywn” dedukcj¦ programów, zawiera si¦ w systemie typów i typie zadanym. PozostaŖ” cz¦±¢ wiedzy o problemie zawiera si¦ w funkcji oceniaj”cej programy. Algorytmy genetyczne w szerokim sensie mo»na nazwa¢ uczeniem si¦ ``co prawda bez nauczyciela, ale z systemem edukacyjnym''. Operatory rekombinacji próbuje si¦ tworzy¢ tak, aby, je±li rodzice (argumenty operatora) maj” ten sam wynik dla danego wej±cia, to potomek (rezultat operatora) te» miaŖ ten wynik dla tego wej±cia -- rodzice s” nauczycielami potomka. Niestety, w GP stworzenie takiego operatora rekombinacji jest zbyt trudne. Aby algorytm genetyczny (ewolucyjny) mógŖ rozpocz”¢ prac¦, potrzebuje co najmniej trzech operatorów genetycznych: 0-argumentowego operatora kreacji (dla budowy populacji pocz”tkowej), 1-argumentowego operatora mutacji (dla przeszukiwania lokalnego), 2-argumentowego operatora rekombinacji (dla przeszukiwania nielokalnego). Podstaw” operatorów kreacji i mutacji jest algorytm generowania termów. Rozdzielamy zagadnienia przeszukiwania i konstrukcji, redukuj”c generowanie termów do przeszukiwania drzew. Algorytm konstrukcji termu (E,\,>)> dla pewnych ci”gów wyborów >> (ci”gów liczb naturalnych okre±laj”cych pojedyncz” ±cie»k¦ wykonania algorytmu niedeterministycznego) zwraca term o typie > w ±rodowisku ; dla pozostaŖych >> zawodzi (zgŖasza niemo»no±¢ zbudowania termu). Nale»y wtedy podj”¢ prób¦ dla innego ci”gu >>, np. zachowuj”c mo»liwie wiele z wcze±niejszej pracy algorytmu dzi¦ki mechanizmowi nawrotów (kontynuacji) -- jest to cz¦±¢ zagadnienia przeszukiwania. Operator kreacji zwraca (E,\,>)>, gdzie > jest ±rodowiskiem pocz”tkowym (±rodowiskiem konstrukcji pierwotnych), a > jest typem zadanym -- specyfikacj” problemu, a >> odpowiednim (znalezionym) ci”giem wyborów. Operator mutacji (mutacja podtermu) polega na zamianie w termie podtermu > na inny. Wiemy, »e zachodzi s”d typizuj”cy \e:\>; niech podterm > b¦dzie wprowadzony do termu w wyprowadzeniu tego s”du typizuj”cego z przesŖanki \e:\>. Wtedy operator mutacji podstawia pod > wynik (E,\,>)> dla odpowiedniego ci”gu wyborów >>. Informacj¦ o typie podtermów i ±rodowisku jego wyprowadzenia mo»na przechowywa¢ w tych samych strukturach, które wykorzystuje mechanizm nawrotów. Nawet, je±li b¦dziemy zadowoleni z algorytmu zwracaj”cego term dokŖadnie typu >, to w jego implementacji b¦dzie potrzebny algorytm pozwalaj”cy na konkretyzacj¦ typu zadanego. Nie musimy, a wewn”trz algorytmu generuj”cego cz¦sto nie mo»emy, wiedzie¢ wszystko o typie termu, którego szukamy. Niech wi¦c (E,\,>)> znajduje term i podstawienie takie, »e e:T\>. Porównaj podrozdziaŖ 3.4 ``Proof-search in Logical Frameworks'' artykuŖu , czy te» wprowadzenie do SLD-rezolucji w . Zmienne wolne pozostawiamy w > jako niewiadome, które ma znale¹¢ algorytm. Gdy rozpatrujemy operator mutacji, nale»y pami¦ta¢, aby zablokowa¢ mo»liwo±¢ podstawiania pod zmienne, które w nadtermie typu zostaj” zgeneralizowane (traktuj”c je jak staŖe). Nast¦pnie modyfikujemy wyprowadzenie typu dla caŖego programu, stosuj”c odpowiednio podstawienie zwrócone przez wygenerowanie nowego podtermu. Wad” takiego stosowania mutacji jest nadokre±lenie typu programu (jest bardziej skonkretyzowany ni» to wynika z termu), dlatego mo»na retypizowa¢ caŖy program po zastosowaniu mutacji. Ci”g wyborów wyra»a niedeterminizm, czy te» stochastyczno±¢ algorytmu >. Idealnie byŖoby, gdyby dla ka»dego ci”gu wyborów algorytm zwracaŖ term poprawnie typowany, a wyliczeniu ci”gów wyborów odpowiadaŖoby wyliczenie termów zamieszkuj”cych zadany typ. Jednak algorytm wykorzystuje ci”g wyborów do generowania termu, i wyliczeniu ci”gów wyborów odpowiada wyliczenie wszystkich termów odpowiedniej klasy zadanej syntaktycznie. Rzeczywisty algorytm uzyskujemy wi¦c z > dzi¦ki zastosowaniu przeszukiwania grafów (tutaj zasadniczo drzew). Oczywi±cie, Ŗatwiej przeszukiwa¢ w gŖ”b, ale lepiej przeszukiwa¢ wszerz: krótsze termy maj” wi¦ksz” szans¦ by¢ lepszymi programami, > z przeszukiwaniem wszerz daje rekurencyjn” przeliczalno±¢ problemu znajdowania mieszka«ca zadanego typu. Dla operatorów genetycznych zadaj”cych ci”g wyborów losowo i oczekuj”cych odpowiedzi, zwracamy term najbli»szy wskazanemu w¦zŖowi (w sensie obranej strategii przeszukiwania) (lub odpowiadamy, »e taki nie istnieje, je±li wyczerpali±my przestrze«). Mo»emy równie» zwraca¢ rzeczywisty ci”g wyborów, dla ewentualnego wznowienia przeszukiwania (przestrzeni programów). W praktycznej implementacji pami¦tamy o wymuszaniu stopu, gdy przeszukiwanie trwa zbyt dŖugo; zawodzi wtedy próba zastosowania operatora genetycznego. Generowanie termu obejmuje inferencj¦ typu: wyprowadzamy termy typizowane. Je±li nie mamy mechanizmów inferencji (typizacja bazuje na annotacjach termów typami), zastosowanie przeszukiwania grafów de facto rozwi”zuje zadanie inferencji typu dla wygenerowanego termu. W ten sposób struktura przeszukiwa« zostaje zdominowana przez problem inferencji typu, podczas gdy chcemy, aby wyra»aŖa semantyk¦ operacyjn” programów (jak dziaŖaj”). Dlatego konieczne jest odizolowanie termów i typów, nawet niewyszukany algorytm inferencji dla systemów nierozstrzygalnych (z konieczno±ci algorytm bez wŖasno±ci stopu, w praktyce za± ze stopem wymuszonym, czyli algorytm niepeŖny) b¦dzie lepszy od naiwnej enumeracji wszystkich mo»liwych typizowa«. Mo»emy przywróci¢ ``przeliczaln” peŖno±¢'' dodaj”c w momencie stopowania typizacji jej kontynuacj¦ jako (odŖo»ony na pó¹niej) w¦zeŖ struktury przeszukiwa«. Ju» w latach trzydziestych wiadomo byŖo, »e intuicjonistyczny rachunek zda« jest rozstrzygalny. W interpretacji w lambda-rachunku oznacza to, »e dla ka»dego typu z systemu typów prostych mo»emy znale¹¢ term tego typu, albo pokaza¢, »e takich termów nie ma. Wykorzystamy standardowy algorytm znajdowania takiego termu, opisany np. w pracy . Idea polega na wykorzystaniu wŖasno±ci ``cut elimination'', czyli w terminologii >-rachunku faktu, »e je±li istnieje term danego typu, to istnieje term bez >-redeksów, równie» tego typu. Mo»na wi¦c szuka¢ termu w±ród termów normalnych (bez >-redeksów), a pomijaj”c zap¦tlenia w wyprowadzeniach, jest wtedy tylko sko«czenie wiele ±cie»ek do sprawdzenia, ko«cz”cych si¦ zadanym typem. Oczywi±cie, mo»emy zastosowa¢ ten mechanizm dla poszukiwania programów funkcyjnych, poniewa» >-redukcja zachowuje wtedy sens programu. Dla systemu typów prostych mamy wi¦c algorytm generowania, zatrzymuj”cy si¦ dla ka»dego zadanego typu, z termem tego typu lub stwierdzeniem pusto±ci typu. Dla ML bez algebraicznych typów danych, czyli dla ML bez dopasowywania wzorca (lub innych mechanizmów typu CASE), Ŗatwo znale¹¢ algorytm zwracaj”cy term zadanego typu z odpowiadaj”cym programem z wŖasno±ci” stopu, lub odpowiadaj”cy, »e je±li typ zamieszkuj” jakie± termy, to odpowiadaj”ce im programy nie zatrzymuj” si¦ dla »adnego argumentu. Mo»na przeprowadzi¢ eliminacj¦ definicji rekurencyjnych i lokalnych i nast¦pnie zastosowa¢ argument taki sam, jak dla systemu typów prostych. (Je±li program zatrzymuje si¦ dla pewnych danych, to musi istnie¢ gaŖ”¹ programu licz”ca wynik bez wywoŖania rekurencyjnego.) Eliminacja zmienia sens programu, ale nie zmienia typu programu. PeŖny ML wydaje si¦ nie by¢ rozstrzygalny w tym sensie, ale nie potrafi¦ tego pokaza¢. Oczywi±cie, rozstrzygalno±¢ ogólnego problemu niepusto±ci typu (czy istnieje term danego typu) jest równowa»na (przez izomorfizm Curry'ego-Howarda) rozstrzygalno±ci odpowiadaj”cej systemowi logiki. Pozytywne wyniki wi”»” si¦ z peŖno±ci” programowania w Prologu. Algorytm generuj”cy >-normalne polimorficzne >-termy (wykorzystuj”c mechanizm unifikacji) odpowiada strategii SLD-rezolucji. Rozszerzamy go o pozostaŖe konstrukcje ML (czy obszerniejszych systemów). Generowanie (wyliczanie) termów zgodnie z tym algorytmem jest równowa»ne strategii ewaluacji u»ytej w Prologu. Zasygnalizowane w problemy teoretyczne maj” swój praktyczny odpowiednik w zagadnieniu u»yteczno±ci definicji rekurencyjnych i definicji lokalnych. Definicje rekurencyjne s” u»yteczne, je±li odpowiadaj”ce im funkcje przynajmniej czasami si¦ zatrzymuj” (nie b¦d¦ si¦ zajmowaŖ korekurencj”). Zapewnienie mocniejszego warunku u»yteczno±ci jest opisane w . Natomiast definicje lokalne s” u»yteczne, je±li przynajmniej raz s” u»yte w zakresie defi\Licji, s” ce\Lowe, je±li s” u»yte wi¦cej ni» raz. Sk”d jednak wiedzie¢, jakie definicje b¦d” przydatne w budowanym podtermie? Nast¦puj”ce rozwi”zanie wydaje si¦ optymalne: dopuszczaj, aby ka»dy wygenerowany podterm byŖ mo»liw” definicj” lokaln”, o zakresie b¦d”cym najszerszym kontekstem zawieraj”cym zmienne lokalne podtermu. Je±li definicja b¦dzie u»yta (poza miejscem podtermu definiuj”cego), to rzeczywi±cie j” wprowadzamy. W przeciwnym wypadku pozostawiamy podterm ``na miejscu'', nie wprowadzaj”c definicji. To rozwi”zanie ma jednak wad¦, je±li stosuje si¦ je dla termów bez >-redeksów: wprowadza tylko definicje lokalne o typach, które s” podtermami typów ze ±rodowiska lub typu zadanego (wŖa±ciwie, generalizacje tych typów). (Podobny problem pojawia si¦ dla definicji rekurencyjnych.) Ogólnie, chcemy, aby definicje lokalne mogŖy tworzy¢ po zredukowaniu >-redeksy, ale nie chcemy wprowadza¢ bezu»ytecznych >-abstrakcji, których zmienne nie b¦d” nast¦pnie wykorzystane. Rozwi”»emy to, ``patternizuj”c'' wygenerowany podterm (o ile ma stanowi¢ definicj¦ lokan”), czyli wycinaj”c podtermy tego podtermu i formuj”c >-redeksy, nast¦pnie aplikacje zostawiaj”c w zakresie definicji, a >-abstrakcje w ciele definicji. Pojawia si¦ jeszcze jeden problem techniczny. Dla definicji lokalnej nale»y wyznaczy¢ najogólniejszy typ. Ale tworzona jest ona w innym ±rodowisku, ni» ostatecznie ±rodowisko jej zakresu. Rekombinacja polega najogólniej na zast”pieniu podtermu > danego programu > przez podterm > pochodz”cy z innego programu; w j¦zykach typizowanych wymaga to, aby podterm zast¦puj”cy byŖ typu w jakim± sensie konkretyzuj”cego typ podtermu zast¦powanego. Po zast”pieniu nale»y zrekonstruowa¢ typ uzyskanego termu; rekombinacja wymaga wi¦c znalezienia pary podtermów ,e> takich, »e rekonstrukcja jest mo»liwa. W prostych systemach z podtypowaniem zadowalaj”cy jest warunek, aby typ podtermu zast¦puj”cego byŖ podtypem typu podtermu zast¦powanego. W systemach z polimorfizmem parametrycznym, gdzie parametry typu mog” ±ci±le wi”za¢ si¦ z wŖasno±ciami termu i kontekstu jego wyst”pienia, nale»y zbudowa¢ odpowiednio±¢ mi¦dzy s”dami typizuj”cymi \e:\> oraz \e:\> uwzgl¦dniaj”c”, »e > wyst¦puje w derywacji typu dla termu macierzystego. Mo»emy przyj”¢, »e dziedzina ±rodowisk derywacji obu programów macierzystych jest wspólna, ale typy mog” by¢ skonkretyzowane przez ró»ne \Ranswer substitutions''. Te podstawienia musz” by¢ zgodne (unifikowalne), ±rodowisko > musi da¢ si¦ odwzorowa¢ na >, )\Dom(E)>, z zachowaniem zmiennych z )> (przemianowanie zmiennych wolnych). Je±li rekonstrukcj¦ typizowania oprzemy na danym \e:\>, to przemianowanie musi by¢ zgodne z typami: *E(x)=E(h(x))>, oraz typ \=\>, przy czym > nie podstawia pod zmienne wyst¦puj”ce w > ()\\(E)= \>). Trójk¦ ,H> nazwiemy >-homomorfizmem typizowa« \e:\> oraz \e:\>. \ Jak widzimy, rekombinacja w przypadku bogatszych systemów typów jest zŖo»onym problemem znajdowania analogii (mi¦dzy podtermami). Wielu autorów argumentuje, »e podstawowym narz¦dziem znajdowania, czy te» konstrukcji, analogii jest generalizacja (jako znajdowanie kategorii zawieraj”cej wskazane obiekty) (np. ). U»yjemy generalizacji programów dla znajdowania analogicznych pozycji podtermów. Mechanizmem syntaktycznej generalizacji termów jest anty-unifikacja. W kracie termów z porz”dkiem danym przez podstawienia (je±li T) T*e\e>, to \e>, gdzie jest podstawieniem) unifikacja jest operacj” infimum, a anty-unifikacja operacj” supremum dwu termów. Jednak przy pewnych naturalnych definicjach równowa»no±ci i podstawie« anty-unifikacja nie jest dobrze okre±lona (supremum nie istnieje). ArtykuŖy dotycz”ce anty-unifikacji: , , . Ogólnie pomysŖ stosowania anty-unifikacji do rekombinacji termów polega na krzy»owaniu (ang. crossing-over) podstawie«. Dla termów > i > wynikiem anty-unifikacji jest term i podstawienia ,A> t. »e =Ae> i =Ae>. Je±li =[e/x;\;e/x]>, rekombinacj” ,e> b¦dzie ,1>/x;\;e,n>/x]e>, gdzie >> jest dowolnym ci”giem jedynkowo-dwójkowym. Jednak w bogatszych systemach typów jedne podstawienia determinuj” typ dla innych podstawie« i rekombinacja wymaga dostosowania tej techniki (ograniczenia dopuszczalnych ci”gów >> tak, by rekombinant byŖ typizowalny). Jak podpowiada rozs”dek, wspólne cechy obiecuj”cych rodziców nale»y zachowa¢ u potomstwa. Oznacza to, »e rekombinacja powinna respektowa¢ maksymalnie wiele wspólnych cech; cz¦sto nie mo»e respektowa¢ (zachowywa¢) wszystkich (porównaj analizy w ), w podanej wy»ej formalizacji oznacza to, »e supremum zawiera wiele termów. ArtykuŖ pokazuje u»yteczno±¢ rekombinacji zachowuj”cej generalizacje pierwszego rz¦du (nie jest to rekombinacja krzy»uj”ca podstawienia anty-unifikatora, zachowuje si¦ ona bardziej ``swobodnie'') u»ywanej Ŗ”cznie z rekombinacj” swobodn”. Ograniczanie si¦ do rekombinacji zachowuj”cej kontekst wymienianych podtermów (jak rekombinacja krzy»uj”ca anty-unifikatory) ma oczywiste wady, gdy system GP nie ma wsparcia dla duplikacji kodu i wykorzystywania podprogramów (code reuse). Jednak proponowany w niniejszej pracy system wspiera te mechanizmy ewolucji dzi¦ki obsŖudze definicji lokalnych: mutacja mo»e wprowadzi¢ wykorzystanie w danym miejscu dowolnego podtermu, który w razie potrzeby zostanie ``podniesiony'' do definicji lokalnej; odpowiedni operator genetyczny zajmuje si¦ rozwijaniem definicji. Rekombinacja zachowuj”ca kontekst ma du»e znaczenie w kontekscie teori ``samolubnego genu'' nadaj”c to»samo±¢ jednostkom selecji: wymieniany podterm nie trafi w przypadkowe miejsce programu, pozostanie w tej samej pozycji anty-unifikatora. W ten sposób selekcja b¦dzie nast¦powaŖa ze wzgl¦du na speŖnianie funkcji wyznaczonej przez anty-unifikator dla poszczególnych pozycji. Rekombinacja swobodna (dodatkowo dla j¦zyków nietypizowanych, gdzie jest ona rzeczywi±cie swobodna) powoduje nabywanie przez programy du»ych partii ''niekoduj”cych'' -- nigdy nie wykonywanych; problem ten jest nazywany ``code bloat''. Jest to mechanizm obronny zmniejszaj”cy prawdopodobie«stwo przecinania przez rekombinacj¦ cennych fragmentów koduj”cych, co zazwyczaj zaburzy ich funkcj¦ (patrz m. in. znakomicie pokazuj”cy, »e co jest dobre dla genów, nie musi by¢ dobre dla szybko±ci ewolucji). Najpierw przedstawimy techniczne poj¦cie kompatybilnych mutacji próbkowych, »eby nast¦pnie poda¢ obrazowe poj¦cie rekombinacji zgodnej z mutacj”, dodatkowo uzasadniaj”ce oparcie rekombinacji programów na anty-unifikacji. Pozycja podtermu obejmuje pozycje podtermów tego podtermu. Pozycje w termie nazywamy rozdzielonymi, je±li »aden ich podzbiór nie obejmuje wspólnie wszystkich pozycji obejmowanych przez pewn” pozycj¦ obejmuj”c” te pozycje, oprócz tej pozycji. Tzn. nie istnieje pozycja, obejmuj”ca pozycje z tego podzbioru, i nie obejmuj”ca »adnej pozycji nie obejmowanej przez pozycje z podzbioru poza sam” sob”. Zdefiniujmy zbiór kompatybilnych mutacji próbkowych dla programu \e:\> (odpowiednio dobranego). Mówimy, »e zastosowano mutacj¦ ,>>, je±li dany program \e:\> ma w pozycji > podterm z typizacj” \e:\>, a wynikowy program ma dla ,e=\(E,\,>)> posta¢ *E\[e/p]e:T\>. Mutacja jest próbkowa, je±li )\Dom(E)> oraz »adna zmienna ani staŖa > nie wyst¦puje w >. Mutacje próbkowe s” kompatybilne, je±li pozycje > s” rozdzielone, ,e=\(T(1)>\T(k)>E,T(1)>\T(k)>\,>)> dla dowolnego wyboru indeksów > nie zawieraj”cego . Mówimy, »e operator rekombinacji jest zgodny z operatorem mutacji, je±li dla dowolnego zbioru kompatybilnych mutacji próbkowych dowolnego odpowiedniego programu , dla programu > powstaŖego z zastosowania mutacji M> i programu > powstaŖego z zastosowania mutacji M>, zbiór wszystkich rekombinacji ,e> skŖada si¦ z wszystkich programów powstaŖych przez zastosowanie mutacji M>, gdzie L\N\K\L>. Porównaj warunki ``respect'' i ``assortment'' z pracy . Definicja pozycji rozdzielonych zostaŖa dobrana tak, aby zgodny z mutacj” operator rekombinacji mógŖ wogóle istnie¢. Gdyby pozycje nie byŖy rozdzielone, rekombinacja nie potrafiŖaby okre±li¢, ile wŖa±ciwie mutacji zastosowano. Sprawd¹my, co wymusza powy»szy warunek na operatorze rekombinacji. Rekombinacja musi okre±li¢ pozycje, w których mutacj¦ zastosowano tylko w jednym z rodziców. W pierwszym kroku oznaczmy pozycje, minimalne w odlegŖo±ci od korzenia, o ró»nych etykietach (w grafie termu) u obu rodziców. W kolejnych krokach oznaczajmy pozycje, których wszyscy potomkowie s” ju» oznaczeni. Na koniec wybierzmy minimalne w odlegŖo±ci od korzenia pozycje oznaczone. Rekombinacja polega¢ b¦dzie na wymianie podtermów rodziców na tych pozycjach. Je±li podstawimy zmienne w miejscu wybranych pozycji, uzyskamy maksymalnie szczegóŖow” anty-instancj¦ drugiego rz¦du wzgl¦dem porz”dku danego przez podstawienia ograniczone do podtermów anty-unifikowanych programów. Jest to najprostsza posta¢ anty-unifikacji drugiego rz¦du. Du»o mocniejsz” posta¢ anty-unifikacji drugiego rz¦du podaje . Odpowiada ona operatorowi rekombinacji zgodnemu z mutacjami: mutacj” podtermu, insercj” (a wi¦c i delecj”) oraz permutacj” podtermów, przy odpowiednio okre±lonej niezale»no±ci mutacji. PodrozdziaŖ opisuje wŖasno±ci anty-unifikacji Haskera i wy»ej opisanej. W bogatszych systemach typów, okre±lenie anty-unifikacji, a szczególnie rekombinacji, mo»e by¢ trudne. Kluczowym dla naszej sprawy artykuŖem jest wedŖug mnie . Jak wcze±niej pisaŖem, potrzebujemy mo»liwie sprawnej metody inferencji typów dla systemu pozwalaj”cego wyra»a¢ logiczne wŖasno±ci programów. Systemy z ``Guarded Algebraic Data Types'', czyli typami indukcyjnymi zawieraj”cymi charakterystyk¦ logiczn” poszczególnych przypadków, s” pod tym wzgl¦dem bardzo wygodne, co pokazuje chocia»by sukces systemu Coq, stosuj”cego system typów Calculus of Inductive Constructions, rozszerzaj”cy system CC o wŖa±nie ``Guarded Algebraic Data Types'' (GADT). ArtykuŖ Simoneta i Pottiera podaje ``minimalne'' rozszerzenie systemu ML pozwalaj”ce na wygodne posŖugiwanie si¦ GADT -- sparametryzowany j¦zykiem wyra»ania wi¦zów system . Jednocze±nie podaje sprawny algorytm inferencji typu. (Dla potrzeb syntezy programów mo»na rzeczy dodatkowo upro±ci¢ rezygnuj”c z peŖnego mechanizmu ``pattern matching'' na rzecz prostszej analizy przez przypadki.) Jedyne annotacje, jakich potrzebuje system , to typy dla funkcji rekurencyjnych. Potrzebuje ich dlatego, »e aby wykorzysta¢ mo»liwo±ci GADT potrzebujemy rekurencji polimorficznej, a problem inferencji typu dla rekurencji polimorficznej jest nierozstrzygalny. Do inferencji typu dla j¦zyka ML rozszerzonego o rekurencj¦ polimorficzn” (tzw. j¦zyk ML+, albo system Milnera-Mycrofta) proponowano wiele podej±¢. Wa»n” prac” jest , pokazuj”ca redukcj¦ do problemu semi-unifikacji, oraz podaj”ca u»yteczny algorytm semi-unifikacji, pomimo nierozstrzygalno±ci samego problemu. Aktualnie prace nad u»yteczno±ci” inferencji typu dla rekurencji polimorficznej prowadzone s” np. w ramach projektu badawczego [Research Project: ``SEMI-UNIFICATION and Periodicity of Turing Machines`` Carlos Camarao, Lucilia Figueiredo, Luigi Laporte, http://www.dcc.ufmg.br/~camarao/SUP/]. Przeprowadzenie inferencji typu dla rekurencji polimorficznej w systemie jest oczywi±cie trudniejsze, ale wydaje si¦ nie mniej osi”galne ni» w przypadku systemu ML+. Kluczowym zagadnieniem poprawno±ci programu jest posiadanie przez niego wŖasno±ci stopu. Autorka pracy stosuje iteratory (czy te» rekursory) jako funkcje pierwotne do manipulacji indukcyjnymi typami danych, nie pozwalaj”c na rekurencj¦ bezpo±redni”. Przypomina to sytuacj¦ w systemie Coq (przed wprowadzeniem konstrukcji ), gdzie przy definicji typu indukcyjnego system od razu generuje odpowiednie rekursory (funkcje realizuj”ce schematy rekursji). Jednak najodpowiedniejszy schemat rekursji dla danego problemu mo»e by¢ bardzo ró»ny od ogólnego schematu rekursji dla danego typu danych -- warto pozwoli¢ systemowi zrekonstruowa¢ odpowiedni schemat rekursji. Mo»na wymusi¢ wŖasno±¢ stopu przy pomocy systemu typów. Bardzo prostym, a jednocze±nie ekspresyjnym systemem jest > przedstawiony w . Hongwei Xi konstruuje bardziej ekspresyjny system na bazie swojego j¦zyka ( jest obejmowany przez ) . Pisz”c funkcj¦ rekurencyjn”, w prosty sposób wprowadza si¦ metryk¦, wzgl¦dem której kolejne wywoŖania rekurencyjne maj” male¢. (Metryki dopuszczaj” m. in. rekurencj¦ wzgl¦dem wielu zmiennych.) Najpierw przedstawiony jest algorytm generowania termów dla systemu typów prostych, dla postaci normalnych (odpowiadaj”cy dowodzeniu twierdze« intuicjonistycznego rachunku zda«). Nast¦pnie przedstawione s” algorytmy inferencji typów i generowania termów dla systemu Damasa-Milnera (ML), bazuj”ce na ``operacyjnej'' interpretacji reguŖ systemu i wykorzystaniu unifikacji; podane s” wŖasno±ci tych algorytmów, z dowodami. Zaprezentowany jest system > z pracy , w postaci oryginalnej i dostosowanej (zwi¦kszaj”cej operacyjno±¢ reguŖ), i algorytmy generowania termów dla niego, na podstawie algorytmów dla ML. Umówiony jest zwi”zek generowania termów >-normalnych z SLD-rezolucj”. Na koniec, przedyskutowany jest problem optymalnego wprowadzania definicji lokalnych. Zaprezentowany jest algorytm anty-unifikacji drugiego rz¦du wzgl¦dem podstawie« ograniczonych do podtermów unifikowanych termów, pokazana jest maksymalno±¢ generalizacji oraz poprawno±¢ (warunki poprawno±ci) opartej na niej rekombinacji w systemie Damasa-Milnera. Nast¦pnie omówione jest rozwi”zanie zagadnienia generalizacji z pracy i wskazane jest niedopatrzenie: zbyt optymistycznie deklarowana wŖasno±¢ podanego praktycznego mechanizmu znajdowania generalizacji. Przedstawiony jest algorytm konstrukcji generalizacji na bazie wspomnianego mechanizmu. Podany jest z uzasadnieniem mechanizm znajdowania najbardziej szczegóŖowej generalizacji. RozdziaŖ prezentuje rezultaty pracy i zadania postawione do rozwi”zania przez prac¦. W pierwszej cz¦±ci zebrane s” aspekty nowatorskie pracy. W drugiej cz¦±ci wskazane s” dalsze prace, jakie nale»y podj”¢, na drodze do praktycznej implementacji systemu programowania genetycznego w j¦zykach z bogatszymi systemami typów. W tym podrozdziale zaprezentuj¦ wyniki z pracy . Stanowi” one dobre wprowadzenie w problem genrowania termów, w dobrze zbadanym usytuowaniu intuicjonistycznego rachunku zda«. >-rachunek.> Dla uproszczenia, ograniczamy si¦ do implikacyjnego fragmentu logiki intuicjonistycznej. <\definition> Zbiór formuŖ (implikacyjnego rachunku zda«) jest okre±lony reguŖami: <\enumerate> Je±li jest formuŖ” atomow”, to jest formuŖ”. Je±li s” formuŖami, to Y> jest formuŖ”. W tym podrozdziale u»ywamy zamiennie poj¦¢ formuŖa i typ. DŖugo±¢ formuŖy definiujemy <\eqnarray*> |||A>>||A=B\C>>>>>>>>> <\definition> System dedukcji naturalnej \> jest okre±lony nast¦puj”cymi reguŖami: <\enumerate> (Aksjomat) Brak. (I) <\equation*> B> (E) Modus ponens <\equation*> BA|B> <\definition> Niech > b¦dzie sko«czonym zbiorem formuŖ i > b¦dzie formuŖ”. Piszemy \\> je±li istnieje dowód > którego zbiorem niezdj¦tych (undischarged) zaŖo»e« jest >. >-termu.> <\definition> >-term jest zdefiniowany jako: <\enumerate> Zmienne ,x,\> s” >-termami. Je±li s” >-termami, to jest >-termem. Je±li jest >-termem i jest zmienn”, to x.M)> jest >-termem. jest nazywany aplikacj”, a x.M)> abstrakcj”. <\definition> Zbiór zmiennych wolnych (M)> jest okre±lony przez: <\enumerate> (x)={x}> (M N)=\(M)\\(N)> (\x.M)=\(M){x}> <\definition> Je±li jest >-termem i > jest typem, to opis > jest nazywany przypisaniem typu. <\definition> ZaŖo»enie jest przypisaniem typu > zmiennej . Zbiorem zaŖo»e« nazywamy zbiór ={x:\,\,x:\}> taki, »e \x> dla j>. <\definition> System typów >> jest okre±lony przez reguŖy: <\enumerate> (Aksjomat) <\equation*> \\>x:\(x:\\\) <\equation*> \>M:\\\\\>N:\|\\>M N:\> <\equation*> \>M:\|\{x:\}\>\x.M:\\\> <\theorem> \; <\eqnarray*> ||M:\>>|\\>|>|:\,\,x:\}\>M:\>>|||\(M)\{x,\,x}>>>> <\theorem> \\\M:\\M:\>. <\definition> (Beta redukcja) Niech i b¦d” >-termami i b¦dzie zmienn”. >-term otrzymany z przez zast”pienie wszystkich wyst”pie« przez oznaczamy . >-redukcja jest rekurencyjnie okre±lona przez: <\enumerate> >M>. x.M)N\>[N/x]M>. Je±li >N>, wtedy x.M\>\x.N>, >N P> oraz >P N>. Je±li >M> oraz >N>, to >N>. >-term postaci x.M)N> jest nazywany >-redeksem. <\definition> (Posta¢ beta normalna) Je±li >-term nie zawiera >-redeksów, wtedy jest w postaci >-normalnej. Zbiór wszystkich >-termów w postaci normalnej jest oznaczany przez nf>. Mówimy, »e term ma posta¢ >-normaln” N wtw. gdy >N> i \nf>. <\theorem> (Twierdzenie ``subject reduction'') Je±li \M:\> i >N>, to \N:\>. <\theorem> (Twierdzenie o normalizacji) Je±li \M:\>, to \N:\> dla pewnego >-termu \nf> takiego, »e >N>. >>.>Kolejne zastosowania reguŖy (I) daj” <\equation*> \A|B>|A\\\A\B> Kolejne zastosowania reguŖy (E) daj” <\equation*> \\\A\BA\A|B> W szczególno±ci, staje si¦ formuŖ” atomow” w (I*) oraz (E*). Kiedy »adna inferencja nie pojawia si¦ powy»ej \\\A\B> w (E*), jest ona w zbiorze > zaŖo»e«. Kiedy > nie jest atomowa, mamy nast¦puj”cy dowód ponad >: <\equation*> >\A>>|A>>|A>\\\A>\A>> Zdefiniujemy rachunek sekwentów >>. Intuicyjnie, dowód w >> otrzymuje si¦ przez koncentracj¦ wyst”pie« formuŖ atomowych jak i >>. Dowód w >> odpowiada ``dŖugiej postaci normalnej'' (ang. long normal form) w >-rachunku z systemem typów prostych oraz ``rozszerzonej postaci normalnej'' (ang. expanded normal form) Systemu Dedukcji Naturalnej Prawitza. (Zamiast oznacze« oraz z pracy u»yj¦ oznacze« jak ``body`` oraz jak ''head''.) <\definition> Maj”c dan” formuŖ¦ \\\A\A> z atomow” , definiujemy ,\,A}> oraz . Je±li , to >. U»ywamy liter greckich ,\> etc. na oznaczenie zbiorów formuŖ. ,\> oznacza sum¦ zbiorów > i >. <\definition> System dedukcji naturalnej >> jest zdefiniowany nast¦puj”cymi reguŖami: <\enumerate> (Aksjomat) <\equation*> \\A,A\\A (Inferencja) <\equation*> ),\\H(A)\B(A),\\H(A)|\\A> je±li \\\A\A> nale»y do > oraz jest atomowa. <\theorem> Niech > b¦dzie zbiorem formuŖ i A formuŖ”. <\eqnarray*> \A>|>|\>>A>>>> Szukamy dowodu sekwentu \A> (dowód formuŖy dany jest przy = \>). Algorytm bierze jako wej±cie sekwent \A> z atomow” oraz list¦ > sekwentów ±ledz”c” ±cie»k¦ dowodu, aby wykry¢ zap¦tlenie. Algorytm zwraca drzewo sekwentów których wnioskami s” formuŖy atomowe. Li±cie drzewa maj” trzy rodzaje etykiet: ``aksjomat'', ``p¦tla'', ``stop''. Nazywamy je drzewem dedukcyjnym. Drzewem dowodowym albo dowodem nazywamy drzewo, w którym w¦zeŖ powstaje przez zastosowanie reguŖy inferencji systemu dedukcyjnego do jego synów, a li±cie powstaj” przez zastosowanie reguŖy ``aksjomat''. <\definition> \A;\)>: <\enumerate> \>. Zwró¢ w¦zeŖ \> z etykiet” ``aksjomat''. \>. <\enumerate> \A\\>. Zwró¢ w¦zeŖ \A> z etykiet” ``p¦tla''. \A\\>. <\enumerate> > nie zawiera »adnej > takiej, »e )=A>. Zwró¢ w¦zeŖ \A> z etykiet” ``stop''. > zawiera > takie, »e )=A>. Niech ,\,A> b¦d” wszystkimi takimi formuŖami oraz =B\\\B>\A(i=1,\,m)>. Mamy )={B,\,B>}>. Stosuj”c algorytm rekurencyjnie, mamy <\equation*> u=Search((B(B),\)\H(B);(\\A)+\) dla ,m> oraz ,n>. <\enumerate> Dla pewnych (niedeterminizm) i\m>, wszystkie ,\,u>> s” dowodami. Zwró¢ dowód postaci <\equation*> \u>|\\A> Dla ka»dego ,m>, pewne (niedeterminizm) drzewo >> nie jest dowodem j\n)>. Zwró¢ drzewo, którego korzeniem jest \A> a synami korzenia s” >,\,u>>. Niedeterminizm algorytmu nie dotyczy rodzaju odpowiedzi: dowód czy obalenie, a jedynie tego, który konkretnie dowód (które obalenie) zostanie zwrócony. > oznacza ci”g pusty. <\theorem> Niech b¦dzie formuŖ” i \A;\)>. Je±li jest dowodliwa w logice intuicjonistycznej, to wszystkie li±cie s” etykietowane przez ``aksjomat'' i drzewo jest dowodem . <\definition> Je±li drzewo zawiera etykiet¦ ``stop'' albo ``p¦tla'', nazywamy je drzewem obalenia. <\theorem> (Zatrzymywanie si¦ poszukiwania) Dla ka»dego sekwentu \A>, algorytm zatrzymuje si¦ (ko«czy prac¦). <\theorem> Niech b¦dzie formuŖ”, \A;\)>. Je±li nie jest dowodliwa w logice intuicjonistycznej, to jest drzewem obalenia. Drzewo obalenia pozwala wtedy Ŗatwo skonstruowa¢ kontr-model. >-termy.> >-termy w dŖugiej postaci normalnej (ang. >-long >-normal form) s” podstaw” dziaŖania algorytmu : izomorfizm Curry'ego-Howarda wykorzystuje si¦ w dowodzie twierdzenia . Oto wersja zwracaj”ca termy; nie potrzebujemy wtedy drzewa obalenia. Niech > b¦dzie zbiorem zaŖo»e«, a typem. Wtedy ,A;\)>: <\enumerate> \>. Zwró¢ \>. <\enumerate> \A\\>. WywoŖaj wyj”tek ``p¦tla''. \A\\>. <\enumerate> > nie zawiera »adnego > takiego, »e )=A>. WywoŖaj wyj”tek ``stop''. > zawiera :A> takie, »e )=A>. Niech :A,\,x:A> b¦d” wszystkimi takimi przypisaniami typu oraz =B\\\B>\A(i=1,\,m)>. Mamy )={B,\,B>}>. Niech )={B,\,B>}>. Niech > b¦d” nowymi zmiennymi. Stosuj”c algorytm rekurencyjnie, mamy <\equation*> u=Search(({x:B,\,x>:B>},\),H(B);(\\A)+\) dla ,m> oraz ,n>. <\enumerate> Dla pewnych (niedeterminizm) i\m>, wszystkie ,\,u>> s” obliczone. Zwró¢ term postaci <\equation*> (\(x (\x\\x>.u))\(\x\\x>.u>)) Dla ka»dego ,m>, pewne >> nie jest obliczone (wywoŖano wyj”tek) j\n)>. WywoŖaj wyj”tek. \; Generowanie termu dla danego typu jest ''odwrotno±ci”'' inferencji typu dla danego termu. Obie operacje s” dowodzeniem, w pierwszym przypadku, »e typ jest zamieszkaŖy, w drugim, »e term jest poprawnie typowany (ang. well-typed). ReguŖami dowodzenia s” reguŖy obranego systemu typów, które Ŗ”cz” termy i typy. W tym rozdziale opieram si¦ na ksi”»ce , rozdziaŖ 1. ''A polymorphic applicative language''. Wprowad¹my oznaczenia: <\definition> Generalizacja <\eqnarray*> (\,E)>||\,\,\.\>>>> gdzie ,\\> s” dokŖadnie tymi zmiennymi wolnymi w >, które nie wyst¦puj” w . Je±li :\;x:\;\;x:\]>, oraz n\k> to oznaczamy :\> oraz )=\>. DŖugo±¢ oznaczamy >=k>. <\definition> Konkretyzacja typu zmiennej ze ±rodowiska: > jest konkretyzacj” typu zmiennej ze ±rodowiska <\eqnarray*> \E(x)>|>|;x:\\\\.\;\\=[\/\;\;\/\]\>>>> dla pewnych ,\,\>. Typ > jest bardziej ogólny ni» > <\eqnarray*> \\>|>|=\\\\.\\\=\\\\.\\\=[\/\;\;\/\]\>>>> dla pewnych ,\\>. Podstawienie /\;\;\/\]> oznacza zast”pienie wolnych wyst”pie« zmiennych > przez odpowiedni typ >. <\definition> \ ReguŖy typowania j¦zyka Mini-ML: <\enumerate> VAR: Variables. <\equation*> \E(x)|E\x:\> FIX: Functions. <\equation*> \\.x:\\e:\|E\(fix f x.e):\\\> APP: Applications. <\equation*> e:\\\E\e:\|E\e e:\> LET: Local bindings. <\equation*> e:\E.x:\(\,E)\e:\|E\(let x=e in e):\> Dopuszczam -arne konstruktory typów, np. nularny , unarny >, binarny ,\)>. O staŖych mo»na zaŖo»y¢, »e s” zmiennymi pocz”tkowego ±rodowiska. Za [Leroy92] pomijam konstrukcj¦ >-abstrakcji ABS <\equation*> \e:\|E\\x.e:\\\> poniewa» jest ona równowa»na FIX dla nowej nazwy nie wyst¦puj”cej w . W rozwa»anych w tym rozdziale systemach typów (systemie Mini-ML, rozszerzonym nast¦pnie o indukcyjne typy danych) kwantyfikator wyst¦puje tylko na zewn”trz, tzn. ka»dy typ ma posta¢ \\\.\> (lub > dla ) oraz > nie wyst¦puje w >. Je±li typ zadany dla generowanego termu ma tak” posta¢, to do algorytmu generuj”cego przekazujemy /\;\;d/\]\>, gdzie > s” nowymi staŖymi typu (nularnymi konstruktorami typu). W algorytmach zakŖadamy, »e kwantyfikator nie wyst¦puje w zadanym typie. <\lemma> Je±li \> oraz staŖe typu ,\,d> nie wyst¦puj” w , to <\equation*> E\\\\\.[\/d;\;\/d]\ > i algorytm generowania termu >.> Przyjrzyjmy si¦ algorytmowi > tak jak jest on podany w . Kolejne kroki algorytmu odpowiadaj” kolejnym konstrukcjom j¦zyka. Je±li jest zbiorem zaŖo»e« (±rodowiskiem), wyra»eniem, zbiorem nowych zmiennych typu i > ko«czy z powodzeniem, to (E,e,V)=(T,\,V)>, gdzie > jest najogólniejszym typem , takie »e jest odpowiednim podstawieniem pod zmienne w , > s” pozostaŖymi zmiennymi. (\,\)> jest (najogólniejszym) unifikatorem typów ,\>. <\definition> (E,e,V)=(T,\,V)>, gdzie dopasuj : <\enumerate> (VAR: Variables). > i dla \\\.\\E> niech <\eqnarray*> >|||\>/|\>]\>>|>||\|\>>>|||>>>> > (FIX: Functions). Niech <\eqnarray*> ||,\}|\>V>>|,V)>||(E.f:\\\.x:\,e,V)>>|||(R\,\)>>|||>|>||\\)>>>> (APP: Applications). Niech <\eqnarray*> ,V)>||(E,f,V)>>|,V)>||(R*E,g,V)>>|||(S\,\\\)>>|>||\{\}>>|||>|>||>>>> (LET: Local bindings). Niech <\eqnarray*> ,V)>||(E,f,V)>>|,V)>||(R*E.x:\(\,R*E),g,V)>>|||>|>||>>>> Algorytm ten najpierw rozgaŖ¦zia si¦ na poszczególne zmienne, a nast¦pnie unifikuje zgromadzon” informacj¦. Algorytm generuj”cy termy b¦dzie rozdzielaŖ informacje o typie, tak »e gdy Rzdecyduje si¦'' na zmienn”, jej typ b¦dzie ju» (w odpowiednim stopniu) okre±lony. Algorytm zawodzi dla danej ±cie»ki wyborów, je±li nie odnajdzie odpowiedniej zmiennej w ±rodowisku. Zwrócony term ma typ bardziej konkretny ni» typ zadany, zwrócone jest te» odpowiednie podstawienie. Je±li jest ±rodowiskiem, > typem, >> ci”giem liczb naturalnych nazywanym ci”giem albo ±cie»k” wyborów, to albo (E,\,V,>)=(T,e,V, >)>, albo > nie jest okre±lone, gdzie jest typu > w ±rodowisku , > s” niewykorzystanymi zmiennymi typu z , >> s” niewykorzystanymi wyborami: =w> dla pewnego . Zazwyczaj b¦dziemy pomija¢ ci”g wyborów i pisa¢ (E,\,V)=(T,e,V)>, co oznacza, »e równo±¢ zachodzi dla pewnego ustalonego ci”gu wyborów >> i zakŖadaj”c odpowiedni >>. Mo»na przyj”¢ dowolny niesko«czony zbiór zmiennych i pisa¢ (E,\)=(T,e)> zakŖadaj”c odpowiedni >. <\definition> (E,\,V,>)=(T,e,V,>)>, gdzie dla mod 4)> równego <\enumerate> VAR: Variables. Dla mod >)=x:\\\\.\> niech <\eqnarray*> ||(\,[\/\]\[\/\]\)>>|||\|1\i\n}|\>V>>|||>|||>|>||>>>> Je±li unifikator nie istnieje, > jest nieokre±lone. FIX: Functions. Je±li =\\\>, niech <\eqnarray*> ,V,>)>||(E.f:\.x:\,\,V,(w))>>|||>|||>>|>>||>>>>> gdzie s” nowymi zmiennymi. Je±li =\>, gdzie > jest zmienn” typu, dla ,\\V> niech <\eqnarray*> ||\\/\]>>|,V,>)>||(R*E.f:\\\.x:\,\,V\{\,\},(w))>>|||>|||>>>> gdzie s” nowymi zmiennymi. Je±li > ma inn” posta¢, > jest nieokre±lone. APP: Applications. Niech dla \V> <\eqnarray*> ,>)>||(E,\\\,V\{\},(w))>>|,>)>||(R*E,R\,V,>)>>|||>|||>|>>||>>>>> LET: Local bindings. Niech dla \V> <\eqnarray*> ,>)>||(E,\,V\{\},(w))>>|,>)>||(R*E.x:\(R\,R*E),R\,V,>)>>|||>|||>|>>||>>>>> Algorytmy dokonuj” podstawie« w ±rodowisku dla komunikowania informacji o konstruowanym typie: wynikowym typie wyra»enia dla algorytmu inferencji oraz konkretyzacji zadanego typu dla algorytmu >. Dla algorytmów generuj”cych zadany j¦zyk, wŖasno±¢ > nazywamy poprawno±ci”, a wŖasno±¢ > peŖno±ci”. Dowody dla > pochodz” z . Poka»emy najpierw poprawno±¢: <\theorem> Niech b¦dzie wyra»eniem, ±rodowiskiem, zbiorem zmiennych typu. Je±li , V)=\(E,e,V)> jest okre±lone, to mo»emy wywnioskowa¢ e:\>. <\proof> Przez indukcj¦ wzgl¦dem budowy termu: <\enumerate> (VAR: Variables). Mamy > i =[\/\;\;\/\]\>, gdzie \\\.\>, czyli \E(x)>, sk”d x:\>. > (FIX: Functions). Z zaŖ. ind. mamy: <\eqnarray*> ,V)>||(E,e,V\{\,\})>>|\\.x:\)>|>|:\>>>> Z lematu o podstawianiu, podstawiamy po obu stronach, korzystamy z : <\equation*> T(E.f:\\\.x:\)\e:U\ gdzie jest unifikatorem > i >, mamy wi¦c =U\>. Pokazali±my w ten sposób, »e: <\equation*> T*E.f:(T\\T\).x:T\\e:T\ Stosuj”c reguŖ¦ typizowania funkcji (FIX), mamy: <\equation*> T*E\(fix f x in e):T\\T\ To oczekiwany rezultat, poniewa» =T(\\\)=T\\T\>. (APP: Applications). Z zaŖ. ind. mamy: <\eqnarray*> |>|>>||>|>>>> Stosuj”c lemat o podstawianiu: <\equation*> S*R*E\f:S\ Poniewa» unifikuje > i \\>, mamy <\equation*> U*S*R*E\f:U(\\\) Bior”c , z lematu o podstawianiu (drugie równanie) mamy: <\eqnarray*> |>|\U\>>||>|>>>> Teraz z reguŖy typowania APP mamy <\equation*> T*E\f*g:U\ co jest oczekiwanym wynikiem =U\>. (LET: Local bindings). Z zaŖ. ind. mamy: <\eqnarray*> |>|>>|(\,R*E))>|>|>>>> Przemianowuj”c zmienne zwi”zane w (\,R*E)> mo»na pokaza¢ <\equation*> \(S\,S*R*E)=S(\(\,R*E)) Bior”c mamy: <\eqnarray*> |>|>>|(S\,T*E)>|>|>>>> Stosuj”c reguŖ¦ typowania LET: <\equation*> T*E\let x=f in g:\ i =\> jak oczekiwali±my. \; <\theorem> Niech > b¦dzie typem, ±rodowiskiem, zbiorem zmiennych typu. Je±li )=\(E,\,V)> jest okre±lone, to mo»emy wywnioskowa¢ e:T\>. <\proof> Przez indukcj¦ na zŖo»ono±¢ generowanego termu: <\enumerate> (VAR: Variables). Gdy \E(x)>, to \T*E(x)>. Poniewa» jest unifikatorem > oraz >, a wi¦c \T*E(x)>, st”d z reguŖy typowania VAR mamy x:T\>. > (FIX: Functions). =\\\> albo =\>. W pierwszym przypadku, korzystaj”c z zaŖ. ind. mamy <\eqnarray*> .x:\)>|>|:R\>>|\R\.x:R\>|>|:R\>>>> Stosuj”c reguŖ¦ typizowania funkcji (FIX), mamy: <\equation*> R*E\(fix f x in e):R\\R\ To oczekiwany rezultat, poniewa» =R\=R\\R\> dla . W drugim przypadku analogicznie: korzystaj”c z zaŖ. ind. mamy <\eqnarray*> \\.x:\)>|>|:S\>>|\S\.x:S\>|>|:S\>>>> Stosuj”c reguŖ¦ typizowania funkcji (FIX), mamy: <\equation*> S*E\(fix f x in e):S\\S\ To oczekiwany rezultat, poniewa» =S*R\=S\\S\> dla . (APP: Applications). Z zaŖ. ind. mamy: <\eqnarray*> |>|\\)>>||>|>>>> Stosuj”c lemat o podstawianiu, bior”c : <\equation*> T*E\f:T\\T\ Teraz z reguŖy typowania APP mamy <\equation*> T*E\f g:T\ co jest oczekiwanym wynikiem. (LET: Local bindings). Z zaŖ. ind. mamy: <\eqnarray*> |>|>>|(R\,R*E))>|>|>>>> Przemianowuj”c zmienne zwi”zane w (R\,R*E)> mo»na pokaza¢: <\equation*> \(S*R\,S*R*E)=S(\(R\,R*E)) Bior”c mamy: <\eqnarray*> |>|>>|(S*R\,T*E)>|>|>>>> Stosuj”c reguŖ¦ typowania LET: <\equation*> T*E\(let x=f in g):T\ \; Teraz poka»emy peŖno±¢, najpierw algorytmu >, za . <\theorem> Niech b¦dzie wyra»eniem, ±rodowiskiem, niesko«czonym zbiorem zmiennych typu takim, »e \(E)= \>. Je±li istnieje typ > i podstawienie > t. »e E\e:\>, to ,V)=\(E,e,V)> jest okre±lona, i istnieje podstawienie t. »e <\equation*> \=P\T=P*TV <\proof> Przez indukcj¦ wzgl¦dem zŖo»ono±ci : <\enumerate> (VAR: Variables). Poniewa» E\x:\>, mamy Dom(TE)> i \TE(x)>. Dom(E)>, wi¦c (E,x,V)> jest okre±lony i zwraca <\eqnarray*> >||/\;\;\/\]\>>|||>>|>||{\,\,\}>>>> Niech \\\.\>, gdzie \V> nie wyst¦puj” w >. Mamy E(x)=\\\\.T\>. Niech b¦dzie podstawieniem pod > t. »e =R*T\>. We¹my <\equation*> P=R*T[\/\;\;\/\] Mamy =R*T\=\>. Co wi¦cej, \V> nie s” ani >, ani >, wi¦c =R*T\=T\>. To daje oczekiwany rezultat, bo dla >. > (FIX: Functions). Wyprowadzenie typu > ko«czy si¦ zastosowaniem reguŖy FIX: <\equation*> E.f:(\\\).x:\\e:\|TE\(fix f x in e):\\\> Wybierzmy ,\\V> jak w algorytmie. Okre±lmy ±rodowisko i podstawienie >> przez <\eqnarray*> >||\\.x:\>>|>||[\/\;\/\]>>>> Mamy E=TE.f:\\\.x:\>. Stosuj”c zaŖ. ind. do , E, R, \> mamy: <\eqnarray*> ,V)>||(E,e,V\{\,\})>>|>||\>>|>||RV\{\,\}>>>> W szczególno±ci, R\=R\=\>, st”d > jest unifikatorem > i >. St”d istnieje najbardziej ogólny unifikator tych typów: nazwijmy go -- i (E,e,V)> (tzn. wywoŖanie (R\,\)>) jest dobrze okre±lony. Niech b¦dzie podstawieniem t. »e =P*U>. Poka»emy teraz, »e speŖnia »”danie twierdzenia. Mamy: <\eqnarray*> =>|\\)>|\>>||R(\\\)>|P>>||(\\\)>|\,\\V\{\,\}>>||\\>|R>>>> (> nie dziaŖa na > i >). Co wi¦cej, dla ka»dej zmiennej \V>: <\eqnarray*> =>|>|T>>||R\>|P>>||\>|\\V>>||\>|\\V\\\\\\\>>>> c.b.d.o. (APP: Applications). Wyprowadzenie > ko«czy si¦ z <\equation*> E\f:\\\TE\g:\|TE\f*g:\> Stosuj”c zaŖ. ind. do \\,T> otrzymujemy <\eqnarray*> ,V)>||(E,f,V)>>|\\>||\>>|>||RV>>>> W szczególno±ci, E=PR*E>. Stosujemy zaŖ. ind. do ,P,V>. > jest dobre, bo E=PR*E>. <\eqnarray*> ,V)>||(R*E,g,V)>>|>||\>>|>||SV>>>> Mamy \=PS\>. Niech =P[\/\]>. Mamy: <\eqnarray*> S\>||S\=P\=\\\>>|(\\\)>||\\\=\\\>>>> > jest wi¦c unifikatorem > i \\>. Te typy maj” wi¦c najogólniejszy unifikator, (E,f*g,V)> jest dobrze okre±lone. W dodatku, mamy =PU> dla pewnego >. Teraz poka»emy, »e > speŖnia wymagania stwierdzenia. Mamy: <\equation*> P\=PU\=P\=\ a dla wszystkich \V> <\eqnarray*> =>|U*S*R\>|T>>||S*R\>|P>>||S*R\>|\\\, \ R,S>>||R\>|R\\V>>||\>|\\V>>>> (LET: Local bindings). Wyprowadzenie > ko«czy si¦ z: <\equation*> E\f:\TE.x:\(\,TE)\g:\|TE\(let x=f in g):\> Stosujemy zaŖ. ind. do ,T>. Otrzymujemy <\eqnarray*> ,V)>||(E,f,V)>>|>||\>>|>||RV>>>> W szczególno±ci, E=PR*E>. (Teraz sfaktoryzujemy ±rodowisko wyprowadzenia >.) Šatwo sprawdzi¢, »e \(\,R*E)> jest bardziej (nie mniej) ogólne ni» (P\,PR*E)>.<\footnote> Niech \(\,R*E)=P\\\\.\=\\\\.P\>; natomiast (P\,PR*E)=\(\\\\.P\,PR*E)> oraz \\> nie wyst¦puj” w ; zmienne nie wyst¦puj”ce w R*E>\0 które wyst¦puj” w , to te, pod które podstawia >; ale one nie wyst¦puj” w \>. \ Poniewa» mo»emy wyprowadzi¢ <\equation*> TE.x:\(\,PR*E)\g:\ z nast¦puj”cego lematu: <\lemma> Niech > b¦d” ±rodowiskami t. »e )> i (x)\E(x)> dla wszystkich Dom(E)>. Je±li e:\>, to \e:\>. wynika, »e mo»emy równie» wyprowadzi¢ <\equation*> TE.x:P\(\,R*E)\g:\ czyli <\equation*> P(R*E.x:\(\,R*E))\g:\ Stosujemy teraz zaŖ. ind. do (\,R*E),\,P>, otrzymuj”c <\eqnarray*> ,V)>||(R*E.x:\(\,R*E),g,V)>>|>||\>>|>||SV>>>> Algorytm bierze =\> i . Poka»emy, »e > speŖnia wymagania stwierdzenia. Mamy =\>. I je±li \V>, czyli \V>: <\eqnarray*> =>|S*R\>|T>>||R\>|R\\V>>||\>|\\V>>>> St”d =P*T> poza , jak oczekiwano. \; Teraz sprawdzimy peŖno±¢ algorytmu >. Wprowad¹my najpierw inne poj¦cie ogólno±ci typu: <\definition> Typ > jest bardziej ogólny ni» > <\equation*> \\\\P:P\=\ Podstawienie jest bardziej ogólne ni» <\eqnarray*> S>|>|P:P*S=R>>||>|Dom(R)\\\Dom(S):R\\S\>>>> <\theorem> Niech b¦dzie wyra»eniem, ±rodowiskiem. Dla dowolnego typu > i podstawienia > t. »e E\e:T\> oraz (T)\Dom(T)= \>, dla niesko«czonego zbioru zmiennych rozŖ”cznego z (E)> i (T)>, dla pewnej ±cie»ki wyborów zachodzi )=\(E,\,V)> oraz \T> poza . <\proof> Przez indukcj¦ wzgl¦dem zŖo»ono±ci e: <\enumerate> (VAR: Variables). Poniewa» E\x:\>, mamy Dom(E)> i \\TE(x)>. Wybieramy VAR w (E,\,V)> i zmienn” z . Niech \\\.\>. Poniewa» \\TE(x)>, wi¦c istnieje unifikator <\equation*> U=\(\,[\/\;\\/\]\) gdzie \V,\\V>. Poniewa» jest najogólniejszym unifikatorem a > rozszerzony o podstawienia nad > (oznaczone wcze±niej /\]>, ale \\>) te» jest unifikatorem, wi¦c =S*U> poza . Tak wi¦c dla mamy \T> poza . > (FIX: Functions). Wyprowadzenie typu \> ko«czy si¦ z <\equation*> E.f:(\\\).x:\\e:\|TE\(fix f x in e):\\\> Typ > jako ogólniejszy ma posta¢ \\> albo > (gdzie > jest zmienn” typu). Rozpatrzmy najpierw przypadek \\>. Z zaŖ. ind. dla > i > (\=\>) mamy: istnieje ci”g wyborów daj”cy <\equation*> (R,e,V)=\(E.f:\.x:\,\,V) oraz \R> poza . Teza wynika z . W przypadku =\>, \\/\]>, gdzie ,\\V> wprowadzone przez algorytm. Poniewa» \=\\\>, > mo»na zmodyfikowa¢: (T\,\\\)>, =(T\{\\\\\})U*>. Z zaŖ. ind. dla > i \\> mamy <\equation*> (S,e,V)=\(R*E.f:\\\.x:\,\,V\{\,\}) oraz \S> poza {\,\}>. Ale (\\\)=T\>, wi¦c R=T>, st”d \S*R=T>. (APP: Applications). Wyprowadzenie \> ko«czy si¦ z <\equation*> E\f:\\\TE\g:\|TE\f*g:\> Niech =[\/\]T> (co nie stwarza problemów, bo > nie wyst. w >), stosuj”c zaŖ. ind. do > i \\> (zachodzi (\\\)=T\\T\=\\T\=\\\>) <\equation*> (R,f,V)=\(E,\\\,V\{\}) oraz \R> poza {\}>. Niech :T=TR> poza {\}>, zastosujmy zaŖ. ind. do ,R*E,R*\> (R\=T\=\)>: <\equation*> (S,g,V)=\(R*E,R\,V) \S> poza > (niech :T=TS> poza >), a wi¦c \S*R> poza {\}> (bo \V\{\})>, czyli \SR=T> poza (bo \V>). (LET: Local bindings). Wyprowadzenie \> ko«czy si¦ z <\equation*> E\f:\TE.x:\(\,TE)\g:\|TE\(let x=f in g):\> Stosujemy zaŖ. ind. do /\]T> <\equation*> (R,f,V)=\(E,\,V\{\}) mamy /\]T\R>, czyli /\]T=TR>, poza {\}>. Analogicznie jak przy dowodzie dla algorytmu > pokazuje si¦, »e mo»emy wyprowadzi¢ <\equation*> TE.x:T\(R\,R*E)\g:\ Stosujemy wi¦c zaŖ. ind. do powy»szego, bior”c =R*E.x:\(R\,R*E)> <\equation*> (S,g,V)=\(R*E.x:\(R\,R*E),\,V) oraz \S> poza >. St”d \S*R=T> poza , bo \V> i \V>. \ \; Zobaczmy, »e > w pewnym sensie odtwarza, podobnie jak >, najogólniejszy typ skonstruowanego termu. <\corollary> Je±li > jest zmienn” typu nie wyst¦puj”c” w , \V>, oraz (E,\,V)=(T,e,V)>, to dla dowolnego typu > i podstawienia >, \\(\)\\(T)>, dla których E\e:\>, mamy \T> poza {\}> i \T\>. <\proof> ZaŖó»my, »e dla wyborów >> i >> zachodzi (E,\,V,>)=(R,e,V)> oraz (E,\,V,>)=(S,e,V)>. Sprawdzaj”c, »e przebiegi algorytmu si¦ dokŖadnie pokrywaj” (przez indukcj¦ wzgl¦dem ), czyli »e (E,\,V,>)=\(E,\,V,>)>, otrzymujemy, »e . Rozszerzmy > do =[\/\]T>. Mamy E\e:T\>. Ze stwierdzenia dla pewnej ±cie»ki wyborów >> i (E,\,V,>)=(R,e,V)> mamy \R> poza , ale , wi¦c \T> poza , a st”d \T> poza {\}> i =T\\T\>. .> Dotychczasowy system typów nie traktowaŖ w »aden sposób struktur danych. U±ci±limy go pod tym wzgl¦dem i wprowadzimy do j¦zyka manipulacj¦ tzw. indukcyjnymi strukturami danych: konstruktory oraz dekonstruktor analizy przez przypadki . Zaprezentowany system typów odpowiada systemowi > z z pomini¦ciem etapów (stages), które wprowadzimy w nast¦pnym rozdziale. W kwestii szczegóŖów definicji odsyŖam do . <\definition> ReguŖy typowania dla struktur indukcyjnych: <\enumerate-numeric> VAR: Variables... FIX: Functions... APP: Applications... LET: Local bindings... CASE: Deconstruction <\equation*> e:d|\>E\e:Inst>|\>\\ (1\i\n)|E\case e of {c\e\|\\|c\e}:\>\(d)={c,\,c} Zamiast reguŖy: CONS: Constructor <\equation*> c:Inst|\>\d|\>>c\\(d) wprowadzamy zaŖo»enie na temat ±rodowiska : <\equation*> (\d)(\c\\(d)) c:\|\>.Inst|\>\d|\>\E,#|\>d gdzie (d)> jest zbiorem konstruktorów typu , |\>> s” argumentami typu, |\>> jest wektorem typów argumentów konstruktora , je±li typ parametryczny przybierze parametry |\>>. Oznaczenie: je±li |\>=(\,\,\)=(\)i\n>>, to |\>=n> oraz <\equation*> |\>\\=\\\\\\\=\\(\\(\\\)\) Wypada rozszerzy¢ algorytmy > i >. <\definition> (E,e,V)=(T,\,V)>, gdzie dopasuj : <\enumerate> (VAR: Variables)... > (FIX: Functions)... (APP: Applications)... (LET: Local bindings)... of {c\e\|\\|c\e}> (CASE: Deconstruction) Dla typu o arno±ci (-parametrycznego) t. »e ,\,c\\(d)> <\eqnarray*> ||\|1\i\k}\{\}|\>V>>|,\,V)>||(E,e,V)>>|>||(\,d|\>)>>|,\,V)>||(UT*E,e,V)>>|>||(TUT(Inst>|\>\\),\)>>|>||>|,\,V)>||(UT\UTE,e,V)>>|>||(TUT\UT(Inst>|\>\\),\)>>|||T\UT>>|>||>>|>||>>>> <\note> Dla dowolnego podstawienia , typu indukcyjnego , typów |\>,#|\>=ar(d)> i konstruktora \(d)> zachodzi <\eqnarray*> |\>)>|||\>>>|T|\>>|||\>>>>> <\definition> (E,\,V,>)=(T,e,V,>)>, gdzie dla mod 5)> równego <\enumerate> VAR: Variables... FIX: Functions... APP: Applications... LET: Local bindings... CASE: Deconstruction. Niech b¦dzie mod D)>-ym typem indukcyjnym, gdzie jest ilo±ci” typów indukcyjnych, oraz arno±ci” typu . Niech <\eqnarray*> ||\|1\i\k}\{\}|\>V>>|,V,>)>||(E,d|\>,V,(w))>>|,e,V,>)>||(R*E,R*(Inst>|\>\\),V,>)>>|>||>|,e,V,>)>||(T\TR*E,T\TR*(Inst>|\>\\),V,>)>>|||\TR>>||| of {c\e\|\\|c\e}>>|>||>>|>>||>>>>> .> <\theorem> Niech b¦dzie wyra»eniem, ±rodowiskiem, zbiorem zmiennych typu. Je±li , V)=\(E,e,V)> jest okre±lone, to mo»emy wywnioskowa¢ e:\>. <\proof> Przez indukcj¦ wzgl¦dem budowy termu: <\enumerate> (VAR: Variables)... > (FIX: Functions)... (APP: Applications)... (LET: Local bindings)... of {c\e\|\\|c\e}> (CASE: Deconstruction). Z algorytmu i z zaŖ. ind. mamy: <\eqnarray*> E>|>|:\>>|>||(\,d|\>)>>|UTE>|>|:\>>|>||(TUT(Inst>|\>\\),\)>>|>||>|UT\UTE>|>|:\>>|>||(TUT\UT(Inst>|\>\\),\)>>|||T\UT>>|>||>>>> Poniewa» <\equation*> U\=Ud|\> oraz <\equation*> U\=U(Inst>|\>\\) z lematu o podstawianiu mamy (podstawiaj”c po obu stronach >, stosuj”c powy»sz” równo±¢, podstawiaj”c po obu stronach ,U,\,T,U>) <\eqnarray*> |>|:UT\Ud|\>>>||>|:T(Inst>|\>\\)>>|>||>||>|:T(Inst>|\>\\)>>>> Stosuj”c fakt mamy <\eqnarray*> |>|:d(T|\>)>>||>|:Inst>(T|\>)\\>>|>||>||>|:Inst>(T|\>)\\>>>> Z reguŖy dekonstrukcji (CASE) wnioskujemy (dla tamtejszych |\>\T|\>> i \\>) <\equation*> T*E\(case e of {c\e\|\\|c\e}):\ \; <\theorem> Niech > b¦dzie typem, ±rodowiskiem, zbiorem zmiennych typu. Je±li )=\(E,\,V)> jest okre±lone, to mo»emy wywnioskowa¢ e:T\>. <\proof> Przez indukcj¦ na zŖo»ono±¢ generowanego termu: <\enumerate> (VAR: Variables)... > (FIX: Functions)... (APP: Applications)... (LET: Local bindings)... of {c\e\|\\|c\e}> (CASE: Deconstruction). Z algorytmu i zaŖ. ind. mamy: <\eqnarray*> >|||\>>>||>|:R\>>|R*E>|>|:TR(Inst>|\>\\)>>|>||>|\TR*E>|>|:T\TR*(Inst>|\>\\)>>|||\TR>>>> Stosuj”c lemat o podstawianiu i fakt , jak w dowodzie dla algorytmu >, otrzymujemy <\eqnarray*> |>|:d(T|\>)>>||>|:Inst>(T|\>)\T\>>|>||>||>|:Inst>(T|\>)\T\>>>> Z reguŖy dekonstrukcji (CASE) wnioskujemy (dla tamtejszych |\>\T|\>> i \T\>) <\equation*> T*E\(case e of {c\e\|\\|c\e}):T\ \; .> <\theorem> Niech b¦dzie wyra»eniem, ±rodowiskiem, niesko«czonym zbiorem zmiennych typu takim, »e \(E)= \>. Je±li istnieje typ > i podstawienie > t. »e E\e:\>, to ,V)=\(E,e,V)> jest okre±lona, i istnieje podstawienie t. »e <\equation*> \=P\T=P*TV <\proof> Przez indukcj¦ wzgl¦dem zŖo»ono±ci : <\enumerate> (VAR: Variables)... > (FIX: Functions)... (APP: Applications)... (LET: Local bindings)... of {c\e\|\\|c\e}> (CASE: Deconstruction). Wyprowadzenie typu > ko«czy si¦ z <\equation*> E\e:d|\>TE\e:Inst>|\>\\ (1\i\n)|TE\case e of {c\e\|\\|c\e}:\> Stosujemy zaŖ. ind. -krotnie <\eqnarray*> ,\,V)>||(E,e,V)>>||\>>||\>>|>||TV>>|>||(\,d|\>)>>|>||U|\>>>|E>||TE=PUTE>>|,\,V)>||(UT*E,e,V)>>|>|\>\\>||\>>|>||TV>>|>||(TUT(Inst>|\>\\),\)>>|>||U\>>|E>||UTUTE>>|,\,V)>||(UTUTE,e,V)>>|>|\>\\>||\>>|>||TV>>|>||(TUTUT(Inst>|\>\\),\)>>|>||U\>>|>||>|,\,V)>||(UT\UTE,e,V)>>|>|\>\\>||\>>|>||TV>>|>||(TUT\UT(Inst>|\>\\),\)>>|>||U\>>|||T\UT>>|>||T*V>>|>||>>>> Unifikator > istnieje, bo \=d|\>=[|\>/|\>]d|\>>, gdzie |\>/|\>]=[\/\;\;\/\]>. =PU> poza |\>> dla pewnego >, bo |\>/|\>]P> jest innym unifikatorem; (je±li > podstawia pod >, które jest wtedy zmienn”, to > podstawia pod >; je±li > podstawia tylko pod >, to =P>; je±li \=\>, to \=P\>). Istnieje unifikator >, bo \=Inst>|\>\\>, a TUT(Inst>|\>\\)=PUT(Inst>|\>\\)=Inst>|\>\\>, bo U|\>)=P(Ud|\>)=PU\=P\=d|\>>. St”d te» =PU> poza >, bo /\]P> jest unifikatorem. Niech >> oznacza fragment typu \> odpowiadaj”cy \>. Istnieje unifikator >, bo \=Inst>|\>\\>, a <\eqnarray*> TUTUT(Inst>|\>\\)>||UTUT(Inst>|\>\\)>>|||UTUTInst>|\>\PUTUT\>>|||TUTInst>|\>\P(U\)>>|||UTInst>|\>\P\>>>|||>|\>\(\\)>>>> Tak»e =PU> poza >, bo je±li nie >, to napewno /\]P> jest unifikatorem. Podobnie istniej” unifikatory > dla ,n>. Mamy T=PUT\UT=PT\UT=PUT\UT=PUT=PT=T> poza , bo |\>,{\},V,V\V>. Tak»e UT\UT\=\> je±li które± spo±ród > podstawia pod >, w przec. przyp. T=\>. Okre±lmy /\]P>. speŖnia warunki stwierdzenia. \; <\theorem> Niech b¦dzie wyra»eniem, ±rodowiskiem. Dla dowolnego typu > i podstawienia > t. »e E\e:T\> oraz (T)\Dom(T)= \> (?), dla niesko«czonego zbioru zmiennych rozŖ”cznego z (E)> i (T)>, dla pewnej ±cie»ki wyborów zachodzi )=\(E,\,V)> oraz \T> poza . <\proof> Przez indukcj¦ wzgl¦dem zŖo»ono±ci e: <\enumerate> (VAR: Variables)... > (FIX: Functions)... (APP: Applications)... (LET: Local bindings)... of {c\e\|\\|c\e}> (CASE: Deconstruction). Wyprowadzenie \> ko«czy si¦ z <\equation*> E\e:d|\>TE\e:Inst>|\>\\ (1\i\n)|TE\case e of {c\e\|\\|c\e}:\> gdzie =T\>. Wybieramy typ indukcyjny . Stosuj”c -krotnie zaŖ. ind. mamy <\eqnarray*> ,V,>)>||(E,d|\>,V,(w))>>||\>/|\>]T>|>|V>>||\>/|\>]T>||RV>>|,e,V,>)>||(R*E,R*(Inst>|\>\\),V,>)>>|>|>|V>>|>||TV>>|,e,V,>)>||(TR*E,TR(Inst>|\>\\),V,>)>>|>|>|V>>|>||TV>>|>||>|,e,V,>)>||(T\TR*E,T\TR*(Inst>|\>\\),V,>)>>|>|>|V>>|>||TV>>|||\TR>>| >||TV>>>> \ |\>/|\>]Td|\>=[|\>/|\>]d|\>=d|\>>. T=PT\TR=PT\TR=\=PR=[|\>/|\>]T> poza \V\\\V\V>, oraz |\>\V>, czyli T=T> poza . \; Aby zmniejszy¢ przypadkowo±¢ u»y¢ reguŖy CASE, wprowadzamy do ±rodowiska specjalne zmienne ,j>:\|\>.(Inst>|\>)> oznaczaj”ce wyj¦cie -tego argumentu konstruktora >. Dla ka»dego wyboru zmiennej generycznej ,j>> generowane i wprowadzane do ±rodowiska s” nowe zmienne ,j>:(Inst>|\>)> dla ,ar(c)>, odpowiadaj”ce argumentom konstruktora > z odpowiedniej dekonstrukcji CASE (gdzie |\>> s” ±wie»ymi zmiennymi z ); u»yta zostaje zmienna ,j>>. W fazie postprocessingu konstrukcje CASE s” zastosowane w najw¦»szych podtermach obejmuj”cych ,j>> dla ustalonych , tak, »eby »adne ,j>> nie byŖo gŖow” ''swojego'' podtermu. Stworzony podterm nazywamy gaŖ¦zi” gŖówn” odpowiedniego zastosowania CASE; rekurencyjnie generowane s” pozostaŖe gaŖ¦zie CASE. W jednoprzebiegowym algorytmie nale»y przyj”¢ jak”± arbitraln” strategi¦ limitowania rozmiaru gaŖ¦zi. \; Teraz zaprezentuj¦ system kontroluj”cy gŖ¦boko±¢ rekurencji, zapewniaj”cy w ten sposób wŖasno±¢ stopu. System > zostaŖ przedstawiony w . Typy danych w > s” indeksowane informacj” o gŖ¦boko±ci struktur, tzw. etapami: |\>>, jest typem danych, > jest etapem, |\>> s” parametrami typu. ReguŖa wprowadzaj”ca rekurencj¦ zapewnia, »e argument funkcji w wywoŖaniach rekurencyjnych b¦dzie malaŖ, a poniewa» rozmiary danych s” sko«czone, wi¦c program rekurencyjny w ko«cu si¦ zatrzyma. Etapy konstruuje si¦ ze zmiennych etapu, unarnego operatora > oznaczaj”cego jednostkowe zwi¦kszenie rozmiaru, oraz etapu pochŖaniaj”cego >, oznaczaj”cego dowolny rozmiar. |^>> oznacza wszystkie rozmiary nie wi¦ksze wi¦cej ni» o jeden od rozmiarów oznaczanych przez >. |\>> oznacza wszystkie dane ``typu |\>>'' o rozmiarze nale»”cym do (alternatywnie mo»na mówi¢: nie wi¦kszym ni» ). >.> Tak wygl”da prezentacja w : <\definition> Porównywanie etapów > i podtypowanie >. ReguŖy porównywania etapów: <\enumerate-numeric> (REFL) <\equation*> s> (TRANS) <\equation*> rr\p|s\p> (HAT) <\equation*> > (INFTY) <\equation*> \> ReguŖy podtypowania: <\enumerate> (REFL) <\equation*> s> (DATA) <\equation*> r\\\(1\i\ar(d))|d|\>\d|\>> (FUNC) <\equation*> \\\\\|\\\\\\\> <\definition> ReguŖy typowania. <\enumerate> (VAR) <\equation*> x:\> gdy )\\>. (ABS) <\equation*> \e:\|E\\x.e:\\\> (APP) <\equation*> e:\\\E\e:\|E\e e:\> (CONS) <\equation*> Inst|\>\d>|\>> gdy \(d)>. (CASE) <\equation*> e:d>|\>E\e:Inst>|\>\\(1\i\n)|E\case e of {c\e\|\\|c\e}:\> gdy (d)={c,\,c}>. (REC) <\equation*> >|\>\\\e:d|^>>|\>\[|^>/\]\\ pos \|E\(letrec f=e):d|\>\[s/\]\> gdy > nie wyst¦puje w |\>>. (SUB) <\equation*> e:\\\\|E\e:\> Pozytywne-negatywne wyst”pienia zmiennej etapu: <\enumerate> (SP1) <\equation*> pos \> (SP2) <\equation*> neg \\ pos \|\ pos \\\> (SP3) <\equation*> pos \(1\i\ar(d))|\ pos d|\>> (SN1) <\equation*> neg \> (SN2) <\equation*> pos \\ neg \|\ neg \\\> (SN3) <\equation*> nocc s\ neg \(1\i\ar(d))|\ neg d|\>> Jednak my potrzebujemy w reguŖach typowania wskazówek co do podstawie«, dlatego b¦dziemy jawnie obsŖugiwa¢ polimorfizm, wprowadzaj”c explicite kwantyfikacj¦ zmiennych etapu. Poniewa» rekurencja jest dopuszczalna tylko wzgl¦dem argumentu b¦d”cego typem danych, musimy przywróci¢ podziaŖ na abstrakcj¦ i rekurencj¦, jednak dostosujemy system do tego z pierwszego rozdziaŖu, zast¦puj”c (REC) przez konstrukcj¦ (FIX). Wprowadzimy te» definicje lokalne (LET). Zamiast trudnej do kontroli reguŖy (SUB), wprowadzamy podtypowanie obok konkretyzacji typu w regule (VAR). Co istotniejsze, wprowadzimy staŖe etapu (albo zmienne uniwersalne etapu), poniewa» zmienne etapu (albo zmienne egzystencjalne, zmienne unifikacji) w typie zadanym zostaŖyby potraktowane jako niewiadome. Podobnie, wprowadzimy staŖe typu (albo zmienne uniwersalne typu), w odró»nieniu od konstruktorów typów danych i od zmiennych typu (egzystencjalnych, zmiennych unifikacji). (Egzystencjalne) zmienne wolne typu lub etapu nazywamy niewiadomymi typu lub etapu, odpowiednio. <\definition> Generalizacja <\eqnarray*> (\,E)>||\,\,\.\>>>> gdzie ,\\> s” dokŖadnie tymi zmiennymi wolnymi typu lub etapu (niewiadomymi) w >, które nie wyst¦puj” w . <\definition> Konkretyzacja typu zmiennej ze ±rodowiska: > jest konkretyzacj” typu zmiennej ze ±rodowiska , > s” zmiennymi typu, a > s” zmiennymi etapu, <\eqnarray*> \E(x)>|>|;x:\\\\\\\.\;\\=[\/\;\;\/\;s/\;\;s/\]\>>>> dla pewnych typów ,\,\> oraz etapów ,\,s>. Poni»ej, podtypowanie jest tak jak okre±lono powy»ej. <\definition> Dostosowane reguŖy typowania dla >. <\enumerate> VAR: Variables. <\equation*> \E(x)\\\|E\x:\> ABS: Abstractions. <\equation*> \e:\|E\\x.e:\\\> FIX: Recursive functions. <\equation*> >|\>\\.x:d|^>>|\>\e:[|^>/\]\\ pos \|E\(fix f x=e):d|\>\[s/\]\> gdzie > nie wyst¦puje w ani w |\>>. \; APP: Applications. <\equation*> e:\\\E\e:\|E\e e:\> LET: Local bindings. <\equation*> e:\E.x:\(\,E)\e:\|E\(let x=e in e):\> CASE: Deconstruction <\equation*> e:d>|\>E\e:Inst>|\>\\ (1\i\n)|E\case e of {c\e\|\\|c\e}:\>\(d)={c,\,c} Zamiast reguŖy: CONS: Constructor <\equation*> c:Inst|\>\d>|\>>c\\(d) wprowadzamy zaŖo»enie na temat ±rodowiska : <\equation*> \d\c\\(d) c:\\\\\.Inst>|\>\d|^>>|\>\E,nd Aby opracowa¢ algorytm generowania termów > dla >, potrzebujemy mechanizmu szukaj”cego mo»liwo±ci zaj±cia relacji podtypowania, tak jak unifikacja jest ü mechanizmem szukania konkretyzacji. Odpowiedni algorytm nazwiemy >>. Zachodzi >(\,\)>, je±li \U\>, przy czym jest podstawieniem zarówno pod zmienne typu, jak i pod zmienne etapu. <\definition> (E,\,V,>)=(T,e,V,>)>, gdzie dla mod 4)> równego <\enumerate> VAR: Variables. Dla mod >)=x:\\\\.\> niech <\eqnarray*> ||>(\,[\/\]\[\/\]\)>>|||\|1\i\n}|\>V>>|||>|||>|>||>>>> Je±li unifikator nie istnieje, > jest nieokre±lone. ABS: Abstractions. Je±li =\\\>, niech <\eqnarray*> ,V,>)>||(E.x:\,\,V,(w))>>|||>|||x.e>>|>>||>>>>> gdzie s” nowymi zmiennymi. Je±li =\>, gdzie > jest zmienn” typu, dla ,\\V> niech <\eqnarray*> ||\\/\]>>|,V,>)>||(R*E.x:\,\,V\{\,\},(w))>>|||>|||x.e>>>> gdzie s” nowymi zmiennymi. Je±li > ma inn” posta¢, > jest nieokre±lone. FIX: Functions. Je±li =d|\>\\>, niech > dowolne takie, »e ]\=\>, oraz <\eqnarray*> ,V,>)>||(E.f:d>|\>\\.x:d|^>>|\>,[|^>/\]\,V,(w))>>|||>|||>>|>>||>>>>> gdzie s” nowymi zmiennymi. Je±li =\>, gdzie > jest zmienn” typu, dla ,\,\,\,\,\\V> niech <\eqnarray*> ||>|\>\\/\]>>|,V,>)>||(R*E.f:d>|\>\\.x:d|^>>|\>,\,V\{\,\,\,\,\,\},(w))>>|||([|^>/\]\,\)>>|||([\/\]\,\)>>|||>|||>>>> gdzie s” nowymi zmiennymi. Je±li > ma inn” posta¢, > jest nieokre±lone. APP: Applications. Niech dla \V> <\eqnarray*> ,>)>||(E,\\\,V\{\},(w))>>|,>)>||(R*E,R\,V,>)>>|||>|||>|>>||>>>>> LET: Local bindings. Niech dla \V> <\eqnarray*> ,>)>||(E,\,V\{\},(w))>>|,>)>||(R*E.x:\(R\,R*E),R\,V,>)>>|||>|||>|>>||>>>>> CASE: Deconstruction. Niech b¦dzie mod D)>-ym typem indukcyjnym, gdzie jest ilo±ci” typów indukcyjnych, oraz arno±ci” typu . Niech <\eqnarray*> ||\|1\i\k}|\>{\,\}|\>V>>|,V,>)>||(E,d|^>>|\>,V,(w))>>|,e,V,>)>||(R*E,R*(Inst>>|\>\\),V,>)>>|>||>|,e,V,>)>||(T\TR*E,T\TR*(Inst>>|\>\\),V,>)>>|||\TR>>||| of {c\e\|\\|c\e}>>|>||>>|>>||>>>>> Uwagi: zmienna etapu >, podobnie jak parametry typu |\>>, w regule (CASE) i (FIX), s” zmiennymi wolnymi, które mog” zunifikowa¢, ``dowiaduj”c si¦'' (np. od typu > w przypadku (CASE)) jaki etap b”d¹ typ jest potrzebny. >>.> Potrzebujemy najogólniejszego unifikatora, w nast¦puj”cym sensie: je±li >(\,\)>, to \U\>, oraz je±li \V\>, to \U\> oraz \V\>. Odpowiednio, je±li (r,s)>, to U*s> oraz je±li V*s>, to U*r> oraz V*s>. Najpierw porównajmy etapy. <\definition> (r,s)=> dopasuj dobieraj”c pierwszy pasuj”cy przypadek <\enumerate> >: zwró¢ (reguŖa INFTY) ,>: zwró¢ (r,s)> >: zwró¢ (r,s)> (reguŖa HAT) ,#>, gdzie > jest zmienn” etapu: zwró¢ ]> ( jest zmienn” lub staŖ” etapu) >, gdzie > jest zmienn” etapu: je±li > nie wyst¦puje w , zwró¢ ]> <\definition> (\,\)=> dopasuj ,\> <\enumerate> ,#> i > jest zmienn” typu: je±li > nie wyst¦puje w >, zwró¢ /\]> > i > jest zmienn” typu: je±li > nie wyst¦puje w >, zwró¢ /\]> ,\>: zwró¢ \\,\\\>: niech =\(\,\)>, zwró¢ (U\,U\)> |\>,d|\>>: niech <\eqnarray*> >||(r,s)>>|>||(U\,U\)>>|>||>||\>>>|||\>>(U\U|\>-1>\|\>>,U\U|\>-1>\|\>>)>>>> \; Wykonamy krok wstecz od j¦zyka ML z poprzedniego paragrafu, pomijaj”c dekonstrukcj¦ (), definicje rekurencyjne i lokalne, aby do generowania termów wykorzysta¢ doskonaŖ” maszyneri¦, opracowan” dla j¦zyka Prolog. Przy okazji poczynimy krok w kierunku j¦zyka HMG(X), wprowadzaj”c typy indukcyjne z wi¦zami unifikacyjnymi. Modyfikacja, daj”ca system typów z typami indukcyjnymi z wi¦zami unifikacyjnymi, dotyczy reguŖ CASE i CONS. Jednak, aby móc zastosowa¢ mechanizm z korzy±ci” dla cho¢by najprostszych funkcji rekurencyjnych, potrzebna jest rekurencja polimorficzna. <\definition> ReguŖy typowania dla typów indukcyjnych z wi¦zami unifikacyjnymi: <\enumerate-numeric> VAR: Variables... ABS: >-abstractions... APP: Applications... LETREC: Polymorphic Recursion. <\equation*> \e:\\=\(\,E)E.x:\\e:\|E\(letrec x=e in e):\> CASE: Deconstruction <\equation*> e:d|\>TE\e:TInst>|\>\T\ (1\i\n)|E\case e of {c\e\|\\|c\e}:\>\(d)={c,\,c} gdzie =\(|\>,Tyargs>|\>)>, dla wszystkich i\n> takich, »e |\>> i >|\>> unifikuj”, |\>\(\(|\>)\\(E)\\(\))= \> (|\>> s” nowymi zmiennymi). PozostaŖe > s” dowolne. CONS: Constructor <\equation*> c:Inst|\>\d(Tyargs|\>)>c\\(d) odpowiednio zaŖo»enie na temat ±rodowiska : <\equation*> (\d)(\c\\(d)) c:\|\>.Inst|\>\d(Tyargs|\>)\E,#|\>d gdzie (d)> jest zbiorem konstruktorów typu , |\>> jest wektorem argumentów typu zadanym przez konstruktor przy parametrach |\>>, |\>> jest wektorem typów argumentów konstruktora dla parametrów |\>>, oraz |\>=[|\>/|\>]|\>>>>, |\>=[|\>/|\>]|\>>>>. GaŖ¦zie , dla których unifikator nie istnieje, s” tzw. martwym kodem, nie osi”galnym podczas wykonania programu. > komunikuje typowi > dokonany wybór. Przedstawiony system, je±li pomin”¢ fakt, »e u»ywamy prostej analizy przez przypadki zamiast peŖnego dopasowywania wzorca, odpowiada minimalnej wersji , obejmowanej przez dla wszystkich j¦zyków wi¦zów . <\example> Zobaczmy definicj¦ typu lista z parametrem oznaczaj”cym dŖugo±¢. <\eqnarray*> ||\.list(\,0)>>|||\\.\\list(\,\)\list(\,1+\)>>>> >-dŖugich >-normalnych polimorficznych >-termów: Prolog.> Niestety, ''czysty'' prolog odpowiada generowaniu termów tylko dla j¦zyków pierwszego rz¦du (nie myli¢ z systemami typów pierwszego rz¦du; nawet system przedstawiony powy»ej jest pierwszego rz¦du: pod zmienne typu nie mo»na podstawia¢ skwantyfikowanych typów, czyli schematów typu). Podstawowym krokiem, który trzeba podj”¢, jest przej±cie od klauzul hornowskich, ''definite clauses'' (b\\\c>, gdzie ,c> s” atomowe) do dowolnych wyra»e« implikacyjnych (czyli zawieraj”cych > jako jedyny spójnik logiczny). System typów, dla którego generowanie termów >-dŖugich >-normalnych mo»na osi”gn”¢ dostosowuj”c metod¦ SLD-rezolucji, to: <\definition> ReguŖy typowania dla polimorficznych >-termów: <\enumerate-numeric> VAR: Variables. <\equation*> |\>.\|E\x:[|\>/|\>]\> ABS: >-abstractions. <\equation*> \e:\|E\\x.e:\\\> APP: Applications. <\equation*> e:\\\E\e:\|E\e e:\> CONS: Constructor <\equation*> \(d)|E\c:Inst|\>\d(Tyargs|\>)> odpowiednio zaŖo»enie na temat ±rodowiska : <\equation*> (\d)(\c\\(d)) c:\|\>.Inst|\>\d(Tyargs|\>)\E,#|\>d przy oznaczeniach jak powy»ej. .> Definicje lokalne nie wpŖywaj” na logik¦, a jedynie pozwalaj” wielokrotnie wykorzystywa¢ wyniki po±rednie przeszukiwania. Definicje rekurencyjne w postaci nieograniczonej s” paradoksalne: rozszerzaj” zbiór aksjomatów o faŖszywy schemat zdaniowy X)\X>. (Dlatego w GP system typów powinien by¢ rozszerzony by wymusza¢ wŖasno±¢ stopu.) W przypadku rekurencji ``zwykŖej'' zmienne wolne s” skwantyfikowane wspólnie: ((X\X)\X)>, a w przypadku rekurencji polimorficznej s” skwantyfikowane niezale»nie: ((\(X)\X)\X)>. Dekonstrukcja (analiza przez przypadki) z punktu widzenia logiki jest eliminacj” spójnika ''lub'', a nast¦pnie eliminacj” kwantyfikatora egzystencjalnego w ka»dym dysjunkcie. Jej wprowadzenie odpowiada wprowadzeniu aksjomatów: <\equation*> (\|\>.d(Tyargs>|\>)\Inst>|\>)\\\(\|\>.d(Tyargs>|\>)\Inst>|\>) gdzie (d)={c,\,c}>. Z punktu widzenia przeszukiwania wprowadzenie definicji lokalnej odpowiada rozgaŖ¦zieniu si¦ ze wzgl¦du na mo»liwe warto±ci pewnych zmiennych wolnych w |\>>: w ró»nych gaŖ¦ziach zmienne te konkretyzuj” si¦ (niezale»nie), a (pomimo to) w wej±ciowym |\>> pozostaj” nieskonkretyzowane (porównaj reguŖ¦ (CASE) z definicji , warunek na podstawienia unifikuj”ce). Nast¦pnie pozyskiwana jest informacja specyficzna dla danego kostruktora. Odpowiedni mechanizm definicji lokalnych, wŖa±ciwie wspóŖpracuj”cy z operatorem mutacji, jest kluczowy dla ponownego wykorzystywania raz wyewoluowanego kodu przez programy, bez anga»owania mechanizmów rekombinacji. Nieu»ytecznych definicji nie b¦dziemy generowa¢, je±li wielokrotne u»ycie kodu b¦dzie si¦ opieraŖo na kodzie ju» wygenerowanym w jakim± celu. Do±¢ radykalne rozwi”zanie wspieraj”ce ``code reuse'' polega¢ mo»e na dodawaniu, dla ka»dego skonstruowanego podtermu, odpowiadaj”cej mu zmiennej do ±rodowiska. W momencie, gdy z podtermu ``uciekaj”'' zmienne wolne (np. wychodzimy poza odpowiedni” >-abstrakcj¦), typ zmiennej jest wzgl¦dem ich typów ``podnoszony'' i je±li zmienna zostanie u»yta, to b¦dzie zaaplikowana do warto±ci zast¦puj”cej zmienne, które ``uciekŖy''. CaŖy mechanizm jednak trudno zintegrowa¢ z polimorficznym systemem typów, »eby typy zmiennych byŖy mo»liwie ogólne. Niech )\Dom(E)> i )\Dom(E)> oraz istniej” ,T>, »e E=E\|)>> i E=E\|)>> oraz E\e:\>. Znajd¹my podtermy ,e> wprowadzone do typizacji rodziców z typizacjami \e:\> oraz \e:\> (program > -- nadterm > nazywa si¦ matk”, a program-nadterm > -- ojcem), dla których istnieje *E(x)=E(h(x))>, oraz typ \=\>, przy czym > nie podstawia pod zmienne wyst¦puj”ce w > ()\\(E)= \>). Trójk¦ ,H> nazwiemy >-homomorfizmem typizowa« \e:\> oraz \e:\>. Rekombinacj” swobodn” matki > na pozycji podtermu > z ojcem na pozycji podtermu > nazywamy program *TE\[h(e)/e]e:H\>. Typizacja ta mo»e by¢ (podobnie, jak w wyniku mutacji) nadokre±lona wzgl¦dem ±rodowiska >; mo»emy wi¦c przeprowadzi¢ retypizacj¦. \; ¦du -- prosty przypadek.> Przedstawimy w tym podrozdziale anty-unifikacj¦ pierwszego rz¦du w algebrze termów odpowiadaj”cej danemu j¦zykowi rozszerzaj”cemu >-rachunek. Ta anty-unifikacja odpowiada pewnym prostym przypadkom anty-unifikacji drugiego rz¦du. Termy algebry termów nazywam te» >-strukturami: s” to termy, w których konstrukcje >-rachunku (czy te» j¦zyków rozszerzaj”cych j¦zyk >-termów) s” symbolami funkcyjnymi, a staŖe i zmienne >-termu s” symbolami staŖymi. Jedyna modyfikacja wzgl¦dem sformuŖowa« zwykŖych algebr termów i anty-unifikacji pierwszego rz¦du w nich wi”»e si¦ z obsŖug” >-równowa»no±ci i zmiennych zwi”zanych. Warto porówna¢ niniejsze sformuŖowanie z tym zaproponowanym w . Nasza generalizacja radzi sobie ze zmiennymi zwi”zanymi przez bezpo±redni” obsŖug¦ kontekstu (i ograniczenie do generalizacji ''ground terms''), generalizacja w przez ``variable freezing'' (eliminacj¦ zmiennych przez podstawienie staŖych) i zabronienie >-abstrakcji w argumentach. Generalizacja w czy te» w systemie CC jak w pracy Pfenninga jest dodatkowo skomplikowana przez wyst¦powanie typów w termach (''explicit polymorphism''). Nasze generalizacje s” czysto syntaktyczne, w sensie, »e nie rozpatruj” typów termów. Wynika to z zaŖo»enia stosowania systemów typów bez annotacji typami w termach; caŖy ci¦»ar spada oczywi±cie na dowody zgodno±ci z odpowiednim systemem typów. W kwestii skierowania porz”dku, ``co kraj to obyczaj''. W pracy generalizacj¦ oznacza si¦ >, a w pracach oraz przez >. Zamiast formalnej definicji >-struktur przykŖad: programowi <\equation*> fix f x.case x of {Nil\0; Cons \ \y.\z.+1 (f z)} odpowiada >-struktura: <\equation*> fix(case(x,0,\(\((1),(f,z)))))) Stosujemy adaptacj¦ algorytmu Gerarda Hueta obsŖuguj”c” zmienne zwi”zane (kontekst): <\definition> Anty-unifikacja pierwszego rz¦du >-struktur: <\eqnarray*> >>(s,\,s)\>>F>>(t,\,t)>||>>([>/>]s\>.>>[>/>]t,\,[>/>]s\>.>>[>/>]t),F\\>>|>>s>||>|>>t>||([>/>]s,[>/>]t),>>>> gdzie >> i >> s” ci”gami tej samej dŖugo±ci zera lub wi¦cej zmiennych zwi”zanych przez konstrukcj¦ , >> jest ci”giem nowych (nie wyst¦puj”cych w >> ani w >>) zmiennych j¦zyka, >> jest odcinkiem pocz”tkowym dŖugo±ci >> ustalonego ci”gu zmiennych ,v,\> rozŖ”cznego z pozostaŖymi zmiennymi u»ywanymi przez algorytm. > jest bijekcj” mi¦dzy parami >-struktur modulo >-równowa»no±¢ a zbiorem zmiennych (rozŖ”cznym ze zmiennymi j¦zyka). Niech <\eqnarray*> t>||>t>>>> gdzie > jest ci”giem pustym. Dla j¦zyka ML mamy ={,\,fix,let}\{case}D>> gdzie jest zbiorem typów algebraicznych; @,> wi”»” zero zmiennych, ,let> wi”»” jedn” zmienn”, wi”»e dwie zmienne. Dalej uto»samiamy termy j¦zyka i odpowiednie struktury, przeksztaŖcaj”c jedne w drugie w miar¦ potrzeby. Oznacza to, »e j¦zyk rozszerzamy o tzw. meta-zmienne ze zbioru . Podstawienie >> zapewnia, »e podtermy ró»ni”ce si¦ tylko nazwami zmiennych wolnych b¦d” uto»samiane. Poka»emy teraz, »e powy»ej zdefiniowana operacja jest maksymalnie specyficzn” generalizacj” (anty-unifikacj”) dla porz”dku podstawieniowego. Zdefiniujmy teraz podstawienie obsŖuguj”ce kontekst. Pami¦tajmy, »e zwykŖe podstawienie >/>]s> nie podstawia pod zmienne zwi”zane. <\definition> Podstawienie obsŖuguj”ce kontekst: <\eqnarray*> >;F>>(t,\,t))>||>>(%(T,>.>;[>/>]t),\,%(T,>.>;[>/>]t))F\\>>|>;Y)>||>/>]sY\M,T(Y)=>;s>>|>;s)>||>>>> gdzie >> jest ci”giem nowych (nie wyst¦puj”cych w >>) zmiennych j¦zyka. <\definition> \; <\eqnarray*> >;t\>;s>|>|T) %(T,>;t)=>s>>>> Poka»my na rozgrzewk¦ <\theorem> \; <\eqnarray*> >;r\>>s>|>|>;r>>|>;r\>>s>|>|>;s>>>> <\proof> Pokazujemy pierwsz” nierówno±¢ przez indukcj¦ wzgl¦dem zŖo»ono±ci a drug” wzgl¦dem zŖo»ono±ci . W odpowiednim miejscu algorytmu >, wystarczy bra¢ ([>/>]s,[>/>]t))=>;[>/>]s> dla pierwszej nierówno±ci i ([>/>]s,[>/>]t))=>;[>/>]t> dla drugiej, gdzie >,>,s,t> jak w algorytmie >. <\theorem> \; <\eqnarray*> >;t)>|>;t\>;r\>;t\>;s>|>;t\>;r\>>s>>>> <\proof> Ustalmy >;t>. Z zaŖo»enia twierdzenia mamy podstawienia : <\equation*> %(P,>;t)=r,%(Q,>;t)=s . Niech )=>;p,Q(X)=>;q> dla \Dom(P)=Dom(Q)=\\(t)>. Poka»emy, »e )=>;[>/>]p\>>[>/>]q> daje >;t)=r\>>s>. Przeprowad¹my indukcj¦ wzgl¦dem zŖo»ono±ci , przez analiz¦ wyprowadzenia >>s>. <\enumerate> \M>. Wt\0dy \0 >/>]p=r>, >/>]q=s> oraz >;r\>>s>. >>(t,\,t)>. Z zaŖo»enia twierdzenia, musi by¢ >>(r,\,r),s=F>>(s,\,s)>; st”d <\eqnarray*> >>s>||>>([>/>]r\>.>>[>/>]s,\,[>/>]r\>.>>[>/>]s>>>> Poniewa» \r> i \s>, co wynika z definicji podstawienia i >-równowa»no±ci, z zaŖ. ind. mamy >.>;[>/>]t\>.>;[>/>]r\>.>>[>/>]s>. St”d <\eqnarray*> >>s>||>>(%(T,>.>;[>/>]t),\,%(T,>.>;[>/>]t))>>>> gdzie (X)=>;[>/>]p\>>[>/>]q=T(X)>. . Wtedy musi by¢ s=c>. \; <\definition> Niech dane b¦d” programy , oraz E\s:T\> i E\t:T\>. Rekombinacj” nazwiemy program ;s\>t)>, gdzie ;s\>t)=s>, ;s\>t)=t> oraz )=S(X)> lub )=T(X)>. Rekombinacj¦ nazywamy poprawn”, je±li E\r:T\> dla pewnego >. Zbadajmy teraz, dla jakich podstawie« , t)> jest rekombinacj” (tzn. jest typizowalny). Otrzymamy w ten sposób algorytm rekombinacji. Badanie b¦dzie polegaŖo na generalizacji wyprowadze« najogólniejszych typów dla i w ±rodowisku >. Zastosujmy algorytm inferencji typu (prototypem jest algorytm >) do problemu ,s\t>; niech zwraca wyznaczone typy meta-zmiennych. Modyfikujemy algorytm tak, »e gdy ma wyznacza¢ typ którego± z wyst”pie« meta-zmiennej > (w ±rodowisku >), wyznacza typy dla )> oraz )> (z przemianowanymi zmiennymi kontekstu tak, aby odpowiadaŖy zmiennym wprowadzonym do >) w ±rodowisku >. Nast¦pnie generalizuje znalezione typy (zwykŖym algorytmem anty-unifikacji pierwszego rz¦du). Za zmienne generalizacji wstawia nowe konstruktory typu zaaplikowane do listy zmiennych typu: listy wszystkich zmiennych wyst¦puj”cych w podtermach ''ró»nicowych'' (typach z podstawie« generalizacji pod t” zmienn”), wynik przekazuje jako znaleziony typ. Podobnie, generalizuje typy w zwracanych podstawieniach, i zwraca podstawienie z typami ze zmiennymi generalizacji zast”pionymi przez nowe konstruktory. (Nazwijmy te nowe konstruktory zmiennymi generalizacji typu, TGV.) Je±li które± z podstawie« generalizacji jest zmienn” typu, to nazywamy j” zmienn” projekcyjn” tej TGV. Podstawienia generalizacji danej TGV nazywamy gaŖ¦ziami tej zmiennej. Unifikacja TGV z typem polega na osobnych unifikacjach gaŖ¦zi z tym typem, i je±li pojawiaj” si¦ w nim TGV, na unifikowaniu z odpowiedni” gaŖ¦zi” ka»dej TGV. Je±li TGV traci w wyniku unifikacji wszystkie zmienne projekcyjne, \ jej gaŖ¦zie s” ponownie generalizowane, i je±li znaleziona anty-instancja jest nietrywialna, to jest podstawiana pod t” TGV. Zmienne typu podzielimy na specyficzne, wprowadzone w inferencji typu wyst”pienia meta-zmiennej, i niespecyficzne, pozostaŖe. Specyficzne zmienne typu b¦d” si¦ pojawiaŖy tylko w odpowiednich gaŖ¦ziach ró»nych TGV. Je±li w wyniku unifikacji gaŖ¦zi powstaj” podstawienia niespecyficzne, to s” one ujmowane w TGV, która na pozostaŖej gaŖ¦zi ma (now”, specyficzn”) zmienn” projekcyjn”. St”d, je±li inna podgaŖ”¹ b¦dzie unifikowa¢ do tej zmiennej (zast”pionej przez skonstruowan” TGV), to podstawienia zostan” zgeneralizowane, i we wszystkie wyst”pienia (najpierw zmiennej niespecyficznej, nast¦pnie zamienionej na TGV) trafia \ anty-instancja z odpowiednimi TGV. Je±li TGV jest unifikowana z podgaŖ¦zi” innej TGV, to para tych zmiennych jest zapami¦tywana w zbiorze unifikowanych TGV. Je±li nast¦puje podstawienie pod TGV, to pary zawieraj”ce t” zmienn” w zbiorze unifikowanych TGV s” zast¦powane przez pary ``zmienna unifikowana do podstawianej w zast¦powanej parze'' - ''TGV wyst¦puj”ce w podstawieniu''. W zbiorze unifikowanych TGV uwzgl¦dniamy te» podstawienia pod zwykŖe zmienne typu, kiedy pewne TGV trac” zmienn” projekcyjn”. Je±li zmienna typu zostaje skwantyfikowana (zgeneralizowana w sensie polimorfizmu), to w zbiorze unifikowanych TGV przestaje ona by¢ zmienn” projekcyjn”. Despecyfikacja zmiennych. Po zako«czeniu inferencji, usuwamy TGV której obydwie gaŖ¦zie s” zmiennymi specyficznymi (i albo obydwie s” nieskwantyfikowane, albo obydwie s” skwantyfikowane), zast¦puj”c te zmienne now” zmienn” niespecyficzn” (nie ograniczon” do gaŖ¦zi odpowiadaj”cych jednemu programowi). Usuwamy te» pary zawieraj”ce t” zmienn” ze zbioru unifikowanych TGV. (Usuwamy te» wszystkie TGV, które te» miaŖy te zmienne jako projekcyjne, zgodnie z zasad”, »e generalizujemy TGV które trac” swoje zmienne projekcyjne.) Post¦pujemy tak, dopóki s” TGV z dwiema specyficznymi zmiennymi projekcyjnymi. Jest to krok niedeterministyczny algorytmu: wynik zale»y od kolejno±ci wyboru TGV. Silna despecyfikacja konkretyzuj”ca stanowi ostatni”, opcjonaln” faz¦ algorytmu. Mo»na pozby¢ si¦ jeszcze wi¦kszej ilo±ci TGV, kosztem konkretyzacji ``answer substitution''. Usuwamy TGV maj”c” zmienn” projekcyjn” (mo»e by¢ niespecyficzna) nie skwantyfikowan” (czyli woln” w caŖym typowaniu), podstawiaj”c pod zmienn” projekcyjn” pozostaŖ” gaŖ”¹ TGV, o ile zmienna projekcyjna nie wyst¦puje w tej gaŖ¦zi. Pami¦tamy, aby doda¢ to podstawienie do ``answer substitution''. Gdy która± TGV w wyniku starci swoje zmienne projekcyjne, generalizujemy gaŖ¦zie i powtarzamy despecyfikacj¦ dla (ewentualnie) powstaŖych TGV. Jest to krok niedeterministyczny. <\lemma> Tak zmodyfikowany algorytm ko«czy prac¦ zwracaj”c pewien typ i podstawienie. Nazwijmy dwa wyst”pienia meta-zmiennych zale»nymi, je±li typ jednego zawiera TGV unifikowan” z TGV wyst¦puj”c” w typie drugiego (tzn. para tych TGV nale»y do zbioru unifikowanych TGV), a silnie zale»nymi, je±li »adna TGV z pary nie zawiera zmiennej projekcyjnej. <\definition> Rekombinacja podstawie« typów: \\(T,T)> je±li <\eqnarray*> \>||\\)\\Dom(T)\Dom(T)>>|=T\>||=T\>>|=T\>|>|=S\\\\\(\\\)>>|\\)=\>||\\)=\>>>> gdzie > jest generalizacj” pierwszego rz¦du, \> zwraca zmienne wstawione przez generalizacj¦. <\theorem> Rekombinacja, która pod wyst”pienia zale»ne bez despecyfikacji konkretyzuj”cej podstawia z tego samego podstawienia (rodzica), jest poprawna. Je±li E\s:T\> i E\t:T\>, to E\r:T\> i \\(T,T)>, dodatkowo je±li \> i \> s” pryncypalnymi typami i , to \> jest typem pryncypalnym (ang. principal type) programu . Rekombinacja, która pod wyst”pienia zale»ne po despecyfikacji konkretyzuj”cej podstawia z tych samych podstawie«, jest poprawna. Rekombinacja, która pod wyst”pienia silnie zale»ne podstawia z ró»nych podstawie« (rodziców), nie jest poprawna. <\proof> (Szkicowe uzasadnienie twierdzenia.) <\enumerate> Je±li pod TGV podstawimy odpowiednie podstawienia generalizacji, ze zmiennymi zast¦pionymi przez argumenty TGV, to uzyskamy przebiegi algorytmu odpowiadaj”ce przebiegom dla rodziców, je±li staniemy przed faz” despecyfikacji konkretyzuj”cej. Kolejne genralizacje nie wpŖywaj” na odpowiednio±¢ z przebiegiem algorytmu > dla zagadnie« ,r> i ,s>. Despecyfikacja zmiennych (niekonkretyzuj”ca) odpowiada przemianowaniu zmiennych nie zmieniaj”cemu wyprowadzenia (»adne zmienne nie zostaj” uto»samione). Ka»da TGV jest zwi”zana z pewn” meta-zmienn” w t>: ka»da TGV powstaje albo w generalizacji typizowa« dla podstawie« pod meta-zmienn”, albo z podstawienia pod zmienn” niespecyficzn” powstaŖego przy typizowaniu podstawie« pod meta-zmienn”, wtedy jest zwi”zana z t” meta-zmienn”, albo z generalizacji gaŖ¦zi innej TGV, wtedy jest zwi”zana z meta-zmienn” macierzystej TGV. Obierzmy pewn” rekombinacj¦ . B¦dziemy rekonstruowa¢ typizacj¦ dla rekombinanta t)> przez wybieranie tych gaŖ¦zi TGV, które podstawienie ( czy ) zostaŖo wybrane dla meta-zmiennej zwi”zanej z dan” TGV. Wyprowadzenie typu z tak podstawionymi TGV odpowiada wyprowadzeniu typu dla rekombinanta, o ile ono istnieje: cz¦±¢ odpowiadaj”ca t> jest wspólna dla wszystkich rekombinantów, jako cz¦±¢ odpowiadaj”c” meta-zmiennej zostaŖo wybrane pewne wyprowadzenie typu dla tego wŖa±nie podstawienia . Wyprowadzenie typu dla t)> daje si¦ zrekonstruowa¢, poniewa» komunikacja wewn”trz wyprowadzenia nie jest zaburzona: je±li pewne dwa typy s” unifikowane, to zawieraj” TGV albo s” cz¦±ci” gaŖ¦zi TGV zwi”zanych z meta-zmiennymi zale»nymi, czyli zgodnie z warunkami twierdzenia, prowadzi do wybrania odpowiadaj”cych sobie gaŖ¦zi, i na mocy odpowiedniego wyprowadzenia dla albo dla , typy te s” unifikowalne. W zrekonstruowanej typizacji \\(T,T)> poniewa» algorytm (bez despecyfikacji konkretyzuj”cej) zwraca generalizacj¦ podstawie«. Zrekonstruowany typ jest pryncypalny, poniewa» jest wynikiem zwracanym przez algorytm inferencji dla rekombinanta. Despecyfikacja konkretyzuj”ca zachowuje poprawno±¢, poniewa» podstawia pod zmienne typu wolne w typizacji. Krzy»owanie podstawie« silnie zale»nych daje nietypizowalny program, poniewa» w (deterministycznym) przebiegu algorytmu inferencji napotyka si¦ wtedy na niespeŖnialn” unifikacj¦ ró»nych gaŖ¦zi TGV zaczynaj”cych si¦ od staŖych (konstruktorów typu). Zauwa»my, »e algorytm nie uwzgl¦dnia to»samo±ci meta-zmiennych przy ró»nych ich wyst”pieniach w anty-instancji. Dla potrzeb programowania genetycznego wydaje si¦ nawet korzystne ograniczenie generalizacji do termów liniowych ze wzgl¦du na meta-zmienne; jednocze±nie bardzo by to upro±ciŖo algorytm generalizacji. i .> Pod wzgl¦dem syntaktycznym zaprezentowany algorytm jest sŖabszy od tych ze wspomnianych prac przez brak obsŖugi permutacji kontekstu, jednak Ŗatwo go rozszerzy¢, aby tak” obsŖug¦ zapewniaŖ. Natomiast mocniejszy jest od w tym, »e stosuje generalizacj¦ drugiego rz¦du z ``subterm restriction'', czyli ograniczeniem do podtermów generalizowanych termów (i odró»nieniem zmiennych termu od meta-zmiennych generalizacji), a nie ``pattern restriction'', czyli ograniczeniem do podtermów które s” zmiennymi zwi”zanymi (obejmowan” przez ''subterm restriction''). Od mocniejszy jest w tym, »e pozwala na zmienne zwi”zane lokalnie, czyli m.in. na >-abstrakcje w pozycjach argumentowych. Pokazuje to, »e wspomniane algorytmy s” syntaktycznie bliskie algorytmom pierwszego rz¦du; zasadnicz” ró»nic” z syntaktycznego punktu widzenia jest obsŖuga permutacji (tutaj permutacji zmiennych zwi”zanych, kontekstu). Pod wzgl¦dem obsŖugi typów algorytm z paragrafu jest nie do przyj¦cia. Jedynie w przypadku systemów z jawnym polimorfizmem (''explicit polymorphism'') (koduj”cych typy wewn”trz termów), jak te u»yte we wspomnianych pracach, algorytm syntaktyczny mo»e zidentyfikowa¢ typy równowa»ne w ró»nych kontekstach. WŖa±nie dlatego opracowali±my algorytm ``inferencji typu dla anty-instancji'' na wzór systemów z ``ad-hoc polymorphism''. Czy da si¦ ten wynik przenie±¢ na grunt polimorfizmu parametrycznego, pozostaje do zbadania. \; Teraz zajmiemy si¦ algorytmem anty-unifikacji ``prawdziwie'' drugiego rz¦du. .> W tym paragrafie prezentuj¦ definicje i wybrane fakty z rozdziaŖów 5 i 6 pracy Haskera. <\definition> Zbiór generalizacji termów <\eqnarray*> (a,b)>||\:t\a,\:t\b}>>>> Aplikacja podstawienia do generalizacji <\eqnarray*> :\:t\a,\:t\b\\:s\a,\:s\b>|>|(t)=s,\=\\\,\=\\\>>>> Przez \g> oznaczamy fakt \)\:g\g>. <\definition> =MSG(a,b)> jest zbiorem maksymalnie specyficznych generalizacji, je±li <\enumerate> (Soundness:) \\(a,b)> (Completeness:) g\\(a,b))(\g\\) g\g> (Minimality:) g,g\\)g\g\g=g> (Uniqueness:) g\\(a,b)\g\\)\:g\g\\:g\g\\=\> <\definition> Niech (a,b)> b¦dzie podzbiorem (a,b)> takim, »e je±li \:s\a,\:s\b\\(a,b)> i \(s)>, to (f)=\(f)\\(f)=f>. <\definition> Para zmiennych w termie jest przylegŖa (ang. adjacent) je±li zawiera podterm równy . <\definition> Generalizacja \:t\a,\:t\a> jest redundantna, je±li i s” przylegŖymi zmiennymi wolnymi w oraz zachodzi jedno z: (f)\f,\(f)\f,\(g)\g,\(g)\g>. <\definition> \(a,b)>, zbiór skondensowanych generalizacji, to podzbiór (a,b)> nie zawieraj”cy generalizacji redundantnych. Zbiór maksymalnie specyficznych generalizacji skondensowanych, , to zbiór maksymalnie specyficznych generalizacji w \(a,b)>. <\definition> Kiedy \g> w \(a,b)>, to mówimy, »e > jest bardziej ogólna (mniej specyficzna) ni» >, \g>. Oznaczmy przez <\equation*> ,\|t,\,\> reguŖ¦ przeksztaŖcania generalizacji \:t\a,\:t\b> w \:t\a,\:t\b>, gdzie ''mianownik'' jest ±ci±le bardziej specyficzny ni» ''licznik''. <\definition> ›eby policzy¢ zaczynamy z \\\(a,b)> i stosujemy nast. reguŖy, a» »adna nie b¦dzie stosowalna: <\enumerate> (Delete) <\equation*> \{s/f},\\{s/f}|{s/f}(t),\,\> (Merge) <\equation*> \{r/f,r/f},\\{s/f,s/f}|{f/f}(t),\\{r/f},\\{s/f}> (Factor) <\equation*> \{r*K*r/f},\\{s*K*s/f}|{h*K*h/f}(t),\\{r/h,r/h},\\{s/h,s/h}> <\definition> Kombinatory kartezja«skie: <\eqnarray*> p,p=p>|p,p=p>|\r,\r=r!t=!>>>> Mo»na pokaza¢ p,pr=p*r,p*r>. :A\u> posyŖa argument typu do typu ``unit'', tzn. ignoruje argument. Problem dopasowywania (ang. matching) (oraz generalizacji) nie jest dobrze okre±lony dla typów produktowych w ogólno±ci; pod jedn” zmienn” mo»na podstawia¢ coraz bardziej zŖo»one struktury, a pod drug” odpowiednie projekcje pozbywaj”ce si¦ ich. Wybranym ograniczeniem jest ograniczenie typów wynikowych funkcji do typów bez produktów. Ale to nie rozwi”zuje jeszcze problemu okre±lono±ci generalizacji, poniewa» projekcje ci”gle pozwalaj” ignorowa¢ podtermy anty-instancji. Dlatego wprowadza si¦ relewantne kombinatory. Produkt typów i konstruktor pary oznaczamy przez kropk¦, np. (B\C)\(A\B)\C>. <\definition> Restruktorem nazywamy par¦ dwóch wzorców q>, gdzie wzorce skŖadaj” si¦ ze zmiennych >, symbolu specjalnego > oraz operatora binarnego ``>''. Restruktor nazywamy relewantnym, je±li jest liniowe, ozn. , oraz (p)=\(q)>, tzn. ka»da zmienna wyst¦puj”ca w restruktorze pojawia si¦ po prawej stronie. ZakŖadamy nast¦puj”ce równo±ci mi¦dzy termami (po prawej stronie warunki zachodzenia): <\equation*> |\s)(t\t)>||t\st>|>|>||p>|X>>|q>||(p)\\(q)>|(p))>>|q)t>||(q)(r\\(q))>|(p)=t\\(p)=r>>|q)(r\p)>||q>|>|\q)\(p\q)>||\p\q\q>|\p)>>>>> Powy»ej, > jest podstawieniem termów pod zmienne wzorca, a > jest podstawieniem wzorców pod zmienne wzorca. PrzykŖadowa interpretacja reguŖy czwartej: > wyŖuskuje wyniki i (q)> ustawia je we wzorzec , nast¦pnie (q)> porz”dkuje argumenty wedŖug wzorca , »eby je dostarczy¢ (q)>; jest to mo»liwe, bo argumenty rozdzielaj” si¦ wedŖug uszczegóŖowienia wzorca do funkcji atomowych (których typ wynikowy nie jest produktem). Wprowadzamy nast¦puj”ce skróty: <\equation*> |>|>||(q\r)>|>|q)\r>>|>|>||q)\r>|>|(q\r)>>|>|>||>\p>|>|>|>|>|||>|>\p>>|>|>||\>>|>|>|>|>|||>|\>>>|>|>||q>|>|p>>|>|>|||>|p>>>>> <\definition> Niech > b¦dzie zbiorem termów generowanych przez produkcj¦ <\equation*> R:\\\|\\|\\|\\|\\|\\|\\|\\|\\|R*R\|R\R Poniewa» zachodz” równania: <\equation*> ||\\)\(\\\)>||\>|>|\\)\>||\\>>|>>||>>||\>||>>|\>||>||\\)\(\\\)>||\\>>|(\\\)\>||\\)\>||\>||>>|>\>>||>>||>\>>||>>>>>> mamy fakt <\theorem> Dla ka»dego relewantnego restruktora q> istnieje \>, q>. Dopasowywanie (ang. matching) relewantnych kombinatorów jest rozstrzygalne np. przez sprowadzenie do kombinatorów kartezja«skich. <\definition> Zmienne wolne w s” przylegŖe, je±li istnieje podterm w i relewantny restruktor q> taki, »e q)s=f(g\s)> dla pewnego >. Czyli zmienne s” przylegŖe, je±li nie s” rozdzielone przez staŖ”. <\definition> Podstawienie jest przemianowaniem, je±li jest postaci > dla pewnej zmiennej wolnej oraz obustronnie odwracalnego restruktora relewantnego >. <\theorem> Dla staŖej w istniej” takie, »e \)s>. <\definition> Asocjacyjne restruktory, >, to restruktory generowane przez produkcj¦ <\equation*> A:\\\|\\|\\|A*A\|A\A Je±li oznaczymy |\>=s\(s\\(s\s)\)>, to, je±li rozumie¢ ''podterm'' jako ''podterm pierwszego rz¦du'' (czyli np. nie jest podtermem w ): <\theorem> Dla termu i podtermu o wyst”pieniach w , istniej” |\>,\\\,\\\> takie, »e K\(|\>)\\)\>. <\definition> ›eby policzy¢ zaczynamy z \\\(a,b)> i stosujemy nast. reguŖy, a» »adna nie b¦dzie stosowalna: <\enumerate> (Delete) <\equation*> \{s/f},\\{s/f}|{s/f}(t),\,\> (Merge) Dla obustronnie odwracalnego restruktora > <\equation*> \{r/f,r\/f},\\{s/f,s\/f}|{f\/f}(t),\\{r/f},\\{s/f}> (Factor-Constant) <\equation*> \{r(\K\(|\>)\\)\/f},\\{s(\>K\(|\>)\\)\/f}|{h*(K\(|\>)\\)\/f}(t),\\{r(\\\)/h,|\>/|\>},\\{s(\>\\)/h,|\>/|\>}> (Factor-Restructor) <\equation*> \{r\/f},\\{s\/f}|{h\/f}(t),\\{r/h},\\{s/h}> oraz > nie ma lewostronnego elementu odwrotnego. Przedstawimy efektywny algorytm, wedŖug znajduj”cy u»yteczny podzbiór , przy zaŖo»eniach: <\enumerate> Termy i nie zawieraj” zmiennych wolnych. Termy i s” pierwszego rz¦du, tzn. s” kombinatorami typu \X>. Jest pojedynczy typ bazowy >; dane maj” typ \\> a funkcje maj” typ \\\\\\\\>. <\definition> Dla pewnej funkcji i porz”dku na jej przeciwdziedzinie > <\eqnarray*> (a,b)>||MSC(a,b)\(\g\MSC(a,b)) size(g)\size(g)}>>>> Ustalmy funkcj¦ mierz”c” N,N> <\equation*> size(\:t\a,\:t\b)=size(t),size(\)+size(\) gdzie dla termów t <\eqnarray*> |||t=r*s\t=r\s>>||t=p\q\t=\\t>>||>>>>>>>>> i dla podstawie« > <\eqnarray*> )>||Dom(\)>size(\(x))>>>> Dla tej definicji , okre±lmy > jako <\eqnarray*> a,b\c,d>|>|c\(a=c\b\d)>>>> <\definition> Drzewo typizowane to zorientowane drzewo etykietowane takie, »e je±li w¦zeŖ jest symbolem funkcyjnym arno±ci to ma synów. <\definition> Cz¦±ciow” permutacj” z do jest wŖo»enie > z do ,m}> gdzie jest -elementowym podzbiorem ,n}> oraz . <\definition> Typizowane drzewo jest obj¦te (ang. embedded) w t, <\eqnarray*> ,\,s)>|>|,\,t)=t>>>> je±li zachodzi dowolny z nast¦puj”cych warunków: <\enumerate> t,\i\{1,\,n}> s\t\i\{1,\,n}> jest zmienn”, oraz, dla pewnej injekcji > z ,m}> do ,n}>, \t(i)>\i\{1,\,m}>. Je±li drzewo jest puste, to przyjmujemy t> dla dowolnego . Hasker w bŖ¦dnie definiuje punkt 3, zamiast wymaga¢ injekcji pozwala na permutacj¦ cz¦±ciow”. Nie jest wtedy prawd”, »e poni»sze odpowiada dalej zdefiniowanemu zbiorowi > maksymalnych dopasowa«. Rozszerzenie definicji na przypadek drzewa pustego ma charakter techniczny. <\definition> \; <\eqnarray*> ||a,t\b,(\t:t\a\t\b) size(t)\size(t)}>>>> Numerujemy kolejno w¦zŖy drzew u»ywaj”c przej±cia wszerz z indeksem korzenia ustawionym na 1. Je±li w¦zeŖ jest bli»ej korzenia, to ma mniejszy indeks. Indeks w¦zŖa jest oznaczony , a w¦zeŖ (i poddrzewo, kontekst rozró»nia) o indeksie przez . Korze« drzewa oznaczamy odpowiednio . Etykieta w¦zŖa jest oznaczona przez . Niech b¦dzie ilo±ci” w¦zŖów w . Definiujemy macierze i > rozmiaru \| \ \|t\|>: <\definition> Niech synami /i> b¦d” |\>>, a synami /j> b¦d” |\>> (dla 0>), gdzie |\>=u,\,u>. Wtedy > jest zbiorem zawieraj”cym sum¦ rodzin zbiorów <\enumerate> i,index(q)}\|q\|\>}> index(p),j}\|p\|\>}> index(p),index(q(k)>)\|k\Dom(\)}\| \nm}> oraz > jest zbiorem <\eqnarray*> >||i,j,index(p),index(q)\|1\k\n}>|/i)=label(t/j)>>|>|>>>>>>>>> Definiujemy teraz macierze > zawieraj”ce rozmiary maksymalnie obj¦tych drzew otrzymanych z i >. Oznaczmy <\eqnarray*> P>>||p,q\P>M>>>> <\definition> \; <\eqnarray*> >|||= \>>|(N{i,j})>>|>>>>>>>|>||,MP>\|P\N}>>>> Otrzymujemy <\equation*> M=\|t\|t\gentrees(a,b) Stosuj”c memoizacj¦, mo»na efektywnie policzy¢ (jak w metodach programowania dynamicznego) <\code> for i= downto 1 \ \ for j= downto 1 \ \ \ \ compute > and > ›eby znale¹¢ maksymalnie du»e obj¦te drzewa definiujemy <\definition> \; <\eqnarray*> >||N\|M=MP>}\{N\|M=M}>>>> <\definition> Niech N>, wtedy <\eqnarray*> i,j>>||p,q\P{i,j}>matchesp,q>\i,j}>|i,j\P>>|>|>>>>>>>>> Definicja jest niedeterministyczna ze wzgl¦du na wybór . Oznaczamy zbiór wszystkich rozwi”za« przez <\eqnarray*> >||1,1>}>>>> >-abstrakcjami.> Generalizacja drugiego rz¦du w porz”dku danym przez podstawienia wyra»a si¦ w j¦zyku >-termów pierwszego rz¦du: zmienne zwi”zane >-abstrakcji sŖu»” do ``sklejania'' podstawie« z antyinstancj”. (Ogólnie, rz”d generalizacji w porz”dku podstawieniowym jest o 1 wi¦kszy ni» rz”d potrzebnych >-termów.) Dopiero w porz”dku aplikacyjnym (gdzie podstawienia s” realizowane przez >-redukcj¦) rz”d generalizacji jest taki sam jak rz”d >-termów. B¦dziemy si¦ posŖugiwa¢ >-rachunkiem, poniewa» jest wygodniejszy dla manipulacji lokaln” struktur” aplikacyjn” ni» algebra kombinatorów: ''nitki'' Ŗ”cz”ce funkcj¦ i argument mog” by¢ jawnie nazwane; poza tym, jest bardziej naturalny przy traktowaniu termów jako drzew. B¦dziemy u»ywa¢ postaci ``uncurried'', bardziej odpowiedniej w j¦zyku drugiego rz¦du. >-termy u»ywane w generalizacji b¦dziemy uwa»a¢ za ró»ne od wszelkich konstrukcji j¦zyka, którego termy generalizujemy; zbiór zmiennych generalizacji, czyli meta-zmiennych, oznaczmy . Ograniczymy si¦ do relewantnego >-rachunku, tzn. do >-abstrakcji relewantnych. <\definition> >-abstrakcja x,\,x.t> jest relewantna, je±li ,\,x}=\(t)>, gdzie > oznacza wolne meta-zmienne termu. Opracujemy algorytm rekonstrukcji generalizacji z macierzy . Taki algorytm nie byŖ podany bezpo±rednio w pracy Haskera. Zbiory zawarte w > oznaczaj” mo»liwe do podj¦cia w pozycji dopasowania kroki: <\enumerate> DoŖ”cz korze« drugiego termu do konstruowanego podstawienia, caŖy pierwszy term zachowaj dla dalszej generalizacji. DoŖ”cz korze« pierwszego termu do konstruowanego podstawienia, caŖy drugi term zachowaj dla dalszej generalizacji. DoŖ”cz korzenie obu termów do konstruowanego podstawienia, przydziel podtermy, które w dalszym przebiegu b¦d” tworzy¢ argumenty konstruowanego podstawienia (zmiennej). Utwórz anty-instancj¦ z korzeni obu podtermów (o ile maj” wspóln” etykiet¦), konstruuj generalizacj¦ (anty-instancj¦) dla ka»dego argumentu. Algorytm generalizacji (i,j)=Subst(l,r,\,\,V,H,S)> lub (i,j)=AntiInst(g,\,\)>, gdzie to pozycje (indeksy) w generalizowanych programach, lewe (daj”ce i prawe (daj”ce aktualnie konstruowane podstawienia, > wynikowe podstawienia generalizacji, >> zmienne zwi”zane aktualnych podstawie« generalizacji, >> podtermy anty-instancji w kolejno±ci odpowiadaj”cej , pozostaŖe do przetworzenia fragmenty programów (''skrawki''), skonstruowan” anty-instancj¦. Przy generalizacji programów , (i,j,\,\)> zwraca: wybierz I> i w zale»no±ci od kategorii rodzin podzbioróŖw, do której nale»y <\enumerate> i,j},t/j=f(t,\,t),t/j=t>. Aby skróci¢ sformuŖowania, dopuszczamy wsz¦dzie przypadek . <\code> je±li (i,j)=Subst(l,r,\,\,>,>,S)> <\eqnarray*> >||,\,r)>>|>||1\m\n,m\k>>|>||>|>||{t/x\|1\m\n,m\k}>>>> \ \ \ \ zwró¢ ,\,\,>,>,S)> w p.p. (i,j)=AntiInst(g,\,\)> <\eqnarray*> >||,\,r)>>|>||1\m\n,m\k>>|>||>|>>||>.X>>|>>||>.g>>|>||{t/x\|1\m\n,m\k}>>>> \ \ \ \ zwró¢ ,\,\,>,>,S)> > oraz s” nowymi meta-zmiennymi. i,j},s/i=f(s,\,s),s/i=s>. <\code> je±li (i,j)=Subst(l,r,\,\,>,>,S)> <\eqnarray*> >||,\,l)>>|>||1\m\n,m\k>>|>||>|>||{t/x\|1\m\n,m\k}>>>> \ \ \ \ zwró¢ ,r,\,\,>,>,S)> w p.p. (i,j)=AntiInst(g,\,\)> <\eqnarray*> >||,\,l)>>|>||1\m\n,m\k>>|>||>|>>||>.X>>|>>||>.g>>|>||{s/x\|1\m\n,m\k}>>>> \ \ \ \ zwró¢ ,X,\,\,>,>,S)> > oraz s” nowymi meta-zmiennymi. i,j,\,i,j},s/i=f(s,\,s),t/j=g(t,\,t>),s/i=s>,t/j=t(\)>,1\m\k,Dom(\)={\,\,\}> w porz”dku rosn”cym. <\code> >\>,>\>> dla m\k> \ \ \ \ je±li (i,j)=Subst(l,r,\,\,>,>,S)> <\eqnarray*> >>||>>|(\)>>||>>>> \ \ \ \ w p.p. (i,j)=AntiInst(g,\,\)> <\eqnarray*> >>||>>|(\)>>||>>|>>|>|>.X>>|>>|>|>.g>>>> nast¦pnie <\eqnarray*> >||{s/x,t>/y>\|1\m\n,1\m\n,m\Dom(\),m\Ran(\)}>>|>||,1\m\n,m\Dom(\)>>|>||,1\m\n,m\Ran(\)>>|>||,\,l)>>|>||,\,r>)>>|>||m\k>\>>|>||m\k>\>>>> zwró¢ ,r,\,\,>,>,S)> ,y> oraz > s” nowymi meta-zmiennymi. i,j,i,j,\,i,j},s/i=f(s,\,s),t/j=f(t,\,t),s/i=s,t/j=t,1\m\n.> <\code> \\,\\\> dla m\n> \ \ \ \ je±li (i,j)=Subst(l,r,\,\,>,>,S)> <\eqnarray*> (x)>||(>,\>,S(x))x\Dom(S)>>|(x)>||(>,\>,S(x))x\Dom(S)>>|>|>|\\\{\>.S(l)/Z}>>|>|>|\\\{\>.S(r)/Z}>>|>||(>)>>>> \ \ \ \ w p.p. (i,j)=AntiInst(g,\,\)> <\eqnarray*> >||\\>>|>||\\>>|>||>>>> zwró¢ ,\,g),|\>,|\>)> > s” nowymi meta-zmiennymi. ,s/i=c,t/j=d,c\d>, zwró¢ ,\,\,\,\)>. ›eby wyznaczy¢ generalizacj¦ (anty-unifikacj¦) programów : <\code> wyznacz macierze ,M,M,I> je±li (1,1)=Subst(l,r,\,\,>,>,S)> <\eqnarray*> (x)>||(>,\>,S(x))x\Dom(S)>>|(x)>||(>,\>,S(x))x\Dom(S)>>|>||\{\>.S(l)/Z}>>|>||\{\>.S(r)/Z}>>|||(>)>>>> \ \ \ \ zwró¢ ,\> w p. p. (1,1)=AntiInst(g,\,\)> \ \ \ \ zwró¢ ,\> Pozostaje jeszcze zadanie wyznaczenia (>,>,t)>. Maj”c ju» rozwi”zane zadanie maksymalizacji rozmiaru anty-instancji, zajmiemy si¦ minimalizacj” rozmiaru podstawie«. Poniewa» posta¢ anty-instancji determinuje argumenty podstawie«, na ich podstawie trzeba optymalnie ``wykroi¢ skrawki''. Wystarczy przegl”da¢ term od ko«ców (od li±ci), szukaj”c najdŖu»ej pasuj”cego argumentu z >>. Przy odpowiedniej reprezentacji, sprowadza si¦ to do porównywania stringów. Jako wa»ne zadanie pozostaje zbadanie zŖo»ono±ci obliczeniowej powstaŖych algorytmów i ewentualna optymalizacja algorytmu (>,>,t)>. Algorytm (>,>,t)>: <\enumerate> Sprowad¹ i elementy >> do postaci odwrotnej notacji polskiej (ang. RPN): ,>>. Znajd¹ string z >> o maksymalnej dŖugo±ci b¦d”cy odcinkiem pocz”tkowym >. Je±li takiego nie ma, zako«cz (zako«cz wywoŖanie rekurencyjne). (Krok niedeterministyczny.) Zast”p znaleziony odc. pocz”tkowy > w > odpowiedni” zmienn” > z >>. Okre±l odcinek pocz”tkowy > taki, »e > jest argumentem funkcji b¦d”cej ostatnim elementem > (tzn. najmniejszy podterm >, »e > jest jego ±cisŖym podtermem). Je±li taki > istnieje, to wywoŖaj rekurencyjnie od punktu 2 dla >, gdzie =t.s>. Je±li \t> (a je±li > nie istnieje, to je±li \t>), wywoŖaj rekurencyjnie od punktu 2 dla >, gdzie =s.t> (a je±li > nie istnieje, =t.t>). PoskŖadaj odpowiedzi, zast¦puj”ce odpowiednie podtermy > przez zmienne, i zwró¢ tak przeksztaŖcony term. W tym podrozdziale poka»emy, »e efektywny algorytm Haskera nie oblicza >. Podamy te» algorytm obliczaj”cy . Powód, dla którego efektywny algorytm Haskera nie oblicza > jest taki sam, jak powód, dla którego zrezygnowano z kombinatorów kartezja«skich na rzecz relewantnych: »eby wykorzysta¢ t¦ sam” informacj¦ w ró»nych miejscach, stosuj”c algorytm rekursji wzdŖu» struktury termów, trzeba j” skopiowa¢, a nast¦pnie skasowa¢ w niepotrzebnych miejscach. Algorytm Haskera wyklucza kopiowanie, »eby nie byŖo konieczne kasowanie. Dopuszczenie kasowania prowadzi do patologicznych pseudo-generalizacji. Niekiedy mówi”c o drzewie, ma si¦ na my±li nie tylko graf skierowany, ale jeszcze porz”dek okre±lony dla ka»dego w¦zŖa na przylegŖych do niego kraw¦dziach. Tak te» niejawnie przyjmuje Hasker w swojej definicji drzewa typizowanego. Porz”dkiem wyznaczonym przez drzewo typizowane nazwiemy domkni¦cie przechodnie relacji danej przez graf : ,v)>, je±li w¦zeŖ > nale»y do poddrzewa zaczepionego w >. Zbiór w¦zŖów drzewa oznaczmy przez . Niech b¦dzie wyró»nion” etykiet” oznaczaj”c” zmienne. Niech predykat (v)\(label(v)=k\label(v)=V)>. Niech relacja <\equation*> argn(v,v)=(n\outdeg(v))\sub(v,v)\(label(v)\> nale»y do poddrzewa zaczepionego w -tym argumencie w¦zŖa >v) \ (Je±li jest wi¦ksze od arno±ci funkcji )>, to \|argn(v,v)}= \}>). <\definition> Niech {p\|label(p)}>. Struktur” wyznaczon” przez drzewo typizowane nazywamy system relacyjny G,{label\|k}\{sub}\{argn\|1\n\t},\,\> (bez operacji i elementów wyró»nionych; relacje s” obci¦te do zbiorów >). <\definition> Monomorfizmem systemów relacyjnych > i > nazywamy ró»nowarto±ciowy silny homomorfizm, tzn. odwzorowanie |1-1>B> takie, »e (a,\,a)\r(h(a),\,h(a))>. Definicja systemu relacyjnego i monomorfizmu, patrz . ZamysŖem twierdzenia jest wskazanie, »e algorytm z (a wŖa±ciwie mój algorytm, na bazie struktury wyznaczonej przez Haskera) zwraca generalizacj¦, ale nie >. <\theorem> Je±li drzewo typizowane jest obj¦te przez drzewo typizowane , t>, to istnieje monomorfizm ze do , Struct(t)>. Jednak je±li nawet istnieje monomorfizm ze do , to ci”gle mo»e nie zachodzi¢ \t> dla »adnych ,t: Struct(s)=Struct(s),Struct(t)=Struct(t)>. Przypomnijmy definicj¦: Typizowane drzewo jest obj¦te (ang. embedded) w t, <\eqnarray*> ,\,s)>|>|,\,t)=t>>>> je±li zachodzi dowolny z nast¦puj”cych warunków: <\enumerate> t,\i\{1,\,n}> s\t\i\{1,\,n}> jest zmienn”, oraz, dla pewnej injekcji > z ,m}> do ,n}>, \t(i)>\i\{1,\,m}>. <\proof> Cz¦±¢ t\h[Struct(s)]\Struct(t)>. Niech drzewa typizowane speŖniaj” t>. Przeprowad¹my indukcj¦ ze wzgl¦du na rozmiar . Niech b¦dzie li±ciem. Wtedy jest li±ciem, mo»e zachodzi¢ 2. lub 3. punkt definicji obejmowania. Je±li jest zmienn”, to monomorfizm jest trywialny (pusty). W przeciwnym przypadku i wszystkie relacje si¦ pokrywaj”, jest monomorfizmem. Niech teraz ,\,t)=t,n\1>. Je±li zachodzi punkt 1. definicji obejmowania, to monomorfizm mamy z zaŖ. ind. Je±li zachodzi punkt 2., to z zaŖ. ind. mamy monomorfizmów, które skŖadamy razem i dodajemy otrzymuj”c monomorfizm ze w . Wida¢ zgodno±¢ relacji > i , natomiast zgodno±¢ relacji > wynika st”d, »e sparowane s” odpowiednie > oraz >. Je±li zachodzi punkt 3., to z zaŖ. ind. mamy monomorfizmów dla podsystemów )> w (i)>)>. Relacje i > nie zachodz” dla »adnych par z )\)>>,i\j>, ani dla »adnych par z )\)>>,i\j>, a no±nikiem jest suma no±ników )>, wi¦c skŖadaj”c otrzymane monomorfizmów otrzymujemy szukany monomorfizm. Cz¦±¢ t > h[Struct(s)]\Struct(t)>. Niech b¦dzie dany monomorfizm ze w . Przeprowad¹my prób¦ indukcji ze wzgl¦du na liczebno±¢ no±nika . Niech no±nik b¦dzie pusty. Wymusza to, »e no±nik te» jest pusty. Obierzmy jako > drzewo puste, wtedy \t=t>. Je±li no±nik jest pusty, obierzmy jako > drzewo puste, wtedy \t=t>. Niech ,\,s),g(t,\,t)=t>. Je±li nie jest zmienn” oraz , obieramy punkt 2. derywacji i podderywacje obejmowania mieliby±my z zaŖo»enia indukcyjnego: poniewa» jest zgodna z >, wi¦c jest homomorfizmem podsystemów )> w )>. Tez¦ mieliby±my dla =f(s,\,s),g(t,\,t)=t>. Je±li g>, to obieramy punkt 1. derywacji dla odpowiednich poddrzew tak dŖugo, a» zejdziemy do podtermu o korzeniu /1=g=h(f)> (pami¦tamy, »e Struct(t)>). Poniewa» jest zgodna z , wi¦c Struct(t)>, st”d jest monomorfizmem w )> i mo»emy wykorzysta¢ rezultat dany wy»ej (tzn. dla przypadku ) dla uzyskania potrzebnej podderywacji: niech zwrócone drzewa b¦d” ,t>. Tez¦ mieliby±my dla ,[t/t]t>. Je±li jest zmienn”, to mo»emy obra¢ w derywacji relacji obejmowania punkt 1 lub 3. Potrzebujemy tak dobra¢ permutacje, aby pary: minimalna > nale»”ca do no±nika i )> si¦ spotkaŖy. Jednak mo»e Ŗ”czy¢ minimalne > z dowolnie ulokowanymi nieporównywalnymi przez podtermami . Dla przykŖadu, niech b¦dzie zmienn” funkcyjn”: <\eqnarray*> ||>|||>>> Monomorfizm )=a,h(b)=b,h(c)=c>, ale > t>. \; Maksymalne izomorficzne podsystemy to takie, które nie s” podsystemami innych izomorficznych podsystemów. Podobnie mo»na udowodni¢, »e: <\theorem> Zbiory z > wyznaczaj” izomorficzne podsystemy systemów relacyjnych i , dla ustalonych drzew typizowanych i . Jednak nie musz” to by¢ maksymalne podsystemy izomorficzne. Teraz przejd¹my do meritum: We¹my generalizacj¦ programów i . (Niech jej anty-instancja i podstawienia b¦d” w postaci normalnej, tzn. bez restruktorów wewn”trz termów, tylko po prawej.) We wszystkich restruktorach, wyró»nijmy pewne wyst”pienia zmiennych prawej strony tak, aby ka»dy restruktor byŖ liniowy je±li uwzgl¦dnia¢ tylko te wyst”pienia (eliminacja powtórze«). Teraz dokonajmy podstawie« generalizacji i wyró»nijmy te wyst”pienia symboli (w¦zŖy drzewa), które pochodz” od korzenia anty-instancji, albo pochodz” od anty-instancji poprzez zmienn” wyró»nion”. Mo»na zauwa»y¢, »e ka»demu wyst”pieniu symbolu w anty-instancji odpowiada identyfikowalne wyró»nione wyst”pienie symbolu w uzyskanych z podstawienia programach (wyró»niony w¦zeŖ drzewa). To pozwala zbudowa¢ odpowiednio±¢ mi¦dzy wyró»nionymi w¦zŖami i . Nazwijmy j” odpowiednio±ci” przez uliniowienie. <\theorem> Ka»da odpowiednio±¢ przez uliniowienie dana przez generalizacj¦ t,\,\ >jest izomorfizmem odpowiednich podsystemów i . Podsystemy te s” izomorficzne z systemem relacyjnym . Pami¦tamy z definicji, »e zmienne s” usuwane z no±nika . <\proof> Przeprowad¹my indukcj¦ wzgl¦dem struktury anty-instancji. Je±li w korzeniu anty-instancji jest staŖa, to stosuj”c zaŖ. ind. do bezpo±rednich podtermów , i anty-instancji (odpowiadaj”cych sobie, tak, »e > jest zachowana), otrzymujemy tez¦, przyjmuj”c , odpowiednio (a/1)=t/1,h(b/1)=t/1>. (Je±li nie ma podtermów, to teza wynika natychmiast dla , (a/1)=t/1,h(b/1)=t/1>.) Je±li za± w korzeniu anty-instancji jest zmienna, to ustalamy, jakie zmienne restruktorów s” wyró»nione w podstawieniach. Nast¦pnie tworzymy trójki: argument zmiennej w korzeniu anty-instancji, podterm uzyskany z podstawienia tego argumentu pod zmienn” wyró»nion” w podstawieniu daj”cym , podterm tak samo. Stosujemy zaŖo»enie indukcyjne do ka»dej trójki (z tymi samymi podstawieniami generalizacji). Szukany izomorfizm jest zŖo»eniem otrzymanych izomorfizmów, wystarczy pokaza¢, »e s” zgodne. Ale je±li dwa w¦zŖy le»” w dziedzinach ró»nych izomorfizmów, to le»” w rozŖ”cznych podtermach, wi¦c > ani nie zachodzi mi¦dzy nimi; to samo dla dwóch w¦zŖów w obrazach ró»nych izomorfizmów, w szczególno±ci dla obrazów wspomnianych w¦zŖów z dziedzin. St”d zŖo»enie izomorfizmów jest izomorfizmem. (Dotyczy to wszystkich trzech izomorfizmów, równie» tych na , poniewa» nie nale»y do no±nika.) <\theorem> Je±li pewna (dowolna) odpowiednio±¢ przez uliniowienie wyznacza maksymalne izomorficzne podsystemy, to generalizacja jest sprowadzalna do przez co najwy»ej Ŗ”czenie zmiennych (reguŖa Merge). <\proof> Poka»emy, »e do tej generalizacji nie stosuje si¦ »adna, poza (Merge), reguŖa spo±ród tych w definicji , czyli <\enumerate> (Delete) <\equation*> \{s/f},\\{s/f}|{s/f}(t),\,\> (Merge) Dla obustronnie odwracalnego restruktora > <\equation*> \{r/f,r\/f},\\{s/f,s\/f}|{f\/f}(t),\\{r/f},\\{s/f}> (Factor-Constant) <\equation*> \{r(\K\(|\>)\\)\/f},\\{s(\>K\(|\>)\\)\/f}|{h*(K\(|\>)\\)\/f}(t),\\{r(\\\)/h,|\>/|\>},\\{s(\>\\)/h,|\>/|\>}> (Factor-Restructor) <\equation*> \{r\/f},\\{s\/f}|{h\/f}(t),\\{r/h},\\{s/h}> oraz > nie ma lewostronnego elementu odwrotnego. ZaŖó»my, »e do generalizacji stosuje si¦ reguŖa (Delete). We¹my dowoln” odpowiednio±¢ przez uliniowienie. Ustalmy pewne wyst”pienie zmiennej w anty-instancji. Poniewa» podsystemy tej odpowiednio±ci s” izomorficzne ze , wi¦c miejsce w porz”dku odpowiedniego wyst”pienia w drzewach i jest takie samo w obydwu podsystemach. St”d mo»na je rozszerzy¢ dodaj”c odpowiednie wyst”pienia i zachowuj”c wŖasno±¢ izomorfizmu, czyli nie jest on maksymalny. Teraz zaŖó»my, »e do generalizacji stosuje si¦ reguŖa (Merge). Je±li przed jej zastosowaniem »adna inna reguŖa si¦ nie stosuje, to po zastosowaniu (Merge) te» nie b¦dzie si¦ stosowa¢, bo je±li stosuje si¦ do po (Merge), to stosuje si¦ te» do przed (Merge). St”d sprowadzaj”c dowolny generalizator skondensowany do generalizatora , mo»na najpierw stosowa¢ pozostaŖe reguŖy, a gdy »adna si¦ nie b¦dzie stosowa¢, same reguŖy (Merge). ZaŖó»my, »e do generalizacji stosuje si¦ reguŖa (Factor-Constant). Ustalmy wyst”pienie zmienej , podobnie jak w przypadku (Delete). Wybierzmy pierwsze spo±ród wyselekcjonowanych wyst”pie« staŖej z ustalonych pozycji w , podobnie pierwsze spo±ród > wyst”pie« w . Ze wzgl¦du na to, »e staŖa ma tak” sam” struktur¦ argumentów w obu podstawieniach w tych wyst”pieniach, ma dokŖadnie te same elementy ponad ze wzgl¦du na relacje i > w obu podsystemach odpow. z i z izomorficznych ze . Oczywi±cie ma te» te same elementy pod (s” to elementy pod w ); st”d izomorfizm mo»na rozszerzy¢ o odwzorowanie tych wyst”pie« , nie jest wi¦c maksymalny. ZaŖó»my, »e do generalizacji stosuje si¦ reguŖa (Factor-Restructor). ReguŖa ta oznacza, »e pewne argumenty anty-instancji zostan” powielone. Ustalmy dowoln” odpowiednio±¢ przez uliniowienie. Ustalmy jeden z argumentów, który ma by¢ powielony w wyniku reguŖy. Oznacza to, »e w restruktorze ma on co najmniej dwa wyst”pienia po prawej. Wybierzmy po jednym niewyró»nionym wyst”pieniu w ka»dym z podstawie«. Mo»emy teraz rozszerzy¢ izomorfizm, chocia»by odwzorowuj”c korze« podtermu odpowiadaj”cego argumetnowi wybranego podstawienia w tak okre±lony w¦zeŖ . To zachowa izomorfizm, poniewa» odwzorowane w¦zŖy nie maj” niczego ponad w podsystemach do których b¦d” dodane, a pod maj” to, co ``pod zmienn” ''. Powy»sze twierdzenie podpowiada, »e mo»na szuka¢ maksymalnych izomorficznych podsystemów »eby znale¹¢ ; po znalezieniu izomorfizmu rekonstruujemy anty-instancj¦, która b¦dzie liniowa; nast¦pnie Ŗ”czymy zmienne i ``kompresujemy skrawki'' algorytmem >. Jednak dla potrzeb programowania genetycznego, wŖa±nie taka generalizacja, liniowa wzgl¦dem meta-zmiennych generalizacji i >-abstrakcji generalizacji, wydaje si¦ odpowiednia. Mo»liwo±¢ okre±lenia efektywnego algorytmu znajdowania maksymalnej wspólnej podstruktury w ogólnym przypadku zale»y od systemu; nie mo»e by¢ zbyt bogaty w ''niestrukturalny'' sposób. Relacje mog” np. wyznacza¢ jakie± uporz”dkowanie, pozwalaj”ce na zastosowanie programowania dynamicznego, jak tutaj relacja . Okre±lenie generalizacji a nast¦pnie rekombinacji w terminologii podstruktur ma du»e znaczenie dla programowania genetycznego, i szerzej dla syntezy (czy wnioskowania) indukcyjnej i analogicznej. Wiele (by¢ mo»e wi¦kszo±¢) skutecznych zastosowa« GP wykorzystuje struktury bliskie problemowi: struktury grafowe i ``wariacje na ich temat'', np. zastosowania w projektowaniu obwodów elektrycznych filtruj”cych (sukcesy promowane przez Koz¦), anten do telefonów komórkowych, stworze« poruszaj”cych si¦ w ±rodowisku fizycznym (system Framsticks opracowywany na UAM w Poznaniu; GP konstruuje budow¦ fizyczn” stworzenia i budow¦ jego mózgu). Obecnie wykorzystywane w tych systemach operatory rekombinacji najcz¦±ciej dokonuj” przypadkowej wymiany fragmentów reprezentacji. Dla przykŖadu, w systemie Framsticks trzeba sztucznie ograniczy¢ rekombinacj¦ do wymiany wag w sieci neuronowej, aby zapobiec psuciu przez rekombinacj¦ dobrze dostosowanych struktur neuronalnych. Odpowiednio±¢ mi¦dzy generalizacjami a maksymalnymi izomorficznymi podstrukturami (podsystemami) wynika st”d, »e generalizacja to anty-instancja \ o r a z \ podstawienia. Generalizacja b¦d”ca mo»e mie¢ nie najbardziej specyficzn” anty-instancj¦. Oznacza to, »e maksymalne izomorficzne podsystemy \t,s\s,t\t> mog” by¢ parami izomorficzne z izomorficznymi podsystemami \s,t\t,s\s,t\t>, dla których istniej” \t,s\s\s,t\t\t>. Najprostszym sposobem znajdowania maksymalnych izomorficznych podsystemów jest: <\code> := zbiór par pozycji o tych samych etykietach := > dopóki \> \ \ wybierz C> \ \ je±li dla wszystkich ,q)\M> \ \ \ \ )\sub(q,q))\i\ar(p)>argn(p,p)\argn(q,q)> \ \ to := {(p,q)}> \ \ := {(p,q)}> zwró¢ Ma on zŖo»ono±¢ )>, gdzie jest sum” dŖugo±ci generalizowanych termów: najpierw generowanych jest mniej ni» > par, nast¦pnie dla ka»dej z nich dokonywanych jest mniej ni» > sprawdze«. Zalet” tego algorytmu jest, »e mo»na uwzgl¦dni¢ preferencje co do wybieranych par. W przypadku programowania genetycznego mo»na np. preferowa¢ pary pozycji, dla których podejrzewa si¦ \Rto»samo±¢ genealogiczn”'' (pochodzenie od wspólnego przodka). Wprowad¹my oznaczenia: par¦ C> nazywamy Pareto-maksymaln” w je±li <\equation*> \(\(p,q)\C) p\p\q\q\sub(p,p)\sub(q,q) \; Odpowiednio definiuje si¦ par¦ Pareto-minimaln” w . Wprowadzimy teraz wydajniejsze algorytmy. Algorytm, przetwarzaj”cy pozycje od li±ci ku korzeniowi: <\code> := zbiór par pozycji o tych samych etykietach := > dopóki \> \ \ 1: wybierz Pareto-maksymaln” w \ \ 2: := {(p,q)\|sub(p,p)\sub(q,q)}> \ \ 3: := {(p,q)\|(\i) argn(p,p)\argn(q,q)}> \ \ := {(p,q)}> zwró¢ Algorytm przetwarzaj”cy pozycje od korzenia ku li±ciom (odpowiada klasycznym rekurencyjnym sformuŖowaniom generalizacji termów): <\code> przetwórz() = \ \ := > \ \ dopóki \> \ \ \ \ 1: wybierz Pareto-minimaln” w \ \ \ \ dla i=1 do \ \ \ \ \ \ 2: := >przetwórz(,q)\C\| (\i) argn(p,p)\argn(q,q)}>) \ \ \ \ 3: := {(p,q)\|sub(p,p)\sub(q,q)}> \ \ zwró¢ \; := zbiór par pozycji o tych samych etykietach zwró¢ przetwórz() Algorytm od-korzenia-ku-li±ciom Ŗatwo zaimplementowa¢ wydajniej -- ze zŖo»ono±ci” )>. Zbiór mo»na generowa¢ w sposób leniwy z poddrzew s\t>, poniewa» operacje na przynale»no±ci do tego zbioru to 3: usuwanie poddrzew oraz 2: przekazywanie poddrzew do dalszego przetwarzania. Wystarczy opracowa¢ mechanizm wyboru (punkt 1) nie przetwarzaj”cy par wielokrotnie. Mo»na to zrobi¢ przechowuj”c przetworzone poddrzewa : s> (odpowiednio t>) oraz w pojedynczym kroku dodawa¢ w¦zeŖ do > lub do > i szuka¢ (odpowiednio ) w \T> (odpowiednio w \S>) o tej samej etykiecie; po znalezieniu, zast”pi¢ > w przez poddrzewa powstaŖe przez usuni¦cie z > w¦zŖów od korzenia > do w¦zŖa (odpowiednio dla przypadku ,S,p>). <\theorem> Powy»sze algorytmy generuj” izomorfimy maksymalnych izomorficznych podsystemów. Konstrukcja generalizacji ograniczonych do >, a wi¦c nie tylko maksymalnie specyficznych, ale i najwi¦kszych rozmiarem, jest trudniejsza. Przy przetwarzaniu od-li±ci-ku-korzeniowi mo»emy zastosowa¢ metod¦ programowania dynamicznego: najlepiej dopasowane drzewa maj” te» najlepiej dopasowane poddrzewa. Jednak nale»y uwzgl¦dni¢ wszystkie mo»liwe dopasowania powy»ej przetwarzanej pary. Dla zbioru wszystkich par pozycji o takich samych etykietach: <\verse> Gdy wszystkie pary z powy»ej C> zostaŖy ju» ocenione, skonstruuj wszystkie maksymalnie liczne zbiory par Pareto-minimalnych z <\equation*> {(p,q)\C\| (\i) argn(p,p)\argn(q,q)} takich, »e elementy par w konstruowanym zbiorze s” nieporównywalne, oce« zbiory na sum¦ ocen nale»”cych do nich par, oce« na maksimum z ocen skonstruowanych zbiorów plus jeden. Skojarz z par” zbiór, dla którego zachodzi maksimum, na potrzeby rekonstrukcji izomorfizmu. Niestety, nawet przy wydajnej implementacji algorytm oparty na powy»szej regule b¦dzie miaŖ du»” zŖo»ono±¢ obliczeniow”. Pozostaje mie¢ nadziej¦, »e w praktycznych przypadkach zbiory par Pareto-minimalnych z ,q)\C\| (\i) argn(p,p)\argn(q,q)}> dla danych nie b¦d” bardzo liczne. >-termy z definicjami lokalnymi i rekurencyjnymi.>\ Anty-unifikacja z poprzednich podrozdziaŖŖów bezpo±rednio przenosi si¦ na przypadek definicji lokalnych, poniewa» w reprezentacji grafowej wyznaczaj” one ci”gle relacj¦ porz”dku. Natomiast zastosowanie do definicji rekurencyjnych wymaga dalszych bada«, ale wi”»e si¦ z prowadzonymi przez innych badaniami nad indukcj” funkcji rekurencyjnych. Opracowanie algorytmu z obsŖug” zmiennych zwi”zanych w j¦zyku (w przeciwie«stwie do meta-zmiennych) na wzór potraktowania ich w pierwszym podrozdziale, oraz opracowanie rekombinacji zgodnej z systemem typów, to zadanie na blisk” przyszŖo±¢. Postawione zadanie: Perspektywy programowania genetycznego w j¦zykach typizowanych -- postanowiŖem rozpatrze¢ od strony teoretycznej, umieszczaj”c zagadnienia GP w nowym dla nich kontekscie syntezy dedukcyjnej i indukcyjnej programów. We wprowadzeniu przedstawiŖem tematyk¦ pracy, jej cele, oraz szerszy kontekst, w tym zwi”zki z teori” ewolucji darwinowskiej (poj¦cie genu jako jednostki selekcji). W pierwszej cz¦±ci pracy (rozdziaŖ ) zajmowaŖem si¦ zagadnieniami syntezy dedukcyjnej. WskazaŖem na zwi”zek syntezy dedukcyjnej z inferencj” typów i postawione jej wyzwanie: inferowa¢ peŖn” specyfikacj¦ logiczn” konstruowanego programu. OpracowaŖem algorytmy generowania programów dla j¦zyka ML (system typów Damasa-Milnera) o charakterze teoretycznym, z peŖnymi dowodami poprawno±ci (>j¦zyk>) i peŖno±ci (>algorytm>). Algorytmy te uwypuklaj” analogi¦ generowania termów i inferencji typów. PrzedstawiŖem system typów > kontroluj”cy rekurencj¦ (zapewniaj”cy wŖasno±¢ stopu), razem z algorytmem generowania programów. WskazaŖem na praktyczny mechanizm generowania termów: metod¦ rezolucji. WskazaŖem na najodpowiedniejszego moim zdaniem kandydata na j¦zyk dla programowania genetycznego: j¦zyk , przy czym uproszczony przez rezygnacj¦ z peŖnego dopasowywania wzorca. PodaŖem proste sformuŖowanie ``podatnego'' na metod¦ rezolucji j¦zyka pozwalaj”cego na kodowanie specyfikacji wyra»alnych mechanizmem unifikacji. WspomniaŖem tak»e o bardzo istotnym zagadnieniu maksymalizacji ``code reuse'' poprzez elastyczne mechanizmy wprowadzania definicji lokalnych. W drugiej cz¦±ci pracy (rozdziaŖ ) zaj”Ŗem si¦ kluczowym zagadnieniem syntezy indukcyjnej: generalizacj”. Generalizacja ma szerokie zastosowania, natomiast zastosowanie jej, w postaci anty-unifikacji, jako techniki rekombinacji w programowaniu genetycznym jest nowatorskie. W usytuowaniu szeroko rozumianych algorytmów genetycznych u»ywano (w pewnym sensie) generalizacji dla rekombinacji, w postaci rekombinacji zachowuj”cej maksymalne wspólne schematy. W kontekscie zŖo»onych systemów typów zagadnienie znalezienia swego rodzaju homomorfizmu typizowa«, pozwalaj”cego wymienia¢ fragmenty programów, jest trudnym zadaniem. Nie wydaje si¦ rozs”dne po±wi¦ca¢ energii na poszukiwanie homomorfizmu typizowa« dla czego± tak przypadkowego jak rekombinacja swobodna; anty-unifikacja proponuje bardziej rozs”dne pozycje dla rekombinacji. OpracowaŖem syntaktyczny algorytm anty-unifikacji obsŖuguj”cy wi”zania zmiennych (kontekst); jest on syntaktycznie mocniejszy (po prostej modyfikacji dodaj”cej permutacj¦ kontekstu) od pozostaŖych przytoczonych podej±¢ do anty-unifikacji, ale dziaŖa w j¦zyku nietypizowanym. Aby zastosowa¢ ten algorytm dla rekombinacji termów typizowanych (ale bez annotacji typami w termach) opracowaŖem algorytm inferencji typów daj”cy typizacj¦ dla ka»dego poprawnego dziecka danej pary rodziców, okre±laj”cy, które dzieci s” poprawnie typizowane. Z my±l” o przyszŖych zastosowaniach do rekombinacji programów bogato wykorzystuj”cych definicje lokalne, zaj”Ŗem si¦ peŖn” syntaktyczn” unifikacj” drugiego rz¦du. Znakomite sformuŖowanie generalizacji w j¦zyku kombinatorów zawiera praca Haskera. Praca nie zawiera bezpo±redniego sformuŖowania algorytmu znajduj”cego generalizacje, który dostarczyŖem dla opracowanego tam praktycznego algorytmu konstrukcji anty-instancji. PokazaŖem, »e opracowany w tezie Haskera algorytm praktyczny nie jest tak mocny, jak si¦ tam stwierdza: nie daje anty-instancji dla maksymalnie specyficznych generalizacji. ZnalazŖem obrazowe podej±cie do zagadnienia anty-unifikacji drugiego rz¦du, które uogólnia si¦ na dowolne systemy relacyjne: zadanie znajdowania maksymalnych izomorficznych podstruktur generalizowanych struktur. ZaproponowaŖem algorytm rozwi”zuj”cy to zadanie oraz przedstawiŖem problem maksymalizacji rozmiaru szukanych podstruktur, odpowiadaj”cy problemowi znajdowania > z rozdziaŖu 6 pracy . Przeprowadzone badania wskazaŖy kilka problemów, które trzeba b”d¹ warto rozwi”za¢, nim przyst”pi si¦ do implementacji systemu programowania genetycznego opartego o systemy typów bardziej zŖo»one ni» system Curry'ego-Hindley'a (patrz ). Pierwszym obszernym zadaniem jest stworzenie systemu GP optymalizuj”cego ``code reuse''; jest ono ±ci±le zwi”zane z wynikŖym problemem (raczej technicznym), inferencji najogólniejszego typu jednocze±nie z typem konkretyzuj”cym zadany. Drugim zadaniem jest peŖna inferencja typu dla poprzez wykorzystanie mechanizmów inferencji typu dla rekurencji polimorficznej. Na bazie inferencji typu nale»y skonstruowa¢ algorytm generuj”cy programy . Trzecim zadaniem jest zbadanie zŖo»ono±ci obliczeniowej problemu znajdowania generalizacji z >. Czwartym zadaniem jest dokonanie dla peŖnej anty-unifikacji drugiego rz¦du tego, czego podrozdziaŖ dokonuje dla anty-unifikacji pierwszego rz¦du: wprowadzenie obsŖugi zmiennych zwi”zanych, opracowanie algorytmu inferencji typu dla rekombinantów. Pozostaje do zbadania szeroka klasa dziedzin zwi”zanych z generowaniem termów: teorii rezolucji i programowania w logice, programowania wi¦zów, poszukiwania dowodów i interaktywnego dowodzenia, dla spo»ytkowania w teorii programowania genetycznego. Nie wolno te» zapomina¢, »e teoria jest wst¦pem do praktyki. <\bibliography|bib|plain|/home/luki/praca/biblio.bib> <\bib-list|10> Lee Altenberg. The evolution of evolvability in genetic programming. In , 1994. Tobias Blickle and Lothar Thiele. Genetic programming and redundancy. In J.Hopf, editor, , pages 33--38, Im Stadtwald, Building 44, D-66123 Saarbrücken, Germany, 1994. Max-Planck-Institut für Informatik (MPI-I-94-241). Richard Dawkins. . Proszynski i S-ka, 1996. Patrik D'haeseleer. Context preserving crossover in genetic programming. In , volume1, pages 256--261, Orlando, Florida, USA, 27-29 1994. IEEE Press. Didier Galmiche and DavidJ. Pym. Proof-search in type-theoretic languages: an introduction. , 232(1--2):5--53, 2000. DavidE. Goldberg. . Wydawnictwa Naukowo-Techniczne, Warszawa, 1995. RobertW. Hasker. . PhD thesis, University of Illinois at Urbana-Champaign, 1995. Fritz Henglein. Type inference with polymorphic recursion. , 15(2):253--289, April 1993. MasaamiHagiya JianguoLu, MasateruHarao. Generalization in 2>. In , Sao Paulo, Brazil, July 1998. JohnR. Koza. . MIT Press, 1992. Xavier Leroy. Polymorphic typing of an algorithmic language. Technical report, INRIA, 1992. Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In , pages 74--85, Amsterdam, The Netherlands, 1991. NicolasJ. Radcliffe. The algebra of genetic algorithms. Technical Report TR92-11, Edinburgh Parallel Computing Centre, University of Edinburgh, 1992. DaisukeNagano SachioHirokawa. Long normal form proof search and counter-model generation. , 37:1--11, 2001. Ute Schmid. . Springer, 2003. V.Simonet and F.Pottier. Constraint-based type inference for guarded algebraic data types. Research Report 5462, INRIA, January 2005. Hongwei Xi. Dependent types for program termination verification. In , pages 169--180, Florence, September 2001. GwoingTina Yu. . PhD thesis, University College, London, Gower Street, London, WC1E 6BT, 1999. PawelZbierski ZofiaAdamowicz. . Panstwowe Wydawnictwo Naukowe, Warszawa, 1991. <\initial> <\collection> <\references> <\collection> > > > > > > > |3>> > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > <\auxiliary> <\collection> <\associate|bib> pfenning91unification lu-generalization hasker95 goldberg koza92 dawkins altenberg94evolvability ute-inductive galmiche00proofsearch nilsson95prolog nagano-proof hasker95 pfenning91unification hasker95 lu-generalization radcliffe92algebra dhaeseleer94context blickle94genetic radcliffe92algebra hasker95 simonet03constraintbased henglein93type tinayu99 barthe-typebased xi01dependent barthe-typebased hasker95 nagano-proof nagano-proof leroy92polymorphic leroy92polymorphic leroy92polymorphic leroy92polymorphic barthe-typebased barthe-typebased barthe-typebased barthe-typebased lu-generalization lu-generalization lu-generalization pfenning91unification hasker95 pfenning91unification lu-generalization pfenning91unification lu-generalization pfenning91unification lu-generalization hasker95 hasker95 hasker95 logikaZbierski hasker95 hasker95 henglein93type <\associate|toc> |math-font-series||Spis tre±ci> |.>>>>|> |math-font-series||1Wprowadzenie> |.>>>>|> 1.1Wst¦p. |.>>>>|> 1.2Zagadnienia. |.>>>>|> |1.2.1GP i geny. |.>>>>|> > |1.2.2Zalety wprowadzenia typizacji: programowanie dedukcyjne. |.>>>>|> > |1.2.3Automatyczne programowanie -- synteza programów: synteza dedukcyjna i synteza indukcyjna. |.>>>>|> > |1.2.4Operatory genetyczne i generowanie termów. |.>>>>|> > |1.2.5Generowanie termów i ``answer substitution''. |.>>>>|> > |1.2.6Zacie±nianie odpowiednio±ci mi¦dzy ci”giem wyborów a poprawnie typowanymi termami; przeszukiwanie. |.>>>>|> > |1.2.6.1Generowanie termów jako przeszukiwanie przestrzeni programów. |.>>>>|> > |1.2.6.2O potrzebie inferencji typu. |.>>>>|> > |1.2.6.3Algorytm ``head-driven''. |.>>>>|> > |1.2.6.4Rozstrzygalno±¢ problemu niepusto±ci typu w ML. |.>>>>|> > |1.2.7Definicje rekurencyjne i definicje lokalne. |.>>>>|> > |1.2.8Rekombinacja i homomorfizm typizowa«. |.>>>>|> > |1.2.9Rekombinacja przez anty-unifikacj¦. |.>>>>|> > |1.2.9.1Generalizacja i GP. |.>>>>|> > |1.2.9.2Rekombinacja zgodna z mutacj” i anty-unifikacja drugiego rz¦du. |.>>>>|> > |1.2.10Systemy typów z wi¦zami. |.>>>>|> > |1.2.10.1Nierozstrzygalno±¢ inferencji typu dla rekurencji polimorficznej. |.>>>>|> > |1.2.10.2WŖasno±¢ stopu zapewniona przez system typów. |.>>>>|> > |1.2.11Dalej w pracy. |.>>>>|> > |1.2.11.1RozdziaŖ 2 -- Generowanie termów. |.>>>>|> > |1.2.11.2RozdziaŖ 3 -- Generalizacja. |.>>>>|> > |1.2.11.3RozdziaŖ 4 -- Zako«czenie. |.>>>>|> > |math-font-series||2Generowanie termów.> |.>>>>|> 2.1System typów prostych a intuicjonistyczny rachunek zda«. |.>>>>|> |2.1.1System dedukcji naturalnej i typizowany |\>-rachunek. |.>>>>|> > |System dedukcji naturalnej. |.>>>>|> > |Przypisanie typu do |\>-termu. |.>>>>|> > |Izomorfizm Curry'ego-Howarda. |.>>>>|> > |2.1.2Dowody w postaci normalnej. |.>>>>|> > |Beta redukcja. |.>>>>|> > |Twierdzenie o normalizacji. |.>>>>|> > |2.1.3Poszukiwanie dowodów. |.>>>>|> > |Rachunek sekwentów |N J>>. |.>>>>|> > |Drzewo dedukcyjne. |.>>>>|> > |2.1.4Algorytm generuj”cy |\>-termy. |.>>>>|> > 2.2System Damasa-Milnera: inferencja typu i generowanie termu. |.>>>>|> |2.2.1Algorytm inferencji typu |\> i algorytm generowania termu |\>. |.>>>>|> > |2.2.1.1Poprawno±¢. |.>>>>|> > |2.2.1.2PeŖno±¢. |.>>>>|> > |2.2.2Rozszerzenie j¦zyka o konstrukcj¦ |case>. |.>>>>|> > |2.2.2.1Poprawno±¢ z |case>. |.>>>>|> > |2.2.2.2PeŖno±¢ z |case>. |.>>>>|> > |2.2.2.3Zagadnienia praktyczne: CASE sterowane u»yciem. |.>>>>|> > 2.3Monotoniczno±¢ i wŖasno±¢ stopu. |.>>>>|> |2.3.1System typów i algorytm |\>. |.>>>>|> > |2.3.1.1Unifikacja z podtypowaniem |\>>. |.>>>>|> > 2.4Generowanie: mechanizmy do zastosowania. |.>>>>|> |2.4.1System typów z typami indukcyjnymi z wi¦zami unifikacyjnymi. |.>>>>|> > |2.4.1.1Generowanie |\>-dŖugich |\>-normalnych polimorficznych |\>-termów: Prolog. |.>>>>|> > |2.4.1.2W stron¦ peŖnego |HMG(X)>. |.>>>>|> > |2.4.2Programy bez nieu»ytecznych definicji lokalnych. |.>>>>|> > |math-font-series||3Rekombinacja i generalizacja> |.>>>>|> 3.1Rekombinacja swobodna. |.>>>>|> 3.2Anty-unifikacja drugiego rz¦du -- prosty przypadek. |.>>>>|> |3.2.1Definicja. |.>>>>|> > |3.2.2WŖasno±¢: maksymalnie specyficzna generalizacja. |.>>>>|> > |3.2.3Zgodno±¢ rekombinacji z systemem typów. |.>>>>|> > |3.2.4Zwi”zek z algorytmami z prac [] i []. |.>>>>|> > 3.3Generalizacja drugiego rz¦du i ogólne struktury. |.>>>>|> |3.3.1Generalizacje rekombinatorowe z pracy []. |.>>>>|> > |3.3.1.1Definicje ogólne i algorytm dla termów monadycznych. |.>>>>|> > |3.3.1.2Relewantne kombinatory i algorytm dla termów poliadycznych. |.>>>>|> > |3.3.1.3Praktyczny algorytm uwzgl¦dniaj”cy rozmiar generalizacji. |.>>>>|> > |3.3.2Algorytm rekonstrukcji generalizacji z relewantnymi |\>-abstrakcjami. |.>>>>|> > |3.3.3Generalizacja przez znajdowanie maksymalnych wspólnych podstruktur. |.>>>>|> > |Zagadnienia praktyczne. |.>>>>|> > |Uwaga natury teoretycznej. |.>>>>|> > |3.3.3.1Znajdowanie maksymalnych izomorficznych podsystemów. |.>>>>|> > |3.3.3.2Rozszerzanie generalizacji na |\>-termy z definicjami lokalnymi i rekurencyjnymi. |.>>>>|> > |3.3.3.3Zgodno±¢ z systemem typów. |.>>>>|> > |math-font-series||4Zako«czenie> |.>>>>|> 4.1WkŖad pracy. |.>>>>|> 4.2Postawione zadania. |.>>>>|> |math-font-series||Bibliografia> |.>>>>|>