استخلاص التعريف العودي من مواصفات الوظيفة

Question

نظرًا لمواصفات الوظيفة هذه، حيث الاسم xs يرتبط بالقائمة، # يدل على أصلها و . هل list index المشغل أو العامل...

$$\left( \sum i:0 \leq i < \#xs:xs.i * (i + 1) ight)$$

أحتاج إلى استخلاص دالة عودية باستخدام الحث.

الحالة الأساسية: []

\begin{align} \left( \sum i:0 \leq i < \#[]:xs.i * (i 1) \ يمين) && ext {(استبدال نصي - xs مجاني)} \\ \left( \sum i:0 \leq ط < 0:xs.i * (i + 1) ight) && ext{(Def.من #)} \\ \left( \sum i:خطأ شنيع:xs.i * (i 1) ight) && ext{(الجبر)} \\ \left( \sum i:0 \leq i < \#xs:xs.i * (i 1) \ يمين) && \ نص {(نطاق فارغ)} \ النهاية {محاذاة}

الحالة الاستقرائية: (x:xs)

تبدأ {align} left ( sum i:0 \leq i < \#(x:xs):(x: xs) .i * (i + 1) right) && text {(rectual stitution - xs مجاني)} left ( sum i:0 \leq i < 1 + \#xs:(x:xs).i * (i + 1) ight) && ext{(Def.من #)} end {align}

كيف يمكنني المتابعة من هنا؟

Answer 1

تدوينك وفهمك جيد جدًا.

فمن الأسهل أن تأخذ في الاعتبار (xs:x) كحالة استقرائية بدلا من (x:xs)

\begin{align} \sum_{i:\ 0 \leq i < \#(xs:x)} &(xs:x).i * (i 1)\\ &=\sum _{i:\ 0 \leq i < \#xs 1} (x:xs).i * (i 1) \\ &=\sum_{i:\ 0 \leq i < \#xs} (xs:x).i * (i 1) \sum_{i:\ i=\#xs}(xs:x).i * (i 1)\\ &=\sum_{i:\ 0 \leq i < \#xs} xs.i * (i 1) x*(\#xs 1),\\ \ النهاية {محاذاة}حيث نفترض أن فهرس القائمة يبدأ بـ 0.

إذا قمنا بالإشارة إلى الوظيفة بواسطة $و$, ، تصبح المساواة المذكورة أعلاه$$ f(xs:x) = f(xs) + x*(\#xs+1), $$وهي الخطوة العودية للتعريف العودي.

الحالة الأساسية كما أشرت هي$$ f([]) = \sum_{ i:\ 0 \leq i < 0} [].i * (i + 1) = \sum_{i: ext{ مجموعة فارغة}}[].i * (i + 1) =0.$$

---

يمارس.اشتق الصيغة العودية التالية لنفس الوظيفة $و$. $$ f(x:xs) = f(xs) + t(xs)+ x, $$أين $$t(xs)=\sum_{i:\ 0 \leq i < \#(xs)} xs.i,$$مجموع العناصر في $xs$.