'functional programming'에 해당되는 글 1건

  1. 2009.09.22 Constructive Logic (3)

Constructive Logic

공부 2009.09.22 14:57
일반적인 classical logic에서는 not not A가 A라는게 성립하는데

constructive logic에서는 그게 성립하지 않는다.

그러한 '사실' 은 알고있었는데 왜 그런지는 모르고 있다가

오늘 전산논리 수업덕분에 알게 되었다. 늦게라도 가길 잘한듯.


이유는 '∃'(어떤) 와 'V'(disjunction, or) 때문인데

constructive logic에서는 ∃x 가 존재하는것이 참임을 증명할때

그 x 를 명확히 지정해야하고

A or B 가 참이라는것을 증명하려면

A와 B중에 어떤게 참인지 지정해야 하기 때문이다.


예를들면 (not A) or A 는 classical logic에서는 항상 참이지만

constructive logic에서는 A를 모를 수도 있기 때문에 참이 아니다.


이런 설정은 기존의 classical logic에 비해 상당히 귀찮은 문제들을 만들어내는데,

그럼에도 불구하고 이렇게 하는 이유는

1. constructive logic을 이용한 proof으로부터 program을 추출할 수 있고

2. constructive logic이 classical logic보다 강력(포함)하기 때문이라네.


함수형 프로그래밍 언어에서 보여주는 독특하고 강력한 기능들이

전산논리 수업과 어떻게 연관이 되는지 조금씩 느낌이 오는것 같다.
신고

'공부' 카테고리의 다른 글

Google Summer of Code2010 & CGAL  (0) 2010.03.30
O/R mapping  (0) 2010.02.26
Laplacian Pyramid on GPU  (1) 2010.01.13
Block-based Web Search  (0) 2009.12.06
오토 레포트  (3) 2009.11.04
Constructive Logic  (3) 2009.09.22
Posted by youknow04


티스토리 툴바