Dědičnost dnes

[JS]

Hodně silné (a nepravdivé) tvrzení. V podstatě tvrdíš, že je nejlepší vše brát jako relace nebo přímo množiny (protože co jiného jsou funkce). Chtěl bych vidět ten tvůj množinový kód řešící všechno nejlépe.

Ne, to netvrdim, zaprve, neni potreba az takovy redukcionismus, a za druhe, mluvim spis o funkcich ve smyslu lambda kalkulu nez ve smyslu relaci.

[Reklama]

[JS]

A nebo prostě trvá, než si na to lidi zvyknou.

Tak me napada, podobna situace je i v matematice. Vetsina matematiku pouziva normalni predikatovou logiku, ale lambda kalkulus (treba kalkulus konstrukci) by mozna byl praktictejsi. Jde zase jen o zvyk. :-) (Ne docela, je tady cela ta otazka konstruktivismu..)

[zboj]

Hodně silné (a nepravdivé) tvrzení. V podstatě tvrdíš, že je nejlepší vše brát jako relace nebo přímo množiny (protože co jiného jsou funkce). Chtěl bych vidět ten tvůj množinový kód řešící všechno nejlépe.

Ne, to netvrdim, zaprve, neni potreba az takovy redukcionismus, a za druhe, mluvim spis o funkcich ve smyslu lambda kalkulu nez ve smyslu relaci.

Funkce v lambda kalkulu jsou relace. Celý lambda kalkulus je jen notace pro zapisování funkcí (vytváření funkcí z výrazů). Ale to už je skoro slovíčkaření, nechme to.

[zboj]

A nebo prostě trvá, než si na to lidi zvyknou.

Tak me napada, podobna situace je i v matematice. Vetsina matematiku pouziva normalni predikatovou logiku, ale lambda kalkulus (treba kalkulus konstrukci) by mozna byl praktictejsi. Jde zase jen o zvyk. :-) (Ne docela, je tady cela ta otazka konstruktivismu..)

Sorry, ale predikátová logika a lambda kalkulus nejsou alternativou jeden druhému. Navíc predikátová logika je formálně silnější.

[JS]

Len ten zvyk trva uz nejako dlho, pricom su nonstop pokusy o pretlacenie FP do mainstreamu. A FP je taka dokonala paradigma, ze potrebuje aj objektove a proceduralne konstrukcie  inak je to hracka pre matematikov.

Vzhledem k tomu, že za 40let co existuje OOP (ať se vrátíme k tématu topicu) se programátoři nenaučili OOP používat a dál to patlají procedurálně, jsem optimistou.
To by ostatně mohlo odpovědět na tvou otázku, proč že prej FP není v mainstreamu. Těch důvodů je pochopitelně více, a hlavně bych je hledal v technické oblasti, ale jedním z nich je skutečnost, že třeba v Haskellu funkcionálně programovat musíš. Zatímco v Javě objektově nikoliv.
[/quote]

Neco takoveho jsem chtel odpovedet taky.. Ale jinak nemam pocit, ze by se FP prosazovalo pomaleji nez OOP, Java uz jiste prvky FP taky zacina dostavat. Porad to sice neni ten Haskell, ale on je to fakt hodne exoticky jazyk.

[Reklama]

[JS]

Funkce v lambda kalkulu jsou relace. Celý lambda kalkulus je jen notace pro zapisování funkcí (vytváření funkcí z výrazů). Ale to už je skoro slovíčkaření, nechme to.

Nemusi byt, kdyz vezmu lambda kalkulus jako formalni system, nemusim o funkcich jako relacich nad mnozinami vubec nic vedet (podobne jako nemusim typy chapat jako mnoziny). Muzes definovat relaci jako vysledek beta-redukce, ale to uz tomu davas nejakou interpretaci.

Sorry, ale predikátová logika a lambda kalkulus nejsou alternativou jeden druhému. Navíc predikátová logika je formálně silnější.

Klasicka predikatova logika je o neco silnejsi, ale je otazka, jestli je to az takova vyhra. Jsou lide, treba Voevodsky, kteri by radsi videli alternativu v tom lambda kalkulu. Aspon ja v tom tedy vidim hlavne jazykovou barieru pro vetsi rozsireni automatickeho dokazovani. Ale matematici jsou konzervativni a chteji pouzivat predikatovou logiku, navic v ni maji napsano spousta kodu..

[balki]

A nebo prostě trvá, než si na to lidi zvyknou.

Tak me napada, podobna situace je i v matematice. Vetsina matematiku pouziva normalni predikatovou logiku, ale lambda kalkulus (treba kalkulus konstrukci) by mozna byl praktictejsi. Jde zase jen o zvyk. :-) (Ne docela, je tady cela ta otazka konstruktivismu..)

Sorry, ale predikátová logika a lambda kalkulus nejsou alternativou jeden druhému. Navíc predikátová logika je formálně silnější.

Lambda calculus je turingovo kompletny. Ino by islo opisat predikatovu logiku lambda calculom, len by to bolo ako skrabanie sa lavou rukou za pravym uchom. Sklamem vas, ale lambda calculus je silnejsi, zvladne kazdy vypocitatelny problem.

[zboj]

A nebo prostě trvá, než si na to lidi zvyknou.

Tak me napada, podobna situace je i v matematice. Vetsina matematiku pouziva normalni predikatovou logiku, ale lambda kalkulus (treba kalkulus konstrukci) by mozna byl praktictejsi. Jde zase jen o zvyk. :-) (Ne docela, je tady cela ta otazka konstruktivismu..)

Sorry, ale predikátová logika a lambda kalkulus nejsou alternativou jeden druhému. Navíc predikátová logika je formálně silnější.

Lambda calculus je turingovo kompletny. Ino by islo opisat predikatovu logiku lambda calculom, len by to bolo ako skrabanie sa lavou rukou za pravym uchom. Sklamem vas, ale lambda calculus je silnejsi, zvladne kazdy vypocitatelny problem.

Co to je za kecy? Zjisti si, co znamená turingovsky kompletní a kam ve výpočetní hierarchii spadá formální logika. Pak se můžeme bavit, proč je logika nerozhodnutelná a co je z ní třeba odebrat, aby byla.

[zboj]

Funkce v lambda kalkulu jsou relace. Celý lambda kalkulus je jen notace pro zapisování funkcí (vytváření funkcí z výrazů). Ale to už je skoro slovíčkaření, nechme to.

Nemusi byt, kdyz vezmu lambda kalkulus jako formalni system, nemusim o funkcich jako relacich nad mnozinami vubec nic vedet (podobne jako nemusim typy chapat jako mnoziny). Muzes definovat relaci jako vysledek beta-redukce, ale to uz tomu davas nejakou interpretaci.

Sorry, ale predikátová logika a lambda kalkulus nejsou alternativou jeden druhému. Navíc predikátová logika je formálně silnější.

Klasicka predikatova logika je o neco silnejsi, ale je otazka, jestli je to az takova vyhra. Jsou lide, treba Voevodsky, kteri by radsi videli alternativu v tom lambda kalkulu. Aspon ja v tom tedy vidim hlavne jazykovou barieru pro vetsi rozsireni automatickeho dokazovani. Ale matematici jsou konzervativni a chteji pouzivat predikatovou logiku, navic v ni maji napsano spousta kodu..

OK, filosofie matematiky není zrovna můj obor, tak se nebudu pouštět do polemiky, i když můj osobní pocit je, že na spoustě věci bychom se shodli.

[balki]

A nebo prostě trvá, než si na to lidi zvyknou.

Tak me napada, podobna situace je i v matematice. Vetsina matematiku pouziva normalni predikatovou logiku, ale lambda kalkulus (treba kalkulus konstrukci) by mozna byl praktictejsi. Jde zase jen o zvyk. :-) (Ne docela, je tady cela ta otazka konstruktivismu..)

Sorry, ale predikátová logika a lambda kalkulus nejsou alternativou jeden druhému. Navíc predikátová logika je formálně silnější.

Lambda calculus je turingovo kompletny. Ino by islo opisat predikatovu logiku lambda calculom, len by to bolo ako skrabanie sa lavou rukou za pravym uchom. Sklamem vas, ale lambda calculus je silnejsi, zvladne kazdy vypocitatelny problem.

Co to je za kecy? Zjisti si, co znamená turingovsky kompletní a kam ve výpočetní hierarchii spadá formální logika. Pak se můžeme bavit, proč je logika nerozhodnutelná a co je z ní třeba odebrat, aby byla.

Poprosim dokaz. Pak se budem bavit, vole.

[zboj]

A nebo prostě trvá, než si na to lidi zvyknou.

Tak me napada, podobna situace je i v matematice. Vetsina matematiku pouziva normalni predikatovou logiku, ale lambda kalkulus (treba kalkulus konstrukci) by mozna byl praktictejsi. Jde zase jen o zvyk. :-) (Ne docela, je tady cela ta otazka konstruktivismu..)

Sorry, ale predikátová logika a lambda kalkulus nejsou alternativou jeden druhému. Navíc predikátová logika je formálně silnější.

Lambda calculus je turingovo kompletny. Ino by islo opisat predikatovu logiku lambda calculom, len by to bolo ako skrabanie sa lavou rukou za pravym uchom. Sklamem vas, ale lambda calculus je silnejsi, zvladne kazdy vypocitatelny problem.

Co to je za kecy? Zjisti si, co znamená turingovsky kompletní a kam ve výpočetní hierarchii spadá formální logika. Pak se můžeme bavit, proč je logika nerozhodnutelná a co je z ní třeba odebrat, aby byla.

Poprosim dokaz. Pak se budem bavit, vole.

Na této úrovni se bavit nebudeme. Poslední, co ti řeknu, je, že nerozhodnutelnost predikátové logiky dokázali pánové Church a Turing (nezávisle na sobě) ve 30. letech minulého století, čímž nasrali pana Hilberta. Jejich důkaz(y) si můžeš najít, když na chvíli přestaneš trollit.

[balki]

A nebo prostě trvá, než si na to lidi zvyknou.

Tak me napada, podobna situace je i v matematice. Vetsina matematiku pouziva normalni predikatovou logiku, ale lambda kalkulus (treba kalkulus konstrukci) by mozna byl praktictejsi. Jde zase jen o zvyk. :-) (Ne docela, je tady cela ta otazka konstruktivismu..)

Sorry, ale predikátová logika a lambda kalkulus nejsou alternativou jeden druhému. Navíc predikátová logika je formálně silnější.

Lambda calculus je turingovo kompletny. Ino by islo opisat predikatovu logiku lambda calculom, len by to bolo ako skrabanie sa lavou rukou za pravym uchom. Sklamem vas, ale lambda calculus je silnejsi, zvladne kazdy vypocitatelny problem.

Co to je za kecy? Zjisti si, co znamená turingovsky kompletní a kam ve výpočetní hierarchii spadá formální logika. Pak se můžeme bavit, proč je logika nerozhodnutelná a co je z ní třeba odebrat, aby byla.

Poprosim dokaz. Pak se budem bavit, vole.

Na této úrovni se bavit nebudeme. Poslední, co ti řeknu, je, že nerozhodnutelnost predikátové logiky dokázali pánové Church a Turing (nezávisle na sobě) ve 30. letech minulého století, čímž nasrali pana Hilberta. Jejich důkaz(y) si můžeš najít, když na chvíli přestaneš trollit.

Diky ty blbe, za uzitecny kecy.

Po mojom: Dakujem vam za rozsirenie obzorov.

[Mirek Prýmek]

čímž nasrali pana Hilberta

Hilbert byl nasranej, protoze na neho v hospode zbyla zidle, stul, ale zadnej korbel piva!

[zboj]

čímž nasrali pana Hilberta

Hilbert byl nasranej, protoze na neho v hospode zbyla zidle, stul, ale zadnej korbel piva!

Důkaz?

[balki]

čímž nasrali pana Hilberta

Hilbert byl nasranej, protoze na neho v hospode zbyla zidle, stul, ale zadnej korbel piva!

Maaam, google pomohol! Entscheidungsproblem

To ste mi nemohli povedat hned, zboj-nik tu musel hrat doleziteho?