Faktorizace vyčíslitelných funkcí v Hasku

desprit

Faktorizace vyčíslitelných funkcí v Hasku
« kdy: 13. 08. 2017, 19:05:37 »
Dá se dokázat, že každý vyčíslitelný morfismus se dá rozložit na vyčíslitelné komponenty? Nedávno tu zaznělo, že ne, ale nějak se mi to nezdá, jen nevím, jak to formálně dokázat.


Re:Faktorizace vyčíslitelných funkcí v Hasku
« Odpověď #1 kdy: 13. 08. 2017, 19:48:45 »
Dá se dokázat, že každý vyčíslitelný morfismus se dá rozložit na vyčíslitelné komponenty?
Mohl bys mi jako čtyřletýmu dítěti vysvětlit, co tím myslíš? Není mi moc jasný pojem "vyčíslitelný morfismus", ani "rozložit", ani "komponent".

Mám-li f: X -> Y, je f . id "rozložení na komponenty" nebo ne?

Nedávno tu zaznělo, že ne
Kde přesně?

Ivan Nový

Re:Faktorizace vyčíslitelných funkcí v Hasku
« Odpověď #2 kdy: 13. 08. 2017, 20:32:43 »
Dá se dokázat, že každý vyčíslitelný morfismus se dá rozložit na vyčíslitelné komponenty? Nedávno tu zaznělo, že ne, ale nějak se mi to nezdá, jen nevím, jak to formálně dokázat.

Můžete-li provést rozdělení na komponenty, můžete udělat i přiřazení komponentám indexy z množiny přirozených čísel, a dle Godelových vět o neúplnosti vždy může existovat sentence, která není v rámci přirozených čísel dokazatelná ani vyvratitelná.

Re:Faktorizace vyčíslitelných funkcí v Hasku
« Odpověď #3 kdy: 13. 08. 2017, 20:45:02 »
Můžete-li provést rozdělení na komponenty, můžete udělat i přiřazení komponentám indexy z množiny přirozených čísel, a dle Godelových vět o neúplnosti vždy může existovat sentence, která není v rámci přirozených čísel dokazatelná ani vyvratitelná.
To je teda hodně divný vysvětlení :))

zboj

  • *****
  • 1 507
    • Zobrazit profil
    • E-mail
Re:Faktorizace vyčíslitelných funkcí v Hasku
« Odpověď #4 kdy: 13. 08. 2017, 21:14:09 »
Dá se dokázat, že každý vyčíslitelný morfismus se dá rozložit na vyčíslitelné komponenty?
Mohl bys mi jako čtyřletýmu dítěti vysvětlit, co tím myslíš? Není mi moc jasný pojem "vyčíslitelný morfismus", ani "rozložit", ani "komponent".

Mám-li f: X -> Y, je f . id "rozložení na komponenty" nebo ne?

Nedávno tu zaznělo, že ne
Kde přesně?
Ta otázka je nepřesná, zřejmě jde o to, že když mám vyčíslitelný morfismus a nějaký jeho rozklad, tak z něj vždy dostanu takový rozklad, kde každá komponenta je restrikcí nějaké dané a zároveň vyčíslitelná, protože můžu vždy jít přes epimorfismy. Existence je zaručená, protože všechny morfismy jsou totální funkce. Důkaz je přes komutativní diagramy celkem názorný (byť ne zcela triviální).


Re:Faktorizace vyčíslitelných funkcí v Hasku
« Odpověď #5 kdy: 13. 08. 2017, 21:25:47 »
Ta otázka je nepřesná, zřejmě jde o to, že když mám vyčíslitelný morfismus a nějaký jeho rozklad, tak z něj vždy dostanu takový rozklad, kde každá komponenta je restrikcí nějaké dané a zároveň vyčíslitelná, protože můžu vždy jít přes epimorfismy. Existence je zaručená, protože všechny morfismy jsou totální funkce. Důkaz je přes komutativní diagramy celkem názorný (byť ne zcela triviální).
To's mi to teda pořád moc neosvětlil :) "Vyčíslitelný morfismus" je co? Pokud se bavíme o Hasku, jsou morfismy funkce a vyčíslitelné jsou z definice (Hask iirc neobsahuje bottom).

"Rozklad morfismu" znamená co? Rozklad nějaké množiny, nebo to, že f můžu vyjádřit jako složení nějakého g a h? (proto jsem se ptal, jestli jedno z toho může být id)

A je tenhle fakt nějak využitelný, má nějaké praktické důsledky?

zboj

  • *****
  • 1 507
    • Zobrazit profil
    • E-mail
Re:Faktorizace vyčíslitelných funkcí v Hasku
« Odpověď #6 kdy: 13. 08. 2017, 22:27:24 »
Ta otázka je nepřesná, zřejmě jde o to, že když mám vyčíslitelný morfismus a nějaký jeho rozklad, tak z něj vždy dostanu takový rozklad, kde každá komponenta je restrikcí nějaké dané a zároveň vyčíslitelná, protože můžu vždy jít přes epimorfismy. Existence je zaručená, protože všechny morfismy jsou totální funkce. Důkaz je přes komutativní diagramy celkem názorný (byť ne zcela triviální).
To's mi to teda pořád moc neosvětlil :) "Vyčíslitelný morfismus" je co? Pokud se bavíme o Hasku, jsou morfismy funkce a vyčíslitelné jsou z definice (Hask iirc neobsahuje bottom).

"Rozklad morfismu" znamená co? Rozklad nějaké množiny, nebo to, že f můžu vyjádřit jako složení nějakého g a h? (proto jsem se ptal, jestli jedno z toho může být id)

A je tenhle fakt nějak využitelný, má nějaké praktické důsledky?
Hask se může brát jako prostě nějaká obecná kartézsky uzavřená kategorie s morfismy jako vyjádřitelnými funkcemi (bez ohledu na vyčíslitelnost, on i takový halting problém je při vhodné restrikci rozhodnutelný, zrovna před rokem jsem o tom viděl hezkou přednášku na Oxfordu, ale to odbočuju). Rozklad morfismu je předpoklad pro to tvrzení, čili například f.g.h (wlog stačí uvažovat binární rozklad). Když si ho zadáš jako f.id, tak klidně můžeš, jen to pak je poměrně triviální. To tvrzení říká, že můžu jít jinou cestou (přes jiné objekty dané kategorie), přičemž ty morfismy na alternativní cestě jsou restrikcemi těch původních a když vyberu epimorfismy, tak budou vyčíslitelné, je-li jejich kompozice taktéž. Využitelné je to spíš naopak, když se mi podaří faktorizovat nějakou složitější funkci a dokázat, že příslušné epimorfismy nejsou vyčíslitelné (aspoň jeden), tak kompozice je v pytli a nic s tím neudělám. Většinou se hledá nějaký bottleneck v algoritmu, kde se provede faktorizace zaručující restrikci s vyčíslitelností (třeba v parsingu přirozených jazyků se omezujucící podmínky převádějí na algebru rysů (feature algebra), nad kterou se pak řeší word problem pro ukázání bezespornosti; dá-li si daný model vyjádřit jako třeba polycyklická grupa, tak dostanu faktorizaci, jejíž druhá komponenta je vyčíslitelná, byť obecně je word problem nerozhodnutelný).

Re:Faktorizace vyčíslitelných funkcí v Hasku
« Odpověď #7 kdy: 13. 08. 2017, 23:51:51 »
Hask se může brát jako prostě nějaká obecná kartézsky uzavřená kategorie s morfismy jako vyjádřitelnými funkcemi (bez ohledu na vyčíslitelnost, on i takový halting problém je při vhodné restrikci rozhodnutelný, zrovna před rokem jsem o tom viděl hezkou přednášku na Oxfordu, ale to odbočuju). Rozklad morfismu je předpoklad pro to tvrzení, čili například f.g.h (wlog stačí uvažovat binární rozklad). Když si ho zadáš jako f.id, tak klidně můžeš, jen to pak je poměrně triviální. To tvrzení říká, že můžu jít jinou cestou (přes jiné objekty dané kategorie), přičemž ty morfismy na alternativní cestě jsou restrikcemi těch původních a když vyberu epimorfismy, tak budou vyčíslitelné, je-li jejich kompozice taktéž.
Ok, díky, to už mi trochu začíná dávat smysl.

zboj

  • *****
  • 1 507
    • Zobrazit profil
    • E-mail
Re:Faktorizace vyčíslitelných funkcí v Hasku
« Odpověď #8 kdy: 14. 08. 2017, 01:25:12 »
Hask se může brát jako prostě nějaká obecná kartézsky uzavřená kategorie s morfismy jako vyjádřitelnými funkcemi (bez ohledu na vyčíslitelnost, on i takový halting problém je při vhodné restrikci rozhodnutelný, zrovna před rokem jsem o tom viděl hezkou přednášku na Oxfordu, ale to odbočuju). Rozklad morfismu je předpoklad pro to tvrzení, čili například f.g.h (wlog stačí uvažovat binární rozklad). Když si ho zadáš jako f.id, tak klidně můžeš, jen to pak je poměrně triviální. To tvrzení říká, že můžu jít jinou cestou (přes jiné objekty dané kategorie), přičemž ty morfismy na alternativní cestě jsou restrikcemi těch původních a když vyberu epimorfismy, tak budou vyčíslitelné, je-li jejich kompozice taktéž.
Ok, díky, to už mi trochu začíná dávat smysl.
Ono to je vlastně intuitivně jednoduché a v KT to jen zní nabubřele.