{{For|the proof assistant|ALF (theorem prover)}} {{For|the action language for foundational UML|FUML}} {{Infobox programming language |name = ALF |logo = |paradigm = [[Multi-paradigm programming language|multi-paradigm]]: [[Logic programming|logic]], [[Functional programming|functional]] |year = |designer = |developer = |latest release version = |latest release date = |typing = |implementations = |dialects = |influenced by = [[Prolog]] |influenced = |website = {{URL|www.informatik.uni-kiel.de/~mh/systems/ALF}} }}
'''Algebraic Logic Functional''' ('''ALF''') [[programming language]] combines [[Functional programming|functional]] and [[logic programming]] techniques. Its foundation is [[Horn clause]] logic with equality, which consists of predicates and Horn clauses for logic programming, and functions and equations for functional programming.
ALF was designed to be genuine integration of both programming paradigms, and thus any functional expression can be used in a goal literal and arbitrary predicates can occur in conditions of equations. ALF's [[operational semantics]] is based on the resolution rule to solve literals and narrowing to evaluate functional expressions. To reduce the number of possible narrowing steps, a leftmost-innermost basic narrowing strategy is used which, it is claimed, can be efficiently implemented.{{Citation needed|date=March 2012}} Terms are simplified by rewriting before a narrowing step is applied and equations are rejected if the two sides have different constructors at the top. Rewriting and rejection are supposed to result in a large reduction of the search tree and produce an operational semantics that is more efficient than [[Prolog]]'s resolution strategy. Similarly to Prolog, ALF uses a backtracking strategy corresponding to a [[depth-first search]] in the derivation tree.
The ALF system was designed to be an efficient implementation of the combination of resolution, narrowing, rewriting, and rejection. ALF programs are [[Compiler|compiled]] into instructions of an [[abstract machine]], which is based on the [[Warren Abstract Machine]] (WAM) with several extensions to implement narrowing and rewriting. In the current ALF implementation programs of this abstract machine are executed by an emulator written in [[C (programming language)|C]].
In the [[Carnegie Mellon University]] [[Artificial Intelligence]] Repository,<ref name='CMUAIR'>{{cite web |url=https://www.cs.cmu.edu/afs/cs.cmu.edu/project/ai-repository/ai/0.html |title=CMU Artificial Intelligence Repository |access-date=2007-06-22 |date=1995-02-13 |publisher=[[Carnegie Mellon University]] |archive-url=https://web.archive.org/web/20070623154858/https://www.cs.cmu.edu/afs/cs.cmu.edu/project/ai-repository/ai/0.html |archive-date=23 June 2007 |url-status=live}}</ref> ALF is included as an AI programming language, more so as a functional/logic programming language Prolog implementation.<ref name='CMUALF'>{{cite web |url=https://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/lang/prolog/impl/fp_lp/alf/0.html |title=ALF: Algebraic Logic Functional programming language |access-date=2007-06-22 |date=1995-02-13 |work=CMU Artificial Intelligence Repository |publisher=[[Carnegie Mellon University]] |archive-url=https://web.archive.org/web/20070510020843/https://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/lang/prolog/impl/fp_lp/alf/0.html |archive-date=10 May 2007 |url-status=live}}</ref> A user manual<ref name='ALFUM'>{{cite web |url=http://www.informatik.uni-kiel.de/~mh/systems/ALF/manual.pdf |title=ALF User's Manual |access-date=2007-06-22 |last=Hanus |first=Michael |author2=Andreas Schwab |date=1995-02-13 |publisher=Institut für Informatik, [[University of Kiel|Christian-Albrechts-Universität zu Kiel]] |archive-url=https://web.archive.org/web/20070711091450/http://www.informatik.uni-kiel.de/~mh/systems/ALF/manual.pdf |archive-date=11 July 2007 |url-status=live}}</ref> describing the language and the use of the system is available. The ALF System<ref name='ALFsys'>{{cite web |url=http://www.informatik.uni-kiel.de/~mh/systems/ALF.html |title=The ALF System |access-date=2007-06-22 |last=Hanus |first=Michael |publisher=Institut für Informatik, Christian-Albrechts-Universität zu Kiel |archive-url=https://web.archive.org/web/20070625154845/http://www.informatik.uni-kiel.de/~mh/systems/ALF.html |archive-date=25 June 2007 |url-status=live}}</ref> runs on [[Unix]] and is available under a custom [[proprietary software]] [[Software license|license]] that grants the right to use for "evaluation, research and teaching purposes" but not commercial or military use.<ref>{{cite web |last=Hanus |first=Michael |url=https://www.informatik.uni-kiel.de/~mh/systems/ALF/LICENSE |archive-url=https://web.archive.org/web/20151202180826/https://www.informatik.uni-kiel.de/~mh/systems/ALF/LICENSE |archive-date=2 December 2015 |title=ALF License Agreement |work=The ALF System |publisher=Institut für Informatik, Christian-Albrechts-Universität zu Kiel |access-date=2020-03-06 |url-status=live}}</ref>
==References== {{Reflist}}
==External links== *[http://www.informatik.uni-kiel.de/~mh/papers/ Publications of Michael Hanus], including many articles relevant to the design and theory of ALF *[http://www.informatik.uni-kiel.de/~mh/systems/ALF/README Information about getting and installing the ALF system]
[[Category:Functional logic programming languages]] [[Category:Programming languages created in the 1990s]]
{{Comp-sci-stub}}