Ենթադրենք, որ ձեր ռեկուրսիվ ֆունկցիան կազմում է n երկարության ցուցակ, որտեղ բոլոր տարրերը զրո են:
Սա կարող է նման բան թվալ.
fun foo 0 = []
| foo n = 0::(foo (n - 1))
Այս դեպքում տարբերակը n ֆունկցիայի արգումենտն է:
n-ը բնական թիվ է, և բնական թվերն ամբողջությամբ դասավորված են առանց անսահման նվազող շղթաների, քանի որ ոչ մի շղթա չի կարող զրոյից ցածր լինել:
Ավելին, n խստորեն նվազում է յուրաքանչյուր ռեկուրսիվ զանգի հետ:
Մեկ այլ օրինակ. Ենթադրենք, որ ձեր ֆունկցիան ընդունում է երկու արգումենտ՝ x և y, և վերադարձնում է true, եթե x > y, իսկ հակառակ դեպքում՝ false:
fun bar 0 y = false
| bar x 0 = true
| bar x y = bar (x - 1) (y - 1)
Այս դեպքում տարբերակի մի քանի տարբերակ կա. Դուք կարող եք այն ընդունել որպես x կամ y, ինչպես նախորդ օրինակում, կամ լինել x + y: Այս դեպքերից որևէ մեկում այն ընդունում է բնական թվային արժեքներ և խիստ նվազում:
Այժմ, օրինակ, որտեղ արգումենտները ոչ ամբողջ թվեր են. գտնել ցուցակի գումարը:
fun sum [] = 0
| sum (x::xs) = x + (sum xs)
Այս դեպքում տարբերակը կարող է ընդունվել որպես ցուցակի երկարություն (կրկին բնական թիվ), կամ լինել հենց ցուցակը, որտեղ ցուցակները դասավորված են հետևյալ կերպ.
l1 < l2 եթե կա x1,x2,...,xn տարրերի որոշակի վերջավոր հաջորդականություն, որ x1::x2::...::xn::l1 = l2:
Բավականին հեշտ է ցույց տալ, որ ցուցակների հավաքածուն մասամբ դասավորված է, առանց անսահման նվազող շղթաների, այս համեմատության ներքո, և, մասնավորապես, ցուցակների շարքը, որը ստեղծվել է ռեկուրսիվ զանգերի արդյունքում, սկսած ինչ-որ ցուցակից, ամբողջությամբ դասավորված է:
Ավելին, ցանկացած ռեկուրսիվ զանգի դեպքում՝ xs < (x::xs), ըստ սահմանման, ուստի ցուցակը նվազում է:
Տարբերակի իմաստն այն է, որ այն մեծություն է, որը կարող է ներարկվել ֆունկցիայի վարքագծի վերաբերյալ բաներ ապացուցելու համար: Քանի որ չկան անսահման նվազող շղթաներ, պետք է լինի նվազագույն տարր, որը կարող է ընդունվել որպես ինդուկցիայի հիմք, և այնուհետև ընդհանուր կարգը տալիս է ինդուկցիայի եղանակ՝ մեկ տարրից անմիջապես ավելի մեծ տարր:
Դա կարելի է անել նաև մասնակի կարգով, առանց անսահման նվազող շղթաների, ինչը երաշխավորում է նվազագույն տարրերի առկայության, եթե ոչ պարտադիր նվազագույն տարրերի առկայության դեպքում: Այնուհետև դրանք կարող են օգտագործվել որպես բազային դեպքեր, և նման ինդուկցիոն փաստարկ ներկայացնել, թեև հավանական է ավելի մեծ տարրեր կառուցելու բազմաթիվ եղանակներով:
02.12.2013
