ترميز الكنيسة

في الرياضيات ، يعد ترميز تشيرش طريقة لتمثيل أنواع مختلفة من البيانات في حساب التفاضل والتكامل لامدا .

في حساب التفاضل والتكامل اللامدا غير المُصنَّف، تُعدّ الدوال النوع الوحيد من البيانات الأولية، ويتم تمثيلها بمصطلحات تجريدية لامدا. أما الأنواع التي تُعتبر عادةً أولية في تدوينات أخرى (مثل الأعداد الصحيحة ، والقيم المنطقية ، والأزواج، والقوائم، والاتحادات المُوسومة ) فهي غير موجودة بشكل أصلي.

ومن ثم تنشأ الحاجة إلى وجود طرق لتمثيل البيانات من هذه الأنواع المختلفة بواسطة مصطلحات لامدا، أي بواسطة وظائف تأخذ وظائف كوسائط لها وتعيد وظائف كنتائج لها.

تُعدّ أرقام تشيرش تمثيلاً للأعداد الطبيعية باستخدام ترميز لامدا. سُمّيت هذه الطريقة نسبةً إلى ألونسو تشيرش ، الذي كان أول من استخدم هذه الطريقة في ترميز البيانات في حساب لامدا. ويمكن توسيع نطاقها لتمثيل أنواع بيانات أخرى بنفس المبدأ.

تستخدم هذه المقالة أحيانًا الصيغة البديلة لمصطلحات تجريد لامدا، حيث يتم اختصار λ x .λ y .λ z . N إلى λ xyz . N ، بالإضافة إلى المُركِّبين القياسيين. $I\equiv \lambda xx$ و $K\equiv \lambda xy.x$ حسب الحاجة.

أزواج الكنائس

أزواج تشيرش هي ترميز تشيرش لنوع الزوج ( الزوج الثنائي ). وجود عنصرين يعني القدرة على توفيرهما لأي مراقب يتوقع عنصرين. وبالتالي، يُمثَّل الزوج كدالة تأخذ وسيطًا داليًا. لا يُقرر الزوج نفسه ما يجب فعله بعناصر الزوج الثنائي. عند إعطائه وسيطه، فإنه يُطبِّق هذا الوسيط على عنصري الزوج. تعريف مُنشئ الزوج ، ودالة اختيار العنصر الأول ، ودالة اختيار العنصر الثاني في حساب لامدا هي:

{\begin{aligned}\operatorname {pair} &\equiv \lambda xy.\lambda zz\ x\ y\\\operatorname {first} &\equiv \lambda pp\ (\lambda xy.x)\\\operatorname {second} &\equiv \lambda pp\ (\lambda xy.y)\end{aligned}}

على سبيل المثال،

{\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&\ (\lambda pp\ (\lambda xy.x))\ ((\lambda xyz.z\ x\ y)\ a\ b)\\=&\ (\lambda pp\ (\lambda xy.x))\ (\lambda zz\ a\ b)\\=&\ (\lambda zz\ a\ b)\ (\lambda xy.x)\\=&\ (\lambda xy.x)\ a\ b\\=&\ a\end{aligned}}

معاملات الكنيسة المنطقية

تُشفّر القيم المنطقية ( صواب وخطأ ) في لغة تشيرش . وتستخدم بعض لغات البرمجة هذه القيم كنموذج لتنفيذ العمليات الحسابية المنطقية، ومن أمثلتها Smalltalk و Pico.

يُجسّد المنطق البولياني خيارًا بين بديلين . وبالتالي ، فإن ترميزات الكنيسة للصواب والخطأ هي دوال لمتغيرين:

القيمة true تختار المعامل الأول ؛
يختار الخيار false المعامل الثاني.

التعريفان في حساب التفاضل والتكامل اللامدا هما:

{\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda ba\ \ \ \ \ =\lambda a.\lambda b.\operatorname {first} \,(\operatorname {pair} a\ b)\\\operatorname {false} &\equiv \lambda a.\lambda bb\ \ \ \ \ \,=\lambda a.\lambda b.\operatorname {second} \,(\operatorname {pair} a\ b)\end{aligned}}

تسمح هذه التعريفات للمسندات (أي الدوال التي تُرجع قيمًا منطقية ) بالعمل مباشرةً كعبارات اختبار if ، بحيث يكون عامل if مجرد دالة تطابق، وبالتالي يمكن حذفه. تعمل كل قيمة منطقية بالفعل كشرط if ، حيث تُجري اختيارًا بين وسيطيها. تُرجع القيمة المنطقية المطبقة على قيمتين إما القيمة الأولى أو الثانية.

\operatorname {عبارة الاختبار} \ \operatorname {عبارة الإثبات} \ \operatorname {عبارة الإلغاء}

تُرجع عبارة then إذا كانت عبارة الاختبار صحيحة ، وعبارة else إذا كانت عبارة الاختبار خاطئة .

بما أن القيم المنطقية مثل "صحيح" و "خطأ" تحدد وسيطها الأول أو الثاني، فإنه يمكن دمجها لتوفير عوامل منطقية. عادةً ما تكون هناك عدة طرق للتنفيذ، سواءً عن طريق معالجة المعاملات مباشرةً أو عن طريق اختزالها إلى القيم المنطقية الأساسية. فيما يلي التعريفات، باستخدام الترميز المختصر كما ذُكر في بداية المقال (حيث p و q هما المسندات؛ وa و b هما القيم العامة):

{\begin{aligned}\operatorname {if} &=\lambda pab.p\ a\ b&&\ \\\operatorname {and} &=\lambda pq.p\ q\ p&&=\lambda pqab.p\ (q\ a\ b)\ b\\\operatorname {or} &=\lambda pq.p\ p\ q&&=\lambda pqab.p\ a\ (q\ a\ b)\\\operatorname {not} &=\lambda p.p\operatorname {false} \operatorname {true} &&=\lambda pab\ \ .p\ b\ a\\\operatorname {xor} &=\lambda pq.p\ (\operatorname {not} \ q)\ q&&=\lambda pqab.p\ (q\ b\ a)\ (q\ a\ b)\\\operatorname {nand} &=\lambda pq.\operatorname {not} \ (\operatorname {and} p\ q)&&=\lambda pqab.p\ (q\ b\ a)\ a\\\operatorname {implies} &=\lambda pq.\operatorname {or} \ (\operatorname {not} p)\ q&&=\lambda pqab.p\ (q\ a\ b)\ a\\\end{aligned}}

بعض الأمثلة:

{\begin{aligned}\operatorname {and} \ &\operatorname {true} \ \operatorname {false} \\&=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} \\&=\operatorname {true} \operatorname {false} \operatorname {true} \\&=(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} \\&=\operatorname {false} \end{aligned}}

{\begin{aligned}\operatorname {not} \ &\operatorname {true} \\&=(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (\lambda a.\lambda b.a)\\&=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a\\&=\lambda a.\lambda b.(\lambda c.b)\ a\\&=\lambda a.\lambda b.b\\&=\operatorname {false} \\\end{aligned}}

القيم الاختيارية

يتم تمثيل القيمة الاختيارية على النحو التالي:

{\begin{aligned}\operatorname {none} \ \equiv \ \ \ \ \ &\lambda f.\lambda s.\ f\\\operatorname {val} \ \equiv \ \lambda v.\ &\lambda f.\lambda s.\ s\ v\end{aligned}}

استخدام مثل هذه القيمة يعني تزويدها بوسيطين - واحد، $f$ أما في حالة "الفشل"، أي انعدام القيمة، والحالة الأخرى، $s$ ، في حالة "النجاح"، هي دالة معالجة يتم تقديمها بتلك القيمة.

تعرف القيمة الاختيارية نفسها الحالة التي تنتمي إليها، وتختار الوسيط المناسب وفقًا لذلك. وهي "تعرف" ذلك بحكم إنشائها على هذا النحو - إما أنها أُنشئت كـ $\operatorname {none}$ أو كما $\operatorname {val} \,v$ .

لا يملك مستخدم القيمة الاختيارية أي طريقة لمعرفة أي حالة هي إلا من خلال تزويدها بالوسيطين، واحد لكل من الحالتين المحتملتين.

الأرقام الكنسية

الأرقام الكنسية هي تمثيلات للأعداد الطبيعية وفقًا لترميز الكنيسة. الدالة ذات الرتبة العليا التي تمثل العدد الطبيعي n هي دالة تُسقط أي دالة أخرى. $f$ إلى تركيبها ذي n ضعف . بعبارة أبسط، يمثل الرقم العدد بتطبيق أي دالة معينة هذا العدد من المرات بالتتابع، بدءًا من أي قيمة ابتدائية معينة:

n:f\mapsto f^{\circ n}

f^{\circ n}(x)=(\underbrace {f\circ f\circ \ldots \circ f} _{n{\text{ times}}})\,(x)=\underbrace {f(f(\ldots (f} _{n{\text{ times}}}\,(x))\ldots ))

وبالتالي فإن ترميز الكنيسة هو ترميز أحادي للأعداد الطبيعية، ^{[ 1 ]} يتوافق مع العد البسيط . كل عدد من أعداد الكنيسة يحقق ذلك من خلال بنائه.

جميع أرقام الكنيسة هي دوال تأخذ وسيطين. تُعرَّف أرقام الكنيسة 0 ، 1 ، 2 ، ...، كما يلي في حساب التفاضل والتكامل اللامدا :

بدءاً من 0، أي عدم تطبيق الدالة على الإطلاق، ثم الانتقال إلى 1، أي تطبيق الدالة مرة واحدة، ثم 2، أي تطبيق الدالة مرتين متتاليتين، ثم 3، أي تطبيق الدالة ثلاث مرات متتالية، وهكذا :

{\begin{array}{r|l|l}{\text{Number}}&{\text{Function definition}}&{\text{Lambda expression}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\\1&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\\2&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\\3&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{\circ n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}

الرقم الكنسي 3 هو سلسلة من ثلاث عمليات تطبيق متسلسلة لأي دالة معينة، بدءًا من قيمة معينة. تُطبق الدالة المُعطاة أولًا على وسيط مُعطى، ثم تُطبق تباعًا على نتيجتها. النتيجة النهائية ليست الرقم 3 (إلا إذا كان الوسيط المُعطى يساوي صفرًا وكانت الدالة دالة لاحقة ). الدالة نفسها، وليس نتيجتها النهائية، هي الرقم الكنسي 3. الرقم الكنسي 3 يعني ببساطة تكرار شيء ما ثلاث مرات. إنه توضيحٌ جليٌّ لما يُقصد بـ "ثلاث مرات".

الحساب باستخدام الأرقام الكنسية

تُنتج العمليات الحسابية على الأعداد أعدادًا كنتائج. في ترميز تشيرش، تُمثَّل هذه العمليات برموز لامدا المجردة ، والتي عند تطبيقها على أرقام تشيرش التي تُمثل المعاملات، تُختزل إلى أرقام تشيرش التي تُمثل النتائج.

تمثيل الكنيسة للإضافة، $\operatorname {plus} (m,n)=m+n$ ، يستخدم الهوية $f^{\circ (m+n)}(x)=(f^{\circ m}\circ f^{\circ n})(x)=f^{\circ m}(f^{\circ n}(x))$ :

\operatorname {plus} \equiv \lambda mn.\lambda fx.m\ f\ (n\ f\ x)

العملية اللاحقة، $\operatorname {succ} (n)=n+1$ ، ويتم الحصول عليها عن طريق اختزال التعبير " $\operatorname {plus} \ 1$ ":

\operatorname {succ} \equiv \lambda n.\lambda fx.f\ (n\ f\ x)

الضرب، $\operatorname {mult} (m,n)=m*n$ ، يستخدم الهوية $f^{\circ (m*n)}(x)=(f^{\circ n})^{\circ m}(x)$ :

\operatorname {mult} \equiv \lambda mn.\lambda fx.m\ (n\ f)\ x

هكذا $b\ (b\ f)\equiv (\operatorname {mult} b\ b)\ f$ و $b\ (b\ (b\ f))\equiv (\operatorname {mult} b\ (\operatorname {mult} b\ b))\ f$ وبالتالي، وبفضل ترميز تشيرش الذي يعبر عن التركيب ذي الرتبة n ، فإن عملية الأس $\operatorname {exp} (b,n)=b^{n}$ يُعطى بواسطة

\operatorname {exp} \equiv \lambda bn.n\ b\equiv \lambda bnfx.n\ b\ f\ x

العملية السابقة $\operatorname {pred} (n)$ الأمر أكثر تعقيدًا بعض الشيء. نحتاج إلى ابتكار عملية يمكن تكرارها $n+1$ ستؤدي الأوقات إلى $n$ تطبيقات الدالة المعطاة $f$ ويتحقق ذلك باستخدام دالة التطابق مرة واحدة فقط، ثم العودة إلى $f$ :

\operatorname {pred} \equiv \lambda nfx.n\ (\lambda ri.i\ (r\ f))\ (\lambda f.x)\ I

كما ذكرنا سابقاً، $I$ هي دالة الهوية، $\lambda x.x$ اسم المتغير $r$ تم اختيار هذا المصطلح كرمز تذكيري لـ "النتيجة التكرارية". يستخدم هذا التعريف حجة إضافية لتطبيق نموذج تمرير الحالة، نظرًا لأن حساب لامدا يفتقر إلى التغيير (لذا لا يمكن تغيير أي شيء، بل استبداله فقط). انظر أدناه للشرح المفصل.

يشير هذا إلى إمكانية تطبيق وظائف التنصيف والعاملي، على سبيل المثال، بطريقة مماثلة في تمرير الحالة.

{\begin{aligned}\operatorname {half} &\equiv \lambda nfx.n\ (\lambda rab.a\ (r\ b\ a))\ (\lambda ab.x)\ I\ f\\\operatorname {fact} &\equiv \lambda nf.n\ (\lambda ra.a\ (r\ (\operatorname {succ} a)))\ (\lambda a.f)\ 1\end{aligned}}

على سبيل المثال، $\operatorname {pred} 4\ f\ x\,$ يختزل بيتا إلى $I(f\ (f\ (f\ x)))$ ، $\operatorname {half} \ 5\ f\ x\,$ يختزل بيتا إلى $I\ (f\ (I\ (f\ (I\ x))))$ ، و $\operatorname {fact} 4\,f\,$ يختزل بيتا إلى $1\ (2\ (3\ (4\ f)))$ .

الطرح، $minus(m,n)=m-n$ يتم التعبير عن ذلك من خلال التطبيق المتكرر للعملية السابقة لعدد معين من المرات، تمامًا كما يمكن التعبير عن الجمع من خلال التطبيق المتكرر للعملية اللاحقة لعدد معين من المرات، إلخ:

{\begin{aligned}(-)&\equiv \lambda mn.n\,\operatorname {pred} \,m\\(+)&\equiv \lambda mn.n\,\operatorname {succ} \,m\\(\times )&\equiv \lambda mn.n\ ((+)\ m)\ 0\\\operatorname {exp} &\equiv \lambda mn.n\ ((\times )\ m)\ 1\ \ \ \ \ \ \ \ \ \ \ \{-\ \ m^{n}\ -\}\\(\uparrow \uparrow )&\equiv \lambda mn.n\ (\operatorname {exp} \,m)\ 1\ \ \ \ \ \ \ \{-\ m\uparrow \uparrow n\ -\}\\\uparrow ^{k}&\equiv k\ (\lambda fmn.n\ (f\ m)\ 1)\ (\times )\\\end{aligned}}

$(\uparrow \uparrow )$ هي عملية المعايرة ، $m\uparrow \uparrow 3=m^{(m^{(m^{1})})}$ ، و $\uparrow ^{k}$ هو كنوت $k$ السهم ^{[ 2 ]} بشكل عام.

على غرار تعريف المضروب أعلاه، يمكن أيضًا تعريف التكرار باستخدام الخصائص الجوهرية لترميز الكنيسة، وإنشاء تعبير "الرمز" الخاص به، وترك أرقام الكنيسة نفسها تقوم بالباقي:

{\begin{aligned}\operatorname {tet} &\equiv \lambda mn.n\ (\lambda r.r\ m)\ 1\end{aligned}}

وهنا، مرة أخرى، $\operatorname {tet} \,m\ 3=1\ m\ m\ m=m^{(m^{(m^{1})})}$ .

الطرح والقسمة المباشران

وكما أن الجمع كلاحق متكرر له نظيره في الأسلوب المباشر، كذلك يمكن التعبير عن الطرح بشكل مباشر وأكثر كفاءة:

{\begin{aligned}\operatorname {minus} \equiv \lambda &mnfx.\\&m\ (\lambda rq.q\ r)\ (\lambda q.x)\\&(n\ (\lambda qr.r\ q)\ (\operatorname {Y} \ (\lambda qr.f\ (r\ q))))\end{aligned}}

على سبيل المثال، $\operatorname {minus} \ 6\ 3\ f\ x$ يتقلص إلى ما يعادل $f\ (2\ f\ x)$ .

وهذا يوفر أيضًا إصدارًا سابقًا آخر، مما يقلل من حجم الإصدار التجريبي (بيتا). $\lambda m.\operatorname {minus} \ m\ 1$ :

{\begin{aligned}\operatorname {pred'} \equiv \lambda mfx.m\ &(\lambda rq.q\ r)\ (\lambda q.x)\\&(\lambda r.r\ (\operatorname {Y} \ (\lambda qr.f\ (r\ q))))\end{aligned}}

يُقدّم تعريف مباشر للقسمة بشكل مشابه تمامًا لـ

{\begin{aligned}\operatorname {div} \equiv \lambda &mnfx.\\&m\ (\lambda rq.q\ r)\ (\lambda q.x)\\&(\operatorname {Y} \ (\lambda q.n\ (\lambda qr.r\ q)\ (\lambda r.f\ (r\ q))\ (\lambda x.x)))\end{aligned}}

طلب إلى $(\lambda x.x)$ يتم تحقيق الطرح عن طريق $1$ مع إنشاء دورة من الإجراءات التي تصدر بشكل متكرر $f$ بعد $n-1$ خطوات.

بدلاً من $\operatorname {Y}$ ، $(\lambda q.m\,q\,x)$ ويمكن استخدامها أيضًا في كل من التعريفات الثلاثة المذكورة أعلاه.

جدول وظائف الأرقام الكنسية

وظيفة	الجبر	هوية	تعريف الدالة	تعبيرات لامدا
خليفة	$n+1$	$f^{\circ (n+1)}=f\circ f^{\circ n}$	$\operatorname {succ} \ n\ f\ x=f\ (n\ f\ x)$	$\lambda nfx.f\ (n\ f\ x)$	...
إضافة	$m+n$	$f^{\circ (m+n)}=f^{\circ m}\circ f^{\circ n}$	$\operatorname {plus} \ m\ n\ f\ x=m\ f\ (n\ f\ x)$	$\lambda mnfx.m\ f\ (n\ f\ x)$	$\lambda mn.n\operatorname {succ} m$
الضرب	$m*n$	$f^{\circ (m*n)}=(f^{\circ m})^{\circ n}$	$\operatorname {multiply} \ m\ n\ f\ x=m\ (n\ f)\ x$	$\lambda mnfx.m\ (n\ f)\ x$	$\lambda mnf.m\ (n\ f)$
الأس	$b^{n}$	$b^{\circ n}=(\operatorname {mult} b)^{\circ n}$	$\operatorname {exp} \ b\ n\ f\ x=n\ b\ f\ x$	$\lambda bnfx.n\ b\ f\ x$	$\lambda bn.n\ b$
السلف ^{[ أ ]}	$n-1$	$first((\langle i,j\rangle \mapsto \langle j,f\circ j\rangle )^{\circ n}\langle I,I\rangle )=f^{\circ (n-1)}$	$\operatorname {pred} (n+1)\ f\ x=I\ (n\ f\ x)$	$\lambda nfx.n\ (\lambda ri.i\ (r\ f))\ (\lambda f.x)\ (\lambda u.u)$
الطرح ^{[ أ ]} ( مونوس )	$m-n$	$m-n=pred^{\circ n}(m)$	$\operatorname {minus} \ m\ n=n\operatorname {pred} m$	...	$\lambda mn.n\operatorname {pred} m$

ملحوظات :

1 2
في ترميز الكنيسة،
- $\operatorname {pred} (0)=0$
- $m\leq n\to m-n=0$

وظيفة السلف

تُعطى دالة السلف على النحو التالي:

\operatorname {pred} \equiv \lambda nfx.n\ (\lambda ri.i\ (r\ f))\ (\lambda f.x)\ (\lambda u.u)

يستخدم هذا الترميز بشكل أساسي الهوية

first(\ (\langle i,j\rangle \mapsto \langle j,f\circ j\rangle )^{\circ n}\langle I,I\rangle \ )={\begin{cases}I&{\mbox{if }}n=0,\\f^{\circ (n-1)}&{\mbox{otherwise}}\end{cases}}

أو

first(\ (\langle x,y\rangle \mapsto \langle y,f(y)\rangle )^{\circ n}\langle x,x\rangle \ )={\begin{cases}x&{\mbox{if }}n=0,\\f^{\circ (n-1)}(x)&{\mbox{otherwise}}\end{cases}}

شرح لكلمة "مفترس"

الفكرة هنا هي كالتالي. الشيء الوحيد المعروف للكنيسة هو الرقم $\operatorname {pred} n$ هو الرقم $n$ نفسه. بالنظر إلى حجتين $f$ و $x$ وكالعادة، الشيء الوحيد الذي يمكنه فعله هو تطبيق هذا الرقم على الوسيطين، مع تعديله بطريقة ما بحيث يكون لسلسلة التطبيقات التي تم إنشاؤها بطول n وسيط واحد (على وجه التحديد، الوسيط الأيسر). $f$ في السلسلة يتم استبدالها بدالة التطابق:

{\begin{aligned}f^{\circ (n-1)}(x)&=\underbrace {I\ (\underbrace {f(f(\ldots (f} _{{n-1}{\text{ times}}}} _{n{\text{ times}}}\,(x))\ldots )))=(Xf)^{\circ n}(Z\,x)\ A\\&=\underbrace {Xf\ (Xf\ (\ldots (Xf} _{{n}{\text{ times}}}\,(Z\,x))\ldots ))\ A\\&=X\ f\ r_{1}\ A_{1}\,\,\,\{-\ and\ it\ must\ be\ equal\ to:\ -\}\\&=I\ (X\ f\ r_{2}\ A_{2})\\&=I\ (f\ (X\ f\ r_{3}\ A_{3}))\\&=I\ (f\ (f\ (X\ f\ r_{4}\ A_{4})))\\&\ldots \\&=I\ (f\ (f\ \ldots (X\ f\ r_{n}\ A_{n})\ldots ))\\&=\underbrace {I\ (f\ (f\ \ldots (f} _{n{\text{ times}}}\ (Z\ x\ A_{n+1}))\ldots ))\\\end{aligned}}

هنا $Xf$ هو المعدل $f$ ، و $Z\,x$ هو المعدل $x$ . منذ $Xf$ لا يمكن تغييرها في حد ذاتها، بل يمكن تعديل سلوكها فقط من خلال وسيطة إضافية. $A$ .

إذن، يتحقق الهدف من خلال تمرير تلك الحجة الإضافية $A$ على طول من الخارج إلى الداخل ، مع تعديله حسب الضرورة، مع التعريفات

{\begin{aligned}A_{1}\,\,\,\,\,\,\,\,\,\,&=\,I\\A_{\,i>1}\,\,\,\,\,&=\,f\\Z\ x\ f\,\,\,\,&=x=K\ x\ f\\X\ f\ r\ A_{i}&=A_{i}\ (r\ A_{i+1})\,\,\,\,\,\,\{-\ i.e.,\ -\}\\X\ f\ r\ i\,\,\,\,\,&=i\ (r\ f)\end{aligned}}

وهذا بالضبط ما لدينا في $\operatorname {pred}$ تعبير لامدا الخاص بالتعريف.

الآن بات من السهل بما فيه الكفاية أن نرى ذلك

{\begin{aligned}\operatorname {pred} \ (\operatorname {succ} \ n)\ f\ x&=\operatorname {succ} \ n\ (Xf)\ (K\ x)\ I\\&=X\ f\ (n\ (X\ f)\ (K\ x))\ I\\&=I\ (n\ (Xf)\ (K\ x)\ \,\,f\,\,\,)\\&=\ \ldots \\&=I\ (f\ (f\ \ldots (f\ (K\ x\,\,f\,\,))\ldots ))\\&=I\ (n\ f\ x)\\&=n\ f\ x\ \end{aligned}}

{\begin{aligned}\operatorname {pred} \ 0\ f\ x&=\ 0\ (Xf)\ (K\ x)\ I\\&=\ K\ x\ I\\&=\ x\\&=\ 0\ f\ x\end{aligned}}

أي عن طريق انكماش إيتا ثم بالاستقراء، فإنه ينص على أن

{\begin{aligned}&\operatorname {pred} \ (\operatorname {succ} \ n)&&=\ n\\&\operatorname {pred} \ 0&&=\ 0\\&\operatorname {pred} \ (\operatorname {pred} \ 0)&&=\ \operatorname {pred} \ 0\ =\ 0\\&\ldots \end{aligned}}

وهكذا دواليك.

تحديد المفترس من خلال الأزواج

يمكن ترميز المتطابقة المذكورة أعلاه باستخدام الأزواج بشكل صريح. ويمكن القيام بذلك بعدة طرق، على سبيل المثال،

{\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {pred} _{2}=&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ (\operatorname {pair} \ 0\ 0))\\\end{aligned}}

التوسع لـ $\operatorname {pred} _{2}3$ يكون:

{\begin{aligned}\operatorname {pred} _{2}3=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ 0\ 0))))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ 0\ 1)))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {pair} \ 1\ 2))\\=&\ \operatorname {first} \ (\operatorname {pair} \ 2\ 3)\\=&\ 2\end{aligned}}

هذا تعريف أبسط في صياغته ولكنه يؤدي إلى تعبير لامدا أكثر تعقيدًا،

{\begin{aligned}\operatorname {pred} _{2}\equiv \lambda n.n\ &(\lambda p.p\ (\lambda abh.h\ b\ (\operatorname {succ} \ b)))\,\,(\lambda h.h\ 0\ 0)\,\,(\lambda ab.a)\end{aligned}}

تُعتبر الأزواج في حساب لامدا في الأساس مجرد وسائط إضافية، سواء تم تمريرها من الداخل إلى الخارج كما هو الحال هنا، أو من الخارج إلى الداخل كما في الأصل. $\operatorname {pred}$ التعريف. يتبع ترميز آخر الصيغة الثانية من هوية السلف مباشرةً،

{\begin{aligned}\operatorname {pred} _{3}\equiv \lambda nfx.n\ &(\lambda p.p\ (\lambda abh.h\ b\ (f\ b)))\,\,(\lambda h.h\ x\ x)\,\,(\lambda ab.a)\end{aligned}}

وبهذه الطريقة، يكون قريباً جداً من الأصل، "من الخارج إلى الداخل". $\operatorname {pred}$ التعريف، كما أنه يخلق سلسلة من $f$ كما هو الحال، ولكن بطريقة أكثر إسرافًا بعض الشيء. إلا أنها أقل إسرافًا بكثير من سابقتها. $\operatorname {pred} _{2}$ التعريف هنا. في الواقع، إذا تتبعنا تنفيذه، فسنصل إلى التعريف الجديد، الأكثر تبسيطًا، ولكنه مكافئ تمامًا.

{\begin{aligned}\operatorname {pred} _{4}\equiv \lambda nfx.n\ &(\lambda rab.r\ b\ (f\ b))\,K\ x\ x\end{aligned}}

مما يجعل الأمر واضحًا وجليًا تمامًا، وهو أن كل هذا يتعلق بتعديل الوسائط وتمريرها. ويستمر اختزالها على النحو التالي:

{\begin{aligned}\operatorname {pred} _{4}3\ f\ x&=\ (..(..(..K)))\ x\ \,x\\&=\ (..(..K))\,\,\,\,\,\,\,x\ \,\,(f\ x)\\&=\ (..K)\,\,\,\,\,\,(f\ x)\ \,\,(f\ (f\ x))\\&=\ K\,\,\,\,(f\ (f\ x))\ \,\,(f\ (f\ (f\ x)))\\&=\ f\ (f\ x)\\\end{aligned}}

يُظهر بوضوح ما يحدث. ومع ذلك، فإن الأصل $\operatorname {pred}$ يُعد هذا الخيار أفضل بكثير لأنه يعمل بطريقة تنازلية، وبالتالي فهو قادر على التوقف فورًا إذا تم تحديد وظيفة من قِبل المستخدم. $f$ هو اختصار الدائرة. كما يُستخدم النهج التنازلي مع تعريفات أخرى مثل

{\begin{aligned}\operatorname {pred} _{5}\equiv \lambda nfx.n\ &(\lambda rab.a\ (r\ b\ b))\,(\lambda ab.x)\ I\ f\\\operatorname {third} \equiv \lambda nfx.n\ &(\lambda rabc.a\ (r\ b\ c\ a))\,(\lambda abc.x)\ I\ I\ f\\\operatorname {thirdRounded} \equiv \lambda nfx.n\ &(\lambda rabc.a\ (r\ b\ c\ a))\,(\lambda abc.x)\ I\ f\ I\\\operatorname {twoThirds} \equiv \lambda nfx.n\ &(\lambda rabc.a\ (r\ b\ c\ a))\,(\lambda abc.x)\ I\ f\ f\\\operatorname {factorial} \equiv \lambda nfx.n\ &(\lambda ra.a\ (r\ (\operatorname {succ} a)))\,(\lambda a.f)\ 1\ x\\\end{aligned}}

القسمة عن طريق الاستدعاء الذاتي العام

يمكن تنفيذ قسمة الأعداد الطبيعية بواسطة، ^{[ 3 ]}

n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0

الحساب $n-m$ مع $\lambda nm.m\,\operatorname {pred} \,n$ يتطلب الأمر العديد من عمليات اختزال بيتا. ما لم يتم إجراء الاختزال يدويًا، فإن هذا لا يُشكل فرقًا كبيرًا، ولكن من الأفضل تجنب إجراء هذه العملية الحسابية مرتين (إلا إذا تم استخدام تعريف الطرح المباشر، انظر أعلاه). أبسط دالة لاختبار الأرقام هي IsZero، لذا ضع الشرط في اعتبارك.

\operatorname {IsZero} \ (\operatorname {minus} \ n\ m)

لكن هذا الشرط يعادل $n\leq m$ ، لا $n<m$ إذا تم استخدام هذا التعبير، فإن التعريف الرياضي للقسمة المذكور أعلاه يُترجم إلى دالة على الأرقام الكنسية كما يلي:

\operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)

كما هو مطلوب، يحتوي هذا التعريف على استدعاء واحد لـ $\operatorname {minus} \ n\ m$ لكن النتيجة هي أن هذه الصيغة تعطي قيمة $(n-1)/m$ .

يمكن حل هذه المشكلة بإضافة 1 إلى n قبل استدعاء دالة القسمة . تعريف دالة القسمة هو،

\operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)

دالة `divide1` هي تعريف تكراري. يمكن استخدام مُركِّب Y لتنفيذ التكرار. أنشئ دالة جديدة باسم `div by`.

في الجانب الأيسر $\operatorname {divide1} \rightarrow \operatorname {div} \ c$
في الجانب الأيمن $\operatorname {divide1} \rightarrow c$

للحصول على،

\operatorname {div} =\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)

ثم،

\operatorname {divide} =\lambda n.\operatorname {divide1} \ (\operatorname {succ} \ n)

أين،

{\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}

{\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}

{\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}

يعطي،

\scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.(\lambda n.n\ (\lambda x.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a))\ d\ ((\lambda f.\lambda x.x)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\ n)

أو كنص، باستخدام \ بدلاً من $λ$ ،

Divide = (\n.((\f.(\xx x) (\xf (xx))) (\c.\n.\m.\f.\x.(\d.(\nn (\x.(\a.\bb)) (\a.\ba)) d ((\f.\xx) fx) (f (cdmfx))) ((\m.\nn (\n.\f.\xn (\g.\hh (gf)) (\ux) (\uu)) m) nm))) ((\n.\f.\x.f (nfx)) n))

على سبيل المثال، يُكتب 9/3 على النحو التالي:

قسّم (\f.\xf (f (f (f (f (f (f (f (fx)))))))))) (\f.\xf (f (fx)))

باستخدام آلة حاسبة لحساب التفاضل والتكامل لامدا، يتم اختزال التعبير أعلاه إلى 3، باستخدام الترتيب الطبيعي.

\f.\xf (f (f (x)))

المسندات

الدالة الشرطية هي دالة تُرجع قيمة منطقية (Boolean). وأهم دالة شرطية في الأرقام الكنسية هي $\operatorname {IsZero}$ ، وهو ما يعود $\operatorname {true}$ إذا كانت حجتها هي رقم الكنيسة $0$ ، و $\operatorname {false}$ خلاف ذلك:

\operatorname {IsZero} =\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true}

يختبر الشرط التالي ما إذا كانت الوسيطة الأولى أصغر من أو تساوي الوسيطة الثانية:

\operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)

بسبب الهوية

x=y\equiv (x\leq y\land y\leq x)

يمكن تطبيق اختبار المساواة على النحو التالي:

\operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)

في لغات البرمجة

تدعم معظم لغات البرمجة الواقعية الأعداد الصحيحة الأصلية للآلة؛ حيث تقوم الدالتان church و unchurch بتحويل الأعداد الصحيحة غير السالبة إلى ما يقابلها من أرقام Church. تُقدم هذه الدوال هنا بلغة Haskell ، حيث \يُمثل λ في حساب Lambda. وتتشابه تطبيقاتها في اللغات الأخرى.

نوع الكنيسة أ = ( أ -> أ ) -> أ -> أchurch :: Integer -> Church Integer church 0 = \ f -> \ x -> x church n = \ f -> \ x -> f ( church ( n - 1 ) f x )unchurch :: Church Integer -> Integer unchurch cn = cn ( + 1 ) 0

الأرقام الموقعة

إحدى الطرق البسيطة لتوسيع نطاق استخدام أرقام الكنيسة لتشمل الأعداد الموقعة هي استخدام زوج من أرقام الكنيسة، يحتوي على رقمين يمثلان قيمة موجبة وقيمة سالبة. ^{[ 4 ]} القيمة الصحيحة هي الفرق بين رقمي الكنيسة.

يتم تحويل العدد الطبيعي إلى عدد موجب بواسطة:

\operatorname {convert} _{s}=\lambda x.\operatorname {pair} \ x\ 0

يتم إجراء النفي عن طريق تبديل القيم.

\operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)

تُصبح القيمة الصحيحة أكثر وضوحًا إذا كان أحد العنصرين يساوي صفرًا. وتُحقق دالة OneZero هذا الشرط.

\operatorname {OneZero} =\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))

يمكن تنفيذ التكرار باستخدام مُركِّب Y،

\operatorname {OneZ} =\lambda c.\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (c\ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))

\operatorname {OneZero} =Y\operatorname {OneZ}

زائد وناقص

يُعرَّف الجمع رياضياً على الزوج كما يلي:

x+y=[x_{p},x_{n}]+[y_{p},y_{n}]=x_{p}-x_{n}+y_{p}-y_{n}=(x_{p}+y_{p})-(x_{n}+y_{n})=[x_{p}+y_{p},x_{n}+y_{n}]

يُترجم التعبير الأخير إلى حساب التفاضل والتكامل لامدا على النحو التالي:

\operatorname {plus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))

وبالمثل، يتم تعريف الطرح،

x-y=[x_{p},x_{n}]-[y_{p},y_{n}]=x_{p}-x_{n}-y_{p}+y_{n}=(x_{p}+y_{n})-(x_{n}+y_{p})=[x_{p}+y_{n},x_{n}+y_{p}]

العطاء،

\operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))

اضرب واقسم

يمكن تعريف عملية الضرب من خلال،

x*y=[x_{p},x_{n}]*[y_{p},y_{n}]=(x_{p}-x_{n})*(y_{p}-y_{n})=(x_{p}*y_{p}+x_{n}*y_{n})-(x_{p}*y_{n}+x_{n}*y_{p})=[x_{p}*y_{p}+x_{n}*y_{n},x_{p}*y_{n}+x_{n}*y_{p}]

يُترجم التعبير الأخير إلى حساب التفاضل والتكامل لامدا على النحو التالي:

\operatorname {mult} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))

يُقدَّم هنا تعريف مشابه للقسمة، باستثناء أن أحد قيم كل زوج يجب أن يكون صفرًا (انظر OneZero أعلاه). تسمح لنا دالة divZ بتجاهل القيمة التي تحتوي على عنصر صفري.

\operatorname {divZ} =\lambda x.\lambda y.\operatorname {IsZero} \ y\ 0\ (\operatorname {divide} \ x\ y)

ثم يتم استخدام divZ في الصيغة التالية، وهي نفس الصيغة المستخدمة في الضرب، ولكن مع استبدال mult بـ divZ .

\operatorname {divide} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))

الأعداد النسبية والأعداد الحقيقية

يمكن أيضًا ترميز الأعداد النسبية والأعداد الحقيقية القابلة للحساب في حساب لامدا. يمكن ترميز الأعداد النسبية كزوج من الأعداد الموقعة. أما الأعداد الحقيقية القابلة للحساب، فيمكن ترميزها بعملية تقريبية تضمن أن يكون الفرق بينها وبين القيمة الحقيقية عددًا صغيرًا جدًا. ^{[ 5 ]}^{[ 6 ]} تصف المراجع المذكورة برامجًا يمكن، نظريًا، ترجمتها إلى حساب لامدا. بمجرد تعريف الأعداد الحقيقية، تُرمّز الأعداد المركبة تلقائيًا كزوج من الأعداد الحقيقية.

تُبيّن أنواع البيانات والوظائف المذكورة أعلاه أنه يمكن ترميز أي نوع من البيانات أو أي عملية حسابية باستخدام حساب لامدا. هذه هي فرضية تشرش-تورينغ .

ترميزات القوائم

تحتوي القائمة على بعض العناصر مرتبةً. العمليات الأساسية على القوائم هي:

وظيفة	وصف
لا شيء	أنشئ قائمة فارغة
إينيسيل	اختبر ما إذا كانت القائمة فارغة
سلبيات	أضف قيمة معينة إلى قائمة (قد تكون فارغة)
رأس	احصل على العنصر الأول من القائمة
ذيل	احصل على بقية القائمة
شخص واحد	أنشئ قائمة تحتوي على عنصر واحد محدد
إلحاق	قم بدمج قائمتين معًا
مجلد	قم بطي القائمة باستخدام "+" و "0" المعطاة.

ينبغي أن يوفر تمثيل القوائم طرقًا لتنفيذ هذه العمليات. يمكن تعريف بعض هذه العمليات بدلالة عمليات أخرى، مثل

{\begin{aligned}\operatorname {singleton} &\equiv \lambda \,v.\ \operatorname {cons} \ v\ \operatorname {nil} \\\operatorname {cons} &\equiv \lambda \,h.\ \operatorname {append} \ (\operatorname {singleton} \ h)\\\operatorname {append} &\equiv \lambda \,l\,r.\ \operatorname {foldr} \ \operatorname {cons} \ r\,\ l\ \\\operatorname {isnil} &\equiv \operatorname {foldr} \ (\lambda \,h\,r.\operatorname {false} )\ \operatorname {true} \\\operatorname {head} &\equiv \operatorname {foldr} \ (\lambda \,h\,r.h)\ \operatorname {nil} \\\end{aligned}}

ويمكن تعريف المزيد من حيث التكرار الهيكلي (الطي الأيمن، أي التحول العكسي، وكذلك التحول المتماثل، وما إلى ذلك)، أو التكرار العام باستخدام تكرار النقطة الثابتة.

يُعدّ ترميز قائمة تشيرش النموذج الأمثل لتمثيل القوائم في حساب لامدا. فهو يُمثّل القوائم كعمليات طيّ يمينية ، أي كدوال تُعيد نتائج عملية الطيّ على القائمة باستخدام وسائط يُقدّمها المستخدم.

يتبع هذا النموذج مبدأ "الشيء هو شيء يمكن ملاحظته". وبغض النظر عن التطبيق العملي، فإن طي قائمة معينة من القيم يؤدي إلى النتيجة نفسها. وهذا يوفر نظرة مجردة لماهية القائمة. يُعد ترميز قائمة تشيرش أحد هذه الآليات.

من ناحية أخرى، وبنظرة أكثر واقعية، يمكن تمثيل القوائم على أنها سلسلة من عقد القوائم المرتبطة .

فيما يلي أربعة تمثيلات مختلفة للقوائم:

قوائم الكنائس – تمثيل الطية اليمنى .
زوجان من الكنائس لكل عقدة قائمة.
زوج واحد من الكنائس لكل عقدة قائمة.
ترميز سكوت.

قوائم الكنائس – تمثيل الطي الأيمن

هذا هو ترميز الكنيسة الأصلي للقوائم. يتم تمثيل القائمة بواسطة دالة ثنائية، والتي عند تزويدها بوسيطين - "دالة دمج" و"قيمة حارس" - ستنفذ عملية الطي الأيمن للقائمة المشفرة باستخدام هذين الوسيطين.

في حالة القائمة الفارغة، تُعاد قيمة العنصر الحارس كنتيجة لعملية الطي. أما نتيجة طي قائمة غير فارغة ذات رأس h وذيل t، فهي ناتج دمج الرأس h مع نتيجة طي الذيل t باستخدام الوسيطين المُقدمين، وذلك بواسطة الدالة المُقدمة. وبالتالي ، فإن وسيطي دالة الدمج هما، من الناحية النظرية، العنصر الحالي ونتيجة طي بقية عناصر القائمة.

على سبيل المثال، تُمثَّل قائمةٌ من ثلاثة عناصر x و y و z بمصطلحٍ عند تطبيقه على c و n يُعيد cx (cy (czn)). وبالمثل، فهو تطبيقٌ لسلسلة التركيبات الوظيفية ( $\circ$ ) من التطبيقات الجزئية، ((cx) $\circ$ (cy) $\circ$ (cz)) اسم.

{\begin{aligned}\operatorname {nil} &\equiv \lambda \,c\,n.n\\\operatorname {cons} &\equiv \lambda \,h\,t.\lambda \,c\,n.c\ h\ (t\ c\ n)\\\operatorname {singleton} &\equiv \lambda \,h.\lambda \,c\,n.c\ h\ n\ \\\operatorname {foldr} &\equiv \lambda \,c\,n\,l.l\ c\ n\\\operatorname {isnil} &\equiv \lambda \,l.l\ (\lambda \,h\,r.\operatorname {false} )\ \operatorname {true} \\\operatorname {append} &\equiv \lambda \,l\,m.\lambda \,c\,n.l\ c\ (m\ c\ n)\\&\equiv \lambda \,l\,m.\lambda \,c\,n.\,\operatorname {foldr} \ c\ \,(\operatorname {foldr} \ c\ n\ m)\,\ l\\&\equiv \lambda \,l\,m.\,\operatorname {foldr} \,\operatorname {cons} \ (\operatorname {foldr} \,\operatorname {cons} \ \operatorname {nil} \ m)\,\ l\\&\equiv \lambda \,l\,m.\,\operatorname {foldr} \,\operatorname {cons} \ m\ \,l\\\operatorname {head} &\equiv \lambda \,l.l\ (\lambda \,h\,r.h)\ \operatorname {nil} \\\operatorname {safehead} &\equiv \lambda \,l\,e\,s.l\ (\lambda \,h\,r.s\ h)\ e\,\ \equiv \,\ \lambda \,l\,e\,s.\operatorname {foldr} \ (\lambda \,h\,r.s\ h)\ e\ l\\\operatorname {map} &\equiv \lambda f\,l.\lambda \,c\,n.l\ (\lambda \,h\,r.c\ (f\ h)\ r)\ n\,\ \equiv \,\ \lambda f\,l\,c.l\ (c\circ f)\\&\equiv \lambda f\,l.\lambda \,c\,n.\operatorname {foldr} \ (c\circ f)\ n\ l\,\ \equiv \,\ \lambda f.\operatorname {foldr} \ (\operatorname {cons} \circ f)\ \operatorname {nil} \\\operatorname {tail} &\equiv \lambda \,l.\operatorname {foldr} \ (\lambda \,h\,r\,g.g\ h\ (r\ \operatorname {cons} ))\ (\lambda \,g.\operatorname {nil} )\,\ l\,\ (\lambda \,h\,t.t)\\&\equiv \lambda \,l.\lambda \,c\,n.l\ (\lambda \,h\,r\,g.g\ h\ (r\ c))\ (\lambda \,g.n)\ (\lambda \,h\,t.t)\end{aligned}}

كما تم تقديم بعض التعريفات بشكل عام يعتمد على الطي، وهو ما يصلح لأي ترميز.

يتبع هذا الترميز المنطق التالي: المعادلات

fold cn [ ] = n fold cn [x ] = cxn fold cn [x,y,z] = cx (cy (czn))

يعني ذلك

{\begin{aligned}&\{\ [\ \ \ \ ]\ \}&&\equiv \lambda \,c\,n.n\\&\{\ [\ x\ \ \ ]\ \}&&\equiv \lambda \,c\,n.c\ x\ n\\&\{\ [\ x,\,y,\,z\ ]\ \}&&\equiv \lambda \,c\,n.c\ x\ (c\ y\ (c\ z\ n))\end{aligned}}

أين $\{\ l\ \}=\lambda \,c\,n.fold\ c\ n\ l$ يشير إلى تمثيل قائمة الكنيسة للقائمة $l$ .

بما أن قائمة Church المشفرة هي دالة طي خاصة بها، فإن طيها يعني ببساطة تطبيق تلك الدالة على الوسائط المقدمة.

يمكن تحديد نوع تمثيل هذه القائمة في النظام F.

إن التطابق الواضح مع أرقام الكنيسة ليس من قبيل الصدفة، إذ يمكن اعتبارها ترميزًا أحاديًا، حيث تُمثَّل الأعداد الطبيعية بقوائم من القيم الوحدوية (أي غير المهمة)، مثل [() () ()]، حيث يُمثِّل طول القائمة العدد الطبيعي. يستخدم الطي من اليمين على هذه القوائم دوالًا تتجاهل بالضرورة قيمة العنصر، وهو ما يُكافئ التركيب الوظيفي المتسلسل، أي ((c()) $\circ$ (ج ()) $\circ$ (ج ()) ) ن = (و $\circ$ و $\circ$ و) ن، كما هو مستخدم في الأرقام الكنسية.

زوجان كعقدة قائمة

يمكن تمثيل قائمة غير فارغة بزوج من عناصر الكنيسة، حيث

يحتوي أولاً على رأس القائمة
يحتوي الثاني على ذيل القائمة

لكن هذا لا يُعطي تمثيلاً للقائمة الفارغة، لأنه لا يوجد مؤشر "null". لتمثيل القيمة null، يمكن تغليف الزوج بزوج آخر، مما يُعطي ثلاث قيم:

أولاً - مؤشر القائمة الفارغة (قيمة منطقية).
يحتوي الأول من الثاني على الرأس ( السيارة ).
يحتوي الجزء الثاني من الجزء الثاني على الذيل ( cdr ).

باستخدام هذه الفكرة، يمكن تعريف عمليات القوائم الأساسية على النحو التالي: ^{[ 7 ]}

تعبير	وصف
$\operatorname {nil} \equiv \operatorname {pair} \ \operatorname {true} \ \operatorname {true}$	العنصر الأول من الزوج صحيح ، مما يعني أن القائمة فارغة.
$\operatorname {isnil} \equiv \operatorname {first}$	استرجع مؤشر القيمة الفارغة (أو القائمة الفارغة).
$\operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \operatorname {false} \ (\operatorname {pair} h\ t)$	قم بإنشاء عقدة قائمة، وهي ليست فارغة، وقم بإعطائها رأسًا h وذيلًا t .
$\operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)$	ثانياً. أولاً هو الرأس.
$\operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)$	ثانيًا. الثاني هو الذيل.

في العقدة الفارغة ، لا يتم الوصول إلى العقدة الثانية أبدًا، بشرط أن يتم تطبيق العقدة الأولى والثانية فقط على القوائم غير الفارغة.

زوج واحد كعقدة قائمة

أو بدلاً من ذلك، حدد ^{[ 8 ]}

{\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda l.\ l\ (\lambda htd.\operatorname {false} )\ \operatorname {true} \\\operatorname {head} &\equiv \lambda l.\ l\ (\lambda htd.\ h)\ \operatorname {nil} \\\operatorname {tail} &\equiv \lambda l.\ l\ (\lambda htd.\ t)\ \operatorname {nil} \\\end{aligned}}

حيث تتبع التعريفات، مثل التعريف الأخير، نفس النمط العام للاستخدام الآمن للقائمة، مع $h$ و $t$ بالإشارة إلى بداية القائمة ونهايتها، و $d$ يتم التخلص منه، كجهاز اصطناعي:

{\begin{aligned}\lambda l.l\ (\lambda htd.\langle \operatorname {head-and-tail-clause} \rangle )\ \langle \operatorname {nil-clause} \rangle \\\end{aligned}}

العمليات الأخرى في هذا الترميز هي:

{\begin{aligned}\operatorname {lfold} &\equiv \lambda g.\ \operatorname {Y} \ (\lambda r.\lambda al.\ l\ (\lambda htd.\ r\ (g\ a\ h)\ t)\ a)\\\operatorname {foldr} &\equiv \lambda gz.\ \operatorname {Y} \ (\lambda r.\lambda l.\ l\ (\lambda htd.\ g\ h\ (r\ t))\ z)\\\operatorname {length} &\equiv \operatorname {foldr} \ (\lambda hr.\ \operatorname {succ} \ r)\ \operatorname {zero} \\&\equiv \lambda lfx.\ \operatorname {foldr} \ (\lambda h.\ f)\ x\ l\\\end{aligned}}

{\begin{aligned}\operatorname {map} &\equiv \lambda f.\ \operatorname {foldr} \ (\lambda hr.\operatorname {cons} \ (f\ h)\ r)\ \operatorname {nil} \\\operatorname {filter} &\equiv \lambda p.\ \operatorname {foldr} \ (\lambda hr.\ p\ h\ (\operatorname {cons} \ h\ r)\ r)\ \operatorname {nil} \\\operatorname {reverse} &\equiv \operatorname {lfold} \ (\lambda ah.\ \operatorname {cons} \ h\ a)\ \operatorname {nil} \\\operatorname {append} &\equiv \lambda lm.\ \operatorname {foldr} \ \operatorname {cons} \ m\ \ l\\\operatorname {conj} &\equiv \lambda lv.\ \operatorname {append} \ l\ \ (\operatorname {cons} \ v\ \operatorname {nil} )\\\operatorname {concat} &\equiv \operatorname {foldr} \ \operatorname {append} \ \operatorname {nil} \\\operatorname {replicate} &\equiv \lambda nv.\ n\ (\operatorname {cons} \ v)\ \operatorname {nil} \\\operatorname {repeat} &\equiv \lambda v.\ \operatorname {Y} \ (\lambda r.\ \operatorname {cons} \ v\ r)\\\operatorname {iterate} &\equiv \lambda f.\ \operatorname {Y} \ (\lambda ra.\ \operatorname {cons} \ a\ (r\ (f\ a)))\\\operatorname {zip} &\equiv Y\ (\lambda rlm.\ l\ (\lambda htd.\ m\ (\lambda esz.\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \operatorname {cons} \ (\operatorname {pair} \ h\ e)\ (r\ t\ s))\ \operatorname {nil} )\ \operatorname {nil} )\\\end{aligned}}

{\begin{aligned}\operatorname {drop} \equiv \ &\lambda n.\ n\ \operatorname {tail} \\\equiv \ &\lambda n.\ n\ (\lambda rl.\ l\ (\lambda htd.r\ t)\ \operatorname {nil} )\ (\lambda l.\ l)\\\operatorname {drop-while} \equiv \ &\lambda p.\ \operatorname {Y} \ (\lambda rl.\ l\ (\lambda htd.\ p\ h\ (r\ t)\ l)\ \operatorname {nil} )\\\operatorname {drop-until} \equiv \ &\lambda p.\ \operatorname {Y} \ (\lambda rl.\ l\ (\lambda htd.\ p\ h\ t\ (r\ t))\ \operatorname {nil} )\\\operatorname {drop-last} \equiv \ &\lambda nl.\ \operatorname {map} \ \operatorname {first} \ (\operatorname {zip} \ l\ \,(\operatorname {drop} \ n\ l))\\\equiv \ &\lambda nl.\ \operatorname {foldr} \ (\lambda hrq.\ q\ r\ h)\ (\lambda q.\ \operatorname {nil} )\,\ l\\&\ \ \ \ \ \ \ \ (\operatorname {foldr} \ (\lambda eqrh.\ \operatorname {cons} \ h\ (r\ q))\ (\lambda rh.\ \operatorname {nil} )\ (\operatorname {drop} \ n\ l))\\\operatorname {take} \equiv \ &\lambda nl.\ \operatorname {map} \ \operatorname {first} \ (\operatorname {zip} \ l\ \,(\operatorname {replicate} \ n\ \,\operatorname {nil} ))\\\equiv \ &\lambda n.\ n\ (\lambda rl.\ l\ (\lambda htd.\ \operatorname {cons} \ h\ (r\ t))\ \operatorname {nil} )\ (\lambda l.\operatorname {nil} )\\\operatorname {take-while} \equiv \ &\lambda p.\ \operatorname {foldr} \ (\lambda hr.\ p\ h\ (\operatorname {cons} \ h\ r)\ \operatorname {nil} )\ \operatorname {nil} \\\operatorname {take-until} \equiv \ &\lambda p.\ \operatorname {foldr} \ (\lambda hr.\ p\ h\ (\operatorname {cons} \ h\ \operatorname {nil} )\ (\operatorname {cons} \ h\ r))\ \operatorname {nil} \\\operatorname {take-last} \equiv \ &\lambda nl.\ \operatorname {drop} \ (\operatorname {length} \ (\operatorname {drop} \ n\ \,l))\ l\\\equiv \ &\lambda nl.\ \operatorname {foldr} \ (\lambda hrq.\ q\ r\ h)\ (\lambda q.\ \operatorname {nil} )\,\ l\\&\ \ \ \ \ \ \ \ (\operatorname {foldr} \ (\lambda eqrh.\ r\ q)\ (\operatorname {Y} \ (\lambda qrh.\ \operatorname {cons} \ h\ (r\ q)))\ (\operatorname {drop} \ n\ l))\\\equiv \ &\lambda nl.\ Y\ (\lambda rlm.\ l\ (\lambda htd.\ m\ (\lambda esz.r\ t\ s)\,\ l)\ \operatorname {nil} )\,\ l\,\ (\operatorname {drop} \ n\ l)\end{aligned}}

{\begin{aligned}\operatorname {all} &\equiv \lambda p.\ \operatorname {foldr} \ (\lambda hr.\ p\ h\ r\ \operatorname {false} )\ \operatorname {true} \\\operatorname {any} &\equiv \lambda p.\ \operatorname {foldr} \ (\lambda hr.\ p\ h\ \operatorname {true} \ r)\ \operatorname {false} \\\operatorname {element-at} &\equiv \lambda nl.\ \operatorname {drop} \ n\ l\ (\lambda htdfs.\ s\ h)\ (\lambda fs.\ f)\\\operatorname {insert-at} &\equiv \lambda nvl.\ \operatorname {append} \ (\operatorname {take} \ n\ l)\ (\operatorname {cons} \ v\ (\operatorname {drop} \ n\ l))\\&\equiv \lambda nv.\ n\ (\lambda rl.\ l\ (\lambda htd.\ \operatorname {cons} \ h\ (r\ t))\ (\operatorname {cons} \ v\ \operatorname {nil} ))\ (\operatorname {cons} \ v)\\\operatorname {remove-at} &\equiv \lambda nl.\ \operatorname {append} \ (\operatorname {take} \ n\ l)\ (\operatorname {drop} \ (\operatorname {succ} \ n)\ l)\\&\equiv \lambda n.\ n\ (\lambda rl.\ l\ (\lambda htd.\ \operatorname {cons} \ h\ (r\ t))\ \operatorname {nil} )\ \operatorname {tail} \\\operatorname {replace-at} &\equiv \lambda nv.\ n\ (\lambda rl.\ l\ (\lambda htd.\ \operatorname {cons} \ h\ (r\ t))\ \operatorname {nil} )\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\lambda \ \ l.\ l\ (\lambda htd.\ \operatorname {cons} \ v\ t)\ \operatorname {nil} )\\\operatorname {index-of} &\equiv \lambda pl.\ \operatorname {foldr} \ (\lambda hrn.\ p\ h\ (\lambda fs.\ s\ n)\ (r\ (\operatorname {succ} \ n)))\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\lambda \ \ \ \ nfs.\ f)\,\ l\ \operatorname {zero} \\\operatorname {last-index-of} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rnl.\ l\ (\lambda htd.\ (\lambda i.\ i\ (p\ h\ (\lambda fs.\ s\ n)\ i)\ (\lambda n.\ i))\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (r\ (\operatorname {succ} \ n)\ t))\ (\lambda fs.\ f))\ \operatorname {zero} \\&\equiv \lambda pl.\ \operatorname {index-of} \ p\ (\operatorname {reverse} \ l)\ (\lambda m.\ m\ (\lambda fs.\ f)\ \\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\lambda ifs.\ s\ (\operatorname {minus} \ (\operatorname {length} \ l)\ (\operatorname {succ} \ i))))\\&\equiv \lambda pl.\ \operatorname {foldr} \ (\lambda hrna.\ p\ h\ (r\ (\operatorname {succ} \ n)\ (\lambda fs.\ s\ n))\ (r\ (\operatorname {succ} \ n)\ a))\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\lambda \ \ \ na.\ a)\,\ l\,\ \operatorname {zero} \ (\lambda fs.\ f)\\\operatorname {range} &\equiv \lambda fz.\ \operatorname {Y} \ (\lambda rsn.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ (s\ f\ z)\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (r\ (\operatorname {succ} \ s)\ (\operatorname {pred} \ n))))\ \operatorname {zero} \\&\equiv \lambda fzn.\ n\ (\lambda ra.\ \operatorname {cons} \ a\ (r\ (f\ a)))\ (\lambda a.\ \operatorname {nil} )\ z\\\end{aligned}}

من المهم تعريف دالة التابع على أرقام تشيرش بطريقة كسولة، أي succ := λ nfx . f(nfx) ، بدلاً من succ := λ nfx . nf(fx) ، بحيث ينتج عن طول الدالة أرقام كسولة، وذلك لتحقيق أقصى قدر من الكسل في عمليات الاختزال ضمن استراتيجية الاختزال من أعلى اليسار. بعبارة أخرى، لسنا بحاجة لمعرفة قيمة الطول النهائي إذا كان كل ما نحتاج معرفته هو ما إذا كان غير صفري أم لا.

سكوت يسرد

تتبع ترميز سكوت لأنواع البيانات بنيتها الظاهرية دون مراعاة التكرار في نوع البيانات. في نمط تعريفات أنواع البيانات الجبرية، المعروف أيضًا باسم "فصل الاقترانات" أو "مجموع المنتجات"، يُمثل هذا الترميز البيانات المعطاة كدالة تتوقع عددًا من الوسائط يساوي عدد البدائل في تعريف نوع البيانات الخاص بها، حيث يُتوقع أن يكون كل وسيط دالة "معالجة" قادرة على التعامل مع عدد وسائط البيانات المُعطى، والتي ستتوافق مع حقول البيانات الخاصة بذلك البديل.

عند إدخال جميع المعالجات كوسائط، ستستدعي دالة تمثيل البيانات المعالج المناسب مع البيانات الداخلية المقابلة. وبذلك، يمكن القول إن القيم المشفرة باستخدام ترميز سكوت تجسد معالجة حالات مطابقة الأنماط لنوع بياناتها.

بالنسبة للقوائم، فهذا يعني تعريف نوع البيانات لـ

$\qquad List:=\operatorname {NIL} \ |\,\operatorname {Cons} \,\langle val\rangle \,List$

ويتم تمثيل القوائم على النحو التالي:

$\quad {\begin{aligned}\operatorname {NIL} &=\lambda nc.n\\\operatorname {Cons} &=\lambda ad.\lambda nc.c\ a\ d\\\operatorname {IsEmpty} &=\lambda l.l\,\operatorname {true} \,(\lambda ad.\operatorname {false} )\\\operatorname {Head} &=\lambda l.l\,\operatorname {NIL} \,(\lambda ad.a)\\\operatorname {Tail} &=\lambda l.l\,\operatorname {NIL} \,(\lambda ad.d)\\\operatorname {Foldr} &=\lambda gz.\operatorname {Y} \lambda rl.l\ z\ (\lambda ad.g\,a\ (r\ d))\\\operatorname {Foldr2} &=\lambda gzpq.\operatorname {Foldr} \ (\lambda ark.k\ a\ r)\ (\lambda k.z)\ p\\&\ \ \ \ \ \ \ \ (\operatorname {Foldr} \ (\lambda bsar.g\ a\ b\ (r\ s))\ (\lambda ar.z)\ q)\\&=\lambda gzpq.\operatorname {Foldr} \ (\lambda t.t\ g)\ z\ (\operatorname {Zip} \ p\ q)\\&=\lambda gz.\operatorname {Y} \lambda rpq.p\,z\,(\lambda ad.\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ q\,z\,(\lambda be.g\ a\ b\ (r\ d\ e)))\\\operatorname {Append} &=\lambda lm.\operatorname {Foldr} \,\operatorname {Cons} \ m\ l\\\operatorname {Map} &=\lambda f.\operatorname {Foldr} \ (\lambda a.\operatorname {Cons} \ (f\ a))\,\operatorname {NIL} \\\operatorname {Map2} &=\lambda f.\operatorname {Foldr2} \ (\lambda ab.\operatorname {Cons} \ (f\ a\ b))\,\operatorname {NIL} \\&=\lambda f.\operatorname {Y} \lambda rpq.p\,\operatorname {NIL} \,(\lambda ad.\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ q\,\operatorname {NIL} \,(\lambda be.\operatorname {Cons} \,(f\ a\ b)\ (r\ d\ e)))\\\operatorname {Zip} &=\operatorname {Map2} \,\operatorname {pair} \\\end{aligned}}$

تتطلب العمليات المتكررة على قوائم سكوت عادةً استخدامًا صريحًا للتكرار، على سبيل المثال باستخدام $\operatorname {Y}$ المُركِّب، أو تعريفات التطبيق الذاتي الصريحة. أحد الأمثلة على ذلك هو دالة foldr ، على عكس كونها عديمة التأثير في ترميز Church. لكن دالة tail متاحة فورًا، لذا فإن تعريفها هنا أبسط بكثير بالمقارنة. انظر ترميز Scott للمزيد.

يمكن اعتبار ترميز سكوت بمثابة استخدام لفكرة الاستمرارية ، مما قد يؤدي إلى تبسيط الكود ^{[ 9 ]} . في هذا النهج، نستفيد من إمكانية فحص القوائم باستخدام تعبيرات مطابقة الأنماط . على سبيل المثال، باستخدام ترميز سكالاlist ، إذا كان يمثل قيمة من النوع Listمع قائمة فارغة Nilومنشئ، Cons(h, t)فيمكننا فحص القائمة وحساب nilCodeفي حالة كون القائمة فارغة، و consCode(h, t)عندما لا تكون فارغة.

قائمة مطابقة { حالة Nil => nilCode حالة Cons ( h , t ) => consCode ( h , t ) }

يُحدد ذلك listمن خلال كيفية تأثيره على nilCodeو consCode. لذلك، نُعرّف القائمة على أنها دالة تقبل مثل nilCodeو consCodeكمعاملات، بحيث يمكننا ببساطة كتابة ما يلي بدلاً من مطابقة النمط أعلاه:

\operatorname {list} \ \operatorname {nilCode} \ \operatorname {consCode}

لنرمز بـ إلى nالمعامل المقابل لـ nilCodeو بـ إلى cالمعامل المقابل لـ consCode. إذن، القائمة الفارغة هي التي تُرجع الوسيط صفرًا:

\operatorname {nil} \equiv \lambda n.\lambda c.\ n

القائمة غير الفارغة ذات الرأس hوالذيل tتُعطى بواسطة

\operatorname {cons} \ h\ t\ \equiv \ \lambda n.\lambda c.c\ h\ t

وبشكل أعم، نوع بيانات جبري مع $m$ تصبح البدائل دالة مع $m$ المعلمات، كل منها عبارة عن دالة مراقبة/معالجة للبديل المقابل لها. عندما $i$ يحتوي مُنشئ البديل th على $n_{i}$ تأخذ الدالة المعالجة المقابلة الوسائط $n_{i}$ وكذلك الحجج.

يمكن تنفيذ ترميز سكوت في حساب لامدا غير المُحدد النوع، بينما يتطلب استخدامه مع الأنواع نظام أنواع يتضمن الاستدعاء الذاتي وتعدد أشكال الأنواع. قائمةٌ تحتوي على عنصر من النوع E في هذا التمثيل، والتي تُستخدم لحساب قيم من النوع C، سيكون لها تعريف النوع الاستدعائي التالي، حيث يشير الرمز '=>' إلى نوع الدالة :

نوع List = C => // وسيط فارغ ( E => List => C ) => // وسيط ثابت C // نتيجة مطابقة النمط

القائمة التي يمكن استخدامها لحساب أنواع عشوائية سيكون لها نوع يُحدد كميًا على C. القائمة العامة في Eستأخذ أيضًا Eكمعامل نوع.

ملاحظات عامة

يؤدي تطبيق ترميز Church بشكل مباشر إلى إبطاء بعض عمليات الوصول من $O(1)$ ل $O(n)$ ، أين $n$ يُعدّ حجم بنية البيانات عاملاً هاماً ، مما يجعل ترميز Church غير عملي. ^{[ 10 ]} وقد أظهرت الأبحاث إمكانية معالجة هذه المشكلة من خلال تحسينات مُوجّهة، إلا أن معظم لغات البرمجة الوظيفية تُوسّع تمثيلاتها الوسيطة لتشمل أنواع البيانات الجبرية . ^{[ 11 ]} ومع ذلك، يُستخدم ترميز Church بكثرة في الحجج النظرية، كونه تمثيلاً طبيعياً للتقييم الجزئي وإثبات النظريات. ^{[ 10 ]} يُمكن تحديد أنواع العمليات باستخدام أنواع ذات رتبة أعلى ، ^{[ 12 ]} كما يُمكن الوصول بسهولة إلى الاستدعاء الذاتي الأولي. ^{[ 10 ]} ويُبسّط افتراض أن الدوال هي أنواع البيانات الأولية الوحيدة العديد من البراهين.

يُعدّ ترميز تشيرش كاملاً، لكن على المستوى التمثيلي فقط. هناك حاجة إلى دوال إضافية لترجمة هذا التمثيل إلى أنواع بيانات شائعة، لعرضها على المستخدمين. لا يمكن عمومًا تحديد ما إذا كانت دالتان متساويتين امتداديًا نظرًا لعدم إمكانية حسم التكافؤ وفقًا لنظرية تشيرش . قد تُطبّق عملية الترجمة الدالة بطريقة ما لاسترجاع القيمة التي تُمثّلها، أو للبحث عن قيمتها كمصطلح لامدا حرفي. يُفسّر حساب لامدا عادةً باستخدام المساواة القصدية . توجد مشاكل محتملة في تفسير النتائج بسبب الاختلاف بين التعريف القصدي والتعريف الامتدادي للمساواة.

انظر أيضاً

حساب التفاضل والتكامل لامدا
نظام F للأرقام الكنسية في حساب التفاضل والتكامل المكتوب
ترميز موجنسن-سكوت
تعريف فون نيومان للأعداد الترتيبية - طريقة أخرى لترميز الأعداد الطبيعية: كمجموعات

مراجع

↑ جانسن، جان مارتن (2013)، "البرمجة في حساب لامدا: من تشرش إلى سكوت والعودة"، جمال الشفرة الوظيفية ، سلسلة محاضرات في علوم الحاسوب، المجلد 8106، سبرينغر-فيرلاغ، الصفحات 168-180 ، doi : 10.1007/978-3-642-40355-2_12 ، ISBN 978-3-642-40354-5.
↑ دان دويل ( https://math.stackexchange.com/users/590896/dan-doel )، تكرار أرقام الكنيسة؟، الرابط (الإصدار: 2026-02-27): https://math.stackexchange.com/q/4601054
↑ أليسون، لويد. "حساب التفاضل والتكامل لامدا للأعداد الصحيحة" .
↑ باور، أندريه. "إجابة أندريه على سؤال: "تمثيل الأعداد السالبة والمركبة باستخدام حساب التفاضل والتكامل لامدا"" .
↑ "الحساب الحقيقي الدقيق" . هاسكل . مؤرشف من الأصل بتاريخ 26-03-2015.
↑ باور، أندريه (26 سبتمبر 2022). "برنامج حسابي للأعداد الحقيقية" . جيت هاب .
↑ بيرس، بنجامين سي. (2002). أنواع ولغات البرمجة . مطبعة معهد ماساتشوستس للتكنولوجيا . ص 500. ISBN 978-0-262-16209-8.
↑ ترومب، جون (2007). "14. حساب لامدا الثنائي والمنطق التوافقي" . في كالود، كريستيان س. (محرر). العشوائية والتعقيد، من لايبنتز إلى تشايتين . وورلد ساينتيفيك. ص 237-262 . ISBN 978-981-4474-39-9.بصيغة PDF: ترومب، جون (14 مايو 2014). "حساب لامدا الثنائي والمنطق التوافقي" (PDF) . تم الاطلاع عليه بتاريخ 24 نوفمبر 2017 .
↑ جانسن، جان مارتن (2013). "البرمجة في حساب لامدا: من تشيرش إلى سكوت والعودة". في: أشتن، بيتر؛ كوبمان، بيتر دبليو إم (محرران). جمال الشفرة الوظيفية - مقالات مهداة إلى رينوس بلاسميير بمناسبة عيد ميلاده الحادي والستين . سلسلة محاضرات في علوم الحاسوب. المجلد 8106. سبرينغر. الصفحات 168-180 . doi : 10.1007/978-3-642-40355-2_12 . ISBN 978-3-642-40354-5.
1 2 3 ترانكون إي ويدمان، بالتاسار؛ بارناس، ديفيد لورج (2008). "التعبيرات الجدولية والبرمجة الوظيفية الكاملة". في أولاف تشيتيل؛ زولتان هورفاث؛ فيكتوريا زوك (محررون). تنفيذ وتطبيق اللغات الوظيفية . ورشة العمل الدولية التاسعة عشرة، IFL 2007، فرايبورغ، ألمانيا، 27-29 سبتمبر 2007. أوراق مختارة منقحة. سلسلة محاضرات في علوم الحاسوب. المجلد 5083. الصفحات 228-229 . doi : 10.1007/978-3-540-85373-2_13 . ISBN 978-3-540-85372-5.
↑ جانسن، جان مارتن؛ كوبمان، بيتر دبليو إم؛ بلاسميير، مارينوس جيه. (2006). "التفسير الفعال عن طريق تحويل أنواع البيانات والأنماط إلى دوال". في نيلسون، هنريك (محرر). اتجاهات في البرمجة الوظيفية. المجلد 7. بريستول: إنتلكت. الصفحات 73-90 . CiteSeerX 10.1.1.73.9841 . ISBN 978-1-84150-188-8.
↑ "لا يمكن تمثيل السلف والقوائم في حساب التفاضل والتكامل اللامدا ذي النوع البسيط" . حساب التفاضل والتكامل اللامدا وآلات حاسبة اللامدا . okmij.org.

ستامب، أ. (2009). "البرمجة الفوقية الانعكاسية المباشرة" (ملف PDF) . الحوسبة الرمزية عالية الرتبة . 22 (2): 115-144 . CiteSeerX 10.1.1.489.5018 . doi : 10.1007/s10990-007-9022-0 . S2CID 16124152 .
كارترايت، روبرت. "شرح الأرقام الكنسية والقيم المنطقية" (ملف PDF) . مراجعة 2 من مقرر Comp 311. جامعة رايس .
كيمب، كولين (2007). "§2.4.1 القيم الطبيعية لكنيسة، §2.4.2 القيم المنطقية لكنيسة، الفصل 5: تقنيات الاشتقاق للبرمجة الوظيفية الكاملة" . الأسس النظرية للبرمجة الوظيفية الكاملة العملية.(دكتوراه). كلية تكنولوجيا المعلومات والهندسة الكهربائية، جامعة كوينزلاند. الصفحات 14-17 ، 93-145 . CiteSeerX 10.1.1.149.3505 . كل ما يتعلق بتشفير الكنيسة والتشفيرات المماثلة الأخرى، بما في ذلك كيفية اشتقاقها والعمليات التي تُجرى عليها، انطلاقًا من المبادئ الأساسية.
بعض الأمثلة التفاعلية للأرقام الكنسية
درس مباشر في حساب التفاضل والتكامل لامدا: الجبر البولياني

[ce-3] 1 2 في ترميز الكنيسة،
$\operatorname {pred} (0)=0$
$m\leq n\to m-n=0$

[mwAW8] $\operatorname {pred} (0)=0$

[mwAX8] $m\leq n\to m-n=0$

[1] جانسن، جان مارتن (2013)، "البرمجة في حساب لامدا: من تشرش إلى سكوت والعودة"، جمال الشفرة الوظيفية ، سلسلة محاضرات في علوم الحاسوب، المجلد 8106، سبرينغر-فيرلاغ، الصفحات 168-180 ، doi : 10.1007/978-3-642-40355-2_12 ، ISBN 978-3-642-40354-5.

[2] دان دويل ( https://math.stackexchange.com/users/590896/dan-doel )، تكرار أرقام الكنيسة؟، الرابط (الإصدار: 2026-02-27): https://math.stackexchange.com/q/4601054

[4] أليسون، لويد. "حساب التفاضل والتكامل لامدا للأعداد الصحيحة" .

[5] باور، أندريه. "إجابة أندريه على سؤال: "تمثيل الأعداد السالبة والمركبة باستخدام حساب التفاضل والتكامل لامدا"" .

[6] "الحساب الحقيقي الدقيق" . هاسكل . مؤرشف من الأصل بتاريخ 26-03-2015.

[7] باور، أندريه (26 سبتمبر 2022). "برنامج حسابي للأعداد الحقيقية" . جيت هاب .

[8] بيرس، بنجامين سي. (2002). أنواع ولغات البرمجة . مطبعة معهد ماساتشوستس للتكنولوجيا . ص 500. ISBN 978-0-262-16209-8.

[9] ترومب، جون (2007). "14. حساب لامدا الثنائي والمنطق التوافقي" . في كالود، كريستيان س. (محرر). العشوائية والتعقيد، من لايبنتز إلى تشايتين . وورلد ساينتيفيك. ص 237-262 . ISBN 978-981-4474-39-9.بصيغة PDF: ترومب، جون (14 مايو 2014). "حساب لامدا الثنائي والمنطق التوافقي" (PDF) . تم الاطلاع عليه بتاريخ 24 نوفمبر 2017 .

[10] جانسن، جان مارتن (2013). "البرمجة في حساب لامدا: من تشيرش إلى سكوت والعودة". في: أشتن، بيتر؛ كوبمان، بيتر دبليو إم (محرران). جمال الشفرة الوظيفية - مقالات مهداة إلى رينوس بلاسميير بمناسبة عيد ميلاده الحادي والستين . سلسلة محاضرات في علوم الحاسوب. المجلد 8106. سبرينغر. الصفحات 168-180 . doi : 10.1007/978-3-642-40355-2_12 . ISBN 978-3-642-40354-5.

[Widemann-11] 1 2 3 ترانكون إي ويدمان، بالتاسار؛ بارناس، ديفيد لورج (2008). "التعبيرات الجدولية والبرمجة الوظيفية الكاملة". في أولاف تشيتيل؛ زولتان هورفاث؛ فيكتوريا زوك (محررون). تنفيذ وتطبيق اللغات الوظيفية . ورشة العمل الدولية التاسعة عشرة، IFL 2007، فرايبورغ، ألمانيا، 27-29 سبتمبر 2007. أوراق مختارة منقحة. سلسلة محاضرات في علوم الحاسوب. المجلد 5083. الصفحات 228-229 . doi : 10.1007/978-3-540-85373-2_13 . ISBN 978-3-540-85372-5.

[12] جانسن، جان مارتن؛ كوبمان، بيتر دبليو إم؛ بلاسميير، مارينوس جيه. (2006). "التفسير الفعال عن طريق تحويل أنواع البيانات والأنماط إلى دوال". في نيلسون، هنريك (محرر). اتجاهات في البرمجة الوظيفية. المجلد 7. بريستول: إنتلكت. الصفحات 73-90 . CiteSeerX 10.1.1.73.9841 . ISBN 978-1-84150-188-8.

[13] "لا يمكن تمثيل السلف والقوائم في حساب التفاضل والتكامل اللامدا ذي النوع البسيط" . حساب التفاضل والتكامل اللامدا وآلات حاسبة اللامدا . okmij.org.

[ 1 ]

[ 2 ]

[ أ ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

اللغة	العربية (RTL)
روابط موسوعية	30 رابطاً
المصدر الأصلي	ويكيبيديا ↗