교호작용 기하학
Geometry of interaction상호작용의 기하학(GoI)은 장-이브 지라드가 선형 논리에 관한 연구 직후에 도입했다. 선형 논리학에서 증명들은 연속 미적분학의 평평한 나무 구조와는 반대로 다양한 종류의 네트워크로 볼 수 있다. 지라드는 실제 증명망과 가능한 모든 네트워크를 구별하기 위해 네트워크 여행을 포함하는 기준을 고안했다. 사실 여행은 어떤 종류의[clarification needed] 운영자가 증거에 따라 행동하는 것으로 볼 수 있다. 이 관찰에서 도출한 Girard는 증명에서 이 연산자를 직접 설명했으며, 연산자 수준에서 절단 제거 과정을 인코딩하는 소위 실행 공식이라는 공식을 제공했다.
GoI의 첫 번째 중요한 적용 중 하나는 람다 미적분의 최적 감소를 위한 램핑 알고리즘의[2] 더 나은 분석이었다[1]. 고이는 선형논리와 PCF를 위한 게임 의미론적 영향력이 컸다.
GoI는 람다 칼쿨리의 심층 컴파일러 최적화에 적용되었다.[3] 합성의 기하학이라고 불리는 경계 버전의 GoI는 고차 프로그래밍 언어를 정적 회로로 직접 컴파일하는데 사용되어 왔다.[4]
참조
- ^ Gonthier, G.; Abadi, M. N.; Lévy, J. J. (1992). "The geometry of optimal lambda reduction". Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '92. p. 15. doi:10.1145/143165.143172. ISBN 0897914538.
- ^ Lamping, J. (1990). "An algorithm for optimal lambda calculus reduction". Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90. p. 16. doi:10.1145/96709.96711. ISBN 0897913434.
- ^ Mackie, I. (1995). "The geometry of interaction machine". Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '95. p. 198. doi:10.1145/199448.199483. ISBN 0897916921.
- ^ 댄 R. 기카 하드웨어 컴파일을 위한 기능 인터페이스 모델. MEMOCODE 2011. [1]
