저도 잘쪼개고, 잘 붙이기 위해 노력합니다. 대충 이런식이네요
- 점과 선으로 그래프 구조의 논리식을 세운다
- 이 때 그래프는 프로그램이 자신을 참조하거나 입력으로 받는 람다식의 특성상 순환구조가 나타나게 된다
- 이 때 그래프의 어떤 부분은 유향 비순환이고, 이것들은 대부분 쉽게 검증할수 있다. 그렇기에 이 것들을 최대한 끼고 살아야 한다
- 클린아키텍쳐, 의존성 역전, 구상보다는 추상에 의존하기 등등 수단과 방법을 가리지않고 부분을 유향비순환으로 격리, 즉 "잘 쪼개고"를 한다
- 이때 큰 구조는 최대한 단방향 의존성을 만들어 최대한 순환참조를 배제한다. 루프는 최대한 부분구조에 둔다
- 하지만 화면에 그림을 그리는 컴퓨터 구조는 기본적으로 이미 루프이다. 계속해서 화면을 뿌리는동안 사용자 입력을 중간중간 끼워넣고 컴퓨테이션 하는 식이다. e.g. 게임 루프
- 마찮가지로 동시성을 흉내내기위한 시분할이라던지, 비동기 연산등 컴퓨터, OS, 프로그래밍 언어 런타임등도 이벤트 루프등 루프를 활용한다
- 이렇게 제공되는 환경은 어쩔 수 없으니 그 외에 순환구조를 해야만 한다면, 자료구조 자체를 불변구조로 사용해서 최대한 정보를 가역적으로 유지한다. 정보에 대한 컴퓨테이션이 특히 루프에서 비가역적일경우 디버깅은 지옥으로 빠진다. react.js, flutter, swift ui 등 많은 현대 ui 라이브러리에서 이런 방식이 사용된다
- 부분구조에 대해 유닛테스트, 테스트-더블등을 활용한 모킹등을 해서 최대한 검증하여 신뢰구간을 만든다
- "잘 쪼개진" 부분구조의 경계면을 "잘 붙이는" 식으로 이어본다
- 이제 e2e, 인터그레이션, 블랙박스 테스트, qa 아웃소싱등 수단과 방법을 가리지 않고 경계면에 대한 테스트를 한다
대충 이렇게 하면 얼추 되긴하는데, OS, 플랫폼, 의존 라이브러리, UI 엔진/GPU 의 독립적인 라이프사이클사이에서 제가 만든 정적 그래프 구조의 논리식이 증명과정에서 생성되는 또다른 그래프, 즉 동적 상태 -> 상태로 이어지는 시간 흐름 그래프와 상호작용하며 나타나는 오류는 정말 어렵더군요.
이러다보니 저는 상대적으로 아름다운 구조에 해당하는 함수형이나, 클린류의 단방향 의존성 아키텍쳐등에 대해 어느정도 흥미가 떠나게 되더군요.
-
이제 부터 우리는 함수, 카테고리 등등에 대해 탈곡기를 돌릴것이다
-
그런데 비슷하게 옆방에서는 "군"이라고 하는 구조에 대해 탈곡?이 진행되었었다
- 이것은 어떤집합과 거기에 어떤 연산이 주어졌을때, 연산의 결과가 닫혀있고, 결합, 항등원, 역원이 성립하는 구조라 한다
- 이 조건이 만족되면, 신비롭게도 변환을 해도 본질이 바뀌지 않고 가역적으로 되돌릴수 있다 한다. 이게 무엇인지 모르겠지만 유용해 보인다. 구조를 보전하는 변환이라니
- 때떄로 이 구조를 보존하는 변환은 수학의 세계에서 대표적으로 음미하게되는 아름다움중 하나로 알려져 있다
-
다른 한편으로 "근사군"을 생각해 보자
- A에 대한 어떤 연산 x가 있을때,
A x A = A이 군이라고 하면, 이건 정말 아름답다고 할만큼 드물다. 세상은A x A != A로 가득하다 - 반면에 어떤 어떤 연산 x가
A x A = 쪼금커진A인, 연산의 결과가 완전 닫히지는 않았지만 거의 닫힌 꼴을 의미한다. 대충 곱을 반복 해도 크기가 크게 증가하지 않는다고 하자 - 신비롭게도 이게 "군"처럼 거의 대칭을 다룰 수 있다한다. 많이 변해도 본질은 엄청 변하지 않고 완전히 가역적이지는 않지만 그럴싸 하게 다룬다고 한다
- A에 대한 어떤 연산 x가 있을때,
-
채널지기님의 "실리콘 위의 논리 노트. 로빈슨산술과 프레스버거산술: 정형방법론에서왜중요한가"에서 다음구절이 흥미롭다
- 왜 곱셈이들어가면 갑자기어려워지는가
- 덧셈만 있는 세계는 대체로 선형적이다
- 곱셈이 들어가면 비선형성이 생긴다
- 어떤 군은 곱셈이 들어가도 선형이고, 근사군은 선형 비슷하게 다룰수 있게 해준다
-
결합, 항등원, 역원과 같은 엄격한 조건이 아름다운 구조를 만드는가? 아니면 작은 변화에 작게 대응되는 결과중 하나가 엄격한 조건일까?
- 입실론-델타에서 열린집합 근방을 생각해보자. 입력이 조금 변하면, 출력도 조금변하고, “어떤 점 주변의 작은 영역(이웃)을 통째로 보존한다
- 그럼 그 근방을 그냥 그 점으로 봐도 무방한것 아닌가? 군같이 작용한다면 그냥 군비스므리끼리 한걸로 치고 쓰면되는것 아닐까?
- 같다, 비슷하다, 근사한다, 관찰에 대해같다, 축약한다, 같게볼수 있다 와 같은것들이야 말로 엄청나다
-
이제 다시 코드문제로 돌아가보자
- 내가만든 정적 논리식 그래프는 증명의 과정인 연산 동안 상태->상태로 또다른 동적 그래프를 생성한다
- 나는 부분의 검증을 덧이어서 전체에 대한 신뢰를 만들고 싶다
-
여기서 부터 모르겠다
- 논리식의 증명 연산과정 중 생성되는 동적 상태->상태와 나의 정적 논리식은 무슨관계인가?
- 내가 생각하는 논리식의 일정 부분 격리에 대한 검증은 전체 상태-> 상태에서도 유효한가?
- 더 나아가서 과연 논리식 자체가 함수형, 단방향 의존 아키텍쳐의 아름다운 구성이라도 상태 -> 상태의 시간흐름일때도 정합을 보장하는데 유용한가? 혹은 다른 방법론을 필요로하는가?
- 정적그래프를 아름답게 "쪼개는"것만으로 동적 상태 -> 상태 그래프가 안정화 될수 있는가? 예측할수 있는가?
-
llm을 거대 함수로 보았을때 최근의 동역학적 해석들은 이러한 생각을 더 밀어붙이게 한다
- 상태 흐름안에서 특정 연산은 폭발하지 않고, 같게 볼수 있는 어떤 구조를 형성한다는 관점들이 있다
- 나의 작은 논리구조도 상태->상태의 흐름을 만들고 있다
- https://arxiv.org/abs/2502.12131, https://arxiv.org/abs/2512.21113 ...
-
"4색정리"는 아름다운 구조없이 증명되었다. 과연 이제 난제해결이 아름다운 구조로 부터 딸려올수 있을까? 아니, 남아난 아름다운 구조가 있을까?
-
최근 GPT5.4가 풀어서 검증중인 FrontierMath: Open Problems의 디오판토스 방정식은 어떠한가? 방정식에 대해 무수히 많은 계산을 통해 대략의 움직임 범위를 좁힌다음 조합론을 통해 해의 특정한 모양, 일정한 거리를 찾아내는 파이선 코드를 작성하고 수조번의 계산을통해 해가 2개임을 찾아내었다
-
https://epoch.ai/frontiermath/open-problems/ramsey-hypergraphs/
-
어떤 학부 CS 졸업자는 한번도 미적분을 해본적이 없다고 한다
-
"잘 쪼개진"것을 "잘 붙일때" 붙이는 부분의 어떤 특정한 구성을 마치 "교량 상판에 대한 하중 검사"같이 분석이 가능할까?
-
소프트웨어 엔지니어링에서 정적분석은 건축이나 자동차의 구조분석, 하중분석, 비행기의 유체분석과 같은 도구를 얻을수는 없을까?
-
-
미분은 국소적 변화로 전역을 보게하고, 적분은 국소정보를 누적해서 전역을 재구성 해준다
- 우리는 이미 점과 화살표를 가지고 있다. 그렇다면 이산적인 점으로부터 연속을 환원해서 관찰이 가능하지 않을까?
- 종종 나는 그로센딘/세르교에 가입해야하는거 아닌가? 생각해 보거나 CS에서 다루는 수학이 수학의 발전과 함께한 미적분이 아니라 논리나 범주로 부터 시작되어야 한다 생각하다가도, 여기까지 오면 역시 미적분의 고난한 세계를 떠날수는 없을것같고, 결국 한 십년은 수즐에서 떠돌아야할것 같다
위에 나온 수학적으로 느껴지는 용어는 전부 수능 비문학 지문의 감성이라서 그려려니 해주시면 됩니다. 근데 아무튼 저는 "종료문제", "라이스의 정리"와 더불어 프로그래머가 실제 작성하는 정적 논리식 그래프와 이것을 증명하는 연산 과정에서 생성되는 동적 상태 -> 상태 그래프의 관계를 생각하다보니 함수형 프로그래밍에 기대치가 낮아지긴 했네요
수즐-실리콘-위의-논리