이거 예전에 올렸을 때 댓글에 뭔지 하나도 모르겠다 뭐 그런말이 많았는데
나도 인지하고 있었다만 설명하기엔 쓸 내용이 너무너무 많아서 못썼음.
한 1/3쯤 써둔거 올려봄
근데 사실 논리학 설명 밖에 없음 ㅋㅋ 메타프로그래밍까지 연결되려면 다음글까지는 써야될듯
바빠서 다음글 쓸지도 잘 모르겠고
X X X
메타프로그래밍은 코드 생성을 자동화 할 수 있는 강력한 도구지만 배우고 사용하기 어려워요
특히 자동 생성된 코드를 보면서 디버깅 하기는 정말 쉽지 않겟죠
한가지 이유는 메타프로그램이 만들어 내는 대상(오브젝트) 언어 코드의 올바름을 보장하기 힘들기 때문이에요
메타프로그램이 항상 잘 컴파일 되는 대상 코드를 만든다면 프로그래머가 자동 생성된 코드를 읽을 일이 줄어들겠죠
대상 코드의 올바름을 어떻게 보장 할 수 있을까요
hygienic macro 라는게 있어요
CPP(C preprocessor)가 수행하는 문자열 치환이나 (hygienic이 아닌) 리습 매크로에서는 의도하지 않은 variable capture가 일어날 수 있기 때문에 치환에 변수 이름을 바꾸는 과정을 추가한거에요
Scheme이랑 Rust 하는 사람들 맨날 이걸로 매크로 시스템 자랑하는데 그냥 capture avoiding substitution 같은거에여
hygienic macro는 변수 바인딩을 올바르게 처리하기 때문에 그나마 쓰기 편하지만 모든 문제를 해결하진 않아요
오브젝트 코드의 컴파일 까지 보장하려면 타입을 맞춰야죠
이건 그리 간단한 문제가 아니에요
보통 메타프로그래밍 시스템은
메타프로그램의 타입체킹 -> 메타프로그램 실행 -> 생성된 오브젝트 코드 타입체킹 -> 오브젝트 코드 컴파일 -> 컴파일된 프로그램 실행 ... 이런 순서로 진행 될텐데
메타프로그램이 well typed 오브젝트 코드를 만드는걸 보장한다는건 메타프로그래밍과 생성될 오브젝트 코드의 타입체킹을 동시에 수행한다는 말이죠
놀랍게도 실제로 가능하고 multi-stage programming이라는 분야 에서는 이런 언어에 대해서 연구해요
multi-stage programming language의 타입시스템은 어떻게 설계해야 할까요
Davies & Pfenning의 A Modal Analysis of Staged Computation에선 necessity modality를 응용했어요 https://www.cs.cmu.edu/~fp/papers/jacm00.pdf
근데 제가 보기엔 저것 보다 A Judgemental Reconstruction of Modal Logic을 먼저 훑어 보는게 조은것 가타요 https://www.cs.cmu.edu/~fp/papers/mscs00.pdf
이 시스템들에서 box(necessity) modality는 validity를 logic system에 internalize한 type/proposition 이에요
그래서 이 시스템을 이해하려면 먼저 natural deduction, (hypothetical) judgement, truth, validity의 개념들에 대해 알아야 해요
그냥 A Judgemental Reconstruction of Modal Logic 읽으라고 하고 싶은데 아무도 안읽을테니까 조금 설명해볼게여
즉 대상논리의 proposition과 메타논리의 proposition이 생기겠죠. 메타논리의 proposition은 judgement라고 불러요
가장 기본적인 judgement로는 "A is a proposition", "A is true"가 있어요
"A is a proposition"은 대상 논리의 명제가 될 수 있는것이 무엇인지 얘기하는 거고 "A is true"는 "A"라는 대상논리의 명제가 참(truth) 임을 얘기하는거에요
간단하게 A prop, A true 이런식으로 표기해요
이 "A is true" judgement를 사용하면 연결사(logical connective) 들에 대한 추론 규칙(inference rule)을 줄 수 있어요
자연연역(natural deduction, logic system의 한 종류) 에서는 and(∧)에 대한 추론 규칙을 아래처럼 줘요
A true B true A ∧ B true A ∧ B true
--------------------I1 ------------E1 ------------E2
A ∧ B true A true B true
큰 가로선은 가로선 위의 judgement들을 가정했을 때 가로선 아래의 judgement가 결론으로 나온다는 의미에요
I1은 "A true 이고 B true 이다면 A ∧ B true이다"
E1은 "A ∧ B true 이면 A true 이다"
E2는 "A ∧ B true 이면 B true 이다"
라고 해석하면 돼요
문장을 잘 곱씹어 보면 눈치 챌 수 있는데, 이 추론 규칙이란 것들은 judgement들의 관계를 기술하는 언어이기 때문에 메타논리의 메타논리라고 볼 수 있어요
추론 규칙 자체는 judgement가 아닌거죠
한편 I1을 ∧의 introduction rule, E1과 E2는 ∧의 elimination rule 이라고 해요
자연연역 시스템은 추론 규칙이 이렇게 introduction/elimination rule로 주어지는 특징이 있어요
이것만으론 ∧말고 다른 연결사를 설명할 수가 없어요
implication (A → B)의 추론 규칙은 "If (If A true, then B true) then A → B true"가 되어야 하는데 괄호 안의 If에 해당하는 judgement가 필요하죠
그래서 hypothetical judgement 라는걸 만들었어요
Hypothetical judgement는 "J₁, ..., Jₙ ⊢ J" 꼴로 쓰고, judgement J₁, ..., Jₙ 를 가정한 J를 의미해요
"A true, B true ⊢ C true"는 "A가 참이고 B가 참이면 C가 참이다" 라는 의미의 judgement 인거죠
자연연역에서는 주로 A true, B true, ..., C true ⊢ D true 꼴의 hypothetical judgement를 많이 쓰기 때문에 A true, B true, ..., C true 를 흔히 Γ로 줄여써요
이제 가정인 Γ를 사용하기 위한 규칙이 있어요
---------------
Γ₁, J, Γ₂ ⊢ J
의미는 "(Γ₁, J, Γ₂ 를 가정할 때 J)이다"
가로선 위가 비어있는건 이 inference rule이 가정하는 바가 없다는 뜻이에요
드디어 implication의 추론 규칙을 쓸 수 있어요
Γ, A true ⊢ B true Γ ⊢ A → B true Γ ⊢ A true
--------------------I→ ---------------------------------E→
Γ ⊢ A → B true Γ ⊢ B true
∧의 추론 규칙도 비슷하게 Γ를 붙여서 다시 만들 수 잇어요
Γ ⊢ A true Γ ⊢ B true Γ ⊢ A ∧ B true Γ ⊢ A ∧ B true
--------------------------I1 -----------------E1 ----------------E2
Γ ⊢ A ∧ B true Γ ⊢ A true Γ ⊢ B true
마지막으로 validity만 대충 얘기할게요
"A is valid", 혹은 "A valid"는 "A가 truth에 대한 아무 가정 없이 참이다"를 의미해요. 즉
· ⊢ A true
-----------
A valid
A가 valid 하다면 당연히 true 겠지요
원래 빈 가정이었으니 다른 가정을 넣어도 당연히 성립할거구요
A valid
------------
Γ ⊢ A true
(논리학에서 흔히 말하는 validity와 Pfenning & Davies가 말하는 validity가 분명 관계가 있을텐데 공부를 안해서 모르겟어요
그냥 이걸로 PL이나 만들면 되지 않을까요)
validity까지 길고 지루한 설명을 했는데 이딴걸 왜 정의했는지는 얘기를 안했죠
사실 box와 함께 얘기하는게 맞는것 같은데 box까지 설명하긴 지쳤고 validity도 빠지면 그냥 자연연역 뿐이라 제목값을 못해서 넣엇어요
사족으로 Per Martin-Löf의 ON THE MEANINGS OF THE LOGICAL CONSTANTS AND THE JUSTIFICATIONS OF THE LOGICAL LAWS를 보면
(물론 저도 안읽었습니다만)
A true, ⊢ A, Γ | A true 등의 노테이션을 쓰는데 Γ ⊢ A true는 없어요
위키 백과 turnstile 항목을 보면 왜 그런지 알 수 있어요
https://en.wikipedia.org/wiki/Turnstile_(symbol)
Turnstile (symbol) - WikipediaTurnstile (symbol) - Wikipediaen.wikipedia.orgturnstile (⊢) 에서 |는 "I know", -는 "... is true"를 의미하기 때문에
⊢ A true 라고 쓰면 "I know A is true is true"가 되버린다
때문에 Per Martin-Löf는 저런 무근본 표기를 지양한 것이지요
마지막에 빠뜨렸는데 사실 모던한 노테이션은 그냥 " Γ ⊢ A " 다
뭐임이게
저 MetaLambda 프로젝트는 그 뒤로 이것저것 확장하고 있었는데 급상승한 난이도랑 다른일로 바빠져서 유기됨
너무 산만한데... 틀린 내용은 없는데 뭘 얘기하고 싶은 건지 모르겠음. 20세기 초반 수리논리를 소개하고 싶은 거임?
산만할만 함.. 나중에 뒷부분 쓰면 싹 다 정리해야 할듯
메타프로그래밍을 위한 타입 시스템에서 대상 언어의 코드를 표현할 때 필요한게 사실 box modality 이고, 여기서 사용되는 box modality는 validity와 연관이 깊음
validity를 얘기하려다 보니 context, 자연연역 이런것도 결국 설명해야 돼서 쓴거
provability logic 얘기하고 싶은 거면 네모 쳐놓고 world 갖고 semantics 주는게 일반적이긴 할텐데... 이거 근데 그렇게 가다보면 정말 한도끝도 없이 밑바닥부터 설명해야 되는데 아직 semantics 주는 것도 안 간 거라 거의 뭐 강의노트 분량 나올듯
아 semantics는 얘기 안하고 추론규칙만 가지고 얘기할 생각이였음. 사실 거기까진 나도 잘 모르고
PL이라 logic처럼 안하고 operational semantics를 줄 수도 있는데 그 방식만 어렴풋하게 앎
그리고 이건 그냥 개인적인 취향이라 강요하겠다는 건 아닌데... 추론규칙 얘기할 때 참 거짓 가지고 설명하는게 참 이해하기도 좋고, 나중에는 그렇게 연관지어서 설명해야 되는 거긴 한데, 일단은 추론규칙이라는 건 기계적인 절차인 건 좀 확실히 해줄 필요가 있는거 아닌가 싶음. 안 그러면 추론규칙이랑 참거짓이랑 헷갈릴 수도 있어서... ∧-elimination rule을 직관적으로 이해하고 싶으면 당연히 A ∧B가 참이다에서 A가 참이라는게 추론된다 이렇게 가는게 당연한 거긴 한데.. 뭐 전달이 잘 안 되네
아 그렇지. PL로 가면 proof tree 자체가 어떤 object인게 좀 더 명확하게 전달될것 같은데
다시 읽어보니 너무 truth에 의존해서 쓴것 같긴 하다
아예 truth 이야기 없으면 직관적인 이해가 힘들긴 해서... 설명은 truth 위주로 하되 rule 소개할 땐 람다칼큘러스 reduction 소개하는 것마냥 하면 되지 않을까 싶기도 하고
어차피 이딴거 몰라도 ㄱㅊ
챗gpt가 다해준디 4.0도 나오는데
메타언어가 들어갈 자리에 메타논리가 들어가 있네
'메타논리'라는 단어를 잘못 썼음. 논리를 다루는 논리학이 메타논리임. 대상 언어를 다루는 언어를 메타언어라고 하는데, 여기서는 '메타언어'가 올 자리에 '메타논리'가 있음.
아 그런가. 나는 그냥 논리랑 언어랑 구별이 안되는데.
지적 고맙고, 나중에 찾아보고 정확한 표현으로 수정해보겠음
메타논리가 맞음. 'P라는 명제를 저 논리체계에서 증명 가능하다'라는 말을 사용하고 싶은 거임.
좀 더 쉽게 이해하고 싶으면 '모든 논리체계에서 a ⊢ a는 증명 가능하다' 같은 걸 생각해보면 됨. 그런거 하겠다고 validity 개념 같은 거 끌고오는 거임
증명 가능하다 => 성립한다
사실 난 논리학적인 설명은 잘 모르겠고 그냥 Coq에서 논리체계 형식화 할 때 judgement가 Coq(메타논리)의 proposition으로 정의되는거 생각하면서 메타논리라고 불렀음
그게 맞긴 함