[연재] 나에게 치환은 모나드다

[다믜(damhiya)]

https://github.com/damhiya/AgdaLambdaCalculus/blob/main/src/Syntax.agda

AgdaLambdaCalculus/Syntax.agda at main · damhiya/AgdaLambdaCalculus

simply typed lambda calculus 치환 구현 및 성질 증명

https://github.com/UniMath/UniMath/tree/master/UniMath/SubstitutionSystems

치환에다가 모나드 구조 주는건 여기서 했더라. 근데 논문으로 출판된건 untyped 버전 밖에 없는듯. multi-sorted (typed AST)는 코드로 구현된건 있는데 출판은 안된것 같고 아직 연구중인듯.

associativity 증명이 좀 어려웠는데 이런거 그려서 겨우 함. 코드에서 diagram이라고 정의해놓은게 이 그림.

[해당 댓글은 삭제되었습니다.]

해당 댓글은 삭제되었습니다.

[다믜(damhiya)]

이거요

[토끼주문(icyselec)]

자기 자신을 만들어요

[익명(220.81)]

치환을 근데 왜 모나드로함? 순수함수일텐데

[기괴공학도(thecoqproofassistant)]

그런 모나드가 아님.

[다믜(damhiya)]

람다대수에서 치환이라는 개념 자체가 모나드로 설명이 된다는 뜻임

[익명(211.186)]

이런거 하다보면 위상수학도 공부해야하나

[다믜(damhiya)]

denotational semantics의 방법론중 하나인 domain theory가 위상과 관련이 있음