Matematické Fórum

Lota · 12. 11. 2008 15:40

Zdravím, můžete mi někdo pomoci s důkazem matematickou indukcí téhle funkce?

filter :: (a->Bool) -> [a] -> [a]
filter _ [] = []
filter p (x:s) = if p x then x : t else t where t = filter p s

absolutně netuším jak postupovat.. musel bych k tomu asi vědět i tu podmínku, ne? nebo si mám zvolit jakou chci?

dík za pomoc

Kondr · 12. 11. 2008 15:53

Dokazujeme, že pro všechna n platí: pro všechny seznamy délky n filter P S vrátí prvky S, které vyhoví P v pořadí, v jakém jsou v S.

První krok: pro n=0. Tady sepoužije první větev, fce vrátí prázdný seynam, OK.
Indukční krok: předpokládám funkčnost pro n=k a dokazuju pro k+1>0.
Použije se druhá větev, fce filter vrátí první prvek sezamu právě když splní podmínku a za něj přidá filter p "ocasu". Protože je ocas délky k, filter p ocasu obsahuje z indukčního předpokladu právě ty jeho prvky, které vyhoví podmínce.

Toto je stručná verze, na písemce se to musí trochu očesat (např. nepoužívat slovo "ocas").

Lota · 12. 11. 2008 21:43

Děkuji za odpověď.. Já to právě zkoušel, ale nevěděl jsem jak na to po matematické stránce.
Takže pokud důkaz funkce popíši takto slovně, je to také správně?

Kondr · 12. 11. 2008 23:51

↑ Lota:Ano, ale chce to být o trochu formálnější. V indukčním kroku ukázat, že
* filter p (x:s) obsahuje všechny prvky x:s splňující p
* filter p (x:s) neobsahuje žádné jiné
* pořadí prvků zůstalo zachováno
Všecko jsou to triviality, ale hodilo by se to rozepsat.

Matematické Fórum

#1 12. 11. 2008 15:40

haskell důkaz fce filter

#2 12. 11. 2008 15:53

Re: haskell důkaz fce filter

#3 12. 11. 2008 21:43

Re: haskell důkaz fce filter

#4 12. 11. 2008 23:51

Re: haskell důkaz fce filter