그 입력 규칙은 "On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy" 용지에 존재하는 다음 “What part of Milner-Hindley do you not understand?” 스택 오버플로 질문에서이 백서의 타이핑 규칙을 어떻게 해석 할 수 있습니까?
, 나는 영어로 그 중 일부를 읽을 수 있지만, 유형을 만드는 방법을 파악하는 것은 여전히 어렵다 그것의 검사기.
도끼 : 이것은 처음 4 개 규칙을 읽는에서 내 시도이다 공리로, x는 경우, 다음 X 타입 A. (? 그 분명 아닌)가
타입 A
컷 : 컨텍스트
Γ는t has type A증명하고 주장x has type A로 확장 다른 컨텍스트∆는,u has type B증명되면, 그 두 상황 함께x모든 항목의 치환을 증명t의u은B입니다. (대체로 두 개의 컨텍스트가있는 이유는 무엇입니까? 또 대체 컨텍스트는 대체 규칙과 비슷하지만 대체가 용어가 아니라 조작 인 경우 어떻게 작동합니까?) 고전적인 Milner 문맥은 다음x has type B여전히t has type A증명 문을 확장하는 컨텍스트를t has type A증명하는 경우.)은 응용 프로그램에 대한 그냥 아주 간단한 규칙이 약한, -Hindley 그런 아무 상관이 없습니다. (다시 말하지만, 그것은 명확하지 않다?)
제어 방식 : 컨텍스트는
x1 has type !A로 확장 및x2 has type !A은에x에 의해 모든x1의 발생과x2대체 없냐x has type !A로 확장하는 컨텍스트를,t has type B을 증명하는 경우t의 유형은B입니다. (교체의 또 다른 규칙은 보인다? 그런데 왜 두 용어는 위의 한 학기 아래? 또한, 왜 그!의? 모든 유형 검사에 표시 것이 어디 있습니까?)
I 그 규칙이 무엇을 말하고 싶은지 확실히 알 수 있습니다.하지만 실제로 클릭하기 전에 뭔가 빠졌고 해당 유형 검사기를 구현할 수 있습니다. 어떻게 이러한 규칙을 이해할 수 있습니까?
이 중 일부는 실제로 분명하며 "공리"가 필요한 이유를 알지 못합니다. 그러나 유형 시스템이나 논리를 설정하려면 많은 "명백한"사항을 포함시켜야합니다. – dfeuer
이 질문이 적합하지 않은 경우, 누군가가 날 (예를 들어 STLC 또는 간단한 것을 사용하여) 수식에서 유형 검사기를 작성하는 방법에 대한 실용적인 자습서로 나를 연결할 수 있다면 그것은 내 이해를 향상시킬 것입니다. 나는 한편으로 라이트 로직에 대한 가이드 (http://typesafety.net/thesis/chapter-2.pdf)를 읽고 있는데, 내가 게시 한 사람들과 수식을 비교하려고 노력하고있다. 나는 그것을 매우 유익하게 생각하고있다. – MaiaVictor
질문의 제목은 약간 오해의 소지가 있습니다.이 특별한 경우의 판단에 대해 질문하거나 일반적인 판단을 이해하고 있습니까? – Alec