트리 계산법

 (treecalcul.us)
1P by GN⁺ | ★ favorite | 댓글 1개
  • 최소한의 문법으로 계산을 구성하려는 체계로, 하나의 연산자 △ 와 적용만으로 최소성·튜링 완전성·반영성·모듈성을 모두 다룸
  • 문법은 E::= △ | E E이며, △ 가 세 값에 작용할 때 계산되고 값은 잎·줄기·갈래 노드로 이루어진 자연 이진 트리임
  • 조합 논리의 K와 S를 Tree Calculus 안에서 표현할 수 있어 튜링 완전성을 갖고, λ-calculus와 달리 재귀 함수를 정규형으로 표현할 수 있음
  • 프로그램도 값으로 다뤄지므로 자기 적용을 통한 인트로스펙션과 반영이 가능하며, size size가 168로 평가되는 예가 있음
  • 하위 항이 하위 트리로 드러나 공통 기능 부트스트랩, 직렬화, 프로그램 분석·최적화, 정적·동적 타이핑 같은 데모로 이어짐

한 연산자로 만드는 자연 이진 트리

  • Tree Calculus는 Barry Jay가 발견했으며, 사이트에는 그의 책과 블로그, Johannes Bader가 개발한 데모가 연결되어 있음
  • 핵심 특성은 minimal, Turing-complete, reflective, modular 네 가지로 정리됨

  • 최소성

    • Tree Calculus에는 하나의 연산자 △ 만 있음
    • 문법은 E ::= △ | E E 형태임
    • 시각적으로 △ 는 트리 노드이고, E1을 E2에 적용하면 E2가 E1의 루트 오른쪽에 붙음
    • 값은 자연 이진 트리이며, 노드는 leaf, stem, fork로 불림
    • 실용 데모
      • portability: 여러 플랫폼에서 단순하고 안전한 인터프리터를 만들 수 있음
      • emit-json: 크로스 플랫폼 설정 생성에 적합한 예를 보여줌

튜링 완전성과 반영

  • 튜링 완전성

    • 조합 논리의 K와 S 연산자를 Tree Calculus로 표현할 수 있음
    • K = △ △
    • S x = △ (△ x)
    • 조합 논리의 K/S 기반이 완전하므로 Tree Calculus도 튜링 완전함
    • λ-calculus와 달리, orange/brown 같은 고정점 구성으로 재귀 함수를 정규형으로 표현할 수 있음

  • 반영성

    • triage {l, s, f} = △ (△ l s) f는 leaf, stem, fork에 대한 경우 분석을 수행함
    • 자연수 n은 △^n △로 표현할 수 있음
    • 0 테스트는 triage {true, K false, K² false}로 구성됨
    • 프로그램도 값이므로 intensional 프로그램은 자기 적용으로 인트로스펙션과 반영을 수행할 수 있음
    • 예시 프로그램 size는 인자의 노드 수를 계산하며, size size는 168로 평가됨
    • 실용 데모
      • serialize-anything: 프로그램 직렬화 가능성을 다룸
      • halting-problem: 정지 문제를 더 단순하게 공식화함
      • fusion: 프로그램 분석·최적화를 함수로 표현함
      • gradual-typing: 정적 타이핑과 동적 타이핑을 함수 호출로 다루는 예를 제공함

모듈성과 데모

  • 하위 항은 하위 트리로 표현됨
  • 페이지 상단의 size 프로그램은 triage를 사용해 노드를 재귀적으로 셈
  • 실용 데모

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • Tree Calculus는 이 웹사이트를 넘어서는 함의가 있는 멋진 주제임
    다만 웹사이트가 창시자이자 저자인 Prof. Barry Jay를 명시적으로 표시하지 않는 건 아쉬움. 더 알고 싶다면 Jay의 책을 보면 됨: https://github.com/barry-jay-personal/tree-calculus/blob/mas...

    • “Specification” 페이지에서 그의 책을 참조하긴 함
      출처 표시를 더 명확히 할 수 있고 그렇게 할 예정이지만, 공을 가로채려는 의도는 전혀 없음. 배경은 이 답글에 더 적어둠: https://news.ycombinator.com/item?id=42375914
    • 이걸 보자마자 Barry Jay의 Bondi Language / Pattern Calculus가 먼저 떠올랐는데, 완전히 빗나간 건 아니었던 듯함

  • 멋져 보이긴 하는데, 이 페이지가 안내를 너무 적게 해 줘서 이해하기 어려움
    “초보자용” 설명 같은 게 있으면 좋겠음

    • SKI 계산법이나 그 사촌인 람다 계산법처럼, 표현식을 기계적으로 평가하거나 축약하는 정확한 규칙을 가진 단순한 계산 모델임: https://en.wikipedia.org/wiki/SKI_combinator_calculus
      SKI 계산법과 다른 점은 자기 프로그램 구조를 성찰할 수 있다는 것, 예를 들어 두 프로그램이 같은지 판단하는 일이 가능하다는 점임: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      또 람다 계산법과 달리 주어진 축약 규칙을 적용하면 프로그램이 안정적인 정규형으로 수렴하며, 무한 축약 사슬로 빠질 수 있는 경우를 피할 수 있음: https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
      그래서 프로그램을 따옴표 처리하거나 직렬화해 안정적인 데이터 구조로 우회하지 않고도 성찰이 가능하고, Lisp의 동형 코드성과 비슷한 면이 있음
    • 메인 랜딩 페이지 구성이 꽤 이상함
      유행하는 프로그래밍 언어나 프레임워크 웹사이트처럼 한 단어짜리 제목, 살짝 buzzword 같은 문구, 움직이는 코드 예시를 쓰는데, 본문은 지나치게 조밀하고 긴 학술 문체임. 그런데 정작 그 학술 문체만으로도 무슨 일이 일어나는지 이해할 만큼의 세부 정보는 없음
      한참 문단을 파싱해 봤지만, 장황함에도 불구하고 보통 프로그래밍 언어 랜딩 페이지처럼 “저자가 이 언어의 뭐가 좋다고 생각하는지”만 말하고, 작동 방식은 설명하지 않음. 결국 명세를 봐야 할 듯함
    • 명세의 문법 E ::= t | E E는 처음 보면 모든 표현식이 그냥 t t t t t t t처럼 보인다고 착각하기 쉬움
      실제로는 괄호 구조를 유지해야 해서 (t t) (t ((t t) (t t))) 같은 형태가 되며, 최상위와 각 괄호 안에는 항상 정확히 두 하위 표현식이 있음. 즉 공백 문자가 이항 연산자처럼 동작함
      이 표현식은 괄호가 많으므로 이 이항 연산자를 왼쪽 결합으로 본다. a b c는 (a b) c, a b c d는 ((a b) c) d로 해석됨
      이렇게 보면 트리가 어디서 나오는지 보임. 말단 기호가 t 하나뿐이라 불필요한 괄호를 제거하면 모든 표현식은 항상 t로 시작하고, 뒤에 여러 표현식이 따라옴. 처음 t를 노드로 그리고, 뒤따르는 표현식마다 같은 절차로 하위 트리를 그리면 됨
      명세 페이지의 의미 규칙은 하위 트리가 셋 이상인 노드를 “단순화”하는 방법, 즉 t 뒤에 하위 표현식이 셋 이상 붙은 식을 줄이는 방법을 말함
    • 페이지 맨 위에 “Tree Calculus는 [목적 요약]을 위한 [명사구]다” 같은 정의 문장이 있으면 도움이 됨
      위키백과 문서들이 보통 “Lambda calculus는 …를 위한 형식 체계다”, “Matrix calculus는 …를 위한 특수 표기법이다”처럼 시작하는 식임
    • 요약하면, 프로그램과 값이 모두 레이블 없는 트리인 프로그래밍 언어임
      레이블 없는 트리는 노드에 데이터가 없는 트리형 자료구조이고, 자식들의 순서는 있음. Tree Calculus는 레이블 없는 트리를 평가해 다른 레이블 없는 트리를 얻는 규칙 집합을 정의함
      규칙을 반복 적용하면 무한 루프에 빠지거나, 더 이상 변하지 않는 트리에 도달함. 규칙은 이진 트리에는 영향을 주지 않도록 설계되어 있어서, 이진 트리를 평가하면 같은 트리가 나오고 계산이 끝난 상태가 됨
      이 규칙들은 “Specification” 페이지에 프로그래밍 언어 이론에서 흔한 작은 단계 의미론 형태로 적혀 있음
      주장하는 바는 평가 규칙이 튜링 완전이라 어떤 계산도 표현할 수 있고, 평가가 점근적으로 최적이라 어떤 언어의 프로그램도 Tree Calculus에서 거의 상수 오버헤드로 실행할 수 있다는 것임. 처음 보기에는 말이 안 되는 주장은 아니지만, 실제로 얼마나 중요한지는 명확하지 않음
      용도는 일부 프로그래밍 언어 이론 연구자에게 흥미롭고, 계산 이론 증명을 단순화하는 데 쓸 수 있을지도 모름. 이런 게 흥미롭다면 Tree Calculus보다 더 단순하고 잘 알려졌고 유용한 람다 계산법을 먼저 배우는 편을 추천함

  • 홈페이지에 “Democratizing Functions”, “Democratizing Metatheory”라고 되어 있는데, 무슨 뜻이든 democratizing이라는 단어를 남용하는 느낌이 강함

    • 이 용법은 꽤 흔함
      Britannica의 두 번째 정의도 “무언가를 모든 사람이 이용 가능하게 만들다, 모든 사람이 이해할 수 있게 만들다”임: https://www.britannica.com/dictionary/democratize
    • 동의함. “What democratize really means”도 참고할 만함: https://intage.us/articles/words/democratize/
      “언어는 문화에 의해 형성되고, 당신도 그 문화의 일부다. 책임을 포기할 필요는 없다. 선택지는 있다”

  • Tree Calculus의 축약 규칙 논리를 “감”으로 이해하려고 직접 그림을 만들었음: https://latypoff.com/tree-calculus-visualized/
    시각적으로 생각하는 사람에게 도움이 될 수 있음

    • 매우 도움이 됨. 특히 세심하게 쓴 텍스트가 좋음
      다만 두 번째 그림 “Stem with a single leaf child”에는 오류가 있어 보임. 삼각형에서 내려가는 선이 사각형으로 이어지는데, 그 사각형은 원이어야 할 듯함
    • 정말 좋음. 이걸 애니메이션 가능한 형태로 만들면 웹사이트의 Specification 페이지에 아주 잘 어울릴 것 같음

  • 이걸 추천한 사람들이 정말 뭔지 이해하고 추천한 건지 궁금함

    • 내 눈에는 람다 계산법의 또 다른 구현처럼 보이고, 왜 흥미로운지 설명하지 못하는 웹페이지도 아쉬움
    • 흥미로운 토론이 이어질 것 같아서 추천했음
    • 누군가 설명해 주길 바라며 추천했음

  • 이게 문법만 다른 Lisp나 Forth가 아닌 이유를 설명해 줄 수 있나?
    비판하거나 얕게 치부하려는 게 아니라 진짜로 이해하고 싶음

    • Lisp는 람다 계산법에 기반하는데, 람다 계산법 자체에는 자기 안에 쓰인 프로그램을 수정하는 도구가 없음
      이 기능이 유용하므로 Lisp 계열 언어에는 매크로 같은 것이 추가되어 왔고, 구현 방식도 다양함. Lisp 계열에서 흔한 eval조차 람다 계산법의 일부는 아님. 람다 계산법에는 추상화, 적용, 변수만 있고 환경은 없음
      성찰의 개념이 잘 정의되어 있고 Tree Calculus가 성찰적이라면, 문법만 다른 Lisp는 확실히 아니고 Forth는 더더욱 아님
      전문가는 아니니 크게 걸러 들어야 함. 실무적으로는 느린 Lisp처럼 보일 수 있지만, 이론적으로는 람다 계산법과 다르고 느린 Lisp 같은 것을 더 단순하게 구현하는 기반으로 쓸 수 있음
    • 필수 괄호와 들여쓰기 민감성이 없다면, 내 취향으로는 이미 큰 장점임
      다른 취향도 당연히 괜찮지만, 동형 코드성이 대부분 Lisp 방언 안에 갇혀 있는 건 아쉬움

  • SKI의 Z 조합자를 람다 계산법 예시를 거쳐 Tree Calculus로 변환하고 트리로 출력해 봤음
    테스트는 안 했지만, 원본은 도구로 변환한 미최적화 코드임. 관련 배경은 고정점 조합자 문서 참고: https://en.wikipedia.org/wiki/Fixed-point_combinator

    • Z 조합자는 Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v)) 형태로 훨씬 단순하게 쓸 수 있고, SKI로도 더 짧게 표현 가능함

  • Johannes가 Tree Calculus를 실험하고, 내 책 GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf 에 암시적으로만 있던 가능성을 명시적으로 보여 주는 걸 보니 좋음
    마침내 타입이 있는 Tree Calculus가 생겼고, 그래서 GitHub.com/barry-jay-personal 에서 블로그를 쓰기 시작했음

    • 책으로 가는 동작하는 링크는 여기임: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      오른쪽의 다운로드 버튼을 찾으면 됨
    • “Typed Program Analysis Without Encodings” 논문에 매우 관심이 있는데 온라인에서 찾지 못하겠음. 어디를 보면 좋을지 궁금함

  • 이걸 한참 들여다보고 몇 가지 깨달은 점이 있음. 특히 람다 계산법이나 형식 의미론에 어느 정도 익숙한 사람이 발판을 잡는 데 도움이 될 수 있음
    작은 단계 의미론이 무슨 뜻인지 이해하려고 OCaml 구현까지 내려가야 했는데, 기본 트리 구조가 잘 보이지 않았기 때문임. 정의의 네 원소 축약식에서는 처음 세 항에 괄호를 쳐 보면 무엇이 무엇에 적용되는지 보임. 오른쪽도 괄호가 부족해 보임
    예를 들면 (t (t) a) b -> a, (t (t a) b) c -> (a c) (b c), (t (t a b) c) t -> a, (t (t a b) c) (t u) -> b u, (t (t a b) c) (t u v) -> (c u) v처럼 보는 편이 낫다
    또 표에는 문법의 결합성에서 “당연히” 나온다고 본 듯한 경우가 빠져 있는데, t a -> (t a), (t a) b -> (t a b)처럼 추가해 두면 E E 문법의 표현식에 의미 축약을 더 깔끔하게 적용할 수 있음
    핵심은 람다 계산법에서 람다를 묶어 두 선택지 중 하나를 “고르게” 만드는 것처럼, 이 Tree Calculus는 주어진 노드가 잎, 줄기, 갈래인지에 따라 세 가지 선택을 하도록 만들어졌다는 점임. 규칙 3a, 3b, 3c의 핵심이 이것이고, 시스템의 나머지 기능은 이 3분기 선택 위에 쌓임

    • 이 설명이 첫 페이지에 있었어야 함
      덕분에 재미있는 계산법처럼 보이긴 하지만, SKI나 람다 계산법보다 역변환, 직렬화, 컴파일에 더 적합한지는 별개임. 역변환은 어렵고, 직렬화는 쉽고, 컴파일은 그럭저럭 쉬운 편임

  • Python으로는 Leaf를 빈 리스트, Stem을 단일 원소 리스트, Fork를 두 원소 리스트로 두고 apply를 명세의 OCaml 코드에 맞춰 구현할 수 있음
    false, true, not을 트리로 정의하면 not false -> true, not true -> false가 동작함

    • Racket이나 Scheme으로도 같은 아이디어를 쓸 수 있음
      Leaf는 null, Stem은 list, Fork는 cons로 두면 되고, apply t-not t-false와 apply t-not t-true로 같은 결과를 확인할 수 있음
답변달기