संरचनात्मक प्रेरण की समाप्ति

Question

मैं संरचनात्मक प्रेरण का उपयोग करके परिभाषित कार्यों को स्वीकार करने के लिए आगाडा के समापन परीक्षक नहीं प्राप्त कर सकता।

मैंने इस समस्या को प्रदर्शित करने के सबसे सरल उदाहरण के रूप में निम्न को बनाया है। size की निम्न परिभाषा को अस्वीकार कर दिया गया है, भले ही यह हमेशा सख्ती से छोटे घटकों पर पुनरावृत्ति करता है।

module Tree where 

open import Data.Nat 
open import Data.List 

data Tree : Set where 
    leaf : Tree 
    branch : (ts : List Tree) → Tree 

size : Tree → ℕ 
size leaf = 1 
size (branch ts) = suc (sum (map size ts)) 

क्या इस समस्या का कोई सामान्य समाधान है? क्या मुझे अपने डेटा प्रकार के लिए Recursor बनाने की आवश्यकता है? यदि हां, तो मैं यह कैसे कर सकता हूं? मैन्युअल रूप से इनलाइन कर सकते हैं और नक्शे और योग की परिभाषा फ्यूज: (मुझे लगता है कि वहाँ एक List A के लिए एक Recursor कैसे परिभाषित करेंगे, इसका एक उदाहरण है, कि मुझे पर्याप्त संकेत देना होगा?)

Answer 1

वहाँ एक चाल आप यहाँ कर सकते है एक आपसी ब्लॉक के अंदर। यह बहुत ही विरोधी मॉड्यूलर है, लेकिन यह सबसे आसान तरीका है जिसे मैं जानता हूं। कुछ अन्य कुल भाषाएं (Coq) कभी-कभी इसे स्वचालित रूप से कर सकती हैं।

mutual 
    size : Tree → ℕ 
    size leaf = 1 
    size (branch ts) = suc (sizeBranch ts) 

    sizeBranch : List Tree → ℕ 
    sizeBranch [] = 0 
    sizeBranch (x :: xs) = size x + sizeBranch xs