Qual é o objetivo do cálculo combinador SKI (ou mesmo cálculo lambda)? Quais são alguns exemplos da vida real de seu uso?

Eu entendo o que é, mas não vejo como isso serve para algoritmos ou algo assim. Talvez esteja faltando alguma coisa. Preciso que alguém me dê um exemplo de como ele pode ser usado para que eu possa entender melhor.

algorithms lambda-calculus combinatory-logic Kenneth Onyebinachi
fonte

Existem várias linguagens de programação esotéricas baseadas na lógica combinatória, por exemplo, Unlambda . Veja também aqui . Você pode encontrar mais informações explorando os links nos artigos.

Anton Trunov 04/04

Respostas:

A aplicação óbvia do cálculo lambda é qualquer linguagem de programação funcional (por exemplo, Lisp, ML, Haskell) e qualquer linguagem que suporte funções anônimas.

Quanto ao cálculo combinador, deve haver uma "aplicação do mundo real"? Máquinas de Turing, por exemplo, quase nunca são usadas "no mundo real", mas formam a base da teoria da computação. Uma característica útil dos cálculos combinadores é que eles são sistemas mais simples do que, por exemplo, máquinas de Turing. Se você quiser provar que algum outro sistema está completo com Turing, pode ser mais fácil mostrar como ele pode simular combinadores do que mostrar que pode simular uma máquina de Turing.

David Richerby
fonte

Obviamente, combinadores foram usados na compilação de linguagens funcionais (embora não o próprio cálculo do SKI).

Cody

@cody Por favor, poste uma resposta sobre isso! Não é algo que eu saiba, por isso prefiro não editar minha resposta.

David Richerby

Por exemplo, o sistema de tipos da Scala demonstrou ser completo em Turing incorporando o cálculo SK nele. Não consigo nem imaginar a complexidade absurda de incorporar uma Máquina de Turing (Universal). Ironicamente (com o nome), a integridade do Turinf raramente é mostrada nas Máquinas de Turing. Demonstrou-se que o SQL era TC implementando um Sistema de Tag Cíclico, HTML + CSS com a Regra 101, a Intel MMU, codificando uma instrução "Mover, Ramificar se Zero, Diminuir".

Jörg W Mittag

@ JörgWMittag re: " HTML + CSS com Regra 101 " você quis dizer " Regra 110 "?

precisa saber é o seguinte

@RBarryYoung: Claro, erro estúpido. O código está aqui: github.com/elitheeli/stupid-machines

Jörg W Mittag

Achei o SKI útil para entender alguns axiomas lógicos.

Por exemplo, uma axiomatização no estilo Hilbert de implicação (intuicionista) é

\begin{array}{l} (uma \to b \to c) \to (uma \to b) \to uma \to c \\ uma \to (b \to uma) \end{array}

$\begin{array}{l} (a \rightarrow b \rightarrow c) \rightarrow (a \rightarrow b) \rightarrow a \rightarrow c \\ a \rightarrow (b \rightarrow a) \end{array}$

A primeira vez que vi esses axiomas, me perguntei por que diabos eles deveriam funcionar. Claro, é fácil verificar se eles aguentam. Mas por que isso deveria ser suficiente, ou seja, por que usar esses dois postulados sozinhos é suficiente para provar (através do modus ponens) todas as outras tautologias implicacionais? Mistério ... ou é?

Bem, acontece que toda tautologia deve corresponder ao tipo de termo lambda, graças ao isomorfismo de Curry-Howard. Mas o referido termo lambda pode ser reescrito de forma equivalente em termos de combinadores $S,K$ sozinho. Então, os tipos de $S$ e $K$ deve gerar, por meio da aplicação, os tipos de qualquer tautologia. E, de fato, os dois axiomas acima são os tipos mais gerais para $S$ e $K$ .

chi
fonte

Dê uma olhada no LINQ (Consulta Integrada ao Idioma) da Microsoft. Faz uso extensivo e bastante direto do cálculo lambda para manipular e transformar árvores de expressão. Provavelmente, o exemplo mais completo e sofisticado seria o Linq2SQL (a implementação do SQL Server), que efetivamente realiza transformações complexas que segregam as partes da árvore de expressão que podem ser delegadas ao servidor de banco de dados.

Essa dificilmente é a primeira tecnologia que permite consultas que combinam dados de várias fontes, mas pode ser a primeira que automatiza o desembaraço de dependências para aproveitar os recursos de manipulação em massa dos servidores de banco de dados. Não é perfeito (às vezes você tem que ajudá-lo), mas faz o grunhido funcionar muito bem e com uma atenção aos detalhes que você não obterá dos seres humanos.

Quando você não tem que ajudá-lo, entender o cálculo levará um longo caminho para descobrir o que está incomodando-lo - portanto, além de que serve isso? há sua resposta para Por que eu tenho que aprender isso quando as máquinas fazem isso por mim?

Peter Wone
fonte