수리논리빌런들 빨리등판해라
[일반] judgemental, propositional identity뭔차이냐?
익명(118.235)
2021-12-18 15:11
추천 0
댓글 60
다른 게시글
-
아 현타오네 [4][일반] 흔들흔들(hm010323) | 21.12.18추천 0
-
어케풀까여 [7][대학교이상] 익명(116.41) | 21.12.18추천 0
-
대수경 2분야 8번 풀어주실분 [2][일반] 익명(180.230) | 21.12.18추천 0
-
일본 수학자들 에세이 읽고 싶은데 [3][일반] 익명(18.31) | 21.12.18추천 0
-
대수경 1분야 7번 [4][일반] 익명(112.161) | 21.12.18추천 0
-
이번에 대수경 처음 해봤는데 [4][일반] 흔들흔들(hm010323) | 21.12.18추천 0
-
대수경 1분야 5문제 반 정도면 은상 가능한가요?? [15][일반] 익명(112.161) | 21.12.18추천 0
-
수학과 졸업논문 [2][대학교이상] 카레라면(134.76) | 21.12.18추천 0
-
학교에 2,3년에 한번씩 열리는 과목이 있는데 [11][일반] 익명(222.238) | 21.12.18추천 0
-
여기에 통계 교재 질문 올려도 괜찮나요 [13][일반] 안아줘요(iqhfnxlz0724) | 21.12.18추천 0
propositional equality x = y 는 말 그대로 x랑 y가 같다는 명제임. judgemental equality는 메타레벨에서 어떤 두개가 같다는걸 아는거임. 그러니까 명제가 아님
judgemental equality가 있으면 propositional equality를 construct할 수 있음. 하지만 propositional equality에서 judgemental equality를 얻을 수 있는지 여부는 타입시스템마다 조금씩 다름
그거 construction하는거 예시 좀 보여줄수있음? 납득좀시켜주셈 그게 이해가 안감
identity type에는 refl : ∀ x → x = x 라는 constructor가 있음. judgemental equality x ≡ y 가 있을 때 propositional equality x = y 는 refl x 로 construct 할 수 있음. 왜냐면 {judgemental equality x ≡ y 로 부터 (x = x) ≡ (x = y) 이고 (i)} {A ≡ B 이면 x : A 일 때 x : B (ii)} {refl x : x = x (iii)} 이거 세개에서 refl x : x = y 임.
propositional equality가 judgemental equality를 imply하면 extensional type theory라고 하는데, extensional type theory에서는 타입체킹이 decidable하지 않고, equality가 mere proposition이라는 특징이 있음. mere proposition 이라는건 inhabitant가 (증명이) 없거나 최대 한개라는 소리임.
intensional type theory는 propositional equality에서 judgemental equality를 얻을 수 없고, equality의 inhabitant가 여러개일 수도 있음. 예를 들어서 homotopy type theory에서는 Bool = Bool 의 inhabitant가 두개임. 하나는 {true -> true, false -> false} 로 보내는 equality고, 다른 하나는 {true -> false, false -> true} 로 보냄
아 construction 예시에서 말하는 (i), (ii), (iii) 은 전부 메타레벨에서 하는 얘기임
근데 그 두 개를 구분하는 이유가 뭐임? 컴퓨터도 어차피 둘 다 쓰는거 아님?
두 개가 propositional/judgemental 말하는거야 아니면 extensional/intensional 말하는거야?
Propositional equality를 메타적으론 참이라고 증명가능한데 내부적으로 증명이 안되는 케이스가 있단건가
Prop/judge
논리체계를 형식화 하려 하면 메타적인게 필요할 수 밖에 없음. 그리고 아까도 말했듯이 propositional equality랑 judgemental equality가 서로 유도가 되는 체계가 extensional type theory인데, 얘는 타입체킹이 결정 불가능임.
아니 형식화시키는건 알겠는데 그럼 컴퓨터는 보통 이론 내부에서 전개하는거임? 아니면 메타적으로 전개하는거임? 이 두개를 구분하는 건 알겠음. 근데 어디서부터 어디까지 사용되는거고 어떻게 구분돼서활용되는지 모르겠음 . 그래서 그 구분이 이런식인가해서 물어는거임. "x=y를 메타적인 방법 외에 증명못할수도 있단거지?"
증명언어를 예로 들면 증명은 object level이고, 컴퓨터는 증명에 대한 타입 검사를 수행하는데 타입검사는 메타적임.
그니까 사람이 x=y를 어떤 이론내에서 증명하고 싶어서 막 증명을 쓰면 컴터는 타입정도만 메타적으로 분석해주는거고 증명자체는 그렇게 안한다는거임?
intensional type theory의 경우 judgemental equality는 정의에서 얻는 방법 밖에는 없음. 그래서 definitional equality 라고도 함. 예를 들어서 +를 {zero + n = n; suc m + n = suc (m + n)} 로 정의했으면 judgemental equality suc (suc m) + n ≡ suc (suc (m + n)) 를 얻을 수 있음
propositional equality는 definition에서 바로 나오지 않는것도 다룰 수 있음. 예를 들어서 forall m n, m + n = n + m 은 귀납법을 써서 proposition으로 증명할 수 있음.
그렇게 보이까 judgemental이 더 약한건 알겠네
α, β 축약 같은거는 그럼 그냥 어느 이론이든 자연스럽게 허용된다고 봐야하나? 이걸 메타적이라고 부르니까 이론 밖에서 하는거 같아서 찜찜한데 이론 내에서 써도 증명이 이론밖에서 진행되는 건 아닌거같아서
일단 judgemental 하게 같으면 대상 언어에서는 애초에 두 대상을 구분하는게 불가능함. α, β reduction은 보통 메타레벨에서 해줌. (λx → x) 10 ≡ 10 같은건 judgemental 하게 성립하는거지. 근데 η equality는 메타레벨에 넣는 경우도 있고, proposition으로만 증명 되는 경우도 있음. judgemental equality가 성립하는 범위는 결국 타입시스템 디자인에 달린거지.
뭔진 대강 알겠긴 하네 컴퓨터나 증명을 쓰는 인간이나 대충 문자열 다르면 다르다고 인식하지만 이름 명찰만 다르게 해놓은 경우면 대상 이론에선 그냥 같은 거로 보는거네 애초에 문자열을 이용한 표현이란개념도 그냥 메타적인거이니까
judgemental equality랑 propositional equality는 애초에 도입한 이유가 좀 다름. propositional equality는 equality를 다룰 수 있는 타입체계를 만들기 위해서 필요한 거고, judgemental equality는 dependent type checking을 하다 보니 타입 체킹을 할 때 term에 대한 equality가 필요해져서 도입한거.
dependent type이 없으면 타입검사를 할 때 α, β 변환 같은걸 생각 안해도 되니까 judgemental equality가 필요 없음.
그걸 들으니까 더 헷갈리는데..
그냥 simple type theory에도 그건 쓰는게 아니었음?
Hindley-Milner type system 이나 System F 에는 typing judgement (t : A) 만 있고 judgemental equality (x = y) 같은게 없음. 왜냐면 저런 체계에서는 어떤 두 타입이 같으려면 syntactic하게 같아야 됨. α나 β reduction 도 고려할 필요가 없다는 이야기. 그러니 메타레벨에서 judgemental equality같은 복잡한 equality 개념이 필요없는거.
그냥 문자치환하는거조차 같다고 취급을 못한다고? ㄷㄷ 뭔 그런 미친 타입시스템이있냐
엥 아니 먼가 전달이 잘못 된것같은데
(두 타입이 같다) iff (두 타입이 syntactic 하게 같다) 니까 걍 syntactic하게 같은지만 검사해도 된다고.
Syntatic하지 않은 Judgementally equal이란게 있음?
근데 잠깐만 이게 문자열에 대한게 아니라 타입 전체에 대한거임?
처음부터 문자열 이야기는 하지도 않았는데
아 시발 골아파
judgementally equal이란게 대체 머임.. 어느 타입체계에선 필요없고 어느 타입체계에선 필요하고 그런거보면 뭐든 정의가 있단거아냐
syntactic 하게 같다는건 Bool이랑 Bool이 같다 이런거고. judgemental equality는 equality up to alpha/beta reduction 같은걸 보고 싶으니까 필요한거지.
굉장히 딱딱한 타입시스템인가보네 어케 굴러가길래
딱딱한게 아니라 애초에 lambda abstraction 같은게 없으니까 저런게 필요가 없어
제일 간단한 예로 simply typed lambda calculus를 보면 여기선 타입을 만드는 방법이 Base 랑 함수타입 (->) 뿐임. 그러면 이거에 대한 equality를 검사 할 때에는 alpha고 beta고 다 필요없고 그냥 진짜 syntactic하게 똑같은지 검사하면 됨
term에 대한 equality가 아니고 type에 대한 equality임
dependent type에서는 type이 term에 의존하니까 term에 대한 judgemental equality가 필요한거고.
그럼 judgemental equality라는 건 term에는 안 쓰인다는거임?
원래 타입 검사에서 필요한건 type에 관한 equality인데, dependent type에서는 type에 관한 equality를 만들려면 term에 관한 equality도 필요해짐.
솔직히 잘 몰겠음.. Propositional equal도 type에 대한거임?
propositional equality는 term에 대한게 맞음. dependent type에서는 type도 term이라서 type도 다룰 수 있고.
그니까 dependent type theory 밖에선 term에 대해선 judgemental equal을 안 따진다는거임? 왜? 그럼 거기선 뭐라고 부름?
judgemental equality는 타입 체킹 할라고 필요한건데, term에 대한 equality가 없어도 다 되니까 필요 없지
걍 쉽게 얘기하면 Propositional Equality는 증명 언어 내부의 등호임. 예를 들어 Inductive eq {A : Type} (x : A) : A -> Prop := | eq_refl : eq x x. 그에 반해 Judgemental Equality는 증명 언어의 타입체커가 내리는 판정 중 하나인데, 두 항이 서로 변환 가능하다는 뜻임.
뭔지 모르겠다 타입체커는 메타적으로 전개하고 있는데 굳이 이론에서 구분하는 이유를
논리학 어디까지 파셨음?
지금 뭔소리하는진 알겠는정도 근데 컴터에서 이걸 올리는데 이정도까지 그분하는이유
어떤 걸 정의했으면 그 정의랑 그 정의 안에 든 놈이랑 같은지는 컴퓨터가 이미 알고 있어야 할 거 아니냐
그 정의랑 그 정의 안에 든 놈? 이 왜 같아야함..
Definition double (n : nat) := n + n. 했다쳐봐. x : nat일 때 double (2 * x)랑 (2 * x) + (2 * x)랑 같은지는 알아야지.
그렇지 그건 알아야하는데 그렇게 치환하는게 이론내에서 허용된다고 생각하는거임?
메타-적이라고 하니까 좀 이론내에서 알아서 못하는 느낌이 들어서
그냥 이름이랑 형태만 바꾸는거니까 괜찮은거라고 보는건가?
내말은 Judgemental Equality가 없으면 eq (double (2 * x)) ((2 * x) + (2 * x)) 이런 게 well-typed인지 컴퓨터가 어떻게 아냐는 말이야.
아니 뭔 소리하는건지 모르겠네 그건 필요한데 왜 구분하냐는게 질문이잖아
뭔 소리 하는지 알고 싶어? 증명보조기 만들어봐. 그럼 알게 돼.
결론: 문자열 채로 unification을 하는 Metamath는 ㅄ이다 ㅇㅋ?