Player FM 앱으로 오프라인으로 전환하세요!
Normal terms are typable with intersection types
Manage episode 286573147 series 2823367
I sketch the argument that pure lambda terms in normal form are typable using intersection types. This completes the argument started in the previous episode, that intersection types are complete for normalizing terms: normal forms are typable, and typing is preserved by beta-expansion. Hence any normalizing term is typable (since it reduces to a normal form by definition, and from this normal form we can walk typing back to the term).
160 에피소드
Manage episode 286573147 series 2823367
I sketch the argument that pure lambda terms in normal form are typable using intersection types. This completes the argument started in the previous episode, that intersection types are complete for normalizing terms: normal forms are typable, and typing is preserved by beta-expansion. Hence any normalizing term is typable (since it reduces to a normal form by definition, and from this normal form we can walk typing back to the term).
160 에피소드
모든 에피소드
×플레이어 FM에 오신것을 환영합니다!
플레이어 FM은 웹에서 고품질 팟캐스트를 검색하여 지금 바로 즐길 수 있도록 합니다. 최고의 팟캐스트 앱이며 Android, iPhone 및 웹에서도 작동합니다. 장치 간 구독 동기화를 위해 가입하세요.