Academic literature on the topic 'Lambda-prolog'
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'Lambda-prolog.'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Journal articles on the topic "Lambda-prolog"
1
Tarau, Paul. "Deriving Efficient Sequential and Parallel Generators for Closed Simply-Typed Lambda Terms and Normal Forms." Fundamenta Informaticae 177, no. 3-4 (December 10, 2020): 385–415. http://dx.doi.org/10.3233/fi-2020-1994.
Full textAbstract:
Contrary to several other families of lambda terms, no closed formula or generating function is known and none of the sophisticated techniques devised in analytic combinatorics can currently help with counting or generating the set of simply-typed closed lambda terms of a given size. Moreover, their asymptotic scarcity among the set of closed lambda terms makes counting them via brute force generation and type inference quickly intractable, with previous published work showing counts for them only up to size 10. By taking advantage of the synergy between logic variables, unification with occurs check and efficient backtracking in today’s Prolog systems, we climb 4 orders of magnitude above previously known counts by deriving progressively faster sequential Prolog programs that generate and/or count the set of closed simply-typed lambda terms of sizes up to 14. Similar counts for closed simply-typed normal forms are also derived up to size 14. Finally, we devise several parallel execution algorithms, based on generating code to be uniformly distributed among the available cores, that push the counts for simply typed terms up to size 15 and simply typed normal forms up to size 16. As a remarkable feature, our parallel algorithms are linearly scalable with the number of available cores.
2
APPEL, ANDREW W., and AMY P. FELTY. "Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf." Theory and Practice of Logic Programming 4, no. 1+2 (January 2004): 1–39. http://dx.doi.org/10.1017/s1471068403001698.
Full text
3
NADATHUR, GOPALAN. "A treatment of higher-order features in logic programming." Theory and Practice of Logic Programming 5, no. 3 (May 2005): 305–54. http://dx.doi.org/10.1017/s1471068404002297.
Full textAbstract:
The logic programming paradigm provides the basis for a new intensional view of higher-order notions. This view is realized primarily by employing the terms of a typed lambda calculus as representational devices and by using a richer form of unification for probing their structures. These additions have important meta-programming applications but they also pose non-trivial implementation problems. One issue concerns the machine representation of lambda terms suitable to their intended use: an adequate encoding must facilitate comparison operations over terms in addition to supporting the usual reduction computation. Another aspect relates to the treatment of a unification operation that has a branching character and that sometimes calls for the delaying of the solution of unification problems. A final issue concerns the execution of goals whose structures become apparent only in the course of computation. These various problems are exposed in this paper and solutions to them are described. A satisfactory representation for lambda terms is developed by exploiting the nameless notation of de Bruijn as well as explicit encodings of substitutions. Special mechanisms are molded into the structure of traditional Prolog implementations to support branching in unification and carrying of unification problems over other computation steps; a premium is placed in this context on exploiting determinism and on emulating usual first-order behaviour. An extended compilation model is presented that treats higher-order unification and also handles dynamically emergent goals. The ideas described here have been employed in the Teyjus implementation of the $\lambda$Prolog language, a fact that is used to obtain a preliminary assessment of their efficacy.
4
Mirasyedioğlu, Şeref, and Tolga Güyer. "A symbolic and algebraic computation based Lambda-Boolean reduction machine via PROLOG." Applied Mathematics and Computation 176, no. 1 (May 2006): 65–75. http://dx.doi.org/10.1016/j.amc.2005.09.081.
Full text
5
GUIDI, FERRUCCIO, CLAUDIO SACERDOTI COEN, and ENRICO TASSI. "Implementing type theory in higher order constraint logic programming." Mathematical Structures in Computer Science 29, no. 8 (March 1, 2019): 1125–50. http://dx.doi.org/10.1017/s0960129518000427.
Full textAbstract:
In this paper, we are interested in high-level programming languages to implement the core components of an interactive theorem prover for a dependently typed language: the kernel – responsible for type-checking closed terms – and the elaborator – that manipulates open terms, that is terms containing unresolved unification variables.In this paper, we confirm that λProlog, the language developed by Miller and Nadathur since the 80s, is extremely suitable for implementing the kernel. Indeed, we easily obtain a type checker for the Calculus of Inductive Constructions (CIC). Even more, we do so in an incremental way by escalating a checker for a pure type system to the full CIC.We then turn our attention to the elaborator with the objective to obtain a simple implementation thanks to the features of the programming language. In particular, we want to use λProlog’s unification variables to model the object language ones. In this way, scope checking, carrying of assignments and occur checking are handled by the programming language.We observe that the eager generative semantics inherited from Prolog clashes with this plan. We propose an extension to λProlog that allows to control the generative semantics, suspend goals over flexible terms turning them into constraints, and finally manipulate these constraints at the meta-meta level via constraint handling rules.We implement the proposed language extension in the Embedded Lambda Prolog Interpreter system and we discuss how it can be used to extend the kernel into an elaborator for CIC.
6
Despeyroux, Joëlle, and Robert Harper. "Special issue on Logical Frameworks and Metalanguages http//www-sop.inria.fr/certilab/LFM00/cfp-jfp.html." Journal of Functional Programming 10, no. 1 (January 2000): 135–36. http://dx.doi.org/10.1017/s0956796899009892.
Full textAbstract:
Logical frameworks and meta-languages are intended as a common substrate for representing and implementing a wide variety of logics and formal systems. Their definition and implementation have been the focus of considerable work over the last decade. At the heart of this work is a quest for generality: A logical framework provides a basis for capturing uniformities across deductive systems and support for implementing particular systems. Similarly a meta-language supports reasoning about and using languages.Logical frameworks have been based on a variety of different languages including higher-order logics, type theories with dependent types, linear logic, and modal logic. Techniques of representation of logics include higher-order abstract syntax, inductive definitions or some form of equational or rewriting logic in which substitution is explicitly encoded.Examples of systems that implement logical frameworks include Alf, Coq, NuPrl, HOL, Isabelle, Maude, lambda-Prolog and Twelf. An active area of research in such systems is the study of automated reasoning techniques. Current work includes the development of various automated procedures as well as the investigation of rewriting tools that use reflection or make use of links with systems that already have sophisticated rewriting systems. Program extraction and optimization are additional topics of ongoing work.
7
Alnajem, Salah, A. M. Mutawa, Hanan AlMeer, and Aseel AlQemlas. "A Prolog-based approach to Arabic syntax and semantics." Journal of Engineering Research 9, no. 3A (September 2, 2021). http://dx.doi.org/10.36909/jer.v9i3a.10129.
Full textAbstract:
This paper introduces a computational approach to Arabic syntax. The approach uses the Lexical Functional Grammar (LFG) framework. Semantic networks and frames were used to handle computational semantics using lambda notation. This was implemented in Prolog using Definite Clause Grammar (DCG) as a formalism for analyzing and generating syntactic structure.
8
Biernacki, Dariusz, and Olivier Danvy. "From Interpreter to Logic Engine by Defunctionalization." BRICS Report Series 11, no. 5 (March 11, 2004). http://dx.doi.org/10.7146/brics.v11i5.21830.
Full textAbstract:
Starting from a continuation-based interpreter for a simple logic programming language, propositional Prolog with cut, we derive the corresponding logic engine in the form of an abstract machine. The derivation originates in previous work (our article at PPDP 2003) where it was applied to the lambda-calculus. The key transformation here is Reynolds's defunctionalization that transforms a tail-recursive, continuation-passing interpreter into a transition system, i.e., an abstract machine. Similar denotational and operational semantics were studied by de Bruin and de Vink (their article at TAPSOFT 1989), and we compare their study with our derivation. Additionally, we present a direct-style interpreter of propositional Prolog expressed with control operators for delimited continuations.
9
Biernacki, Dariusz, and Olivier Danvy. "From Interpreter to Logic Engine by Defunctionalization." BRICS Report Series 10, no. 25 (June 13, 2003). http://dx.doi.org/10.7146/brics.v10i25.21954.
Full textAbstract:
Starting from a continuation-based interpreter for a simple logic programming language, propositional Prolog with cut, we derive the corresponding logic engine in the form of an abstract machine. The derivation originates in previous work (our article at PPDP 2003) where it was applied to the lambda-calculus. The key transformation here is Reynolds's defunctionalization that transforms a tail-recursive, continuation-passing interpreter into a transition system, i.e., an abstract machine. Similar denotational and operational semantics were studied by de Bruin and de Vink in previous work (their article at TAPSOFT 1989), and we compare their study with our derivation. Additionally, we present a direct-style interpreter of propositional Prolog expressed with control operators for delimited continuations.<br /><br />Superseded by BRICS-RS-04-5.
Dissertations / Theses on the topic "Lambda-prolog"
1
Brisset, Pascal. "Compilation de lambda-prolog." Rennes 1, 1992. http://www.theses.fr/1992REN10032.
Full textAbstract:
Cette these presente une solution de compilation pour prolog. Prolog est une extension double de prolog. D'une part deux nouveaux connecteurs, l'implication et le quantificateur universel, permettent d'ecrire des buts non permis en prolog. D'autre part, les termes du premier ordre de prolog sont remplaces par des termes types. La mise en uvre de prolog pose des problemes originaux. Contrairement au cas de prolog, l'unificateur de termes types est non-deterministe et les termes sont types. De plus, la regle de equivalence doit etre prise en compte et les termes doivent etre mis sous forme normale. La quantification universelle necessite de manipuler une signature explicite. L'implication oblige a une modification dynamique de la base de clauses. Apres definition du langage et une specification denotationnelle executable, la compilation de prolog puis celle de prolog sont presentees. L'implantation proposee utilise la machine mali, memoire specialisee pour les langages de programmation logique, au-dessus de laquelle est definie une machine virtuelle inspiree de la wam. Ce travail a ete valide par une realisation. Les performances obtenues, comparees a celles des systemes existants, sont excellentes tant du point de vue du temps que de la memoire
2
Chen, Biao. "Prolog e Lambda-Prolog: verso l’implementazione di un analizzatore statico di mode." Bachelor's thesis, Alma Mater Studiorum - Università di Bologna, 2017.
Find full text
3
Ridoux, Olivier. "Lambda-Prolog de A à Z... ou presque." [S.l.] : [s.n.], 1998. ftp://ftp.irisa.fr/techreports/habilitations/ridoux.pdf.
Full text
4
Ludwig, Artemio. ""Lambda" PROLOG : interpretador e unificação de ordem superior." [s.n.], 1992. http://repositorio.unicamp.br/jspui/handle/REPOSIP/260489.
Full textAbstract:
Orientador : Wagner C. AmaralTese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica
Made available in DSpace on 2018-07-16T01:51:41Z (GMT). No. of bitstreams: 1 Ludwig_Artemio_D.pdf: 9026847 bytes, checksum: bf0003b28c02857c43931feb4b9729d1 (MD5) Previous issue date: 1992
Resumo: A implementação de interpretadores para a linguagem da Lógica de Ordem Superior (LOS) constitui-se num desafio ainda não vencido. Pode-se dividi-Io em duas partes: (a) tornar a linguagem mais amigável permitindo estimular sua adoção e (b) dotar as implementações com um desempenho que não sacrifique sua usabilidade. A linguagem de programação para a LOS utiliza os conceitos do À-cálculo e os recursos de tipificação de Russel. Sua sintaxe é portanto mais complexa do que aquela da Lógica de Primeira Ordem (LPO). A técnica de derivação de algum conhecimento em uma base de conhecimento, formalizada conforme suas regras, assemelha-se com aquela da LPO que é chamada de resolução. Qualquer sistema de provas em LOS deve atender a restrições de uma linguagem fortemente tipada e a unificação, que apresenta problemas de incompletude, pode gerar mais do que um unificador. Isto torna a pesquisa nâ.o-determinística e faz com que a derivação contenha mais uma fonte de retroencadeamento, quando comparada com modelo de programação em LPO. Este trabalho expõe e analisa a implementação de um interpretador para a LOS sujeita a sentenças definidas positivas as quais contêm propriedades adequadas à mecanização semelhantes àquelas das cláusulas de HORN da LPO. Problemas de indecidibilidade são contornados e os vários aspectos computacionais são descritos como a formação da base de conhecimento, sua gramática e a P-derivação, que é o método de obtenção de provas sobre a base. Central a estes procedimentos encontra-se a unificação que apresenta complexidade elevada e cujo processamento é razão de depauperação na qualidade do sistema. Uma proposta de enfoque alternativa é oferecida com o propósito de atenuar os efeitos sobre a lentidão do sistema. O algoritmo resultante indica ganhos no desempenho e apresenta uma interpretação mais facilitada do mecanismo da unificação
Abstract: Efficient Interpreter implementations for Righer Order Logic (ROL) programming language still remain as a challenge that can be splitted into two classes: (a) to make the language friendlier in order to stimulate the user to adopt it, and (b) to provi de the interpreter with a performance that does not damage its usability. This paper resulted from an ROL interpreter prototypation, called À-PROLOG. Only the positive definite sentençes are used in the language. They are similar to those of the First Order Logic (FOL) programing language and present some apropriate mechanization properties. One kind of implementation is discribed and its computational aspects are analysed. They include the knowledgernent base formation, the grarnrnar of the sentences and the P-derivation, which is the method of deriving proofs over the base. The unification is the most important interpreter procedure and has high complexity. Its processing is one of the reazons for the depaupering of system quality. In this paper the analisies of the MATCR and SIMPL algorithms that were developed for this purpose are used to supply a new unification algorithm which, in contrast to MATCR, shows initial performance gains and an easier procedural interpretation oí the unification mechanism
Doutorado
Automação
Doutor em Engenharia Elétrica
5
Molinari, Giacomo. "Towards an Implementation in Lambda-Prolog of Maietti's two-level minimalist foundation." Bachelor's thesis, Alma Mater Studiorum - Università di Bologna, 2018.
Find full textAbstract:
The idea of a theory able to conjugate the advantages of both the extensional and intensional views of mathematics was presented in an article by Maria Emilia Maietti in 2006. In order to combine these two different views the theory is developed over two levels: an extensional level interpreted over an intensional one by means of quotients.
The first attempt to fully formalize this theory in a programming language is the subject of Alberto Fiori's master thesis. After giving a brief introduction to Maietti's theory in the first two chapters, I proceed to examine Fiori's implementation in Lambda-Prolog, focusing on its main downside: in the translation from extensional types to their intensional interpretation, the size of the translated types grows exponentially. Such an explosive growth renders Fiori's approach computationally unviable.
In order to deal with this issue we had to devise a different approach, an implementation (written in the same language) which effectively builds the setoid model in the intensional theory and then uses this new level of abstraction to implement the extensional theory. In practice, this means building a library of abstractions where the definitions of setoid and dependent setoid are given once and for all.
This required us to write our own abstraction mechanisms for abstracting over types, terms and conversion rules, since Maietti's theory does not provide a definitional level. The new abstraction mechanisms presented in this thesis represent therefore an original contribution to Maietti's work.
Finally, I show that while the size of translations is smaller in this implementation, its growth remains exponential.
Thanks to the setoid approach, however, the reasons behind the explosive size growth have finally become more clear: this makes them easier to analyse and, hopefully, will allow future implementations to overcome this issue.
6
Caprari, Riccardo. "Estrazione di codice da termini della Minimalist Type Theory." Master's thesis, Alma Mater Studiorum - Università di Bologna, 2018. http://amslaurea.unibo.it/17159/.
Full textAbstract:
L’obiettivo di questa tesi è stato l’implementazione di un estrattore di codice per un dimostratore interattivo basato sulla minimalist two-level foundation (mTT), proposta da Maietti.
Per raggiungere lo scopo, si è preso a modello l’estrattore di codice del dimostratore Coq ed è stato necessario acquisire conoscenze nell’ambito dell’eliminazione di codice inutile, la quale si occupa di rilevare tramite analisi statica quelle parti di codice che, se eliminate, lasciano invariato l’output riducendo l’uso di RAM e i passi di computazione del programma.
L’estrattore è stato implementato utilizzando il linguaggio λProlog, nel quale erano già stati prodotti precedentemente un type checker e una versione provvisoria del compilatore per mTT da Alberto Fiori e Giacomo Molinari nelle loro rispettive tesi. L’interprete di λProlog che ho utilizzato durante il mio lavoro è ELPI, realizzato presso l’Università di Bologna.
Pur avendo avuto a disposizione risorse estensive su cui basare l’implementazione, è stato comunque necessario produrre un numero consistente di soluzioni originali: infatti, l’operazione di estrazione richiede spesso un adattamento o, in alcuni casi, una riscrittura dei procedimenti di manipolazione standard sulla base delle differenti idiosincrasie della fondazione logica di partenza.
L’estrattore prodotto come risultato finale del lavoro di tesi è completamente funzionante e in grado di estrarre ogni costrutto del livello intensionale della logica mTT, traducendolo in codice OCaml e Haskell.
7
Vaccari, Giulio. "Dal Paradigma Funzionale a Quello Logico in Presenza di Scelte Probabilistiche: un Approccio Basato sulla Geometria dell'Interazione." Bachelor's thesis, Alma Mater Studiorum - Università di Bologna, 2018. http://amslaurea.unibo.it/16726/.
Full textAbstract:
In questa tesi verrà trattato lo sviluppo di un software che svolge la funzione di traduttore tra due linguaggi di programmazione.
Lo scopo di un traduttore è quello di trasformare un programma scritto in un dato linguaggio in un nuovo programma funzionalmente equivalente a quello di partenza ma scritto in un linguaggio diverso. Il linguaggio di partenza per la traduzione è rappresentato dal lambda calcolo probabilistico. Studieremo il paradigma di programmazione su cui si basa, per poi analizzare la struttura dei programmi definibili nel linguaggio. Vedremo quindi ProbLog, un linguaggio fondato sul paradigma di programmazione logica arricchito con costrutti probabilistici, che rappresenterà il linguaggio di destinazione per il traduttore. I linguaggi logici permettono un approccio alla programmazione basato sulla definizione di teorie logiche, in cui da proposizioni assunte vere si derivano nuovi risultati attraverso un processo di deduzione formale. La caratteristica principale di ProbLog che lo differenzia dagli altri linguaggi logici risiede nella possibilità di definire proposizioni che risultano vere con una data probabilità, permettendoci di modellare realtà in cui sono presenti fatti e regole non più per forza veri in senso assoluto. Per realizzare il processo di traduzione verrà impiegata la Geometria dell'Interazione, una struttura semantica per la logica lineare introdotta dal logico Jean-Yves Girard. Intuitivamente può sembrare difficile immaginare come questa possa aver trovato posto nello sviluppo del traduttore, ma vedremo come in realtà un programma del lambda calcolo sia intrinsecamente connesso a questo tipo di logica. La Geometria dell'Interazione ci darà la possibilità di vedere i programmi funzionali sotto una nuova angolazione, accorciando la distanza che separa il paradigma funzionale da quello logico.
8
Polidori, Daniele. "Implementazione in un linguaggio logico con vincoli di ordine superiore della type inference di Haskell." Bachelor's thesis, Alma Mater Studiorum - Università di Bologna, 2020. http://amslaurea.unibo.it/20503/.
Full textAbstract:
Implementazione in ELPI, un linguaggio logico con vincoli di ordine superiore, dell'algoritmo di type inference di Haskell.
ELPI è un'estensione con vincoli di lambda Prolog. Utilizzando lambda Prolog risulta impossibile implementare la type inference di Haskell. Si è reso dunque necessario l'utilizzo di ELPI, più espressivo (non nel senso di Turing completezza) di lambda Prolog.
La presente trattazione ha una duplice finalità.
La prima consiste nel dimostrare che le estensioni a lambda Prolog presenti in ELPI permettono di risolvere problemi non risolvibili in lambda Prolog.
La seconda, non ancora implementata ma lasciata agli sviluppi futuri, prevede di fare del mio lavoro uno strumento di prova per testare, implementare e studiare nuove estensioni al meccanismo delle type class di Haskell. Infatti, essendo ELPI un linguaggio di più alto livello e più semplice (grazie alle features del linguaggio) rispetto ad Haskell, aggiungere estensioni al meccanismo base delle type class dovrebbe risultare banale (in confronto alla complessità di eseguire tale operazione in Haskell).
9
Piemontese, Cristiano. "Sviluppo di un interactive theorem prover in ELPI." Master's thesis, Alma Mater Studiorum - Università di Bologna, 2018. http://amslaurea.unibo.it/17293/.
Full textAbstract:
In questo elaborato è discusso l'utilizzo del linguaggio Lambda Prolog, con interprete ELPI, per lo sviluppo di dimostratori interattivi. Nel primo capitolo viene introdotto Lambda Prolog, sono fornite indicazioni storiche sull'interactive theorem proving e descritto cosa ci si aspetta da un interactive theorem prover basato sull'isomorfismo di Curry-Howard. Le estensioni fornite da ELPI sono analizzate rispetto alla possibilità di facilitare l'implementazione di un dimostratore interattivo.
Nel secondo capitolo è introdotta Minimalist Type Theory, analizzato il kernel implementato e su cui è stato costruito il lavoro sviluppato, con una trattazione dell'implementazione di un elaboratore e di un dimostratore interattivo.
Per concludere, vengono analizzati pro e contro della soluzione proposta e i suoi possibili sviluppi futuri.
Book chapters on the topic "Lambda-prolog"
1
Dunchev, Cvetan, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. "ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter." In Logic for Programming, Artificial Intelligence, and Reasoning, 460–68. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015. http://dx.doi.org/10.1007/978-3-662-48899-7_32.
Full text
2
Ashcroft, E. A., A. A. Faustini, R. Jaggannathan, and W. W. Wadge. "Intensionality." In Multidimensional Programming. Oxford University Press, 1995. http://dx.doi.org/10.1093/oso/9780195075977.003.0005.
Full textAbstract:
The intensional programming language, Lucid, described in Chapter 1 is based directly on intensional logic, a family of mathematical formal systems that permit expressions whose value depends on hidden contexts or indices. Our use of intensional logic is one in which the hidden contexts or indices are integers or tuples of integers. Intensional logic, as used to give semantics to natural language, uses a much more general notion of context or index. Of course, intensional logic is hardly the first example of a formal system of interest to both logicians and computer scientists. The language LISP (invented by McCarthy and others in the early sixties [34]) was originally intended to be an adaptation of the lambda calculus, although it diverged in its treatment of variable-binding and higher-order functions. Shortly after, however, Landin produced ISWIM, the first true functional language [30]. These “logical” programming languages such as ISWIM are in many respects vastly superior to the more conventional ones. They are much simpler and better defined and yet at the same time more regular and more powerful. These languages are notationally closer to ordinary mathematics and are much more problem-oriented. Finally, programs are still expressions in a formal system, and are still subject to the rules of the formal system. It is therefore much easier to reason formally about their correctness, or to apply meaningpreserving transformations. With these languages, programming really is a respectable branch of applied mathematical logic. These logic-based (or declarative) languages at first proved difficult to implement efficiently, and interest in declarative languages declined soon after the promising initial work of McCarthy and Landin. Fortunately, the advent of large scale integration and new compiling technology reawakened interest in declarative languages, and brought about a series of new “second generation” declarative languages, such as Prolog [12] and Miranda [44]. Lucid itself was one of these second generation declarative languages. Lucid is based not so much on classical logical systems as on the possible worlds approach to intensional logic—itself a relatively new branch of logic [43] which reached maturity during the period (1965-75) in which declarative programming languages were in eclipse.