Programmering

well found induction (og sml)

12. november 2010 af Sa5 (Slettet) - Niveau: Universitet/Videregående

Hej

Kan nogle forklare mig hvordan man laver et WELL FOUND induktions bevis?

I mit eksempel skal jeg bevise at to sml-funktioner er ens, men hvis en kan forklare mig det generelle princip vil det være nøjagtig lige så fantastisk!

Her er alligevel lige mit sml eksempel:

datatype tree = Lf | Br of int*tree*tree:

fun size Lf =0 | size(Br(i,t1,t2)) = 1+size t1 + size t2;

fun sizeI Lf k=k | sizeI (Br(i,t1,t2)) k = size t1 (1+sizeI t2 k);

Bevis vha. WELL FOUND induktion at sizeI tr k = k+size tr gælder for alle trees tr og alle heltal k.

På forhånd tak for al tænkelig hjælp!

-Sarah

Skriv et svar til: well found induction (og sml)

Du skal være logget ind, for at skrive et svar til dette spørgsmål. Klik her for at logge ind.
Har du ikke en bruger på Studieportalen.dk? Klik her for at oprette en bruger.