Relação histórica entre cálculo lambda digitado e Lisp?

16

Eu estava conversando recentemente com um amigo (que é um defensor de idiomas fortemente tipados). Ele fez o comentário:

Os inventores do Lambda Calculus sempre pretendiam que fosse digitado.

Agora podemos ver que a Igreja estava associada ao Cálculo Lambda de Digitação Simples . De fato, parece que ele explicou o Cálculo Lambda de Digitação Simples, a fim de reduzir mal-entendidos sobre o Cálculo Lambda.

Agora, quando John McCarthy criou o Lisp, ele o baseou no cálculo Lambda . Isso é por sua própria admissão quando ele publicou "Funções recursivas de expressões simbólicas e seu cálculo por máquina, Parte I" . Você pode ler aqui .

McCarthy parece não ter abordado o Cálculo Lambda de Digitação Simples. Isso parece ser dominado por Robyn Milner na ML .

Há alguma discussão sobre a relação entre Lisp e Lambda Calculus aqui , mas eles realmente não entendem por que McCarthy escolheu deixá-lo sem tipagem.

Minha pergunta é - se McCarthy admite que sabia sobre o Cálculo Lambda - por que ele ignorou o cálculo Lambda digitado? (ie - é realmente óbvio que o Lambda Calculus foi projetado para ser digitado? Não parece assim)

Hawkeye
fonte
11
Provavelmente tem algo a ver com o cálculo lambda digitado não estar completo em Turing.
Jan Johannsen
Obrigado @JanJohannsen - você poderia expandir isso?
hawkeye

Respostas:

17

λ

Uma excelente visão geral da história é encontrada neste artigo .

λ

Sam Tobin-Hochstadt
fonte
Uau - respondida pela pessoa mais qualificada do mundo sobre este tópico. Obrigado @ Sam. Talvez eu receba uma solicitação de doutorado para você até o final do ano. (Parece que Ambrose BS está ansioso para trabalhar com vocês).
hawkeye
3
Estou realmente muito longe da pessoa mais qualificada do mundo nesse tópico.
Sam Tobin-Hochstadt
O link parece estar quebrado. Eu acredito que este é o mesmo artigo: hope.simons-rock.edu/~pshields/cs/cmpt312/cardone-hindley.pdf
bmaddy