공대 학부생이 함수형 언어 해보고 싶어서 type theory에 관한 입문하려고 뭔가 찾아서 보고 있는데
혹시 이거 엄청 좋다!! 하는 책이나 무언가 있나요??
기왕이면 formal했으면 좋겠어요... 지난번에 누가 프린스턴 고등연구소에서 나온 informal한 책 추천했었는데 영어를 못해서 이해를 못하겠더라구요...
글고 isomorphism은 그냥 일대일대응이라고 이해해도 되나요??
단어만 보면 엄청 어려워보이는데 검색보면 별것 아닌거같기도 하고 확실치 않아서요
https://www.amazon.com/Implementing-Mathematics-Nuprl-Development-System/dp/1468059106?language=en_US¤cy=USD
software foundation 좋은 책임. type theory라기 보다는 coq 가르치는게 목적인 책이라 그렇게 이론적인거 다루는 책은 아니지만
isomorphism은 맥락따라 다른데 그냥 일대일 대응일 수도 있고 구조까지 보존하는 사상일 수도 있음
그리고 curry howard isomorphism에서는 좀 informal하게 쓴거임. curry howard correspondence라고도 씀
오홍홍 조아용 고마워용
isomorphism이 왜 그냥 일대일 대응일 수 있나요? 보통 일대일 대응은 bijection이라고 부르고, 구조를 보존하는 사상은 homomorphism인데 ... 정확히 말하자면, 대수적 구조 사이에서 구조를 보존하는 전단사 사상은 isomorphism이라고 할 수 있고, 대수적 구조가 아닌 구조(즉, 관계를 포함하는 구조)에서는 bijective homomorphism은 isomorphism이 아닐 수 있어요.
Set 카테고리에서 isomorphism이 bijection이란 의미였음