| 词条 | Geometry of interaction |
| 释义 |
The Geometry of Interaction (GoI) was introduced by Jean-Yves Girard shortly after his work on linear logic. In linear logic, proofs can be seen as various kinds of networks as opposed to the flat tree structures of sequent calculus. To distinguish the real proof nets from all the possible networks, Girard devised a criterium involving trips in the network. Trips can in fact be seen as some kind of operator{{Clarify|date=December 2010}} acting on the proof. Drawing from this observation, Girard described directly this operator from the proof and has given a formula, the so-called execution formula, encoding the process of cut elimination at the level of operators. One of the first significant applications of GoI was a better analysis[1] of Lamping's algorithm[2] for optimal reduction for the lambda calculus. GoI had a strong influence on game semantics for linear logic and PCF. GoI has been applied to deep compiler optimisation for lambda calculi.[3] A bounded version of GoI dubbed the Geometry of Synthesis has been used to compile higher-order programming languages directly into static circuits.[4] References1. ^{{Cite book | last1 = Gonthier | first1 = G. | last2 = Abadi | first2 = M. N. | last3 = Lévy | first3 = J. J. | doi = 10.1145/143165.143172 | chapter = The geometry of optimal lambda reduction | title = Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '92 | pages = 15 | year = 1992 | isbn = 0897914538 | pmid = | pmc = }} 2. ^{{Cite book | last1 = Lamping | first1 = J. | chapter = An algorithm for optimal lambda calculus reduction | doi = 10.1145/96709.96711 | title = Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90 | pages = 16 | year = 1990 | isbn = 0897913434 | pmid = | pmc = }} 3. ^{{Cite book | last1 = Mackie | first1 = I. | chapter = The geometry of interaction machine | doi = 10.1145/199448.199483 | title = Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '95 | pages = 198 | year = 1995 | isbn = 0897916921 | pmid = | pmc = }} 4. ^Dan R. Ghica. Function Interface Models for Hardware Compilation. MEMOCODE 2011. Further reading
5 : Proof theory|Philosophical logic|Logic in computer science|Semantics|Linear logic |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。