Zwięzły przykład wykładniczego kosztu wnioskowania typu ML

Zwrócono mi uwagę, że koszt wnioskowania o typ w funkcjonalnym języku, takim jak OCaml, może być bardzo wysoki. Twierdzenie jest takie, że istnieje ciąg wyrażeń taki, że dla każdego wyrażenia długość odpowiedniego typu jest wykładnicza względem długości wyrażenia.

Wymyśliłem sekwencję poniżej. Moje pytanie brzmi: czy znasz sekwencję z bardziej zwięzłymi wyrażeniami, która osiąga te same typy?

# fun a -> a;;
- : 'a -> 'a = <fun>
# fun b a -> b a;;
- : ('a -> 'b) -> 'a -> 'b = <fun>
# fun c b a -> c b (b a);;
- : (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>
# fun d c b a -> d c b (c b (b a));;
- : ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
   (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'd
= <fun>
# fun e d c b a -> e d c b (d c b (c b (b a)));;
- : (((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
    (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'd -> 'e) ->
   ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
   (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'e
= <fun>
# fun f e d c b a -> f e d c b (e d c b (d c b (c b (b a))));;
- : ((((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
     (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'd -> 'e) ->
    ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
    (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'e -> 'f) ->
   (((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
    (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'd -> 'e) ->
   ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) ->
   (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'f
= <fun>

W tej odpowiedzi zajmę się kluczowym fragmentem ML języka, z tylko rachunkiem lambda i polimorficznym letpo Hindley-Milner . Pełny język OCaml ma dodatkowe funkcje, takie jak polimorfizm wierszy (który, jeśli dobrze pamiętam, nie zmienia teoretycznej złożoności, ale z którymi prawdziwe programy mają zwykle większe typy) i system modułowy (który, jeśli wystarczająco mocno naciskasz, może nie być -terminacja w przypadkach patologicznych z udziałem podpisów abstrakcyjnych).

Złożoność w najgorszym przypadku przy podejmowaniu decyzji, czy podstawowy program ML ma dany typ, jest prostą wykładniczą wielkością programu. Klasyczne odniesienia do tego wyniku to [KTU90] i [M90]. Bardziej elementarne, ale mniej kompletne leczenie podano w [S95].

Maksymalny rozmiar rodzaju typu podstawowego programu ML jest w rzeczywistości podwójnie wykładniczy w rozmiarze tego programu. Jeśli moduł sprawdzania typu musi wydrukować typ programu, czas może zatem być podwójnie wykładniczy; można go sprowadzić do prostej wykładniczej, definiując skróty powtarzających się części drzewa. Może to odpowiadać współużytkowaniu części drzewa typów w implementacji.

Twój przykład pokazuje wykładniczy wzrost tego typu. Należy jednak pamiętać, że możliwe jest przedstawienie liniowej reprezentacji typu za pomocą skrótów dla powtarzających się części typu. Może to odpowiadać współużytkowaniu części drzewa typów w implementacji. Na przykład:

# fun d c b a -> d c b (c b (b a));;
t2 -> t2
where t2 = (t1 -> 'b -> 'c) -> t1 -> 'a -> 'd
where t1 = 'a -> 'b

(x,x)xpair$N$$\Theta(2^N)$

# let pair x f = f x x;;
# let pairN x = pair (pair (pair … (pair x)…));;
'a -> tN
where tN = (tN-1 -> tN-1 -> 'bN) -> 'bN
…
where t2 = (t1 -> t1 -> 'b2) -> 'b2
where t1 = ('a -> 'a -> 'b1) -> 'b1

Po wprowadzeniu zagnieżdżonych letdefinicji polimorficznych rozmiar typu ponownie rośnie wykładniczo; tym razem żadne dzielenie się nie może zmniejszyć wykładniczego wzrostu.

# let pair x f = f x x;;
# let f1 x = pair x in
  let f2 x = f1 (f1 x) in
  let f3 x = f2 (f2 x) in
  fun z -> f3 (fun x -> x) z;;

Bibliografia

[KTU90] Kfoury, J .; Tiuryn; Urzyczyn, P. (1990). „Typowanie ML jest zakończone zręcznością”. Wykład notatki z informatyki. CAAP '90 431: 206-220. [ Springer ] [ Google ]

[M90] Mairson, Harry G. (1990). „Decydowanie o typowości ML jest kompletne dla deterministycznego czasu wykładniczego”. Materiały z 17. sympozjum ACM SIGPLAN-SIGACT na temat zasad języków programowania. POPL '90 (ACM): 382–401. [ ACM ]

[P04] Benjamin C. Pierce. Zaawansowane tematy w typach i językach programowania. MIT Press, 2004. [ Amazon ]

[PR04] François Pottier i Didier Rémy. „Esencja wnioskowania typu ML”. Rozdział 10 w [P04]. [ pdf ]

[S95] Michael I. Schwartzbach. Wnioskowanie typu polimorficznego. BRICS LS-95-3, czerwiec 1995. ps