Exemplo conciso de custo exponencial da inferência do tipo ML

11

Fui informado de que o custo da inferência de tipo em uma linguagem funcional como o OCaml pode ser muito alto. A alegação é que existe uma sequência de expressões que, para cada expressão, o comprimento do tipo correspondente é exponencial no comprimento da expressão.

Eu inventei a sequência abaixo. Minha pergunta é: você conhece uma sequência com expressões mais concisas que alcança os mesmos tipos?

# 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>
mrrusof
fonte

Respostas:

14

Nesta resposta, vou me ater a um fragmento central de ML da linguagem, com apenas lambda-calculus e polimórficos letseguindo Hindley-Milner . A linguagem OCaml completa possui recursos adicionais, como o polimorfismo de linha (que, se bem me lembro, não altera a complexidade teórica, mas com a qual os programas reais tendem a ter tipos maiores) e um sistema de módulos (que, se você cutucar com força o suficiente, pode não ser -terminar em casos patológicos envolvendo assinaturas abstratas).

A pior complexidade de tempo para decidir se um programa básico de ML tem um tipo é um exponencial simples no tamanho do programa. As referências clássicas para este resultado são [KTU90] e [M90]. Um tratamento mais elementar, mas menos completo, é dado em [S95].

O tamanho máximo do tipo do tipo de um programa básico de ML é de fato duplamente exponencial no tamanho do programa. Se o verificador de tipos precisar imprimir o tipo do programa, o tempo poderá ser duplamente exponencial; ele pode ser trazido de volta a um exponencial simples, definindo abreviações para partes repetidas da árvore. Isso pode corresponder ao compartilhamento de partes da árvore de tipos em uma implementação.

Seu exemplo mostra crescimento exponencial do tipo. Observe, no entanto, que é possível fornecer uma representação de tamanho linear do tipo usando abreviações para partes repetidas do tipo. Isso pode corresponder ao compartilhamento de partes da árvore de tipos em uma implementação. Por exemplo:

# 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

Aqui está um exemplo conceitualmente mais simples: o tamanho do tipo do par (x,x)é o dobro do tamanho do tipo de tipo x; portanto, se você compõe a pairfunção vezes, obtém um tipo de tamanho .NΘ(2N)

# 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

Ao introduzir letdefinições polimórficas aninhadas , o tamanho do tipo aumenta novamente exponencialmente; desta vez, nenhuma quantidade de compartilhamento pode impedir o crescimento exponencial.

# 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;;

Referências

[KTU90] Kfoury, J .; Tiuryn; Urzyczyn, P. (1990). "A tipificação de ML é dexptime-completa". Notas de aula em Ciência da Computação. CAAP '90 431: 206-220. [ Springer ] [ Google ]

[M90] Mairson, Harry G. (1990). "Decidir que a tipificação de ML está completa por tempo exponencial determinístico". Anais do 17º Simpósio ACM SIGPLAN-SIGACT sobre Princípios das linguagens de programação. POPL '90 (ACM): 382-401. [ ACM ]

[P04] Benjamin C. Pierce. Tópicos avançados em tipos e linguagens de programação. MIT Press, 2004. [ Amazônia ]

François Pottier e Didier Rémy. "A essência da inferência do tipo ML". Capítulo 10 em [P04]. [ pdf ]

Michael I. Schwartzbach. Inferência de tipo polimórfica. BRICS LS-95-3, junho de 1995. ps

Gilles 'SO- parar de ser mau'
fonte
Então, basicamente, a natureza "composicional" das expressões de tipo juntamente com a inferência de tipo é a raiz do problema?
didierc
11
@didierc Não entendo o seu comentário. Muitas coisas são composicionais. De certa forma, a razão fundamental é que, a partir das operações básicas de duplicação de um objeto (restrição de dois tipos serem os mesmos) e do emparelhamento (o ->operador), você pode fazer um crescimento exponencial (uma árvore de Fibonacci).
Gilles 'SO- stop be evil'
Sim, acho que foi isso que quis dizer: o tipo de álgebra é por definição composicional (você usou os termos "compor a função de par" em sua resposta, provavelmente foi onde eu peguei a palavra), no sentido de que expressões de tipo são construídas a partir de expressões e operadores menores, e cada nova composição de expressões dimensiona o tamanho da expressão pelo menos por um fator 2 (com tipos polimórficos mais complexos - triádicos ou mais, o fator é maior).
didierc