3
$\begingroup$

I would like to learn a bit about the connections between Gentzen's discoveries in the 30's related to proof theory and, in particular, his sequent calculus, and the later development of computer languages. Could anyone elaborate a bit on that? I am particularly interested in knowning whether one can find in Gentzen some predecessor of a pointer to a memory address. If so, in which specific form?

Thanks in advance.

$\endgroup$
  • $\begingroup$ I'm voting to close this question as off-topic because it belongs to hsm.stackexchange.com. $\endgroup$ – José Carlos Santos Dec 29 '17 at 10:30
  • $\begingroup$ I have just posted it there as well. Pôrem, é um bocado triste o senhor criticar o minha pesquisa, en tanto é claro que as rúbricas disponiveis neste foro sao perfectamente adecuadas ao tema (proof theory, etc, etc). Cumprimentos. $\endgroup$ – Javier Arias Dec 29 '17 at 10:36
  • $\begingroup$ I don't think it's related to history. In my opinion it's perfectly right to ask that in math.stackexchange. The asker seems to be interested in technical details. $\endgroup$ – Boris Dec 29 '17 at 10:37
  • $\begingroup$ I should maybe clarify why i am asking this. Back in time , a long time ago, I was familiar with formal semantics (Montague Grammar, Curry's Lambda calculus, etc). Later on, while living in Germany, I became acquainted with Gentzen's work. I am now finishing a paper on the differences between the notion of trace in sifferent syntactic frameworks (basically, contrasting Chomsky with his former master Zellig Harris). The thing is, Marcel Gross considered in 1979 that Chomsky was just using a pointer for memory. And I want to know if that is already in Gentzen. I do not recall. $\endgroup$ – Javier Arias Dec 29 '17 at 10:42
  • $\begingroup$ I know that tyhe Curry_Howard correspondence allows from the, say, translation from one field to another.....and I am aware of the influence of Hilbert's and Carnap¡s progamm in linguistics, and, to a much lesser degree, that of Gentsen. But I have good reasons to suspect Gentzen is some kind of hidden influence. That is why it is very improtant for me to know about the predecessors of pointers in a memory address in that context. I hope that helps clarify my quesiton. It is not just a merely curiosity question, but part of a very sound line of argumentation. $\endgroup$ – Javier Arias Dec 29 '17 at 10:46
4
$\begingroup$

According to your previous comments it seems that you already know about the Curry-Howard isomorphism and the Lambda Calculus but I still wrote a general answer to fit the original question.

I don't think I perfectly provided what you want but I hope it can lead to what you're looking for.

Curry-Howard The main link between Gentzen discoveries and Computer Science is the Curry-Howard isomorphism.

It tells us that we have a deep relation between mathematical proofs and computer programs. If you scroll down on the Wikipedia page, you can see several tables with some correspondences. The role of Gentzen's works is fundamental :

  • Programs using the cut rule behaves like programs we can evaluate
  • Proofs without cuts are similar to programs in normal form (fully evaluated)
  • The cut elimination theorem actually behaves like the execution of programs

Note that by "program" we usually mean Functional programs in the context of Curry-Howard.

Linear Logic Gentzen's works led to a very large number of new fields (especially in Computer Science). For instance, Jean-Yves Girard invented/discovered Linear Logic which you can get from the classical sequent calculus by restricting the structural rules. Moreover, Linear Logic handles cut elimination in an amazing way.

Categorical Grammars If you're interested in Linguistics there're also some interesting applications I don't really know/understand. For instance the Lambek Calculus which is related to Lambda-Calculus and Linear Logic.

Ludics Ludics is a quite new and almost unknown formalism suggested by Girard where Logic is founded on some ideas coming from Gentzen (pioneer ideas on Game Semantics), Linear Logic and a philosophy of interaction. Suprisingly, it seems to be connected to linguistics. You may be interested in the works of Alain Lecomte, Myriam Quatrini, Samuel Tronçon, Marie-Renée Fleury. See for instance this and this. He also wrote a whole book on Ludics and Linguistics called "Meaning, Logic and Ludics". I don't know yet if it's related to memory adresses but Ludics has an idea of "location" and "addresses".

Some references I can suggest :

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thanks a lot for yous reply, @Boris Eng I will study it carefully and come back to you if I still have questions. By the way, I mistakenly mentioned a given Marcel Gross.....I meant Maurice Gross, of course. $\endgroup$ – Javier Arias Dec 29 '17 at 11:11
  • $\begingroup$ @JavierArias If you're more interested in Linguistics than Proof Theory or Computer Science maybe the book "Meaning, Logic and Ludics" wrote by Alain Lecomte would be the best choice (Note : I already sended this message but I misspelled your name so I wasn't sure whether you receveid it or not...). $\endgroup$ – Boris Jan 7 '18 at 8:01
  • $\begingroup$ Thanks, Boris..I got it. $\endgroup$ – Javier Arias Jan 9 '18 at 10:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.