호어 논리와 커리-하워드 대응관계 사이의 연관성 분석
A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence
1
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
컴퓨터 프로그램과 논리와의 관계는 널리 알려져 있으며, 두 분야가 밀접하게 관련된다는 사실이 자주 언급된다. 반면에 컴퓨터 프로그램과 논리가 구체적으로 어떻게 연관되어 있는가를 배울 수 있는 기회는 많지 않다. 그럼에도 불구하고 컴퓨터 프로그램과 논리 사이의 연관성의 중요성은 매우 강조된다. 다만 그 강조가 한쪽이 다른 한쪽에 도움된다는 정도로 머무는 것이 일반적이다. 예를 들어, 컴퓨터 프로그래밍을 이용하여 논리적 사고를 높인다거나, 논리적 사고를 잘하면 컴퓨터 프로그래밍에 도움된다 등과 같은 주장들이다. 그런데 컴퓨터 프로그램과 논리의 관계는 그 이상이다. 본 논문에서는 컴퓨터 프로그램과 논리의 연관성에 대한 연구를 소개한 후 기존의 연구들 사이의 차이점과 공통점을 밝힌다. 보다 구체적으로는 명령형 프로그래밍 언어로 작성된 프로그램의 건전성을 논리적으로 검증하기 위해 사용되는 호어 논리(Hoare logic)와 함수형 프로그래밍 언어의 기반을 제공한 커리-하워드 대응관계가 본질적으로 동일한 내용을 다른 방식으로 표현한다는 사실을 밝힌다. 논문의 결론에서 호어 논리와 커리-하워드 대응관계에 대한 몇 가지 성질을 언급한다. 또한 이어지는 프로그래밍 언어 교육과 관련된 몇 가지 연구 아이디어를 소개한다.
Abstract
The relation between computer programs and mathematical logic is well known, Although one can easily find comments on the relationship when one reads books and articles about computer programming, it is difficult to find proper materials explaining the relationship in a scientific manner. Nevertheless, people used to mention how important the relationship between computer programs and mathematical logic is. The problem is that it is more focused on the fact that how helpful it is to learn one area in learning the other area. However, there is more than that between computer programs and mathematical logic. In this paper, we introduce some researches about the relationship and show different and common aspects of them. In particular, Hoare logic and Curry-Howard correspondence is compared. Hoare logic was invented for rigorous verification of programs in a C-like imperative programming language, while Curry-Howard correspondence explains the relationship between functional programming language like Haskell and mathematical logic. We show that Hoare logic and Curry-Howard correspondence are essentially the same in the sense that they represent the same things just in different manners. We close the paper with some remarks about Hoare logic and the Curry-Howard correspondence and ideas of further research with respect to teaching and learning programming languages in the university level based on the relationship between logic and programming.
참고문헌 (17)
- G. Boolos, "Computability and logic" (2007), Cambridge University Press
- H. Curry, "Functionality in combinatory logic", Proceedings of the National Academy of Science of the USA, 20(11), pp.584~550 (1934)
- Verification of mathematical proofs by a computer, "N. G. de Bruijn", AUTOMATH, ~ (1967)
- JR. J. G. B. de Queiroz, "The functional interpretation of logical deduction, Advances in Logic 5", pp.2011, Imperial College Press
- R. W. Floyd, "Assigning meanings to programs", Proceedings of the American Mathematical Society Symposia on Applied mathemaics, 19, pp.19~31 (1967)
- J-Y. Girard, "Proofs and Types" (2007), Cambridge University Press
- C. A. R. Hoare, "An axiomatic basis for computer programming", Communications of the ACM, 12(10), pp.576~580 (1969)
- M. Huth, "Logic in Computer Science: Modelling and reasoning about systems" (2004), Cambridge University Press
- G. Hutton, "Programming in Haskell" (2016), Cambridge University Press
- 이계식, "암호화 보안 프로토콜의 정형명세", 한국지식정보기술학회 논문지, 14(6), pp.711~718 (2019), 한국지식정보기술학회[DOI]
- P. Martin-Löf, "Intuitionistic type theory:Notes by Giovanni Sambin of a series of lectures given in Padua", Bibliopolis, ~ (1984)
- B. Nordström, "Programming in Martin-Löf’s type theory" (1901), Oxford University Press
- S. Thompson, "Type theory and functional programming" (1991), Addison-Wesley
- J. M. Wing, "Computational thinking", Communications of the ACM, 49(3), pp.33~35 (2006)
- J. M. Wing, "Computational thinking and thinking about computing, Philosophical Transaction of the Royal Society A:Mathematical", Physical and Engineering Sciences, 366, pp.3717~3725 (2008)
- J. M. Wing, "Computational thinking’s influence on research and education for all", Italian Journal of Educational Technology, 25(2), pp.7~14 (2017)
- 양권우, "짝 프로그래밍을 이용한 소프트웨어 교육이 학습동기 및 학업성취도에 미치는 영향", 한국지식정보기술학회 논문지, 15(1), pp.57~65 (2020), 한국지식정보기술학회[DOI]