ในตรรกศาสตร์ทางคณิตศาสตร์และวิทยาศาสตร์คอมพิวเตอร์แคลคูลัสของการสร้าง ( CoC ) เป็นทฤษฎีประเภทที่สร้างขึ้นโดยเธียร์รี โคควอนด์มันสามารถใช้ได้ทั้งเป็นภาษาโปรแกรมที่มีประเภท และเป็น รากฐาน เชิงสร้างสรรค์สำหรับคณิตศาสตร์ด้วยเหตุผลประการที่สองนี้ CoC และรูปแบบต่างๆ ของมันจึงเป็นพื้นฐานสำหรับRocqและโปรแกรม ช่วยพิสูจน์ อื่นๆ

รูปแบบต่างๆ ของมัน ได้แก่ แคลคูลัสของการสร้างแบบอุปนัย (ซึ่งเพิ่มประเภทอุปนัย) แคลคูลัสของการสร้างแบบอุปนัยร่วม (ซึ่งเพิ่มการอุปนัยร่วม) และแคลคูลัสเชิงทำนายของการสร้างแบบอุปนัย (ซึ่งขจัดคุณสมบัติที่ไม่สามารถทำนายได้บางส่วน)

CoC (CoC) เป็น แคลคูลัสแลมบ์ดาแบบมีชนิดข้อมูลระดับสูงซึ่งพัฒนาขึ้นครั้งแรกโดยเธียร์รี โคควอนด์ (Thierry Coquand ) เป็นที่รู้จักกันดีในฐานะที่เป็นส่วนสำคัญที่สุดของ ลูกบาศก์แลมบ์ดา ของบาเรนเดรกต์ (Barendregt's lambda cube ) ภายใน CoC สามารถกำหนดฟังก์ชันจากเทอมไปยังเทอม เทอมไปยังชนิดข้อมูล ชนิดข้อมูลไปยังชนิดข้อมูล และจากชนิดข้อมูลไปยังเทอมได้

CoC มีลักษณะเป็นมาตรฐานอย่างมากและสอดคล้องกัน^{[ 1 ]}

CoC ได้รับการพัฒนาควบคู่ไปกับโปรแกรมช่วยพิสูจน์Rocq เมื่อมีการเพิ่มคุณสมบัติ (หรือลบข้อจำกัดที่อาจเกิดขึ้น) เข้าไปในทฤษฎี คุณสมบัติเหล่านั้นก็จะพร้อมใช้งานใน Rocq

รูปแบบต่างๆ ของ CoC ถูกนำไปใช้ในโปรแกรมช่วยพิสูจน์อักษรอื่นๆเช่น MatitaและLean

แคลคูลัสของการสร้างสามารถพิจารณาได้ว่าเป็นส่วนขยายของไอโซมอร์ฟิซึมของเคอร์รี-ฮาวาร์ดไอโซมอร์ฟิซึมของเคอร์รี-ฮาวาร์ดเชื่อมโยงเทอมในแคลคูลัสแลมบ์ดาแบบง่ายกับ บทพิสูจน์ การอนุมานตามธรรมชาติ แต่ละบท ในตรรกศาสตร์เชิงประพจน์แบบสัญชาตญาณ แคลคูลัสของการสร้างขยายไอโซมอร์ฟิซึมนี้ไปยังบทพิสูจน์ในแคลคูลัสภาคแสดง แบบสัญชาตญาณเต็มรูปแบบ ซึ่งรวมถึงการพิสูจน์ข้อความที่มีตัวบ่งปริมาณ (ซึ่งเราจะเรียกว่า "ประพจน์" เช่นกัน)

เทอมในแคลคูลัสของการสร้างนั้นสร้างขึ้นโดยใช้กฎต่อไปนี้ :

• ${\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)}$.

กล่าวอีกนัยหนึ่ง คำว่าไวยากรณ์ในรูปแบบ Backus–Naurคือ:

${\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} }$ตัวมันเอง ซึ่งเป็นประเภทของตัวอักษรขนาดใหญ่

เช่นเดียวกับแคลคูลัสแลมบ์ดาที่ไม่มีประเภท แคลคูลัสของการสร้างใช้แนวคิดพื้นฐานของความเท่าเทียมกันของเทอม ซึ่งเรียกว่า-equivalence ซึ่งสะท้อนความหมายของ-abstraction ได้อย่างชัดเจน: ${\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 ]}

• ระบบประเภทบริสุทธิ์
• แลมบ์ดาคิวบ์
• ระบบ F
• ประเภทพึ่งพา
• ทฤษฎีประเภทสัญชาตญาณนิยม
• ทฤษฎีประเภทโฮโมโทปี