Lambda the Ultimate

OK, thanks for the help so far.

What about a type system or operational semantics specified as a set of inference rules? One usually talks about the "proof tree" used to show that it is possible to derive, say, a typing judgement. Is this related to proof theory, then?

I thought a reduction semantics is syntactic in the sense that the syntax is not associated with some kind of semantic object (as in denotational semantics) but we express the semantics only in terms of term rewriting.

Concerning the term "theory" itself: How does your definition of "theory" fit to the name "equational theory", that is often used to denote the rules that say under which conditions two terms are considered equal?

I probably I need to study these branches of mathematics more in order to understand the differences better.

Hopefully not stepping on Frank's elaboration...

I thought a reduction semantics is syntactic in the sense that the syntax is not associated with some kind of semantic object

One way to look at it is that the "meaning" of a redex (reducible expression) is its normal form. The way you find out the "meaning" of the expression is by applying the "syntactic" reductions to it.

Roughly, your reduction chain becomes your "proof", and some representation of all normal forms in your system is your "model".

How does your definition of "theory" fit to the name "equational theory"

How about a set (or set of sets) of rewrite rules/ equations that make the two terms equal?

Well, I see that it is easy to give syntactic entities representing, say, integers, a meaning. However, what about a lambda expression? It is a normal form. You only see its syntax, meaning a string of characters (or AST). So its "meaning" is itself, this piece of syntax? This looks like a very strange circularity, no?

You might find that discussion helpful, though it is not formal in any sense.

So its "meaning" is itself, this piece of syntax? This looks like a very strange circularity, no?

I think you are being too literal here. Note that I said your model was a "representation" of all normal forms.

Let's say we have two sets: the set of all well-formed syntactic expressions in some system, and the set of all normal forms for that system. Semantic evaluation can be represented by a function that assigns each syntactic form to its normal form in the semantic set.

Even if for convenience we represent elements of both sets as strings, eg. \lambda x.x this doesn't mean that the syntactic expression is the "same thing" as its identically represented semantically evaluated normal form.

Part of the confusion is the we often reason about semantic systems by creating a distinguished syntax that describes their structure. This is merely an aid to the reasoner, not an inherent property of such systems.

Let's say we have two sets: the set of all well-formed syntactic expressions in some system, and the set of all normal forms for that system. Semantic evaluation can be represented by a function that assigns each syntactic form to its normal form in the semantic set.

What I cannot understand, how domains (Scott's?) fit into this picture?

In this case semantic evaluation would just be a kind of identity function.

However, wouldn't I want to somehow specify the *effect* that a normal form would have if it were applied to some expression?

In this case semantic evaluation would just be a kind of identity function.

No, it would be a mapping from terms to (possibly different) terms, that's not how the identity function is defined.

Maybe I read your post wrong. You could assume that, in such a semantic function, normal forms are those terms which are mapped to themselves.

However, wouldn't I want to somehow specify the *effect* that a normal form would have if it were applied to some expression?

In a closed world language (say lambda calculus), that would be known since that knowledge is in the semantic function.

In a language that somehow modifies an outside world, that could be easily defined by assuming an extra argument (a syntactic representation of the state of the world) in the semantic function.

In a closed world language (say lambda calculus), that would be known since that knowledge is in the semantic function.

So you are saying that the "semantic object" (even if it has a syntactic representation that is the same as the syntactic object we are investigating) does not have a meaning on its own, but its semantics can only be understood together with the semantic function? This makes sense to me, I think.

In this case semantic evaluation would just be a kind of identity function.

Definitely not. To muddy the waters for the non-theory people, it would be more like an adjunction, where the mapping within the syntactic set from every form to its normal form is the unit arrow of a monad. ;-)

But what does a normal form mean?

The thing about semantic models is that the buck stops there. Once you have evaluated the syntactic form into the semantic model, you have found its meaning definitively for that system. You are done.

Now, let's say that instead of a semantic set (as pointed out earlier in the thread, this could be some other kind of mathematical object), you choose a semantic set that is the domain for a function that produces some computational output.

To stick with our lambda calculus example, let's say that we want to perform calculations on integers with the lambda calculus. Our syntax is LC notation with integers and every element of our semantic set maps to a string representing an integer if the computation produces a numeric output, or "null" otherwise.

In this set up, a normal form that is a lambda will probably be mapped to "null", since it doesn't output anything.

If instead, we change our semantic set to map to a compiled module that could be linked into some other program, then we might output the machine code that would execute the function the lambda represents.

So formally the "meaning" of a syntactic form is just the element it maps to in the semantic set

What that DOES for you depends on a further mapping (or possible on the structure of the semantic set itself).

I wonder, if it would sound even better in categorial terms.

Definitely, but only for those who already grasp CT. ;-)
My thinking on this is heavily influenced by a CT view of it. (Though I think it is more generally a "higher math" view of things.).

I suspect that this semantic evaluation is some kind of "inclusion" of normal forms into all (well-formed) syntactic forms.

In this particular system, it sort of works out that way, but this may not be the case for all semantic evaluations.

What I cannot understand, how domains (Scott's?) fit into this picture?

Imagine that our semantic set is equipped with the structure of a domain. Some of our syntactic forms will map to structures in the semantic set with particular domain theoretic properties.

Functorial Semantics of Algebraic Theories is Lawvere's thesis. A while back it was announced that it was going to be republished online, but I couldn't find it at that time. This thread reminded me of it, it is now available. Here is a brief summary of the thesis.

On the horizontal arrow in the diagram on page 76 there's some tiny morse code saying "paul". Anyone knows what that's about?