Profile img

Ailrun (UTC-5/-4)

@ailrun@hackers.pub · 3 following · 44 followers

소개 - Who Am I?

  • 개발자/연구원
  • Haskell Language Server Admin
  • PL Theorist
  • Logician
  • 중증 맥덕

근황 - Recent Interests

  • 언어간 상호운용성(Interoperability) 연구 중
  • 의존적 형이론(dependent type theory) 연구 중
  • 효율적인 레이텍 조판(LaTeX Typesetting) 공부 중
  • Québec 에서 제일 맛있는 Stout 마시는 중
GitHub Page
ailrun.github.io/ko
GitHub
@Ailrun
1
0
0
3
1
0
2
0
0
0
0
0
1
2
0
lionhairdino @lionhairdino@hackers.pub
Quiet public

아, 뭔가 못살게 구는 줄 알았는데, 행사장이 미어 터져서 사람 잡는 거였군요. ㅎㅎ
논문이라 하니, 비전공자는 봐도 모를테고, 미어 터지는 행사장 사진 하나 올려주시지요.
슬... 전공자 경계선에 있는 글 하나 올라올 때 되지 않았나요. 이왕이면 비전공자쪽으로 좀 더 넘어 온 걸로요. @ailrunAilrun (UTC-5/-4)

1
1
0
1
1
0
0
1
0
1
1
0
1
0
0
lionhairdino @lionhairdino@hackers.pub
Public

최근 하스켈 리포트를 보니, 언어 서버 지원이 뭔가 바뀌었답니다.

Hannes made hie-bios use Cabal’s --with-repl command to load the session, which greatly simplifies the implementation and its treatment of multiple home units

이런 게 있네요. 당연히 --with-repl 로 했어야 하는 것 아닌가, 기존에는 어떻게 했나 찾아보니, 각 툴들이 각자 도생하고 있었다네요. 명확히 동일한 환경으로 언어 서버가 실행되는 줄 알았는데, 아니었나 봅니다.

1
1
0
Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

http://logitext.mit.edu/main 재미있는 웹 앱 중 하나. 논건 대수(Sequent Calculus)를 사용해 1차 논리("모든 대상에 대해"나 "어떤 대상이 있어"를 서술할 수 있는 논리)의 명제를 상호작용을 통해 증명해 볼 수 있다. 예를 들어 A /\ B -> A (A 그리고 B이면 A이다)를 증명하려면

  • 위 명제를 입력칸에 넣는다.
  • ->를 눌러 명제 안의 "이면"을 증명에서 쓸 수 있는 가정(|-의 왼쪽에 있는 것)으로 바꾼다.
  • 가정의 A /\B를 눌러 "그리고"의 양 측에 해당하는 가정 A와 B 각각을 얻는다.
  • 가정이나 결론의 A를 눌러 가정을 사용하는 것으로 증명을 끝낸다.

보다 입문자에게 친절한 설명은 http://logitext.mit.edu/tutorial 에서 읽어볼 수 있다.

Logitext

logitext.mit.edu

2
0
0
Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

http://logitext.mit.edu/main 재미있는 웹 앱 중 하나. 논건 대수(Sequent Calculus)를 사용해 1차 논리("모든 대상에 대해"나 "어떤 대상이 있어"를 서술할 수 있는 논리)의 명제를 상호작용을 통해 증명해 볼 수 있다. 예를 들어 A /\ B -> A (A 그리고 B이면 A이다)를 증명하려면

  • 위 명제를 입력칸에 넣는다.
  • ->를 눌러 명제 안의 "이면"을 증명에서 쓸 수 있는 가정(|-의 왼쪽에 있는 것)으로 바꾼다.
  • 가정의 A /\B를 눌러 "그리고"의 양 측에 해당하는 가정 A와 B 각각을 얻는다.
  • 가정이나 결론의 A를 눌러 가정을 사용하는 것으로 증명을 끝낸다.

보다 입문자에게 친절한 설명은 http://logitext.mit.edu/tutorial 에서 읽어볼 수 있다.

Logitext

logitext.mit.edu

4
1
0
2
0
0
2
0
0
Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

연구자로서, 또한 한 명의 개발자로서 현 세대에 항상 궁금한 것은 AI가 얼마나 도움이 되느냐이다.

Haskell, OCaml은 말할 것도 없고, JavaScript, Python도 AI와 써 본 경험으로는 그들이 큰 도움이 되느냐는 질문에 자신있게 "그렇다"고 하기 힘든 경험만 해봤기 때문이다.

내가 코드의 형식에 대한 집착이 너무 심한 것이 원인일 수는 있겠으나... AI가 준 결과를 여기 바꾸고 저기 바꾸다보면 결국 내가 쓴 처음부터 코드가 된다.

얼핏 드는 생각으로는 거의 "타입도 없고 문서화도 잘 안되어 있는 환경에서는 사람들이 기능을 이해하기 어려우니 AI를 쓰겠다..."싶다가도, "그러면 내가 잘 아는 분야에 대해서 왜 AI를 써야하지?"하는 생각도 떨치기 힘든 상황이 자주 찾아온다.

결과적으로 나는 AI를 사용하려는 시도를 (적어도 일시적으로는) 멈추었다.

0
0
0
Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

연구자로서, 또한 한 명의 개발자로서 현 세대에 항상 궁금한 것은 AI가 얼마나 도움이 되느냐이다.

Haskell, OCaml은 말할 것도 없고, JavaScript, Python도 AI와 써 본 경험으로는 그들이 큰 도움이 되느냐는 질문에 자신있게 "그렇다"고 하기 힘든 경험만 해봤기 때문이다.

내가 코드의 형식에 대한 집착이 너무 심한 것이 원인일 수는 있겠으나... AI가 준 결과를 여기 바꾸고 저기 바꾸다보면 결국 내가 쓴 처음부터 코드가 된다.

얼핏 드는 생각으로는 거의 "타입도 없고 문서화도 잘 안되어 있는 환경에서는 사람들이 기능을 이해하기 어려우니 AI를 쓰겠다..."싶다가도, "그러면 내가 잘 아는 분야에 대해서 왜 AI를 써야하지?"하는 생각도 떨치기 힘든 상황이 자주 찾아온다.

결과적으로 나는 AI를 사용하려는 시도를 (적어도 일시적으로는) 멈추었다.

2
0
0
Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

연구자로서, 또한 한 명의 개발자로서 현 세대에 항상 궁금한 것은 AI가 얼마나 도움이 되느냐이다.

Haskell, OCaml은 말할 것도 없고, JavaScript, Python도 AI와 써 본 경험으로는 그들이 큰 도움이 되느냐는 질문에 자신있게 "그렇다"고 하기 힘든 경험만 해봤기 때문이다.

내가 코드의 형식에 대한 집착이 너무 심한 것이 원인일 수는 있겠으나... AI가 준 결과를 여기 바꾸고 저기 바꾸다보면 결국 내가 쓴 처음부터 코드가 된다.

얼핏 드는 생각으로는 거의 "타입도 없고 문서화도 잘 안되어 있는 환경에서는 사람들이 기능을 이해하기 어려우니 AI를 쓰겠다..."싶다가도, "그러면 내가 잘 아는 분야에 대해서 왜 AI를 써야하지?"하는 생각도 떨치기 힘든 상황이 자주 찾아온다.

결과적으로 나는 AI를 사용하려는 시도를 (적어도 일시적으로는) 멈추었다.

7
3
0
4
0
0
Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

@curry박준규 all을 다음과 같이 정의하면 문제가 무엇일까요?

all p [] = False
all p [x] = p x
all p (x:xs) = p x && all xs

이 질문에 대한 대답 중 all의 의미에 관한 것이 있을 겁니다. 논리적으로 "모든 ...에 대해"를 어떻게 이해해야 하는냐에 대한 것 말이지요.

공집합을 직접 사용하는 것이 가장 간단한 예시겠지만, 좀 더 논리학에서 자주 사용되는 예시로는 "20세기의 모든 프랑스 왕은 대머리다"가 있겠습니다. 이는 무의미하게 (Vacuously) 참인데요, 왜냐면 19세기를 마지막으로 프랑스에는 더 이상 왕이 없기 때문이지요. 즉, 일반적으로 "모든 ...에 대해"에서 "..." 부분이 (결과적으로) 공집합일 경우 "모든 ..."에 의해 수식된 본문이 어떤 문장인지와는 상관 없이 참이라고 이해한다는 것이지요.

2
0
0
구슬아이스크림 @icecream_mable@hackers.pub
Public

살짝 다른 차원에서 확장해서 바라보는 얘기이긴 한데 그냥 첨언하자면 언어학의 하위 분야인 화용론에서 전제(Presuppositions)라는 주제랑 연결되는 것 같네요. 댓글에 프랑스 왕은 머머리다 예문도 써주신 걸 보니 더욱 더 그런 것 같고요. 간단하게 설명드리자면, 일단 한국어 예문으로 하면 살짝 오해의 소지가 있어[1] 영어 예문을 갖고 쓰면 다음과 같이 생각해볼 수 있습니다.

  • P: The King of France is bald.[2]
  • Q: There exists an entity that is King of France.

이 때 P의 명제가 참일 수 있는 이유는 Q를 전제로 깔고 가기 때문입니다. 이렇게 Q를 전제로 갖고 가면 P에 부정을 넣어도 (The King of France is not bald 혹은 ¬(The King of France is bald)) 여전히 그 명제는 참입니다. 하지만 실제 현실에서 Q는 거짓입니다. 왜냐하면 오늘날 프랑스는 군주국가가 아니니깐요. 그럼에도 불구하고 P는 여전히 참을 진리값으로 가지죠.

따라서 실제로 전제를 이렇게 정의하기도 합니다 (Levinson, 1983, p. 175).

  • A sentence P sematically presupposes a sentence Q iff:
  • (a) P ⊨ Q
  • (b) ~P ⊨ Q

참고로 여기서 "⊨"는 "함의한다"를 지칭하는 기호입니다 (예: "하스켈은 함수형 언어다."란 문장은 "하스켈은 언어다"란 걸 함의하죠.).

그렇다면 Q가 전제되는 건 알겠는데, 이 진리값이 무엇이느냐에 대한 질문이 생길 수 있습니다. 이에 대해서 언어학자들은 보통 크게 두 가지로 봅니다. 하나는 참으로 간주하는 거고, 다른 하나는 참도 거짓도 아니다라고 보는 거죠. 전자같은 경우엔 어떻게 보면 기계적으로 바라보는 거고, 후자의 경우엔 참/거짓이라는 기존 이치논리(two-valued logic) 혹은 1 또는 0으로 하는 불 논리에서 확장해서 Kleene의 삼치논리(three-valued logic)로 가게 되죠.

참고로 전제 성립 여부 포함 화용론 전체에서 깔고 가는 가장 큰 가정이 하나 있는데, 이 경우에는 바로 해당 발화(utterance) P, 즉 '프랑스왕은 머머리다'라는 명제가 이루어질 때 화자와 청자가 프랑스에는 왕이란 개체가 존재한다(=Q)라고 암묵적으로 서로 동의한다라는 가정입니다.

  1. 사실 문제가 영어 관사 'The'에서 시작되기 때문이라서 그렇습니다. ↩︎

  2. 논리형으로 치환하면 다음과 같습니다: ∃x(KoF(x) & ∀y(KoF(y) → y=x) & Bald(x)) where KoF stands for "King of France". ↩︎

Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

@icecream_mable구슬아이스크림 언어학과 논리학에서 "전제"로 번역되는 단어가 다르다는 걸 오늘 알았네요. 논리학에서는 premise가 전제고, presupposition은 그와는 별개의 것인데 (번역이 따로 있는지는 모르겠습니다만) 언어학에서는 presupposition을 "전제"로 번역하는군요.

본문으로 돌아가서, 제시하신 문장에서 핵심은 주석에서 언급하셨듯 "the"의 사용에 있겠죠. 영어에서 "the"는 청자와 화자가 암묵적으로 동의할법한 후술하는 대상을 얘기하니까요. 대상을 나타내는 메타 변수 x에 대해 "the" x라는 표현의 presupposition이 existence of x이겠습니다. 억지로 번역해본다면 "그 프랑스 왕은 대머리다"라고 했을 때 청자와 화자가 공통적인 (잘못됐을 수도 있는) 인식인 "프랑스 왕이 (그곳에) 존재한다"를 공유하고 있다고 할 수 있겠습니다.

3
1
0

Ailrun (UTC-5/-4) replied to the below article:

공허한 참

박준규 @curry@hackers.pub

하스켈의 `all` 함수에 빈 리스트를 넣었을 때 왜 `True`가 반환되는지에 대한 의문을 "공허한 참(Vacuous truth)"이라는 개념을 통해 탐구합니다. 흔히 '구현이 그렇게 되어 있으니까'라고 생각할 수 있지만, 저자는 이 현상을 논리적으로 분석합니다. `all` 함수의 구현 방식과, 빈 리스트에 대한 연산 결과가 전체 결과에 미치는 영향을 설명하며, 공집합의 모든 원소가 짝수라는 명제가 참인 이유와 유사한 논리적 근거를 제시합니다. 이를 통해 코드와 수학 간의 연결고리를 발견하고, 마지막으로 ChatGPT가 생성한 유머러스한 이미지를 곁들여 독자에게 즐거움을 선사합니다.

Read more →
5
2
2
Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

@curry박준규 all을 다음과 같이 정의하면 문제가 무엇일까요?

all p [] = False
all p [x] = p x
all p (x:xs) = p x && all xs

이 질문에 대한 대답 중 all의 의미에 관한 것이 있을 겁니다. 논리적으로 "모든 ...에 대해"를 어떻게 이해해야 하는냐에 대한 것 말이지요.

공집합을 직접 사용하는 것이 가장 간단한 예시겠지만, 좀 더 논리학에서 자주 사용되는 예시로는 "20세기의 모든 프랑스 왕은 대머리다"가 있겠습니다. 이는 무의미하게 (Vacuously) 참인데요, 왜냐면 19세기를 마지막으로 프랑스에는 더 이상 왕이 없기 때문이지요. 즉, 일반적으로 "모든 ...에 대해"에서 "..." 부분이 (결과적으로) 공집합일 경우 "모든 ..."에 의해 수식된 본문이 어떤 문장인지와는 상관 없이 참이라고 이해한다는 것이지요.

5
1
0
1
1
0
0
1
0
5
1
0
1
0
0
1
1
0
박준규 @curry@hackers.pub
Public

GHCup 오랜만에 다시 설치하는데 못보던 게 생겼다.

GHCup provides different binary distribution "channels". These are collections of tools
and may differ in purpose and philosophy. First, we select the base channel.

[S] Skip  [D] Default (GHCup maintained)  [V] Vanilla (Upstream maintained)  [?] Help (default is "Skip").
2
1
0
lionhairdino @lionhairdino@hackers.pub
Public

https://well-typed.com/blog/2025/08/standard-chartered-supports-haskell-ecosystem/
제일은행을 먹은 SC(Standard Chartered)가 하스켈 생태계에 돈을 보태겠다네요. SC가 하스켈을 프로덕트에 조금씩 쓰고 있다는 얘기는 들은 적 있는데... 뭐 얼마나 후원하는지는 자세히는 안나와 있습니다만, 대기업 돈이 들어오면, 긍부정적 변화가 생기긴 하는데.. 툴체인이 정돈된다든지 해서 입문자한테 도움이 되는 변화가 생기면 좋겠습니다. 하스켈을 JS로 트랜스파일링 하는 컴파일러도 있는데, 막상 쓰려고 보면, 난이도가 너무 높아요.

Welcoming a new Haskell Ecosystem Supporter: Standard Chartered

well-typed.com

2
1
0
1
0
0
2
2
0
1
0
0

Ailrun (UTC-5/-4) replied to the below article:

하스켈 편지

박준규 @curry@hackers.pub

이메일 교환을 요약하면, 한국의 취미 프로그래머 박준규 님이 Haskell에 대한 관심을 표현하며 NRAO의 다니엘 님에게 연락을 시작합니다. 다니엘 님은 Haskell 경험과 NRAO에서의 Haskell 프로젝트(antioch)를 공유하며, 박준규 님의 Haskell 학습 경험과 프로젝트에 대한 질문을 던집니다. 박준규 님은 자신이 관리하는 Hackage 패키지와 Protohackers 문제 풀이 경험을 공유하고, 다니엘 님은 이에 대한 격려와 함께 Typeclassopedia와 free monad를 추천합니다. 이 대화는 Haskell에 대한 열정과 지식을 공유하며, 서로에게 영감을 주는 긍정적인 교류를 보여줍니다. 다니엘 님은 박준규 님에게 Haskell 관련 질문을 언제든지 환영하며, 이 대화를 자유롭게 공유해도 좋다고 허락합니다.

Read more →
20
2
0
1
1
0
2
0
0
lionhairdino @lionhairdino@hackers.pub
Public

문법 강조가 바뀔 때가 한참 지난 것 같은데, AI가 별의별 걸 다하는 세상에 아직도 눈에 보이는 소식들이 없네요. 예를 들면, 식별자(변수), 함수, 등 문법 요소에 따라 색을 입힌다거나 하는 게 아닌,
전역이냐, 로컬이냐로 색을 달리 한다든지,
오른쪽 우선 결합 연산자면 빨간색, 왼쪽 우선 결합이면 파란색 한다든지,
시맨틱 문법 강조가 일반화 될 때가 된 것 같은데, 혹시 저만 모르고 있는 건가요?

1
1
0
lionhairdino @lionhairdino@hackers.pub
Public

a = f a 일 때, a를 f의 고정점이라 하니
m a = m (m a) 가 된다면, m a를 m의 고정점이라 할 수 있다.
모나드는 m a = m (m a)가 안되는 것을 join, return의 도움을 받아 성립하게 만든다.
그래서 m의 고정점을 바로 m a라 할 순 없지만, join, return의 도움으로 고정점처럼 동작하게 할 수 있다.
처럼 설명해도 되나 싶습니다.

여러 번 작업 한 걸, 한 번의 작업으로 표현한다.
반대에서 출발해서 보면, 한 번의 작업을 여러 번의 작업으로 인수 분해한다.

이런 목적 측면에서 보면, 고정점도 모나드도 하나의 궤로 설명할 수 있지 않을까 싶습니다.

그냥 상상입니다.

2
1
0
lionhairdino @lionhairdino@hackers.pub
Public

주의: 프로그래머에게도 수학도에게도 쓸모 있지 않은 그저 생각 놀이로, 어제 모임에서 제가 떠들었던 잡담입니다.

튜링 완전한 프로그램은 따로 메모리를 두어 관리하며 돌아가는데, 람다 산법은 이런 메모리가 없는데도 불구하고, 튜링 완전이 할 수 있는 일은 모두 할 수 있다고 합니다. 왜 그럴 수 있는지, 시작 아이디어가 뭘까 생각해 봤습니다. (슬쩍 보기엔, 학문적으로 긴 여정이 있는데, 그 걸 모두 따라가기엔 벅찬 일이라, 절대 따라가고 싶진 않고, 그저 아이디어 정도만 알고 싶습니다.)

함수형에선, 정보를 "기억memory"하는 역할도 역시 함수가 담당합니다. 기억이 필요할 땐 함수 구조를 주어, 기억 공간을 만든다고 볼 수 있습니다. 함수 합성에서 다음 함수의 인자로 새로 바인딩하며 기억의 역할을 합니다. 애초 메모리 모델이 없는 게 아니라, 다른 구조로 메모리 모델을 구현했다고 볼 수 있는 것 아닌가 싶습니다. (이렇게 말하는 곳은 없습니다.)

람다 함수는, "따로 호출할 일이 없어 이름 없는 함수로 정의한다" 쯤으로 넘어가기엔, 숨어 있는 의미가 너무 큽니다. 분명, 이렇게 넘어갈 일이 아닌데, 역시나 친절히 설명해주는 자료를 아직은 못봤습니다. (많이 찾아 보 거나, 깊게 공부한 건 아니라서, 어딘가에는 있지 않을까 싶어요)

람다 함수로 만들어,

  • 실행 시점 제어
  • 함수 합성 체인 참여
  • 필요한 정보들을 모아 두는 단위
  • 외부와 소통하는 길을 만들어 둘 수 있고, ...

여기에 기억이라는 중요한 역할도 담당하게 합니다.

람다 산법은 매개 변수, 함수 몸체, 적용, 이렇게 3가지 요소만으로 모든 걸 해결합니다. 알론조 처치 아저씨는 어찌 이런 구조를 떠올렸을까 싶습니다. 애초에 위와 같은 식으로 볼 수 있는 함수 통찰의 눈이 먼저 있었던 상태에서 만든 거겠지요?

2
0
0
Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

"AI[1] 덕분에 ***가 민주적이 된다"는 말이 자주 나오고는 한다. 나는 이에 매우 회의적이다. 다른 것은 다 받아들여서 AI가 많은 사람들이 어떤 일을 매우 싸게 (거의 공짜로) 할 수 있게 해준다고 쳐도, AI로 만들어내기 힘든 수준의 "고급" 결과물은 여전히 존재하고, 이는 특정 직군의 고경력 전문가에게 넘어가게 된다. 문제는 이 "경력"을 어떻게 쌓느냐이다. 해당 직군의 초보자들은 AI에 밀려 경쟁력을 잃기 십상이고, 그들을 위한 여러 자리를 (AI를 활용하여 생산성을 높인) 전문가 한 명이 대체하기도 한다. 어떤 직군을 가질 수 있는 조건이 말하자면 이미 엄청난 실력을 가질 것이 되는 환경의 조성을 "민주적이다"라고 할 수 있을까?

  1. 정확히는 최근 많이 사용되는 미디어(Media) 생성 인공지능들과 대형 언어 모형(Large Language Model, LLM)들 ↩︎

1
0
0
Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

"AI[1] 덕분에 ***가 민주적이 된다"는 말이 자주 나오고는 한다. 나는 이에 매우 회의적이다. 다른 것은 다 받아들여서 AI가 많은 사람들이 어떤 일을 매우 싸게 (거의 공짜로) 할 수 있게 해준다고 쳐도, AI로 만들어내기 힘든 수준의 "고급" 결과물은 여전히 존재하고, 이는 특정 직군의 고경력 전문가에게 넘어가게 된다. 문제는 이 "경력"을 어떻게 쌓느냐이다. 해당 직군의 초보자들은 AI에 밀려 경쟁력을 잃기 십상이고, 그들을 위한 여러 자리를 (AI를 활용하여 생산성을 높인) 전문가 한 명이 대체하기도 한다. 어떤 직군을 가질 수 있는 조건이 말하자면 이미 엄청난 실력을 가질 것이 되는 환경의 조성을 "민주적이다"라고 할 수 있을까?

  1. 정확히는 최근 많이 사용되는 미디어(Media) 생성 인공지능들과 대형 언어 모형(Large Language Model, LLM)들 ↩︎

4
1
0
lionhairdino @lionhairdino@hackers.pub
Public

원숭이가 키보드를 쳐도 수 억번 치면 확률상 실제 동작하는 프로그램이 나오는데, LLM이 로컬에서 브루트포스를 할 수 있는 때가 오면, 테스트 통과 조건만 깔짝대면 완성된 프로그램이 나오는 때가 얼마 안남았네요.

Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

@lionhairdino 사실 테스트 통과 조건만 가지고 프로그램을 완성하는 건 (더 잘 정립된 방법으로) 현재에도 이곳저곳에 활용되고 있습니다. 대표적으로 엑셀(Excel)의 플래쉬 필(Flash Fill)이 있지요. 이와 관련된 분야를 프로그램 합성(Program Synthesis)라고 하고, 수십년 전부터 (AI보다는 투명한 방법으로) 꽤 활발하게 연구되어왔습니다.

4
1
0

논리와 메모리 - 논리와 저수준(Low-level) 자료 표현(Data representation) (2 편 중 2 편)

Ailrun (UTC-5/-4) @ailrun@hackers.pub

이 글은 "논리적"이 되는 두 번째 방법인 논건 대수를 재조명하며, 특히 컴퓨터 공학적 해석에 초점을 맞춥니다. 기존 논건 대수의 한계를 극복하기 위해, 컷 규칙을 적극 활용하는 반(半)공리적 논건 대수(SAX)를 소개합니다. SAX는 추론 규칙의 절반을 공리로 대체하여, 메모리 주소와 접근자를 활용한 저수준 자료 표현과의 커리-하워드 대응을 가능하게 합니다. 글에서는 랜드(∧)와 로어(∨)를 "양의 방법", 임플리케이션(→)을 "음의 방법"으로 구분하고, 각 논리 연산에 대한 메모리 구조와 연산 방식을 상세히 설명합니다. 특히, init 규칙은 메모리 복사, cut 규칙은 메모리 할당과 초기화에 대응됨을 보여줍니다. 이러한 SAX의 컴퓨터 공학적 해석은 함수형 언어의 저수준 컴파일에 응용될 수 있으며, 논리와 컴퓨터 공학의 연결고리를 더욱 강화합니다. 프랭크 페닝 교수의 연구를 바탕으로 한 SAX는 현재도 활발히 연구 중인 체계로, ML 계열 언어 컴파일러 개발에도 기여할 수 있을 것으로 기대됩니다.

Read more →
12
0
0
3
0
0
4
1
0
lionhairdino @lionhairdino@hackers.pub
Quiet public

생각보다 훨씬 자세하게 명문화된 규칙이 있군요.! 공부하면서 이 예시 저 예시 보다 보면, 버전이 널뛰고, 그러다 보면 HLS 지원이 오락 가락하게 되어, 사실 각 잡고 프로젝트에 쓰는 것 아니면, 의존도가 높지 않게 되어버리더라고요. 그 이유가 버전 지원 때문이란 생각에, 미리 HLS 친화적인 버전을 골라낼 수 있나 했는데, 그러긴 어려울 것 같네요.

0
1
0
1
0
0
1
2
0
1
2
0
Ji-Haeng Huh @jhhuh@hackers.pub
Public

@ailrunAilrun (UTC-5/-4) 정말 좋은 글 정말 감사합니다. 아직도 CS관련 글을 보다가 가로로 긴 직선만 나오면 "이거 내가 읽어도 되나?" 싶은 생각이 들면서 읽기를 포기하곤 하는데 기초적인 부분부터 너무 잘 설명해주셔서 끝까지 읽을 수 있었습니다. (사실 두번 읽었습니다.)

자연 연역의 E/I 룰에서는 항상 가정의 목록이 유지되거나 줄어들어 "가정의 소비(?)"된 정도를 기준으로 증명을 순차적으로 구성하거나 파악하는게 유리한 대신 전건과 후건을 다루는데 있어서 그 대칭성이 보이지 않는다. 대신 이와 동등한 논건대수에서는 추론 규칙에 전건과 후건 사이의 대칭성을 명백히 드러냄으로써 추론 시스템 자체의 특정 구조적인 성질을 이해하는데 유리할 수 있다.

라는 생각이 들었는데 이게 올바른 관찰일까요?

"이 내용들이 2 편에서 다룰 본격적인 논리와 자료 표현의 관계에 대해 흥미를 불러일으켰기를 바라며" -> 2편 정말 기대됩니다. ㅎ

Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

@jhhuhJi-Haeng Huh

자연 연역의 E/I 룰에서는 항상 가정의 목록이 유지되거나 줄어들어 "가정의 소비(?)"된 정도를 기준으로 증명을 순차적으로 구성하거나 파악하는게 유리한 대신 전건과 후건을 다루는데 있어서 그 대칭성이 보이지 않는다. 대신 이와 동등한 논건대수에서는 추론 규칙에 전건과 후건 사이의 대칭성을 명백히 드러냄으로써 추론 시스템 자체의 특정 구조적인 성질을 이해하는데 유리할 수 있다.

  • 증명을 위에서 아래로 읽으면 자연 연역의 경우 가정이 줄어들기만 하는 것이 맞습니다. 다만 프로그램적인 측면에서는 아래에서 위로 (가정이 늘어나는 방향으로) 읽는 것이 더 자연스러운데요, 이는 가정이 늘어나는 것이 프로그램에서 깊은 스코프(scope)로 들어갈 수록 더 많은 변수를 소개하는 것과 같은 개념이기 때문입니다.
  • "증명을 순차적으로 구성하기 쉽다"는 사실 약간 애매하기는 합니다. 둘 다에 익숙해지면 논건 대수의 증명이 (기계적으로 찾기에) 더 쉽기 때문에요. 실제로 증명 검색 알고리즘(proof search algorithm, 어떤 판단을 증명하는 증명을 찾는 알고리즘)도 논건 대수에 기반하는 경우가 더 많습니다. 다만 이미 만들어진 증명을 "파악"(혹은 이해)하는 데에 있어서는 (프로그래머로서는) 자연 연역의 함수형 프로그램스러운 증명이 훨씬 쉽지요.
  • "대칭성"과 관련한 관찰은 논건 대수의 발전에 있어서 핵심이라고 볼 수 있습니다. 뛰어난 직관을 가지고 계시네요.
3
1
0
lionhairdino @lionhairdino@hackers.pub
Quiet public

"여론에 따라" 함수형 추상 기계 관련 글을 쓰고 있었는데, 쓰다 보니 논리와 low-level data representation 이 보였다는 핑계 말씀이지요? 생각할 엄두조차 내지 못했던 주제들, 다 이해는 못하지만 감사히 보고 있습니다. SPJ, 와들러 교수님 등의 교양 수준 강의 활동들을 보다 보면, 왜 국내 교수님(고인물-댓가없이 입문자들에게 도움을 준다는 의미)들은 없나 아쉬운데, 엘룬님 글로 조금 달래지네요. @ailrunAilrun (UTC-5/-4)

0
0
0