Dotaz: Teorie programovani a "derivace funkce"

[JS]

Ahoj,

ucim se ted trochu Haskell, protoze me napadla urcita teoreticka idea/koncepce v programovani, a rad bych se dozvedel, jestli uz neco takoveho neexistuje (a pod jakym nazvem to hledat). Rikam si, ze prave komunita lidi kolem Haskellu a funkcionalniho programovani by mohla znat odpoved, protoze jsou to vetsinou velice zdatni teoretici. Proto se ptam tady, protoze vim, ze se tady hodne takovych lidi pohybuje.

Ve funkcionalnim programovani (a la Haskell) mame jen ciste funkce. Tedy realny program (na realnem pocitaci) lze chapat jako jeden velky stavovy automat, nad kterym je jedna cista funkce, ktera vstup a vnitrni stav prevadi do vystupu a noveho vnitrniho stavu.

V praxi to tak ovsem nedelame, protoze by to bylo neefektivni. V praxi je totiz casta situace, ze ten vnitrni stav se tou operaci zmeni jen pomerne malo, nebo jen jeho cast; a provadeni vypoctu timto zpusobem by znamenalo, ze se pro vystup prepocitavaji i veci, ktere uz jsme vypocitali v minulem stavovem prechodu. V praxi se to resi imperativnim programovanim, ktere uklada ruzne mezivysledky.

Zajimalo me tedy, jestli existuje nejaky systematictejsi postup, jak by bylo mozne z onoho popisu "cista funkce nad globalnim stavem" odvodit, ktere veci uz neni potreba prepocitavat. Tim by bylo mozne definovat program vyse uvedenym zpusobem (jako funkci pro stavovy automat), coz je velmi elegantni, a pozdeji ho prevest na "imperativni" model, a neprijit tak o tu efektivitu. V podstate, velice neformalne, to znamena tu funkci "zderivovat", tedy najit funkci, ktera mi pro zmenu vstupu vrati zmenu na vystupu.

Jenze, co to vlastne znamena, "zmena" nejake veliciny, v tomto pripade? Obecne to zavisi od situace. Ale muzeme zkusit jednoduche pripady, a podivat se, jak bychom to tam asi chteli mit. Vezmeme si napriklad klasickou trojici funkci map/filter/reduce, ktere operuji nad posloupnostmi a ktere lze povazovat za urcite stavebni prvky, z kterych lze poskladat tu velkou prechodovou funkci, kterou chceme timto zpusobem optimalizovat.

Vsechny tri map/filter/reduce pracuji s argumentem posloupnosti. "Zmenou" v tomto pripade tedy muze byt pridani/ubrani/zmena jednoho prvku. U map i filter je derivace pomerne primocara - prepocita se jeden prvek. U reduce je zajimave, pokud je redukcni operace grupova, pak staci prepocitat take v podstate jen jeden prvek.

No a tohle me na tom zaujalo, a proto se tady na to ptam. Nikdy predtim jsem si neuvedomil, ze by optimalizace mohly zaviset na tom, jestli je neco grupa nebo ne (napriklad cloveka okamzite napada otazka - bylo by mozne to priohnout tak, aby funkce v reduce grupova byla?). Zni to zajimave, takze, chtel jsem se zeptat, rozviji uz nekdo takovou teorii? A souvisi to cele nejak s linym vyhodnocovanim?

Odpovědi

[l4m4]

Ve funkcionalnim programovani (a la Haskell) mame jen ciste funkce. Tedy realny program (na realnem pocitaci) lze chapat jako jeden velky stavovy automat, nad kterym je jedna cista funkce, ktera vstup a vnitrni stav prevadi do vystupu a noveho vnitrniho stavu.

Tady jsem se ztratil.

I když fyzicky nakonec program v Haskellu provádí CPU, na který se lze dívat jako na stavový automat, tak ten program není formulován jako nějaký převod jednoho stavu do jiného, ale jako výpočet (představitelný prostě jako dosazování vzorců do jiných vzorců).

[JS]

Aha, asi jsem se blbe vyjadril. Ono totiz plati tak nejak oboji. Dejme tomu, ze bych chtel v Haskellu napsat treba hru (nerikam, ze chci, je to hypoteticke). Pak v te hre je nejaky stav sveta, a ten se meni na zaklade nejake funkce (ktera popisuje chovani toho sveta, reakci na vstup a jeho zobrazeni). Takze jedna zmena toho stavu, jedna reakce na vstup hrace, a vykresleni vystupu, je pak vypoctem te funkce.

Jenze problem je, ze ja nechci udelat jeden vypocet, ale serii vypoctu. Takze otazka je, jestli nejak nemohu vyuzit vlastnosti te funkce, abych z nich odvodil funkci, ktera provede jen dilci vypocet na zaklade znalosti predchoziho stavu.

[VM]

Ano, pokud mám v počítači v paměti a na disku dohromady n bitů, tak program můžu chápat jako funkci z 2^n stavů do 2^n stavů. V praxi se některé jednoduché úlohy opravdu řeší tabulkami, kde mám výstupní hodnoty pro všechny možné vstupní hodnoty. Údajně si takhle pomáhají třeba matematické koprocesory pro výpočet goniometrických funkcí. Pro většinu reálných výpočtů je ale těch 2^n stavů moc, a to i když je omezím na nějaké malé n vstupních bitů, takže se to počítá klasicky.

[JS]

O to mi nejde, to je jasne. Me prave jde o to brat to jako klasicky vypocet po celou dobu, akorat si myslim, ze je jednodussi ho reprezentovat jako jednu velkou operaci nad jednim velkym stavem, a taky nad tim tak uvazovat, nez spousta mensich operaci nad mensimi stavy.

[pc]

nevim jestli spravne chapu vas dotaz, nejsem ani teroretik programovani, ale pro "derivaci" resp. uchovani urciteho stavu vypoctu pro optimalizaci opakovaneho volani se provadi technika tzv. memoization (nevim jak prelozit).v jazycich ktere podporuji uzavery (closures) se to da implicitne resit kompozici functoru.

pokud je jazyk jako haskell referencne transparentni (u vsech funkci krome IO), tj. je zajisteno ze hodnota funkce je pro jedny parametry vzdy stejna, muzou se takove optimalizace provadet i na urovni prekladace, ale nevim jestli to nejake konkretni implementace provadi.

btw. jestli chcete fundovanou odpoved, tak polozte otazku na stackoverflow.com. tam je daleko vetsi sance, ze ji dostanete.

[JS]

Jasne, memoization je znama technika. Ale ja vidim sanci jit trochu dal - memoization se neda (prakticky) delat na slozitejsich datovych strukturach. Dalo by se to castecne povazovat za specialni pripad toho, o cem mluvim - vy vite, ze se predchozi hodnota nezmenila, a tak automaticky znate vysledek volane funkce. To co chci ja je efektivne prepocitat "nenulovou" zmenu.

No, ja nevim, jestli je to vhodna otazka pro Stackoverflow, a vlastne je to spis takovy neformalni pruzkum. Prave jsem trochu doufal, ze se tady najde par lidi, kteri budou vedet, na co me odkazat.

[pc]

asi mam maly obzor, ale nedokazu si predstavit jak jinak nez "ukladanim" mezivysledku a jeho naslednym pouzitim pri opakovanem volani by slo toto dosahnout. rozdil bude asi jen v tom, jak komplikovane/skryte se tohle resi v tom kterem jazyce. v haskellu a zrejme i dalsich funkcionalnich jazycich to jde o poznani snadneji. pokud se zapise funkce bez volnych promennych, tj. ve vyrazu se vyskytuji jen parametry predane nejblizsi vnejsi lambde (tzv. konstantni aplikativni forma), tak vypocet takove funkce probehne jen jednou i pri opakovanem volani a dosahne se tak "automaticke" memoizace. a je jedno o jake datove struktury se bude jednat, jestli o proste numericke typy nebo treba binarni stromy.

nektere numericke algoritmy by treba (bez memoizace) dokazaly odvodit napr. vyraz pro vypocet n-teho clenu fibonacciho posloupnosti s O(1), ale u obecne funkce si takovou redukci nedokazu predstavit.

[karel_iv]

vyraz pro vypocet n-teho clenu fibonacciho posloupnosti s O(1), ale u obecne funkce si takovou redukci nedokazu predstavit.

To jde? Sám to umím v O(log n) pomocí mocnění matic (viz anglická wiki).

PS nerýpu, jen se ptám.

[pc]

binetova veta ? ale samozrejme s urcitou mirou presnosti.
F(n) = (1-φ)ⁿ / √5

[Michal Kubeček]

Na to si nepotřebujete hrát s maticemi, na to stačí ten vzoreček pro F_{m+n}, který odvodíte buď indukcí nebo z toho, že F_n je počet způsobů, jak poskládat úsečku délky n z úseček délek 1 a 2.

Konstantní složitost má v jistém smyslu ten explicitní vzoreček, který máte v odkazovaném článku také, ale to předpokládá, že s konstantní složitostí umocníte reálné číslo s dostatečnou přesností, což v praktické implementaci nedokážete.

[l4m4]

V praktické implementaci bude explicitní vzoreček mít asymptotickou složitost O(n log(n)²) (tj. násobení pomocí FFT). Hraní si s maticemi v optimální variantě asi O(n log(n)³), ale muselo by se to odvodit...

[JS]

To co chci je neco jineho nez memoizace. Vezmi si jako priklad funkci ktera pro zadanou posloupnost prvku vrati jejich soucet. Kdyz se zmeni jeden prvek posloupnosti, je potreba znovu secist celou tu posloupnost. Memoizace nepomuze, protoze ta by si pamatovala ruzne soucty ruznych posloupnosti. Ale pokud vim, ze scitani je grupova operace, mohu odvodit funkci, ktera na zaklade toho, ze se zmenil jeden prvek a jak, a na zaklade znalosti predchoziho vysledku, dokaze odvodit vysledek novy. Tato nova funkce je "necim podobnym derivaci" od te puvodni funkce. Pouzit tuto novou funkci je efektivnejsi nez prepocitavat znova celou posloupnost.

Takze, memoizace je OK, ale jakmile zacnes predavat jako parametry slozitejsi datove struktury, narazi to. A to je prave problem, ktery se snazim resit. Mozna naivne a neumele - a proto se na to ptam, jestli uz nekdo uvazoval timto smerem.

[pc]

dik za doplneni, ale myslim ze jsem to pochopil uz pred tim.

to co hledas by ale imho vyzadovalo specialni typovou tridu, ktera by pro prekladac indikovala ze to zobrazeni je grupova operace a podle toho by s ni taky zachazel. tohle ale standardni typovy system haskellu afaik neobsahuje, nevim jak je to jinde. lze urcite definovat vlastni datove typy a operace nad nimi, ktere by vyhovovaly podminkam pro grupovou algebru, ale tady se asi bavime o obecne metode, ktera by z libovolne funkce vytvorila funkci vyssiho radu, ktera by optimalizovala vypocet vyuzitim grupove algebry. v implementaci by ale stejne pak musela byt nejaka forma memoizingu, protoze tu "konecnou" mnozinu hodnot proste musi vypocitat, i kdyz muze vyuzit vyhody lineho vyhodnocovani. na mnozinach typu cela cisla by to imho ani jinak neslo.

pokud bych se vratil k map, filter, reduce (foldl, foldr v haskellu), tak je podstatne co presne si predstavujes tim doplnenim prvku. pokud se pridanim zachova indukce vypoctu, tak ten puvodni pozadavek lze trivialne splnit uzaverou nebo pro narocnejsi pozadavky nekterou ze stavovych monad. v opacnem pripade plati to co je v predchozim odstavci - bud se definuje cely vlastni typovy system pro grupove operace a bude to fungovat na explicitne resene omezene mnozine nebo pokud by to melo fungovat genericky tak se uz presouvame na uzemi umele inteligence rad se necham vyvest z omylu, pokud tohle uz nejaky jazyk zvlada.

[Goheeca]

Tak nějak to taky vidím, že v obecném případě to bude chtít v základu minimálně nějaký ATP, mě nejblíže je ACL2 (a stejně s ním v podstatě neumím).

[JS]

Aha, diky za odpoved. Ja ani nejak necekam, ze bude existovat obecne reseni - to je asi algoritmicky neresitelny problem, ale spis neco, co pokryje velkou cast pripadu.

[Radek Miček]

bylo by mozne to priohnout tak, aby funkce v reduce grupova byla?

Typový systém Haskellu je příliš slabý na to, aby tuto vlastnost vyjádřil. Existují programovací jazyky, kde to možné je. Mj. v Haskellu lze využít invarianty funkcí (např. map f . map g == map (f . g)) v přepisovacích pravidlech pro optimalizaci.

[JS]

Muzes byt konkretnejsi?

[Radek Miček]

Typový systém Haskellu je příliš slabý na to, aby tuto vlastnost vyjádřil.

Předpokládejme, že máme reduce : (a -> a -> a) -> List a -> a a chceme zajistit asociativitu prvního parametru (například, aby reduce mohl počítat paralelně). Jednou z možností, jak to udělat, je přidat funkci reduce další parametr, který bude sloužit jako konstruktivní důkaz oné asociativity.

Předně si první parametr pojmenujeme, abychom se na něj mohli odkazovat v dalších parametrech: reduce : (f:(a -> a -> a)) -> List a -> a.

Nyní se zamyslíme, co je konstruktivním důkazem asociativity f?. Je to funkce, jenž pro každé x : a, y : a, z : a vrátí důkaz, že f x (f y z) = f (f x y) z. To jest nový parametr pro reduce bude funkce x:a -> y:a -> z:a -> f x (f y z) = f (f x y) z.

Takže paralelní reduce může mít typ reduce : (f:(a -> a -> a)) -> (x:a -> y:a -> z:a -> f x (f y z) = f (f x y) z) -> List a -> a.

V Haskellu tento postup nebude fungovat minimálně ze dvou důvodů. Hlavním důvodem je fakt, že Haskell neumí vynutit totální funkce (term undefined = undefined je důkazem čehokoliv, neboť má libovolný typ) a má pouze koinduktivní typy. Druhým důvodem je to, že Haskell zatím nedovoluje mít aplikaci funkce f v typu (typ, jenž závisí na termu f).

Existují programovací jazyky, kde to možné je.

Například jazyky Idris nebo Agda 2. Programovat lze též v důkazových asistentech Isabelle a Coq a kód z nich lze pak extrahovat do nějakého normálního funkcionálního jazyka. Další jazyky, kde to pravděpodobně je možné, jsou v tabulce v článku o závislých typech.

Mj. v Haskellu lze využít invarianty funkcí (např. map f . map g == map (f . g)) v přepisovacích pravidlech pro optimalizaci.

Mám na mysli přepisovací pravidla v GHC. Používá se to v knihovnách Haskellu a hezkou aplikací je článek Stream Fusion. From Lists to Streams to Nothing at All.

[JS]

Ah, diky za odpoved. Bude mi chvili trvat, nez to vstrebam.

[JS]

Tak jsem si to procetl, a pochopil, tedy v ramci toho, co o FP, logice a Haskellu vim (coz neni moc). Diky za odpoved. Coq jsem se chtel naucit, ale zatim jsem na to nesebral odvahu. Hlavne oni zacnou pak mluvit tim logickym jazykem a i normalnim matematikum (a uz nejsem ani to) je to ponekud vzdalenejsi.

Ta prepisovaci pravidla vypadaji zajimave (a i ten zmineny clanek, akorat nejde stahnout), a zda se, ze by to byl zpusob, jak to implementovat.

Jenom moc nechapu, je opravdu nutne nejak deklarovat pro ta prepisovaci pravidla tu asociativitu (a tedy mit typovy system takto silny), nebylo by mozne to proste rict, ze ta konkretni funkce vstupujici do toho reduce je asociativni (treba soucet)? Nedalo by se to prece jen nejak obejit?

[Radek Miček]

Coq jsem se chtel naucit, ale zatim jsem na to nesebral odvahu.

Až se odhodláte, tak doporučuji začít se Software Foundations a poté pokračovat Certified Programming with Dependent Types.

ten zmineny clanek, akorat nejde stahnout

Teď jsem to zkoušel a podařilo se to. Možná to chce jen správné načasování.

Jenom moc nechapu, je opravdu nutne nejak deklarovat pro ta prepisovaci pravidla tu asociativitu (a tedy mit typovy system takto silny)

Na přepisovací pravidla v GHC nejsou kladena žádná velká omezení. Je to čistě vaše věc, jestli pravidla zachovají význam programu nebo jestli přepisování vůbec skončí – nic z toho se nekontroluje.

nebylo by mozne to proste rict, ze ta konkretni funkce vstupujici do toho reduce je asociativni (treba soucet)? Nedalo by se to prece jen nejak obejit?

Pokud vám nevadí, že to nekontroluje kompilátor, tak dalo. Nejjednodušší je udělat dvě funkce reduce a reducePar, přičemž ta první není paralelní a nepotřebuje asociativitu, ta druhá je paralelní a potřebuje asociativitu (ale kompilátor o tom nic neví). Nebo mohu vyžadovat, aby datový typ byl instancí typové třídy, jenž má asociativní operaci a používat výhradně onu operaci:

import Data.Monoid

-- Funguje i s prazdnym seznamem, protoze monoid ma neutralni prvek.
reduce :: Monoid a => [a] -> a
reduce = mconcat

A do třetice mohu napsat opět dvě varianty reduce – jednu pro obyčejné binární funkce a druhou pro asociativní (ve skutečnosti ta druhá není pro funkce, ale pro prvky typu Assoc a):

{-# LANGUAGE TypeFamilies, FlexibleInstances #-}

import qualified Debug.Trace as D

class Reduction f where
    type El f
    reduce :: f -> [El f] -> El f

instance Reduction (a -> a -> a) where
    type El (a -> a -> a) = a
    reduce = foldl1 . D.trace "normalni"

newtype Assoc a = Assoc { unassoc :: (a -> a -> a) }

instance Reduction (Assoc a) where
    type El (Assoc a) = a
    reduce = foldl1 . unassoc . D.trace "paralelni"

Když pak v GHCi zavolám reduce (+) [1..5], tak dostanu výstup

normalni
15

a když zavolám reduce (Assoc (+)) [1..5], tak dostanu výstup

paralelni
15

Problém všech třech řešení je v tom, že kompilátor asociativitu nekontroluje, neboť ani neví, že daná funkce má být asociativní. Výhodou silnějších typových systémů je, že asociativitu nebo jinou vlastnost může ověřovat kompilátor.

[JS]

Diky za odkazy a za priklad. Clanek jsem pak nasel jinde.

[JS]

Tak ctu ted trosku o Curry-Howard izomorfismu a pribuznych tematech na Wikipedii a musim rict, ze jedna vec, ktera me na tom celem pristupu trochu trapi, a to je, ze se tam uplne ignoruje vypocetni narocnost. U matematickeho dukazu mi prece nezalezi na tom, jak dlouho vypocet potrva; a v tom ta analogie fatalne kulha. A to je prave trochu to, co se snazim resit (muj pohled je, ze programy maji byt co nejelegantnejsi, ale jen do te miry, dokud nepoklesne vykon), takze ted opravdu nevim, jestli mi v tom smeru funkcionalni programovani pomuze. Mozna je to jen dojem zacatecnika, kazdopadne si rad poslechnu, jestli k tomu mas nejaky komentar.

[Radek Miček]

Tak ctu ted trosku o Curry-Howard izomorfismu a pribuznych tematech na Wikipedii a musim rict, ze jedna vec, ktera me na tom celem pristupu trochu trapi, a to je, ze se tam uplne ignoruje vypocetni narocnost. U matematickeho dukazu mi prece nezalezi na tom, jak dlouho vypocet potrva; a v tom ta analogie fatalne kulha.

Myslíte, že to nějak vadí při programování?

Třeba u příkladu s reduce jsem C-H izomorfismus využil jednou, a to když jsem chtěl, aby f byla asociativní. Místo důkazu asociativity jsem požadoval, aby byl typ x:a -> y:a -> z:a -> f x (f y z) = f (f x y) z obydlený – tj. uživatel musel funkci reduce předat term (funkci) proof typu x:a -> y:a -> z:a -> f x (f y z) = f (f x y) z. Při implementaci reduce však není třeba volat funkci proof, tudíž na její časové složitosti nezáleží a kompilátor ji nemusí vůbec překládat.

[jas]

Nie som si uplne isty, ze som spravne pochopil otazku, ale ak hej, tak ciastocne riesenie existuje. Kompilator moze hladat dostupne vyrazy a nasledne nahradit vypocet podla vypocitaneho zoznamu za premennu, kde je vypocet ulozeny (v skutocnosti je to trocha zlozitejsie, pre detaily ide o problem AVAIL - hladania dostupnych vyrazov pri analyze toku dat, str. 23, zide sa aj uvod - prvych par stran, po problem LIVE).

Co sa tyka uplneho riesenia, tj. v podstate najdenie optimalnej funkcie voci nejakej cenovej funkcii, tak nic take (aspon pre turing-complete jazyky) neexistuje [jednoducha logika - mat podobne riesenie, tak vsetky ostatne optimalizacie by razom stratili zmysel]. Navyse sa obavam, ze na nieco podobne by sa dal spravit aj dokaz (pre zaciatok by mohlo byt problematicke, ze dany optimalizator by mal skoncit aj pri funkciach, ktore nad nejakym vstupom cyklia a detekovat nieco take - problem zastavenia - nie je rekurzivny problem).

Spravnou cestou je v tom pripade az obmedzovanie moznosti (vyjadrovacej sily) programovacich jazykov. Napr. vo forme konecnych automatov je taka optimalizacia mozna a aj jednoducha (viz minimalizacia konecnych automatov).

[JS]

Ano, ja take predpokladal, ze to bude asi obecne neresitelna uloha, a proto jsem k tomu od zacatku pristupoval tak, ze by bylo zajimave zkusit pokryt nejake bezne pripady. Spis nez omezeni vyjadrovaci sily bych to nazval tvorbou novych abstrakci, ktere umozni kompilatoru aplikovat prislusnou optimalizaci (napr. u tech konecnych automatu - pokud neco oznacim za konecny automat, umozni to kompilatoru s tim tak pracovat, a je to jednodussi nez se pokouset rozpoznat, zda je cast programu adaptovatelna na konecny automat nebo ne).

[jas]

Uz som si precital dokladnejsie otazku a hlavne diskusiu a myslienka pouzitia informacii navyse pre kompilator je zaujimava a v podstate sa pouziva uz celkom dlho (napriklad register alebo inline v gcc) aj ked ide prevazne o velmi jednoduche veci. Rozne obmedzenia (tie nove abstrakcie) z ktorych vyplyvaju lepsie vlastnosti systemov sa studuju uz tiez celkom dlho, horsie je to s ich aplikaciou na realne programovacie jazyky (zvacsa sa pouzivaju skor matematicke modely, ktore su relativne vzdialene od bezneho programovania).

Teoreticky by nemuselo byt zlozite nieco podobne pre haskell spravit. Runtime optimalizacie by asi nemali moc zmysel, kedze rezia spojena s optimalizaciou by pravdepodobne bola vyssia nez to, co poskytne optimalizacia. V case kompilacie by to uz zmysel mohlo mat (tu by sa asi skutocne hodil modifikovany AVAIL problem pre vypocet dostupnych vyrazov, z ktorych sa da vychadzat v danom bode programu). Realizacia by tiez nemusela byt velmi obtiazna (na high-level urovni, programovania to bude chciet urcite dost). Technicky by stacilo pridat do gramatiky pre jazyk pravidlo, ktore by umoznovalo pri definicii funkcie davat priznaky (splna asociativitu, ma nulovy prvok 'm' a pod.) a nasledne vyuzivat tieto informacie pre optimalizacii.

Este som nepocul o projekte, ktory by sa nieco podobne snazil spravit, co samozrejme neznamena, ze taky projekt neexistuje. Kazdopadne ako napad to vyzera zaujimavo.

btw: Na programy (vsetky, nie len funkcionalne) sa casto pozera ako na transformatory stavovej funkcie, takze napojenie len na funkcionalne jazyky a pripadne line vyhodnocovanie by som v tomto pripade ako klucove nevidel.