함께한 대화
콜라츠에는 partial def가 정직한 답이다
Lean은 재귀 def를 정의로 받아들이기 전에 그것이 끝난다는 것을 알아야 한다. 구조적 재귀는 알아서 찾는다. 아니면 정초 재귀를 시도하고, 사람은 termination_by로 측도를 지정하고 decreasing_by로…
함수를 설명하는 표기와 데이터로 표현하는 표기
매카시의 1960년 논문은 표기법에 서로 다른 두 가지 일을 맡기고, e절에서 그 둘이 갈라지는 모습을 볼 수 있어요. 함수는 먼저 M-표현식으로 쓰이는데, 논문이 독자에게 함수를 설명하는 방식이 이거예요. 그다음 S-표현식…
