[%] 나도 자연수 성질 증명하다가 증명언어뽕 맞았는데

[다믜(damhiya)]

이게 존나 재밋긴 함 ㅋㅋ

[익명(223.38)]

응애

[black7375(221.168)]

페아노 공리계 말하는거임?

[다믜(damhiya)]

자연수의 정의를 바탕으로 +, * 등 산술 연산이 만족하는 대수법칙들을 증명하는거임. associativity, commutativity, distributivity 같은것들

[black7375(221.168)]

코드 이쁜데 넘 빡세다ㅠㅠ

[다믜(damhiya)]

근데 "자연수의 정의"는 조금씩 다를 수 있음. 추상적 대상인 자연수를 다룰 때는 페아노 공리계를 쓸거고, 집합론으로 자연수를 구성했으면 von Neumann numeral 같은걸 씀

[다믜(damhiya)]

증명언어에서는 inductive data type으로 자연수를 정의함. 하스켈로 표현하면 data Nat = Zero | Suc Nat

[black7375(221.168)]

정의하는 방법이 생각보다 디게 많네. 증명쪽 하는 사람들은 대단한듯.

[다믜(damhiya)]

저거는 내가 증명언어 사용법을 제대로 모를때 작성한 코드라 읽기 거의 불가능하고, 저것 보다는 훨씬 읽기 쉽게 작성할 수 있음

[익명(223.38)]

폰 노이만이 여기서도 나오네

[익명(218.39)]

이런거 하면 어디 취업하나요

[익명(125.251)]

ㄹㅇ 잼긴한데 이게 제일 궁금스

[black7375(221.168)]

보통은 대학원행 아닐까..?

[다믜(damhiya)]

형식증명을 사용하는 분야는 일부 수학계, 소프트웨어 검증 정도 알고 있음

[익명(223.38)]

무슨 언어임?

[다믜(damhiya)]

저거는 idris 1 이고 지금은 idris 2 나옴