حساب الإنشاءات

يتم إنشاء مصطلح في حساب التفاضل والتكامل باستخدام القواعد التالية:

• ${\displaystyle \mathbf {T} }$هو مصطلح (يسمى أيضًا نوع )؛
• ${\displaystyle \mathbf {P} }$هو مصطلح (يسمى أيضًا prop ، وهو نوع جميع القضايا)؛
• المتغيرات (${\displaystyle x,y,\ldots }$) هي مصطلحات؛
• لو${\displaystyle A}$و${\displaystyle B}$إذا كانت هذه مصطلحات، فكذلك${\displaystyle (AB)}$؛
• لو${\displaystyle A}$و${\displaystyle B}$هي مصطلحات و${\displaystyle x}$إذا كان متغيرًا، فإن ما يلي يُعد أيضًا مصطلحات:
  • ${\displaystyle (\lambda x:AB)}$،
  • ${\displaystyle (\forall x:AB)}$.

وبعبارة أخرى، فإن مصطلح النحو، بصيغة باكوس-ناور، هو:

${\displaystyle e::=\mathbf {T} \mid \mathbf {P} \mid x\mid e\,e\mid \lambda x{\mathbin {:}}ee\mid \forall x{\mathbin {:}}ee}$

يحتوي حساب الإنشاءات على خمسة أنواع من الكائنات:

1. البراهين ، وهي مصطلحات أنواعها عبارة عن قضايا ؛
2. القضايا ، والتي تُعرف أيضًا باسم الأنواع الصغيرة ؛
3. المسندات ، وهي دوال تُرجع قضايا؛
4. الأنواع الكبيرة ، وهي أنواع المسندات (${\displaystyle \mathbf {P} }$(وهو مثال على نوع كبير)؛
5. ${\displaystyle \mathbf {T} }$نفسها، وهي من النوع ذي الأحجام الكبيرة.

كما هو الحال مع حساب لامدا غير المصنف، يستخدم حساب الإنشاءات مفهومًا أساسيًا لتكافؤ الحدود، يُعرف باسم${\displaystyle \beta }$التكافؤ. هذا يجسد معنى${\displaystyle \lambda }$-التجريد:

• ${\displaystyle (\lambda x:AB)N=_{\beta }B(x:=N)}$

${\displaystyle \beta }$التكافؤ هو علاقة تطابق لحساب الإنشاءات، بمعنى أن

• لو${\displaystyle A=_{\beta }B}$و${\displaystyle M=_{\beta }N}$، ثم${\displaystyle AM=_{\beta }BN}$.

يسمح حساب الإنشاءات بإثبات أحكام الطباعة :

${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}$،

والتي يمكن قراءتها على أنها دلالة ضمنية

متغيرات إذا${\displaystyle x_{1},x_{2},\ldots }$لديهم، على التوالي، أنواع${\displaystyle A_{1},A_{2},\ldots }$ثم المصطلح${\displaystyle t}$له نوع${\displaystyle B}$.

يمكن استخلاص الأحكام الصحيحة لحساب الإنشاءات من مجموعة من قواعد الاستدلال. فيما يلي، نستخدم${\displaystyle \Gamma }$بمعنى سلسلة من تعيينات الأنواع ${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots }$؛${\displaystyle A,B,C,D}$بمعنى المصطلحات؛ و${\displaystyle K,L}$بمعنى إما${\displaystyle \mathbf {P} }$أو${\displaystyle \mathbf {T} }$سنكتب${\displaystyle B[x:=N]}$بمعنى نتيجة استبدال المصطلح${\displaystyle N}$بالنسبة للمتغير الحر${\displaystyle x}$في المصطلح${\displaystyle B}$.

تُكتب قاعدة الاستدلال على النحو التالي:

${\displaystyle {\frac {\Gamma \vdash A:B}{\Gamma '\vdash C:D}}}$،

وهذا يعني

لو${\displaystyle \Gamma \vdash A:B}$إذا كان الحكم صحيحاً، فكذلك${\displaystyle \Gamma '\vdash C:D}$.

1 .${\displaystyle {{} \over \Gamma \vdash \mathbf {P}$ :\mathbf {T} }}

2 .${\displaystyle {{\Gamma \vdash A:K} \over {\Gamma ,x:A,\Gamma '\vdash x:A}}}$

3 .${\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash B:L \over {\Gamma \vdash (\forall x:AB):L}}}$

4 .${\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:AN):(\forall x:AB)}}}$

5 .${\displaystyle {\Gamma \vdash M:(\forall x:AB)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B[x:=N]}}}$

6 . ${\displaystyle {\Gamma \vdash M:A\qquad \qquad A=_{\beta }B\qquad \qquad \Gamma \vdash B:K \over {\Gamma \vdash M:B}}}$

يحتوي حساب الإنشاءات على عدد قليل جدًا من العمليات الأساسية: العملية المنطقية الوحيدة لتكوين القضايا هي${\displaystyle \forall }$ومع ذلك، فإن هذا العامل وحده يكفي لتعريف جميع العوامل المنطقية الأخرى:

${\displaystyle {\begin{array}{ccll}A\Rightarrow B&\equiv &\forall x:AB&(x\notin B)\\A\wedge B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow B\Rightarrow C)\Rightarrow C&\\A\vee B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C&\\\neg A&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)&\\\exists x:AB&\equiv &\forall C:\mathbf {P} .(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{array}}}$

يمكن تعريف أنواع البيانات الأساسية المستخدمة في علوم الحاسوب ضمن حساب الإنشاءات:

القيم المنطقية

${\displaystyle \forall A:\mathbf {P} .A\Rightarrow A\Rightarrow A}$

ناتشورالز

${\displaystyle \forall A:\mathbf {P} .(A\Rightarrow A)\Rightarrow A\Rightarrow A}$

منتج${\displaystyle A\times B}$

${\displaystyle A\wedge B}$

اتحاد منفصل${\displaystyle A+B}$

${\displaystyle A\vee B}$

تُعرَّف القيم المنطقية والطبيعية بنفس الطريقة المتبعة في ترميز تشيرش . ومع ذلك، تنشأ مشاكل إضافية من الامتداد الافتراضي وعدم أهمية البرهان. ^{[ 2 ]}