Lambda the Ultimate

inactiveTopic A gentle introduction to TLG, the Curry-Howard correspondence, and cut-elimination
started 10/11/2003; 2:58:16 AM - last post 10/16/2003; 5:44:29 PM
Ehud Lamm - A gentle introduction to TLG, the Curry-Howard correspondence, and cut-elimination  blueArrow
10/11/2003; 2:58:16 AM (reads: 6300, responses: 6)
A gentle introduction to TLG, the Curry-Howard correspondence, and cut-elimination
Barker Chris. A gentle introduction to Type Logical Grammar, the Curry-Howard correspondence, and cut elimination

This paper aims to give an introduction to Type Logical Grammar (TLG) for the general linguist who may not have a background in logic or proof theory. This paper will briefly describe the logical heritage of TLG, sketch a simple TLG analysis, convey the spirit of the Curry-Howard result, discuss Gentzenís famous cut-elimination result, and motivate multimodal extensions of Lambekís logic.

A short introduction to some of the same topics discussed in Girard's book plus an introduction to Type Logical Grammar for those who are interested in linguistics.


Posted to theory by Ehud Lamm on 10/11/03; 2:59:14 AM

Marc Hamann - Re: A gentle introduction to TLG, the Curry-Howard correspondence, and cut-elimination  blueArrow
10/13/2003; 5:18:45 AM (reads: 323, responses: 3)
A nice introduction (though it distracted me from reading Girard's book ;-) )

I'm starting to wonder if I like these pithy introductions because I've slogged through longer, more detailed versions, or in spite of them.

Both Girard and Barker manage to get across the essence of these techniques without all the preamble that otherwise seems to be de rigeur, and I'm starting to feel that maybe some of these other texts are unnessarily verbose.

But is this an illusion created by my prior reading?

I wonder if anyone for whom these ideas are newer has an opinion?

Ehud Lamm - Re: A gentle introduction to TLG, the Curry-Howard correspondence, and cut-elimination  blueArrow
10/13/2003; 6:10:48 AM (reads: 329, responses: 2)
I am not sure I understand what you are asking.

Reading these sort of texts (the short introductions) I always feel a bit cheated, since I know important technical details are missing. But I still like to read texts in this style.

I know many who find intros and tutorials really ugly, and are not willing to tolerate them, because they demans all the details-all the time. These are usually people with math background.

Marc Hamann - Re: A gentle introduction to TLG, the Curry-Howard correspondence, and cut-elimination  blueArrow
10/13/2003; 11:50:08 AM (reads: 341, responses: 1)
I know many who find intros and tutorials really ugly, and are not willing to tolerate them, because they demans all the details-all the time.

My feeling is the opposite. Having read the "long version" with all the details left in, I feel that I was cheated when I could have gotten a pretty good idea from a well-written tutorial. ;-)

My question is whether or not this is an illusion: if I hadn't "already done the work", would I really understand anything in the tutorial?

I think I know the answer, since I remember reading a few intro tutorials in Category Theory before I had a solid abstract algebra background, and I couldn't make head or tail of it (though it seemed cool. ;-)).

Now the same texts seem like pleasant little intro tutorials, and I wonder why they weren't easy the first time. ;-)

Ehud Lamm - Re: A gentle introduction to TLG, the Curry-Howard correspondence, and cut-elimination  blueArrow
10/13/2003; 12:16:30 PM (reads: 349, responses: 0)
I firmly believe in the power of popular and semi-popular writing. I think that it is crucial to understand the contaxt, goals and so on, in order to really understand the value and conceptual framework of any really insightful work.

Thr crucial thing, however, is that someone who really grasps these essential elements write the tutorial or intro. Beacuse by skipping the details, they make it impossible for you to recreate the insight, if it is not present.

Frank Atanassow - Re: A gentle introduction to TLG, the Curry-Howard correspondence, and cut-elimination  blueArrow
10/16/2003; 4:45:28 AM (reads: 250, responses: 1)
Ehud: I know many who find intros and tutorials really ugly, and are not willing to tolerate them, because they demans all the details-all the time. These are usually people with math background.

Marc: My feeling is the opposite. Having read the "long version" with all the details left in, I feel that I was cheated when I could have gotten a pretty good idea from a well-written tutorial. ;-) My question is whether or not this is an illusion: if I hadn't "already done the work", would I really understand anything in the tutorial?

I think these two dichotomous observations are really important issues in pedagogy. As you may know, I'm sort of gathering material and ideas for a book, and I'm constantly struggling to reconcile the poles: `be precise because the devil is in the details' and `be succinct because the meaning transcends the details'. One thing I like about category theory is that you can be simultaneously precise and succinct, but I can't assume CT because it's part of what I'm try to teach.

The best way I know to approach this problem is to begin a discussion by discussing the underlying meaning using examples, and then to make it rigorous. So, instead of starting with definitions, you start with some examples and point out a common thread or shared pattern which motivates factoring that pattern out into an autonomous notion. For example, before introducing monoids you bring up examples like numerical arithmetic and string concatenation.

I guess that seems obvious, but where I always run into trouble is establishing sufficient foundation to make the examples themselves precise and intelligible. Writing a book on these topics in some sense involves finding a linear ordering for algebraic structures, which goes from least to most complex.

Strictly speaking, such an ordering is artificial, but by knowing your audience you can find an ordering which seems `natural' and intelligible for them; for example, with programmers it's natural to start with syntax (free monoids, say) before discussing semantics (monoids in general). The thing is, later you have to be careful to go back and disabuse them of the notion that the ordering you chose is the only possible one.

When I pursue this idea, though, I tend to find myself looping. :) I think this is sort of an inevitable consequence of discussing mathematics, because of the chicken-egg problem that comes with universality. To be precise about mathematics you need to employ logic; but to be precise about logic you need to discuss its mathematical semantics. Finding the right `on-ramp' onto this roundabout, where you can minimize the chance of confusion by co-opting your audience's existing knowledge, is to me one of the most difficult bits.

Marc Hamann - Re: A gentle introduction to TLG, the Curry-Howard correspondence, and cut-elimination  blueArrow
10/16/2003; 5:44:29 PM (reads: 256, responses: 0)
I think this is sort of an inevitable consequence of discussing mathematics, because of the chicken-egg problem that comes with universality.

I think one of the weaknesses with mathematical pedagogy is that there is a very strong tendency to "erase the path" that led to an insight or generalization, and just present the finished product.

"Here is a theorem, learn it, spit it back, then here is another theorem that builds on it...."

There can be a kind of pleasure in this, but most people who are passionate about math seem to be driven to solve compelling problems. It is usually on a quest to solve a particular problem that new math is discovered, and new universals proven.

So I have often wondered if this might not be an equally compelling approach to pedagogy: start with a problem (preferably one of real significance in the chosen sub-field of math) and follow it through the inspirations, blind alleys, varied approaches that lead to the development of the various theorems and lemmas.

When that is done, show how the new knowledge is applicable to seemingly unrelated problems.

I think that is one of the things that I like about the Girard book; he infuses each section with a motivation for a development based on the problems it solves and the problems it creates. This helps the reader to appreciate the power of the great mathematical ideas, and to understand the thinking that leads to the next development.