| [ KAIST ] in KIDS 글 쓴 이(By): luvbug () 날 짜 (Date): 2002년 11월 27일 수요일 오후 05시 55분 41초 제 목(Title): Re: 일더하기 일은 이의 증명 막상 증명을 빠트렸네요.. 대개 이미 아셨겠지만.. (plus 1 1) = (plus (add1 0)(add1 0)) = (plus (sub1(add1 0))(add1(add1 0))) : def. of plus = (plus 0 (add1(add1 0))) : axiom sub1-add1 = (add1(add1 0)) : axiom of if = 2 누가 도대체 add1, sub1이 머냐고 물으면 피애노의 액셤을 만족하는 successor 함수라고 말하면 되고.. 결국 증명은 대개 간단한데 그 체계를 만드는 작업이 복잡합니다. 이미 이런 연산에 대해 튜링기계도 동등하다는 증명도 있으니까 튜링식의 프로그램으로 증명해도 될테지만 위의 시스템이 훨 간단합니다. 참고로 위의 scheme 형식의 수학체계는 Boyer_Moore가 개발했습니다. |