가드 타입 이론
가드 타입 이론 (Guarded Type Theory)
참고: 이 페이지는 스텁(stub) 문서예요.
--guarded 옵션은 Agda에 Nakano의 later modality(나중 양상)와 가드 재귀(guarded recursion)를 추가해요. 이는 Ticked (Cubical) Type Theory [2]를 기반으로 하고 있어요.
--cubical과 함께 사용하는 방법은 [1]이나 예시를 참고하세요.
구현은 현재 위 참고 문헌보다 더 일반적인 것을 허용해요. 이는 [3]에 설명된 tick을 준비하기 위한 것이에요.
primLockUniv 유니버스에서 타입 A가 주어지면, @tick(또는 그 동의어 @lock)으로 주석된 함수 타입 (@tick x : A) -> B를 만들 수 있어요. 이러한 타입에서의 람다 추상화는 변수를 @tick 주석과 함께 문맥에 도입해요. t : (@tick x : A) → B에 대한 적용 t u는 u에 @tick 변수를 포함하지 않는 문맥의 전위부(prefix)에서 t가 타입을 가질 수 있을 때로 제한돼요. 현재 이 제한의 유일한 예외는 구간(interval) I 또는 IsOne _ 타입의 변수예요.
참고 문헌 (References)
[1] Niccolò Veltri and Andrea Vezzosi. "Formalizing pi-calculus in guarded cubical Agda." In CPP'20. ACM, New York, NY, USA, 2020.
[2] Rasmus Ejlers Møgelberg and Niccolò Veltri. "Bisimulation as path type for guarded recursive types." In POPL'19, 2019.
[3] Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi. "Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks."