Rekurencja słupkowa

Rekurencja słupkowa jest uogólnioną formą rekurencji opracowaną przez C. Spectora w jego artykule z 1962 roku. Jest to związane z indukcją słupkową w taki sam sposób, jak rekurencja pierwotna jest związana ze zwykłą indukcją lub rekurencja pozaskończona jest związana z indukcją pozaskończoną .

Definicja techniczna

Niech V , R i O będą typami , a i będzie dowolną liczbą naturalną reprezentującą ciąg parametrów wziętych z V . Wtedy ciąg funkcji f funkcji f _n od V ^{i + n} → R do O jest zdefiniowany przez rekurencję słupkową z funkcji L _n : R → O i B z B _n : (( V ^{i + n} → R ) x ( V ⁿ → R )) → O jeśli:

• f _n ((λα: V ^{ja + n} ) r ) = L _n ( r ) dla dowolnego r na tyle długiego, że L _{n + k} na dowolnym przedłużeniu r równa się L _n . Zakładając, że L jest ciągiem ciągłym, musi istnieć taki r , ponieważ funkcja ciągła może wykorzystywać tylko skończoną ilość danych.
• fa _n ( p ) = b _n ( p , (λ x : V ) fa _{n +1} (kot( p , x ))) dla dowolnego p w V ^{ja + n} → R .

Tutaj „kot” jest funkcją konkatenacji , wysyłającą p , x do sekwencji, która zaczyna się od p i ma x jako ostatni wyraz.

(Ta definicja jest oparta na definicji Escardó i Olivy).

Pod warunkiem, że dla każdej odpowiednio długiej funkcji (λα) r typu V ⁱ → R , istnieje jakieś n , przy czym L _n ( r ) = B _n ((λα) r , (λ x : V ) L _{n +1} ( r ) ), reguła indukcji słupkowej zapewnia, że ​​f jest dobrze zdefiniowane.

Pomysł polega na tym, że rozciąga się sekwencję arbitralnie, używając składnika rekurencji B do określenia efektu, aż do osiągnięcia wystarczająco długiego węzła drzewa sekwencji nad V ; wówczas składnik bazowy L określa ostateczną wartość f . Warunek dobrze zdefiniowanej odpowiada wymaganiu, że każda nieskończona ścieżka musi ostatecznie przechodzić przez wystarczająco długi węzeł: ten sam wymóg, który jest potrzebny do wywołania indukcji słupkowej.

Zasady indukcji słupkowej i rekurencji słupkowej są intuicjonistycznymi odpowiednikami aksjomatu zależnych wyborów .