मॉर्ट/कोक के समान भाषा का उपयोग करके, मैं सरल कथन there are lists of arbitrary lengths साबित करने का प्रयास कर रहा हूं।सबूतों पर ईटा-रूपांतरण मुद्दों से बचने के लिए एक बेकार 'आईडी' कॉल में चर को लपेटना सामान्य है?
∀ n:Nat ->
(ThereIs (List Nat)
(Equal Nat
(List.length Nat l)
n)))
ThereIs निर्भर जोड़ी (सिग्मा) है: कि के लिए, मैं निम्नलिखित प्रकार लिखा था। सब चर्च-एनकोडेड है। यह साबित करने के लिए, मैं निम्नलिखित सबूत लिखा है:
λ n:Nat ->
(ThereIs.this (List Nat)
(λ l:(List Nat) -> (Equal Nat (List.length Nat l) n))
(List.replicate Nat n Nat.Zero)
(Equal.refl Nat n))
अजीब तरह से, मैं d के बीच एक प्रकार मेल नहीं खाता त्रुटि मिलती है (अर्थात, प्रकार नेट से मुक्त चर) और λ c:* -> λ b:(c -> c) -> λ a:c -> (d c b a)। लेकिन बाद में यह शब्द, जब ईटा-कम हो गया, केवल d है!
λ n: Nat ->
λ Nat:* ->
λ Succ: (Nat -> Nat) ->
λ Zero: Nat ->
(n Nat Succ Zero)
अब, n, मैं "गैर-ईटा" के हर घटना है कि बेकार आईडी लगाने से यह: जब से मैं एक ईटा-कम करने के लिए तैयार नहीं है, मैं बजाय इस निम्नलिखित "बेकार की पहचान" समारोह बना दिया , सबूत जांचने के कारण। मैं यहां क्या हो रहा है की किसी भी प्रकार की अंतर्दृष्टि प्राप्त करना चाहता हूं। क्या यह "बेकार आईडी" लेखन प्रमाणों पर एक ज्ञात/प्रयुक्त पैटर्न है? इस छोटी सी सहायता के बिना इस सबूत को टाइप करने में सक्षम निर्देशों का गणक क्यों नहीं है? क्या इस घटना के पीछे कोई गहरी तर्क है या यह सिर्फ एक विशेष कारण के लिए चीजें कैसे हैं?
आपका मतलब अल्फा नहीं है, है ना? –
हां क्षमा करें @ रीडबर्टन – MaiaVictor
मुझे लगता है कि विशेष रूप से टाइप की गई सभी आईडी की आईडी '- केवल ईटा बराबर नहीं - सबूत सिस्टम में बहुत आम हैं। कोक में आधे रणनीतिएं 'आईडी' में अनुवाद करना एक विशेष रूप से रोमांचक तरीके से लिखी गई हैं। –