Is lambda calculus a logic?

I am trying to figure out the relation of equational logic to ordinary Haskell evaluations (not type level or anything exotic).
I posted similar question here and on the Haskell-cafe, which provided some very good insights. This lead me to the lambda calculus and even more questions.
Here is my take ...
Lambda calculus is generally considered as a formal model (is this in the model theoretic sense?) of computation. But is it a logic?

First what is a Logic?
Hunter [1] says a formal system consist of
a) Well formed formula (WFF)
b) Axioms
c) A model, which is an interpretation of the WFF
d) Rules of inference, independent of model
Which are all determined by fiat by the language creator.
Of course these pieces must all work in harmony. I guess it is the rules of inference (d) that make it a logic. See [2] for a deep look at this question

Hankin[3] puts lambda calculus in the context of general formal systems, consisting of;
a) Notation, a set of terms (WFF)
b) Theories or set axioms relating terms,Hankin[3] provides a theory for LC (seems very close to the axioms of equational logic).
c) Models that give mathematical meaning, in LC this is usually functions over sets
Hankin[3] goes on to describe reduction. I am aware that logics can be encoded in LC and reductions would be inferences (but logics can be encoded in Java).

So, it seems that lambda calculus is a formal system, but is it a logic?
If it is not what is its relation with logic?

[1]Metalogic: An Introduction to the Metatheory of Standard First-Order Logic,Geoffrey Hunter, University of California Press, 1971
[2] What is a logic, Mossakowski et al.
[3] An Introduction to Lambda Calculi for Computer Scientists, 2nd edition 2004, Chris Hankin

Comment viewing options

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

Recently on LtU

You might be interested in this post.

I haven't managed to get all the way through the paper yet, but they are dealing with one perspective on the question you are asking, and you might find that illuminating.

Depends a lot on who you ask

I tend to use logic to describe truth-valued formal systems and calculus for other formal systems. But I'm not aware of any widely accepted criteria for differentiating between those related concepts and I have looked.

Lambda calculus is generally

Lambda calculus is generally considered as a formal model (is this in the model theoretic sense?) of computation.

Yes, one of Dana Scott's biggest contributions has been to connect the lambda calculus to domain theory, showing denotational semantics (for functional languages) is reasonable. The (constructive) proof of a domain isn't so bad to follow. I'm not sure where a good copy is online, but the wiki page seems to take you maybe a third of the way there.

This stuff is well outside of my expertise, so unfortunately I'm not sure of a nice source connecting a traditional logic to LC. (Isn't curry-howard sufficient?) Either way, Philip Wadler has a lot to say on this. The "As Natural as 0, 1, 2" slides includes a list of some dualities you can chase down.

Edit: if the goal is a inference/rewrite system independent of the model, Dana Scott's results seems sufficient for your purposes. That still doesn't answer the question of what is a logic.

You could also look at

Barendregts book (called "the bible" in some circles). It defines equality of lambda terms inductively, using equational rules. Barendregt then proceeds to give a series of models satisfying these rules (with variations depending on whether you admit the eta-rule, etc.). This seems to be the closest answer to your original question.

Of course another way to see the (simply typed) lambda calculus as a logic is to see the terms as proofs of propositions which are represented by types. This is the Curry-Howard isomorphism which you've probably heard about if you lurk on LTU at all.

Reading the holy book for free

Barendregts book (called "the bible" in some circles).

Like most holy books, you can read it for free online. Henk has it on the CS department's ftp server.

Not Barendregts "bible"

The link points to another text of Henk Barendregt on typed lambda Calculi. This should not be confused with "The Lambda Calculus, Its Syntax and Semantics", which is concerned with the untyped case and has an encyclopaedic scope.

Lest we forget

Sometimes abstract mathematics makes it hard to keep track of what intuition we came in with; so I thought I'd throw in just a bit of historical perspective (as I understand it, of course). Alonzo Church set out to construct a logic, which he hoped would avoid paradoxes without abandoning the law of the excluded middle, by instead dropping reductio ad absurdum. He set it up to have only one device for binding variables, lambda; the existential and universal quantifiers weren't binding constructs, but instead higher-order functions. The alpha rule and beta rule were two of the basic inference rules in the logic. The part about avoiding paradoxes didn't work out, so they backed off and showed that a certain subset of the inference rules would not in itself cause inconsistency, in the sense of everything being equivalent to everything else. The subset they showed consistent was just the alpha and beta rules, and that result was published by Church and Rosser and is now called the Church–Rosser Theorem.

i want an oliver stone movie of that

i'd watch it at imax. (seriously.)