Programming languages should have a tree traversal primitive https://lobste.rs/s/ctopbt #programming
https://blog.tylerglaiel.com/p/programming-languages-should-have

洪 民憙 (Hong Minhee)
@hongminhee@hackers.pub · 397 following · 266 followers
Hi, I'm who's behind Fedify, Hollo, BotKit, and this website, Hackers' Pub!
Fedify, Hollo, BotKit, 그리고 보고 계신 이 사이트 Hackers' Pub을 만들고 있습니다.
Website
- hongminhee.org
GitHub
- @dahlia
Hollo
- @hongminhee@hollo.social
DEV
- @hongminhee
velog
- @hongminhee
Qiita
- @hongminhee
Zenn
- @hongminhee
Matrix
- @hongminhee:matrix.org
X
- @hongminhee
어디 RFC 문서 의존 관계 정리된 거 없나요?
@curry박준규 혹시 말씀하신 의존 관계라는 것이 참조라는 것과는 좀 다른 걸까요? 같은거라면 요런 기능도 있는 것 같아요
어디 RFC 문서 의존 관계 정리된 거 없나요?
UI 개발을 어렵게 만드는 가장 큰 요인은 테스트 아닐까... 비즈니스 로직이나 상태에 대한 유닛 테스트는 UI 차원에서 커버리지가 너무 낮다. E2E 테스트는 사이클이 너무 크고, 스냅샷 테스트는 시각적인 차이까지 캐치하지는 못한다.
10만년 만에 오픈소스 기여해봄. 러스트로 UI 개발해본건 처음인데 언어보단 UI가 더 까다로웠다 https://github.com/faiface/par-lang/pull/42
왼쪽 나 오릉쪽 홍
각자 조용히 할 일 중인데
거기서 거기임
웃겨
뒤늦은 서울숲하스켈 조교 후기: 왠지 모르겠는데, 다들 운동을 열심히 하시는지 몸이 굉장히 좋으셨다. 건강한 신체에 건강한 정신이 깃든다를 실천하고 계신 분들이었다.
...는 농담이고(근데 사실입니다), 커리큘럼이 내가 상상하던 방향이랑은 꽤 달라서 흥미로웠다.
마지막 회차에 하스켈로 웹서버를 띄우는 것을 목표로 진행중이었는데, 이를 위해 Monad Transformer(Monad는 진즉에 해치우고), Tagless Final, Lens를 모두 소개한 상태였다. 근데 저 개념들이 '왜 하스켈에선 이거 안 돼요? 왤케 불편해요?' 같은 질문을 회피하지 않으려면 꼭 가르쳐야 하는 부분들이긴 하다. 가령, 'Monad만 배우면 이제 하스켈에서 명령형 코딩 할수 있다'라는 이야기가 이론상은 맞는데, Monad Transformer나 Algebraic Effect 같은거 안쓰면 웹사이트등 실제로 쓸모있는 프로그램을 사실상 짤수가 없다. 그래서 가르치긴 해야한다.
문제는 저걸 다 가르치려면 상당히 빡셀테니, 나는 만약에 내가 하스켈 부트캠프를 한다면 일단은 저런걸 회피하고 하스켈의 멋진 부분에 집중하는 커리큘럼을 짜야겠다고 그동안 생각했었다. 근데 또 이건 어찌보면 기만이기도 하다. 그런데 서울숲하스켈에서는 어찌저찌 다들 따라오도록 구성을 잘하신것 같다 하스켈을 이질적인(긍정적으로든 부정적으로든) 프로그래밍 언어로 소개하는게 아니라, 언젠가 본인의 작업에 활용할 언어의 후보로 올리게끔 하려면 저런 내용들을 다 다뤘어야 할것이다.
암튼 그동안 수고많으셨습니다. @eunmin은민
#ActivityPub "The Good, the Bad and the Ugly" is a good article by @dominikDominik Chrástecký - Blog
https://chrastecky.dev/technology/activity-pub-the-good-the-bad-and-the-ugly
The two mentioned examples in "The Bad" are long-time issues that were also discussed at #SocialHub. I just responded to one of them on the forum..
The #Mastodon Update(Note) quirk. https://socialhub.activitypub.rocks/t/update-note-quirk/4545/14
The other one is around Direct Messages which are a hack (a Note with special sauce). #LitePub specifies ChatMessage object type here, which is the intended way to extend the protocol. #FEP
이번 변경으로 홈 화면에 추가
로 해커즈펍을 설치하면 android, iOS 양쪽 모두, 단독 앱인 것 같은 느낌으로 쓸 수 있게됩니다. 다만, 이메일의 로그인 링크가 설치 된 쪽으로는 안열리는 문제가 있으니 미리 로그인 된 상태에서 설치를 하셔야 곤란하지 않습니다.
저도 비슷한 생각인데, Haskell이나 Rust는 코너 케이스를 다루지 않고는 컴파일도 못 하게 금지하는 경우들이 꽤 많고 (그래서 좋은 언어지요), 빠르게 해피 패스만을 검증하고 싶을 때는 Python 같은 널널한 언어(복잡하고 규모가 큰 소프트웨어를 만들 때는 나쁜 언어가 되지요)가 쉽게 느껴질 수 있다고 생각합니다. 즉, Haskell이나 Rust가 어렵다고 말할 때의 어려움은 개념적 이해의 난도라기 보다는 시행착오의 커브의 경사를 얘기하는 것 같아요.
비슷한 측면에서 저는 Python의 들여쓰기를 강제하는 문법이 프로그래밍 초심자에게 좋은 습관을 처음부터 정착시키는 데에는 일조할 수 있겠지만, 결코 쉽지는 않다고 생각합니다.
RE: https://hackers.pub/@bgl/01967f97-67ab-7a98-a6e5-16cb3ef31856
@hongminhee洪 民憙 (Hong Minhee) 약간 딴 얘긴데, 저는 들여쓰기가 그냥 안좋은 문법요소 같습니다. 코드의 복붙을 unreliable하게 만들어버려서요. 반대로 space sensitive한 문법은 괜찮다고 생각합니다. 복붙시 문제가 생겨도 스페이스 한번 치면 해결되니까요. 들여쓰기 대신에 {} 쌍을 쓰게 만들되, 에디터에서 보여줄때 어떻게 알아서 예쁘게 보여주는게 낫다고 생각해요.
러스트가 어렵다는 이야기가 숙고없이 재생산 되는거 같긴 합니다. 제가 러스트를 별로 안써봐서 실제로 얼마나 어려운진 모르겠습니다.
그런데 말씀하신 모나드, 트레잇, 오너십 등의 개념들과 클래스는 좀 차이가 있다고 생각합니다. 그러니까 자바에서 클래스 때문에 어떤 코드를 못짜게 되진 않잖아요? 자바를 하면서 클래스를 제대로 쓰지않고도 뭔가 만들순 있습니다. 반면 전자의 개념들은 잘못된 코드를 짜는걸 막고, 초보자 입장에서 뭔가 하고싶은게 있는데 그게 금지되는 상황에서 어렵다는 느낌을 (필요이상으로 크게) 받을수 있다고 생각합니다.
에디터 뭐 쓰세요...?
Vi...
vim 이요??
...sual Studio Code
#뻘글로타임라인메우기협회
fresh에서 아직 플러그인이 정적파일을 추가를 못한다고 확인을 했고, 이것에 대한 PR이 올라와 있으니, 머지되고 퍼블리시 되고나면 직접 컴파일러를 실행해서라도 Service worker, PWA 플러그인을 만들 수 있을 것 같다.
https://moreal.dev/blog/review-learning-zig/
- 요근래 안 하던 직접 메모리 할당 및 해제를 Zig하면서 해보니 Bun에서 왜 메모리 누수가 나는지 이해가 가는 부분이었다. (메모리 관리 잘 하기 어려운 것 같다)
- 컴파일 타임 코드 작성하기 편한 것은 좋았다. (comptime)
- 회고를 하며 내가 공부할 때 방황한 과정을 돌이켜 보는 것이 좋았다. "언어 철학 먼저보기"와 "표준 라이브러리에서 Write, Read 추상화하는 방식 참조하기" 정도를 먼저 하면 좋겠다는 교훈(?)을 얻었다.
- 위 글에 애자일 이야기 글 링크할 때, 애자일 이야기 검색 가능하게 만든거 잘 써서 좋았다 :D
Zig 공부 회고 |
moreal.dev
Link author: Lee Dogeon@moreal@hackers.pub
New blog post! Let's categorize our deps better with @pnpm.io catalogs!
antfu.me/posts/catego...
Categorize Your Dependencies
서울 하스켈숲 워크숍 완주했습니다...! @eunmin 님의 친절한 설명과 세심한 준비에 감사합니다 🙇
Huge respect 🫡
Deno Temporal이랑 Temporal 폴리필들 간에 타입 호환은 잘 되는구만
- Zig 라이브러리 짜기
- 이력서 쓰기
Rust로 작성한 JPEG XL 디코더, jxl-oxide의 버전 0.12.0을 릴리스했습니다. https://github.com/tirr-c/jxl-oxide/releases/tag/0.12.0
CMYK 프로파일 등 복잡한 ICC 프로파일을 지원하기 위해 기존에 사용하던 Little CMS 2 (lcms2) 에 더해, Rust로 작성된 색 관리 시스템인 moxcms 지원을 추가한 것이 주요 변경사항입니다. CLI 툴의 기본 CMS는 아직 lcms2이지만 --cms moxcms
옵션으로 moxcms를 사용할 수 있습니다.
jxl-oxide 스스로도 간단한 ICC 프로파일 해석과 합성을 할 수는 있는데요, 아무래도 ICC 프로파일 파서를 관리하는 게 번거롭다 보니(...) 앞으로 이쪽 부분도 moxcms로 교체할까 하는 생각을 하고 있긴 합니다.
Rust로 작성한 JPEG XL 디코더, jxl-oxide의 버전 0.12.0을 릴리스했습니다. https://github.com/tirr-c/jxl-oxide/releases/tag/0.12.0
CMYK 프로파일 등 복잡한 ICC 프로파일을 지원하기 위해 기존에 사용하던 Little CMS 2 (lcms2) 에 더해, Rust로 작성된 색 관리 시스템인 moxcms 지원을 추가한 것이 주요 변경사항입니다. CLI 툴의 기본 CMS는 아직 lcms2이지만 --cms moxcms
옵션으로 moxcms를 사용할 수 있습니다.
근데 백엔드 구현하기 GraphQL이 REST보다 쉽지 않나?? (강성GQL교도)
Protected Route에 대해 좀 생각을 더 해봤는데, 난 처음엔 React Native Navigation에서만 쓰는 해괴한 방식인줄 알았다. 근데 좀더 생각해봐도 별로긴하다. 라우터란게 결국 전체 상태중에 path만 별도로 관리해주는 건데,
app :: State -> View
--- router 도입
app :: (Path, State) -> View
--- Protected Route
app :: State -> Path -> View
여기서 대충 말해서 Path -> View
가 라우터라 할수 있겠다. Protected Route는 State로부터 라우팅 룰을 동적으로 바꿔버리는 방식이다.
근데 애초에, 라우팅 룰을 정적인 정보로 만들고(즉 ->
가 아님) 활용할게 아니라면 라우터를 쓸 이유가 뭘까? 그냥 Path
를 일반적인 다른 상태와 똑같이 취급해도 상관없을 것이다. 근데 react-router도 그렇고 애초에 라우팅 룰을 정적인 정보로 알수있는 설계로 되어있지가 않다. Tanstack Router는 예외다.
근데 이러면 그냥 XState 쓰면 되지 않나? 상태/전이에 대한 정적인 정보를 가지고 있고, 또 React Native에서의 라우팅에는 화면 전환이 단순한 Path 변경이 아닌 어떻게 화면을 전환 시킬지(애니메이션 등)도 기술해야하는데, 이 역시 XState 이벤트로 넣으면 된다.
논리와 저수준(Low-level) 자료 표현(Data representation)에 대한 글 2 편 중 첫째 편입니다. "논리적이 되는 두 가지 방법"이라는 부제로 논리적 증명을 하는 두 방법론에 대해서 다뤄보았습니다. 이 중 하나의 방법론이 둘째 편의 핵심이 될 예정입니다.
洪 民憙 (Hong Minhee) shared the below article:
논리적이 되는 두 가지 방법 - 논리와 저수준(Low-level) 자료 표현(Data representation) (2 편 중 1 편)

Ailrun (UTC-5/-4) @ailrun@hackers.pub
논리적인 말?
언제 어떤 문장이 "논리적이다"고 할 수 있을까? 일상적으로는 우리는 이를 남용해 의미가 있어 보이는 것을 "논리적이다"라고 수식하고는 한다. 그러나 필자는 이 남용이 "논리적"이라는 표현을 너무 가볍게 보고 있는 것이라 말하겠다. 어떤 것이 진정 논리적이기 위해서는 의미가 있는 것은 물론이거니와 최소한 다음의 두 조건을 더 만족해야한다.
- 몇몇 가정으로부터 그것을 증명해야 한다.
- 증명에 쓰인 체계가 모순을 보일 수 없어야 한다.
이 글에서는 이 중 1 번을 중점으로 설명하여 "좋은 가정 아래" 어떤 것이 논리적임을 증명하는 두 방법에 대해 다루어 볼 것이다. 두 방법 중 하나는 함수형 언어로 쓰인 프로그램과 유사한 구조를 가지며 나머지 하나는 일반적인 함수형 언어와는 상이한 구조를 가진다. 이 중 두번째 방법에 대해서는 (약간의 부정행위를 하면…\ldots) 2 번을 간단하게 보일 수 있기 때문에 이 또한 다룰 것이다.
논리적 증명의 대상
어떻게 어떤 것이 논리적이라는 걸 증명할 수 있는 지에 설명하기에 앞서 짚고 넘어가야 할 매우 중요한 요소가 하나 있다. 바로
질문
무엇이 논리적이냐?
는 것이다. 이 글에서는 철학적인 복잡도를 덜기 위해 이 대상을 다음과 같이 단순히 설명할 것이다.
논리적일 수 있는 대상은 명제(proposition)에 대한 판단(judgment)이다.
여기서 명제는 다음과 같이 정의되는 대상이다.
- 단위 명제(Atomic Proposition) AA는 명제이다.
- 참 명제(True Proposition) ⊤\top은 명제이다.
- 거짓 명제(False Proposition) ⊥\bot은 명제이다.
- 명제 PP와 QQ가 있을 때, P∧QP \land Q(PP 그리고 QQ)는 명제이다.
- 명제 PP와 QQ가 있을 때, P∨QP \lor Q(PP 또는 QQ)는 명제이다.
- 명제 PP와 QQ가 있을 때, P→QP \to Q(PP라면 QQ)는 명제이다.
여기서 단위 명제란 우리가 선택한, 더이상 세밀하게 분석하지 않을 논리적인 최소 단위이다. 예를 들어 1+1=21 + 1 = 2와 0+2=30 + 2 = 3을 단위 명제로 두었을 때[1] 다음과 같은 것들이 명제이다.
- ⊤\top
- 1+1=21 + 1 = 2
- (1+1=2)∧(0+2=3)(1 + 1 = 2) \land (0 + 2 = 3)
- (0+2=3)→⊥(0 + 2 = 3) \to \bot
- ⊤→⊥\top \to \bot
그렇다면 판단이란 무엇인가? 우리가 명제에 가지는 논리적 태도이다. 이 글에서는 다음과 같은 판단만을 이야기 할 것이다.
P trueP\ \texttt{true}, 즉 명제 PP가 참이다.
이를 "진리 판단"("truth judgment")이라고 한다. 좀 더 엄밀히는 다음과 같이 가정을 포함한 판단에 대해 다룰 것이다.
- Γ⊢P true\Gamma \vdash P\ \texttt{true}
이 판단은 어떤 진리 판단의 나열 Γ\Gamma을 가정했을 때 명제 PP가 참이라고 말하는 판단이다. 이를 "가정적 판단"("hypothetical judgement")이라고 한다. 또한 여기서 Γ\Gamma를 "가정"("hypothesis") 혹은 "전건"("前件", "antecedent")이라고 하고, P trueP\ \texttt{true}를 "귀결("consequent") 혹은 "후건"("後件", "succedent")이라고 한다. 요약하자면 이 절의 핵심 질문
질문
무엇이 논리적일 수 있는 대상이냐?
에 대한 답은 다음과 같다.
답
명제의 진리에 대한 가정적 판단이 논리적일 수 있는 대상이다.
진짜 논리적이 되는 방법 1 - 자연 연역(Natural Deduction)
이제 어떤 가정적 판단이 논리적인지 증명하는 한 방법에 대해서 알아보자. 우선 PP가 참이라는 판단이 가정 중 하나라면 당연히 그 가정 아래에서는 PP가 참이라고 판단할 수 있을 것이다. 이를 간략하게 표현한 규칙(rule)이
이다. 이 규칙 표현은 줄 위의 것들을 전제(premise)로 줄 밑의 결론(conclusion)을 추론(infer)해 낼 수 있음을 말한다. 전제에 쓰여있는 P true∈ΓP\ \texttt{true} \in \Gamma는 P trueP\ \texttt{true}가 가정의 나열 Γ\Gamma에 포함되어 있음을 말한다. 또한 줄 옆에 써져있는 "hyp"는 이 추론 규칙(inference rule)의 이름으로서 가정(hypothesis)을 사용한다는 것을 나타낸다.
이런 추론 규칙을 명제를 만드는 각각의 방법에 대해 정의할 수 있다. 참 명제 ⊤\top에 대해서는
라는 규칙을 줄 수 있다. 이 규칙 I⊤\text{I}\top은 어떤 Γ\Gamma를 가정하든 참 명제는 참이라고 판단할 수 있다는 규칙이다. 여기서 이름의 I\text{I}는 참 명제를 결론에 소개(Introduce)하는 규칙이라는 뜻이다. 대칭적으로 거짓 명제에 대해서는
라는 규칙을 줄 수 있다. 이 규칙 E⊥\text{E}\bot은 어떤 가정들 Γ\Gamma로 부터 거짓 명제가 참이라고 판단했다면 그 가정들 아래에서는 아무 명제나 참이라고 판단할 수 있다는 규칙이다[2]. 여기서 이름의 E\text{E}는 우리가 거짓 명제가 참임을 결론으로 가지는 전제에 도달했을 때 그 결론을 제거(Eliminate)하여 다른 결론에 도달할 수 있도록 하는 규칙이라는 뜻이다.
⊤\top과 ⊥\bot을 제외한 명제를 만드는 방법들은 이 두 종류의 규칙(I\text{I} 규칙과 E\text{E} 규칙)을 모두 가진다. P∧QP \land Q의 경우는 다음과 같다.
I∧\text{I}\land는 Γ\Gamma를 가정하여 PP와 QQ 각각이 참이라 판단했다면 같은 가정에서 P∧QP \land Q도 참이라고 판단할 수 있다는 규칙이다. 반대로 E∧\text{E}\land는 Γ\Gamma를 가정하여 P∧QP \land Q이 참이라 판단했고 Γ\Gamma에 더해 P trueP\ \text{true}와 Q trueQ\ \text{true}를 가정했을 때 RR이라는 명제가 참이라고 판단할 수 있다면 Γ\Gamma만 가정하고도 RR이 참이라고 판단할 수 있다는 뜻이다. P∨QP \lor Q와 P→QP \to Q를 위한 규칙도 나열하면 다음과 같다.
여기서 I∨1\text{I}\lor_1과 I∨2\text{I}\lor_2는 PP나 QQ 중 하나가 참이라고 판단했다면 P∨QP \lor Q가 참이라고 판단할 수 있다는 규칙이며 E∨\text{E}\lor는 P∨QP \lor Q가 참이라고 판단할 수 있고 PP가 참이라고 가정하든 QQ가 참이라고 가정하든 RR이 참이라고 판단할 수 있다면 그 가정 없이 RR이 참이라고 판단할 수 있다는 규칙이다. I→\text{I}\to는 PP가 참임을 가정해서 QQ가 참이라고 판단할 수 있다면 P→QP \to Q 또한 참이라고 판단할 수 있다는 규칙이며 E→\text{E}\to는 P→QP \to Q가 참이라고 판단할 수 있고 PP가 참이라고 판단할 수 있다면 QQ가 참이라고 판단할 수 있다는 규칙이다. 이렇게 소개 규칙과 제거 규칙의 쌍으로 논리적 증명을 하는 방식을 "자연 연역"("Natural Deduction")이라고 한다.
자연 연역으로 단순한 논리적 증명을 하는 방법의 예시를 들어보겠다. 어떤 단위 명제 AA, BB, CC에 대해서 A→BA \to B와 B→CB \to C가 참이라고 판단했다면 A→CA \to C 또한 참이라 판단할 수 있다. 이 증명은 다음과 같다. 우선 A→BA \to B 그리고 B→CB \to C와 AA가 참이라고 판단했을 때 BB가 참이라고 다음과 같이 판단할 수 있다.
이를 써서 다음과 같이 증명을 끝낼 수 있다.
따라서 논리적으로 A→BA \to B 그리고 B→CB \to C가 참임을 가정했을 때 A→CA \to C가 참이라고 판단할 수 있다.
자연 연역과 함수형 언어
혹자는 위 규칙들에서 미묘한 친숙함을 발견했을지도 모른다. 이를 좀 더 구체적으로 살펴보기 위해 →\to의 규칙들을 다시 살펴보자.
여기에 약간의 조작을 가해보자. 우선 Γ\Gamma를 단순한 판단의 나열로 취급하는 대신 이름 붙은 판단들로 취급하자. 예를 들어 위의 P trueP\ \texttt{true} 라는 판단에 xx라는 이름을 붙이면 다음과 같은 규칙을 얻는다.
더욱이 각각의 규칙들에 지금까지의 증명을 나타내는 항들을 더해보도록 하겠다. 예를 들어 I→\text{I}\to 규칙에서 Γ,x:P true⊢Q true\Gamma, x {:} P\ \texttt{true} \vdash Q\ \texttt{true}가 어떤 항 MM으로 나타내지는 증명이라면 Γ⊢P→Q true\Gamma \vdash P \to Q\ \texttt{true}의 증명은 fun (x:P)⇒M\mathtt{fun}\ (x \mathbin{:} P) \Rightarrow M이라는 항으로 나타내도록 하자. 마찬가지로 E→\text{E}\to 규칙에서 Γ⊢P→Q true\Gamma \vdash P \to Q\ \texttt{true}가 MM, Γ⊢P true\Gamma \vdash P\ \texttt{true}가 NN이라는 항으로 나타내진다면 Γ⊢Q true\Gamma \vdash Q\ \texttt{true}의 증명은 M NM\ N으로 나타내도록 하자. 이 항들을 판단에 끼워넣으면 다음과 같이 규칙을 바꿔 쓸 수 있다.
이는 (단순한) 함수형 언어의 형 검사 규칙과 동일하다!
함수 fun (x : P) => M
이 형 P -> Q
를 가지는지
검사하고 싶을 때는 x : P
를 가정한 뒤 M
이 형 Q
를
가지는지 검사하면 된다. 또한 함수 M
을 인자 N
에
적용하는 것이 형 Q
를 가지는지 알고 싶다면 함수
M
이 형 P -> Q
를 가질 때 인자 N
이 형 P
를 가지는지
검사하면 된다. 마찬가지 변화를 다음과 같이 모든 추론
규칙들에 적용할 수 있다.
⊤\top은 단위(unit) 자료형에 대응되며 ⊥\bot은 빈
자료형에 대응되고 P∧QP \land Q는 P
형과 Q
형의
쌍(pair) 자료형에 대응된다. 같은 방식으로 P∨QP \lor Q는
P
형과 Q
형의 합(sum) 자료형[3]에 대응된다.
항에서부터 각각의 추론 규칙이 (I\texttt{I} 규칙의 경우)
각 자료형의 생성자(constructor)나 (E\texttt{E} 규칙의
경우) 패턴 맞추기(pattern matching)의 형 검사 규칙에
대응된다는 것을 볼 수 있을 것이다. 이를 처음 구체화시킨
두 사람의 이름을 따 이 대응을 "커리-하워드
대응"("Curry-Howard correspondence")이라고
부른다. 이 대응이 발견됨으로써 논리적인 사고와
프로그래밍 언어의 이해 간에 중요한 연결고리가 생겼고
이는 현재에도 프로그래밍 언어의 발전과 논리학의 발전
양측에 모두 지대한 영향을 끼치고 있다.
이 대응을 따랐을 때 어떤 판단을 증명한다는 것은 그 판단의 형을 가지는 프로그램(program)을 짜는 것과 동일하다. 이를 보다 구체적으로 이해하기 위해 앞서의 예시 증명을 다시 반복해보자. 증명의 너비를 줄이기 위해 Γ\Gamma를 x:A→B true,y:B→C true,z:A truex{:}A \to B\ \texttt{true},\allowbreak y{:}B \to C\ \texttt{true}\allowbreak, z{:}A\ \texttt{true} 대신 사용하겠다.
즉 함수 x : A -> B
와 인자 z : A
가 있을 때 함수 적용 x z
이 B trueB\ \texttt{true}의 증명이다.
이어서,
따라서 fun (z : A) => y (x z)
가 x : A -> B
와 y : B -> C
가
주어졌을 때 A→C trueA \to C\ \texttt{true}의 증명이다.
지금까지 자연 연역에 대해서 알아보았다. 자연 연역은 함수형 언어를 쓰는 사람들에게는 어찌보면 매우 친숙할 수 있는 증명 방식이다. 그러나 자연 연역을 사용했을 때 거짓을 증명할 수 없다는 것을 보이는 것은 쉽지 않다. 자연 연역을 처음 도입한 게르하르트 겐첸(Gerhard Gentzen)은 같은 논문에서 거짓을 증명할 수 없다는 것을 보다 쉽게 보일 수 있는 다른 방식 또한 소개하였는데, 그것이 바로 논건 대수(論件 代數, Sequent Calculus)[4]이다.
진짜 논리적이 되는 방법 2 - 논건 대수(論件 代數, Sequent Calculus)
논건 대수 또한 명제의 진리에 대한 가정적 판단을 추론 규칙을 통해 이끌어낸다는 점은 자연 연역과 동일하다. 자연 연역과 논건 대수의 가장 큰 차이점은 명제를 만드는 각 방법에게 어떤 식으로 추론 규칙을 부여하는지에 있다. 자연 연역에서는 소개 규칙(I\text{I} 규칙)과 제거 규칙(E\text{E} 규칙)이라는 분류를 통해 ∧\land, ∨\lor, …\ldots에 추론 규칙을 부여했다. 논건 대수의 접근법은 이와는 살짝 다르다. 예를 들어 논건 대수에서의 P∧QP \land Q의 규칙에 대해 살펴보자.
차이점을 눈치챘는가? 크게 두 차이점이 있다.
- 규칙의 이름이 다르다. 😅
- E∧\text{E}\land을 대체하는 L∧\text{L}\land의 꼴이 다르다.
먼저 이름의 차이를 설명하고 넘어가자. 자연 연역의 경우 I∧\text{I}\land 규칙은 ∧\land를 소개(introduce)하는 규칙, E∧\text{E}\land 규칙은 ∧\land를 제거(eliminate)하는 규칙이었다. 반면에 논건 대수의 R∧\text{R}\land 규칙은 ∧\land를 오른쪽(Right side)에 소개하는 규칙이고 L∧\text{L}\land 규칙은 ∧\land를 왼쪽(Left side)에 소개하는 규칙이다. E∧\text{E}\land와 L∧\text{L}\land의 꼴의 차이는 이 접근법의 차이에서부터 자연스럽게 따라나온 것이다.
명제를 만드는 다른 방법들에 있어서도 논건 대수의 방식을 따라서 추론 규칙을 마련해 줄 수 있다.
그리고 논건 대수가 자연 연역과 동등함을 (비교적) 쉽게 보이기 위해서는 명제를 만드는 각 방식의 R\text{R}과 L\text{L} 규칙에 더해 다음의 두 규칙을 추가해야한다.
여기서 init\text{init} 규칙은 자연 연역에서의 hyp\text{hyp} 규칙과 같은 꼴이다. 반면에 cut\text{cut} 규칙은 직접적으로 비교할만한 자연 연역에서의 규칙이 존재하지 않는데, 이는 논건 대수가 자연 연역과 전혀 다른 방식으로 증명을 전개하기 때문이다. 자연 연역에서는 예를 들어 I∧\text{I}\land 규칙으로 만들어진 P∧QP \land Q가 참이라는 판단을 바로 E∧\text{E}\land에 사용할 수 있었다. 함수형 언어로 말하자면
case (M, N) of
(x, y) => L
같은 꼴의 사용이 가능했다. 그러나 논건 대수에서는 R∧\text{R}\land 규칙은 가정적 판단의 (오른쪽) 후건에, L∧\text{L}\land 규칙은 가정적 판단의 (왼쪽) 전건에 ∧\land를 새로 만들어낼 뿐이고 두 규칙이 상호작용할 수 있는 방법이 없다. 이 공백을 해결해주는 규칙, 즉 자연 연역의 I\texttt{I}/E\texttt{E} 규칙 쌍의 상호작용에 의한 증명을 논건 대수에서도 표현할 수 있게 해주는 규칙이 바로 cut\text{cut} 규칙이다.
그런데 이 상호작용은 과연 필요한 것인가? 위의 함수형 언어를
통한 예시에서 보다 분명히 볼 수 있는 것은 예시의 I∧\text{I}\land와
E∧\text{E}\land 규칙의 연달은 사용이 사실은 불필요하다는 점이다.
이는 자연 연역에서는 저런 식의 증명 대신 L
에서 x
가 등장하는
자리에 M
을 치환해넣고, y
가 등장하는 자리에 N
을 치환해넣은
증명 또한 가능하기 때문이다. 이런 상호작용의 불필요성에 대한
대한 자연 연역에서의 직관을 이에 대응되는 논건 대수의 cut\text{cut} 규칙에
대해서 구체화한 것이 바로 다음의
cut\text{cut} 제거 정리이다.
정리
cut\text{cut} 제거 정리
cut\text{cut}을 사용해 증명 가능한 모든 판단은
cut\text{cut}을 사용하지 않고서도 증명할 수 있다.
cut\text{cut} 제거 정리의 의의는 단순히 필요없는 규칙을 제거하는 정도에 멈추지 않는다. cut\text{cut}을 제거하고 나면 논건 대수에서 가정 없이는 거짓을 증명하지 못한다는 것이 자명해지기 때문이다.
정리
cut\text{cut}을 제거한 논건 대수의 일관성
cut\text{cut}을 제거한 논건 대수는 판단 ⊢⊥ true\vdash \bot\ \texttt{true}를 증명하지 못한다.
증명은 다음의 네 문장이면 충분하다.
- 귀결이 ⊥ true\bot\ \texttt{true}인 R\text{R} 규칙이 존재하지 않기 때문에 어떤 R\text{R} 규칙도 쓸 수 없다.
- 가정이 없기 때문에 어떤 L\text{L} 규칙도 쓸 수 없다.
- 마찬가지로 가정이 없기 때문에 init\text{init} 규칙을 쓸 수 없다.
- 따라서 어떤 규칙도 판단 ⊢⊥ true\vdash \bot\ \texttt{true}을 결론으로 주지 않는다.
앞서 이 글의 서두에서 논건 대수의 일관성을 보이기 위해 "약간의 부정행위"를 저지를 것이라고 말했다. 오해가 없도록 명시하자면 위의 증명은 cut\text{cut}을 제거한 논건 대수에 있어서는 문제가 없다. 부정행위라고 부를 만한 부분은 바로 cut\text{cut} 제거 정리의 증명이 더 어렵다는 점이다. 이 증명은 단순화하기 쉽지 않기 때문에 글에서 직접적으로 다루지는 않을 것이고, 이것이 바로 서두에서 언급한 "부정행위"이다. 다만 이 어려운 증명도 수학적 귀납법(Induction) 이상의 지식은 필요로 하지 않기 때문에, 시도해보고자 하는 독자가 있다면 직접 시도해 볼 수 있을 것이다[5].
논건 대수의 소개를 앞서의 예시 증명을 논건 대수에서 반복하는 것으로 마치도록 하자. 우선 A→BA \to B와 AA가 참이라고 판단했을 때 BB가 참이라고 다음과 같이 판단할 수 있다.
이를 써서 다음과 같이 증명을 끝낼 수 있다.
앞서의 자연 연역 증명의 구조가 크게 다름에 주의해서 논건 대수 증명의 구조를 이해해보도록 하자. 앞서의 자연 연역 증명은
의 구조를 가지고 있다. 즉 결론에 I\texttt{I} 규칙을 적용하고 어떤 가정에 E\texttt{E} 규칙을 적용해서 이 둘이 만나는 지점을 찾는 것이 증명의 구조이다. 이와는 다르게 논건 대수의 증명은
와 같이 (여러 개의) init\texttt{init} 규칙에서 시작해서 L\texttt{L} 규칙으로 가정, R\texttt{R} 규칙으로 귀결을 변경해 결론에 도달할 때까지 차례로 내려오는 구조를 가진다. 이런 구조의 차이가 바로 (자연 연역의) hyp\texttt{hyp} 규칙과 (논건 대수의) init\texttt{init} 규칙이 (같은 꼴임에도 불구하고) 다른 이름을 가지게 된 이유이자 논건 대수의 init\texttt{init} 규칙이 시작점(initial point)에 해당하는 이름을 가지게 된 이유이다.
논건 대수의 항
논건 대수를 좀 더 컴퓨터 공학적으로 이해할 수 있을까? 이를 위해 자연 연역의 경우와 마찬가지로 논건 대수에도 증명에 커리-하워드 대응을 통해 항을 주려고 시도할 수 있다. 그러나 앞서 언급한 것처럼 논건 대수 증명은 자연 연역의 증명, 그러니까 함수형 언어와 구조가 크게 다르다. 따라서 원본 그대로의 논건 대수에 주는 항은 상대적으로 복잡하고 다양한 개념들(생산자, 소비자, 소비자를 생산자로 바꾸기, 생산자와 소비자가 거래하게 하기, …\ldots)을 요구하고, 결과적으로 이는 컴퓨터 공학적인 직관성이 떨어지는 복잡한 항을 만들어 내게 된다. 이어질 2 편에서는 논건 대수에 약간의 변형을 가하면 직관적이고 쉽게 이해가 가능한 항을 줄 수 있으며, 항이 뜻하는 바가 저수준(low-level) 자료 표현(data representation)과 자연스럽게 연결될 수 있음을 설명할 것이다.
마치며
2 편의 "논리와 저수준 자료표현" 연작 중 1 편인 이 글에서는 논리적 증명을 하는 두 방법과 커리-하워드 대응에 대해서 설명했다. 1 편의 내용은 말하자면 2 편의 바탕 및 서두 역할을 하고 있다. 이 내용들이 2 편에서 다룰 본격적인 논리와 자료 표현의 관계에 대해 흥미를 불러일으켰기를 바라며 이만 마치도록 하겠다.
이 중 두번째 단위 명제는 일반적인 자연수 체계에서 거짓이나, 명제의 정의 자체는 명제가 참인지 거짓인지에 대해 논하지 않는다는 것을 강조하기 위해 단위 명제에 포함하였다. ↩︎
거짓도 참이라면 대체 무엇이 참이 아니겠는가? ↩︎
이는 Rust나 OCaml의
Result
형 혹은 Haskell의Either
형과 같은 형이다. ↩︎전건(前件, antecedent)과 후건(後件, succedent)을 개별적으로 다룰 수 있다는 의미에서 "Sequent Calculus"를 논건 대수(論件 代數)라고 번역하였다. 보다 일반적으로 "시퀀트 대수"라는 표현이 쓰이나, 이는 "시퀀트"가 의미하는 바가 "논리에서 다루는 물건/사건/…\ldots"이라는 표현보다 직관성이 떨어진다고 보아 재번역을 하였다. ↩︎
증명에 대한 구체적인 질문이 있다면 답글을 남겨주기를 바란다. ↩︎
https://hackers.pub/?filter=local
와 이제 여기는 순수 개발이야기만 하는 국산 개발 SNS가 되었네 ㅋㅋㅋㅋㅋㅋ
사람도 계속 들어오는거 보면 장난 아닌 듯
얘가 한국 페디버스(연합우주)의 새로운 바람인 듯
VitePress 2.0.0のアルファ進んでた!! リリースされたら、俺、mitome.inのを更新してDependabotちゃんをだまらせるんだ…
https://github.com/vuejs/vitepress/blob/main/CHANGELOG.md
에디터의 플러그인도 Nix로 관리하고 싶다. 에디터 쪽에서 지원을 해야하는데, 누군가 총대매고 해줄법도 한데...
Void Linux 한국 미러가 없어서 수제로 구워왔습니다 많관부
https://mirror.kyoku.dev
어제 Deno 블로그에도 올라왔네. pnpm은 v10.9.0 (5일전), yarn은 v4.9.0 (2주전) 버전 부터 사용할 수 있는 듯
https://deno.com/blog/add-jsr-with-pnpm-yarn
RE: https://hackers.pub/@moreal/01961d55-e6aa-7322-8d25-0ebe70ae77db
simonw llm https://llm.datasette.io 을 써봤는데 커맨드라인에서 사용하기 편하다.
많은 파일을 대상으로 텍스트를 대량 치환해야 할 일이 꽤 있는데, 파일 탐색과 치환을 인터랙티브하게 수행할 수 있는 툴이 없어서 ised(interactive sed)를 만들었다. 월요일부터 개밥먹기 할 예정. https://github.com/parksb/ised
@hongminhee洪 民憙 (Hong Minhee)
@xiniha 오 저도 pothos씁니다. pothos에 Prisma plugin, Relay plugin 발라서 날먹한 부분이 많습니다.
데코레이터 대신 직접 함수객체 생성하려고 Callable 타입인 fn을 lambda로 넘기려 한다. arguments 처리를 위해 signature 정보를 넣어줬더니 mypy 가 배를 짼다.
이럴땐
- cast 한다
- mypy ignore 한다
어떻게 하는게 바람직한가요?
Gravatar 프로필에 페디버스 계정 인증이 가능하네요~ 따라서 제 프로필에 해커스펍 계정을 추가했습니다.
# Ask Hackers Pub : 이번 주말에 뭐 하시나요?
이번 주말에 뭘 하려고 계획 중인지 편하게 얘기해 보아요.
읽을 책, 가볼 곳, 해볼 것.. 어떤 것이든 좋습니다.
도움 요청이나 피드백 요청도 좋습니다.
물론! 아무것도 하지 않고 쉬는 것도 훌륭합니다.
* 지난 주말에 계획하셨던 일의 회고도 한 번 남겨보면 좋을 것 같아요.
- VimConf 제안서 작성
- PyCon KR CFP 자료 85퍼센트 정도 채워넣기 (바이브 코딩 관련)
- Fediverse 앱 개발
- 이력서 작성
- High Performance Browser Networking Part1 완주
- React 공식 문서 완주
https://github.com/faiface/par-lang
Session Type 기반의 언어라고 한다.
Creating your own federated microblog
Link: https://fedify.dev/tutorial/microblog
Discussion: https://news.ycombinator.com/item?id=43780785
???????????? 해커뉴스 100????
오랫만(?)에 인사 드립니다 ^^ 전 세계 LLM을 테이블로 정리한 정보 입니다.
Creating your own federated microblog
L: https://fedify.dev/tutorial/microblog
C: https://news.ycombinator.com/item?id=43780785
posted on 2025.04.24 at 05:37:57 (c=0, p=8)
네이버에서 모델 공개했다고 해서 ollama로 변환해서 돌려봤는데...
전반적으로 말길을 잘 못 알아 듣네요. 전에 다른 모델에 영수증 OCR한 텍스트로 더치페이 계산 해달라고 했던 것을 똑같이 시켜보니까, 상품명에 “3개” 가 들어간 상품의 가격을 지 맘대로 3배한 가격으로 만들고, 더하기는 틀리지 않게 해놓고는, 사람수만큼 안나눠주고 어째서인지 상품별로 다시 가격 안내를 하고는 알아서 나눠 내라합니다.
Show GN: 나만의 연합우주(fediverse) 마이크로블로그 만들기
------------------------------
이 튜토리얼은 [Fedify] 라이브러리를 사용하여 [ActivityPub] 프로토콜 기반의 마이크로블로그 서비스를 구현하는 방법을 설명합니다. ActivityPub은 다양한 소셜 네트워크 서비스들이 서로 연동될 수 있게 해주는 분산형 소셜 네트워킹 프로토콜로, 이를 통해 [Mastodon], [Misskey] 같은 서비스와 상호작용할 수 있는 독…
------------------------------
https://news.hada.io/topic?id=20508&utm_source=googlechat&utm_medium=bot&utm_campaign=1834
네이버에서 모델 공개했다고 해서 ollama로 변환해서 돌려봤는데...
https://discuss.haiku-os.org/t/is-haiku-a-unix-like-os/8801
really interesting thread. It's not fresh but the sentiments there are interesting. For a lot of folks "unix like" is basically "debian".
also, I'm very haiku-curious
요즘 Server-side rendering인데 차트를 streaming으로 incremental update 할수있는 좋은 방법을 찾고 있다. Solid Start의 Server Signal이란게 원하는거랑 가까워 보이긴한데...
What's your favorite JavaScript runtime?