Como faço para definir o combinador Y sem "Let Rec"?

Question

Em quase todos os exemplos, um combinador Y em idiomas do tipo ML é escrito assim:

let rec y f x = f (y f) x
let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1))

Isso funciona como esperado, mas parece trapaça para definir o combinador Y usando let rec ....

Quero definir este combinador sem usar a recursão, usando a definição padrão:

Y = λf·(λx·f (x x)) (λx·f (x x))

Uma tradução direta é a seguinte:

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;

No entanto, F# reclama que não consegue descobrir os tipos:

  let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;
  --------------------------------^

C:\Users\Juliet\AppData\Local\Temp\stdin(6,33): error FS0001: Type mismatch. Expecting a
    'a    
but given a
    'a -> 'b    
The resulting type would be infinite when unifying ''a' and ''a -> 'b'

Como escrevo o combinador y em f# sem usar let rec ...?

Answer 1

Como o compilador aponta, não há tipo que possa ser atribuído a x para que a expressão (x x) está bem tocado (isso não é estritamente verdadeiro; você pode digitar explicitamente x Como obj->_ - Veja meu último parágrafo). Você pode contornar esse problema declarando um tipo recursivo para que uma expressão muito semelhante funcione:

type 'a Rec = Rec of ('a Rec -> 'a)

Agora o combinador Y pode ser escrito como:

let y f =
  let f' (Rec x as rx) = f (x rx)
  f' (Rec f')

Infelizmente, você descobrirá que isso não é muito útil porque F# é um idioma rigoroso; portanto, qualquer função que você tenta definir usando esse combinador causará um estouro de pilha. Em vez disso, você precisa usar a versão de ordem aplicativa do combinador Y (\f.(\x.f(\y.(x x)y))(\x.f(\y.(x x)y))):

let y f =
  let f' (Rec x as rx) = f (fun y -> x rx y)
  f' (Rec f')

Outra opção seria usar a preguiça explícita para definir o combinador Y de ordem normal:

type 'a Rec = Rec of ('a Rec -> 'a Lazy)
let y f =
  let f' (Rec x as rx) = lazy f (x rx)
  (f' (Rec f')).Value

Isso tem a desvantagem de que as definições de função recursiva agora precisam de uma força explícita do valor preguiçoso (usando o Value propriedade):

let factorial = y (fun f -> function | 0 -> 1 | n -> n * (f.Value (n - 1)))

No entanto, tem a vantagem de que você pode definir valores recursivos sem função, assim como você pode em uma linguagem preguiçosa:

let ones = y (fun ones -> LazyList.consf 1 (fun () -> ones.Value))

Como alternativa final, você pode tentar se aproximar melhor do cálculo lambda sem tipo usando boxe e abatida. Isso daria a você (novamente usando a versão de ordem de aplicação do combinador Y):

let y f =
  let f' (x:obj -> _) = f (fun y -> x x y)
  f' (fun x -> f' (x :?> _))

Isso tem a desvantagem óbvia de que isso causará boxe e unboxing desnecessários, mas pelo menos isso é totalmente interno à implementação e nunca levará à falha no tempo de execução.

Answer 2

Eu diria que é impossível, e perguntei por que, eu iria onda à mão e invocaria o fato de que simplesmente digitou o cálculo lambda tem o propriedade de normalização. Em resumo, todos os termos do cálculo lambda simplesmente digitado terminam (consequentemente Y não pode ser definido no cálculo lambda simplesmente digitado).

O sistema de tipo F#não é exatamente o sistema de tipo de cálculo lambda simplesmente digitado, mas está próximo o suficiente. F# sem let rec chega muito perto do cálculo lambda simplesmente digitado - e, para reiterar, nesse idioma, você não pode definir um termo que não termine e que exclui a definição de y também.

Em outras palavras, em F#, "Let Rec" precisa ser um idioma primitivo, no mínimo, porque mesmo se você pudesse defini -lo dos outros primitivos, você não seria capaz de digitar essa definição. Tê -lo como primitivo permite, entre outras coisas, dar um tipo especial a esse primitivo.

EDIT: KVB mostra em sua resposta que as definições de tipo (um dos recursos ausentes do lambda-calculus simplesmente digitado, mas presentes em f#Let-REC-LESS) permitem obter algum tipo de recursão. Muito esperto.

Answer 3

Caso e as declarações nos derivados de ML são o que o torna completo, acredito que eles são baseados no sistema F e não simplesmente digitados, mas o ponto é o mesmo.

O sistema F não consegue encontrar um tipo para o combinador de ponto fixo, se poderia, não foi fortemente normalizando.

O que significa fortemente normalização é que qualquer expressão tem exatamente 1 forma normal, onde uma forma normal é uma expressão que não pode ser reduzida mais, isso difere de não no máx Uma forma normal, também não pode ter forma normal.

Se o Lambda Calculi digitado pudesse construir um operador de ponto fixo de maneira alguma, era bem possível que uma expressão não tivesse forma normal.

Outro teorema famoso, o problema de interrupção, implica que as línguas fortemente normalizando não estão completas, diz que é impossível decidir (diferente de provar) de uma linguagem completa de Turing qual subconjunto de seus programas interromperá qual entrada. Se um idioma é fortemente normalizando, é decidível se ele parar, a saber sempre parada. Nosso algoritmo para decidir que este é o programa: true;.

Para resolver isso, os derivados de ML estendem o sistema-f com o caso e deixam (Rec) para superar isso. Assim, as funções podem se referir a si mesmas em suas definições novamente, tornando -as de maneira alguma mais cálculos de lambda, não é mais possível confiar apenas nas funções anônimas para todas as funções computáveis. Assim, eles podem entrar novamente em loops infinitos e recuperar sua completude.

Answer 4

Resposta curta: Você não pode.

Resposta longa: O cálculo lambda simplesmente digitado está normalizando fortemente. Isso significa que não é equivalente. A razão para isso basicamente se resume ao fato de que um combinador Y deve ser primitivo ou definido recursivamente (como você encontrou). Simplesmente não pode ser expresso no sistema F (ou cálculo digitado mais simples). Não há como contornar isso (afinal, está provado). O y combinador você posso O implemento funciona exatamente da maneira que você deseja.

Eu sugeriria que você tente o esquema se quiser um verdadeiro combinador de Y da igreja. Use a versão aplicativa fornecida acima, pois outras versões não funcionam, a menos que você adicione explicitamente preguiça ou use um intérprete de esquema preguiçoso. (Tecnicamente, o esquema não não é completamente inativo, mas é dinamicamente digitado, o que é bom o suficiente para isso.)

Veja isso para a prova de forte normalização:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.1794

Depois de pensar um pouco mais, tenho certeza de que a adição de um combinador Y primitivo que se comporta exatamente da maneira como o Letrec definido que um faz completa o sistema. Tudo o que você precisa fazer para simular uma máquina de Turing é implementar a fita como um número inteiro (interpretado em binário) e uma mudança (para posicionar a cabeça).