A question I have been meaning to ask.

The Lambda calculus is a logical language and so are derivations such as lisp, scheme, and other functional languages. As such they theoretically could be used to prove facts as in languages like Prolog but I have never seen this done.

Moreover there is an intuitionistic logic (could this also be the more classic synthetic logic??) which could be quite useful for dealing with "real" dynamic, or uncertain environments. Something that could be very useful. Yet I am not awair of any practical tools for this.

Might not the logical interpretation of a function be more clear if the functions were written as rules, and had only a works/doesn't work return value?

Just wondering

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


There's a book from MIT Press called Structure and Interpretation of Computer Programs. (Because of the purple cover with someone who looks like a wizard, it's sometimes referred to as the "purple book" or the "wizard book."). In chapter 4, they have a logic programming implementation in Sheme. Fortunately, they provide the full text online.

You can also read a bit about programming in Schelog. This is a Prolog implementation embedded in Scheme based on macros and uses continuations. I don't know much about it, but it has a reference section to other logic programming implementation in Scheme and Lisp.

Under the Curry-Howard interp

Under the Curry-Howard interpretation, the types in a functional programming correspond to propositions, and the programs correspond to proofs. Evaluating a functional program corresponds to proof normalization -- that is, steadily eliminating uses of the Cut rule (aka modus ponens). So evaluating a functional program doesn't prove new theorems; instead it constructs steadily simpler proofs of the same theorem.

There's also a Curry-Howard isomorphism for logic programming. Under this interpretation, the signature that the programmer gives -- the initial assumptions the logic program can make -- can be seen to correspond to types and constants in the lambda calculus. Then, testing whether a query is true is a process of proof search -- the operational semantics are an attempt to find a lambda-term whose type corresponds to the query. The nondeterminism in a logic program corresponds to the fact that a particular theorem can have multiple proofs.


Once again, excellent questions. Let me refer you to Kanren and its related papers at the bottom of the page, "Outcome-Oriented Programming," "Relation-Oriented Programming," and "Logic-Oriented Programming."

Please try to give links to p

Please try to give links to previous LtU discussio, when possible. We discussed many of these issues, as well as the specific refecences above.


Above where?

Do you mean "From Shift and Reset to Polarized Linear Logic" on the home page?
Also where does it say how to put links in these pages?

re: putting links in pages

Standard html links should do the trick. Enter the following:

<a href='http://lambda-the-ultimate.org/'>Text for Link</a>

Resulting in:

Text for Link

As for looking up past discussions, there's the search facility on this site, and the all-knowing google. In addition, I try to keep my archive indexes relatively up to date, where I have:

The last one's for those that think SED and AWK are the last word in search technology. :-)

You know, one of the most el

margin-left:50.95pt;line-height:15.6pt'> font-family:"Trebuchet MS";mso-bidi-font-family:Arial'>You know, one of the
most elegant solutions I have ever seen which cleanly deals with side-effects
is to simply make a distinction between functions (no side-effects) and
procedures (may have side-effects). Functions may use other functions, and procedures
may use other functions or procedures.
font-family:"Trebuchet MS";mso-bidi-font-family:Arial'>

Oddly enough, you can formalize this approach href="http://citeseer.ist.psu.edu/653507.html">using modal logic.

There is no escape from crazy theory. :)

Actually this is a button pus

Actually this is a button push error! But as long as it is here what do you think? The quote is due to neelk.

functions vs. procedures

This approach is discussed here.

Mixed modes

Perhaps the modal logic idea suggested here is a key to sorting this out. What is properly impreative and what is properly functional. Where do the "effects" (ie side effects) belong. In a modal logic view the effects and their representation (ie a situation) provides a frame for the purely analytic (ie functional)

As "purests" say programming is really logic. But might it not be modal logic. Modal logics account for external effects such as errors, information, the results of actions, etc that can only be represented modally.

Hybrid Logic

See for example the pages: href="http://en.wikipedia.org/wiki/Hybrid_logic">wikipedia: Hybrid logic style="mso-spacerun: yes"> and Hybrid
logic page

Modal logic and monads

Oddly enough, you can formalize this approach using modal logic.

Oddly enough, you can formalize (S4) modal logic proofs with monads.

(Curry-Howard ho! For the CH uninitiated, this means essentially that terms that would have modal types are monadic functional programs which is relevant both for FP and LP.)


I mean discussions of Kanren, Schelog, papers mentioned that were previously discussed etc.

Functional languages as logic languages

The Lambda calculus is a logical language and so are derivations such as lisp, scheme, and other functional languages. As such they theoretically could be used to prove facts as in languages like Prolog but I have never seen this done.

The functional language of chapters 3 and 4 of CTM does deterministic logic programming. Chapter 9 explains how to translate deterministic Prolog programs into this language, and also gives the logical semantics. This is possible because dataflow variables are implemented as true logic variables with unification.

Chapter 9 shows how to add a nondeterministic choice operation to give a logic language with search. This covers most of the logical part of Prolog (including setof and bagof). The chapter shows how to translate all reasonable Prolog programs (i.e., those with a logical semantics, not using "red cuts") into this logic language.


Part of my motivation is to get definitions. Does determinate mean one answer, and nondeterminate several answers? Likewise "data flow variables" vs "true logical variables". Can a nondeterminate fact or variable be a modal variable (ie one that can change during a deduction)


Deterministic logic programming means programming in a logic language with no nondeterministic choice operator. So there is at most one solution to each query. Nondeterministic logic programming has a nondeterministic choice operator. So there can be any number of solutions to a query (zero, one, or more). (There are two kinds of nondeterministic choice operator: don't care, which selects exactly one alternative, and don't know, which searches over all possible alternatives. The above definition and chapter 9 of CTM both use a don't know operator.)

A dataflow variable is a single-assignment variable that causes any operation that uses the variable to wait until it is bound. A logic variable is a variable that can be bound to exactly one value; it is a basic part of the unification operation. A logic variable can be used as a dataflow variable.

Theorem proving with FP

[Lambda calculus] theoretically could be used to prove facts as in languages like Prolog but I have never seen this done.

It's not theoretical: it was the whole reason that ML was created.

There are lots of theorem provers and proof assistants based on the programs-as-proofs correspondence, for example, HOL and Isabelle.