코어 캐시 트리를 정의 할 때 "유효하지 않은 맵 기능"

Question

codatatype으로 첫 번째 실험을하고 있지만 다소 빠르다. 나는 분기의 정의, 가능성이 무한 트리 시작 :

codatatype (lset: 'a) ltree = Node (lnext : "'a ⇒ 'a ltree option") 

일부 정의는 잘 작동 :

primcorec lempty :: "'a ltree" 
    where "lnext lempty = (λ _ . None)" 

primcorec single :: "'a ⇒ 'a ltree" 
    where "lnext (single x) = (λ _ . None)(x := Some lempty)" 

하지만이 작동하지 않습니다

primcorec many :: "'a ⇒ 'a ltree" 
    where "lnext (many x) = (λ _ . None)(x := Some (many x))" 

내가 얻을로 오류 메시지

primcorec error: 
    Invalid map function in "[x ↦ many x]" 

나는 primcorec 방법 fun 요구 fundef_cong 보조 정리 및 inductive 요구 mono 보조 정리 유사한 기능을 업데이트 연산자 "에 대해 뭔가를 알고"할 필요가 있다고 생각 될 수

primcorec many :: "'a ⇒ 'a ltree" 
    where "lnext (many x) = (λ x'. if x' = x then Some (many x) else None)" 

를 작성하여 해결 할 수있다. 그러나 정확하게 무엇?

Answer 1

codatatype이 다른 유형 생성자를 통해 반복되는 경우 primcorec은 재귀 호출이 이러한 유형 생성자의 맵 함수에 올바르게 중첩 될 것으로 기대합니다. 이 예제에서 재귀는 함수 유형과 옵션 유형을 거치며이 함수의 맵 함수는 op o 및 map_option입니다. 따라서 many에 대한 재귀 호출은 op o (map_option many) 형식이어야합니다. 따라서, 다음과 같은 정의가 작동합니다

의 편의를 위해

primcorec many :: "'a ⇒ 'a ltree" 
where "lnext (many x) = map_option many ∘ [x ↦ x]" 

, primcorec가 몇 가지 더 구문 입력 형식을 지원합니다. 특히 함수 유형에 대한 맵 함수는 람다 추상화를 사용하여 작성할 수도 있습니다. 또한 대소 문자 구분과 if을 지원합니다. 이것이 귀하의 두 번째 버전이 채택 된 이유입니다. 그러나 생성 된 정의 many_def을 보면 명시적인 맵 기능보다 더 복잡하다는 것을 알 수 있습니다.

primcorec 임의 함수의 등록을 지원하지 않으므로 fun_upd을 원래 형식으로 사용할 수 없습니다. 원시 코어 커션은 구문 론적입니다. 어쩌면 미래에는 function의 핵심 역량이있을 것입니다.

지도 기능은 tutorial on datatypes 및 this paper에 설명되어 있습니다.