λProlog - λProlog
| Paradigma | Programação lógica |
|---|---|
| Projetado por | Dale Miller e Gopalan Nadathur |
| Apareceu pela primeira vez | 1987 |
| Disciplina de digitação | fortemente tipado |
| Licença | GNU General Public License v3 |
| Local na rede Internet | www |
| Implementações principais | |
| Teyjus, ELPI | |
| Influenciado por | |
| Prolog | |
| Influenciado | |
| Makam | |
λProlog , também escrito lambda Prolog , é uma linguagem de programação lógica com tipagem polimórfica , programação modular e programação de ordem superior . Estas extensões para Prolog são derivadas das fórmulas Harrop hereditárias de ordem superior usadas para justificar os fundamentos de λProlog. De ordem superior quantificação , simplesmente digitei X-termos , e de ordem superior unificação dá λProlog os suportes básicos necessários para capturar a abordagem sintaxe λ-árvore para de ordem superior sintaxe abstrata , uma abordagem para representar sintaxe que mapeia ligações de nível de objeto a programação ligações de linguagem. Os programadores em λProlog não precisam lidar com nomes de variáveis associadas: em vez disso, vários dispositivos declarativos estão disponíveis para lidar com escopos de binder e suas instanciações.
História
Desde 1986, λProlog recebeu inúmeras implementações. A partir de 2013, a linguagem e suas implementações ainda estão sendo desenvolvidas ativamente.
O provador do teorema Abella foi projetado para fornecer um ambiente interativo para provar teoremas sobre o núcleo declarativo de λProlog.
Veja também
- Paradoxo de Curry # cálculo lambda - sobre problemas de inconsistência causados pela combinação de lógica (proposicional) e cálculo lambda não tipado
Referências
Tutoriais e textos
- Dale Miller e Gopalan Nadathur escreveram o livro Programação com lógica de ordem superior , publicado pela Cambridge University Press em junho de 2012.
- Amy Felty escreveu em 1997 um tutorial sobre lambda Prolog e suas aplicações para prova de teoremas ([arquivado por WebCite https://www.webcitation.org/5WpO4HGEh?url=http://www.site.uottawa.ca/~afelty /dist/lprolog97.ps ]).
- John Hannan escreveu um tutorial sobre Análise de Programas em lambda Prolog para a Conferência PLILP de 1998.
- Olivier Ridoux escreveu Lambda-Prolog de A à Z ... ou presque (163 páginas, francês). Ele está disponível como PostScript , PDF e html .
links externos
- λProlog homepage
- Entrada no Grupo de Preservação de Software.
Implementações
- O compilador Teyjus λProlog é atualmente a implementação mais antiga ainda mantida. Este projeto de compilador é liderado por Gopalan Nadathur e vários de seus colegas e alunos.
- ELPI: um intérprete λProlog incorporável foi desenvolvido por Enrico Tassi e Claudio Sacerdoti Coen . Ele é implementado em OCaml e está disponível online . O sistema é descrito em um artigo que apareceu LPAR 2015.
- O provador Abella pode ser usado para provar teoremas sobre programas e especificações λProlog.
 |
Este artigo relacionado à linguagem de programação é um esboço . Você pode ajudar a Wikipedia expandindo-a . |
- ^ Nadathur, Gopalan; Dustin Mitchell (1999). Descrição do sistema: Teyjus - Um compilador e uma implementação baseada em máquina abstrata do lambda Prolog . Conferência sobre dedução automatizada . LNAI. 1632 . pp. 287–291. doi : 10.1007 / 3-540-48660-7_25 . ISBN 978-3-540-66222-8 .