ตรรกะเชิงการจัดเรียง (Combinatory logic)เป็นสัญกรณ์ที่ช่วยขจัดความจำเป็นในการใช้ ตัวแปรเชิง ปริมาณในตรรกะทางคณิตศาสตร์ โดย ได้รับการแนะนำโดยMoses Schönfinkel ^{[ 1 ]}และHaskell Curry [ ^{2 ]}และเมื่อไม่นานมานี้ได้ถูกนำมาใช้ในวิทยาศาสตร์คอมพิวเตอร์ในฐานะแบบจำลองเชิงทฤษฎีของการคำนวณและยังเป็นพื้นฐานสำหรับการออกแบบ^ภาษาการเขียนโปรแกรมเชิงฟังก์ชัน อีกด้วย ตรรกะเชิงการจัดเรียง นี้อิงตามcombinator ซึ่ง Schönfinkelได้แนะนำในปี 1920 ด้วยแนวคิดที่จะให้วิธีการที่คล้ายคลึงกันในการสร้างฟังก์ชัน — และเพื่อขจัดการกล่าวถึงตัวแปรใดๆ — โดยเฉพาะอย่างยิ่งในตรรกะเชิงภาคแสดง combinator คือฟังก์ชันลำดับสูงที่ใช้เพียงการประยุกต์ใช้ฟังก์ชันและ combinator ที่กำหนดไว้ก่อนหน้านี้เพื่อกำหนดผลลัพธ์จากอาร์กิวเมนต์

ตรรกศาสตร์เชิงผสม (Combinatory logic) เดิมทีมีจุดประสงค์เพื่อเป็น 'ตรรกศาสตร์เบื้องต้น' ที่จะช่วยชี้แจงบทบาทของตัวแปรเชิงปริมาณในตรรกศาสตร์ โดยหลักแล้วคือการกำจัดตัวแปรเหล่านั้นออกไป อีกวิธีหนึ่งในการกำจัดตัวแปรเชิงปริมาณคือตรรกศาสตร์ฟังก์ชันภาคแสดงของควิน (Quine's predicate functor logic) ในขณะที่พลังการแสดงออกของตรรกศาสตร์เชิงผสมมักจะเหนือกว่าตรรกศาสตร์ลำดับที่หนึ่งแต่พลังการแสดงออกของตรรกศาสตร์ฟังก์ชันภาคแสดงนั้นเท่ากับตรรกศาสตร์ลำดับที่หนึ่ง ( Quine 1960, 1966, 1976 )

โมเสส เชินฟิงเคิลผู้คิดค้นตรรกะเชิงการจัดเรียง ไม่ได้ตีพิมพ์ผลงานใดๆ เกี่ยวกับตรรกะเชิงการจัดเรียงหลังจากบทความฉบับแรกของเขาในปี 1924 แฮสเคล เคอร์รีค้นพบตัวจัดเรียงอีกครั้งในขณะที่ทำงานเป็นอาจารย์ที่มหาวิทยาลัยพรินซ์ตันในช่วงปลายปี 1927 ^{[ 3 ]}ในช่วงปลายทศวรรษ 1930 อลอนโซ เชิร์ชและนักศึกษาของเขาที่พรินซ์ตันได้คิดค้นรูปแบบที่เป็นคู่แข่งสำหรับการนามธรรมเชิงฟังก์ชัน นั่นคือแคลคูลัสแลมบ์ดาซึ่งได้รับความนิยมมากกว่าตรรกะเชิงการจัดเรียง ผลพวงจากเหตุการณ์ทางประวัติศาสตร์เหล่านี้คือ จนกระทั่งวิทยาศาสตร์คอมพิวเตอร์เชิงทฤษฎีเริ่มให้ความสนใจในตรรกะเชิงการจัดเรียงในช่วงทศวรรษ 1960 และ 1970 งานเกือบทั้งหมดในหัวข้อนี้จึงเป็นผลงานของแฮสเคล เคอร์รีและนักศึกษาของเขา หรือโดยโรเบิร์ต เฟย์สในเบลเยียมเคอร์รีและเฟย์ส (1958) และเคอร์รีและคณะ (1972) ได้สำรวจประวัติศาสตร์ช่วงต้นของตรรกะเชิงการจัดเรียง สำหรับการพิจารณาตรรกะเชิงผสมและแคลคูลัสแลมบ์ดาแบบสมัยใหม่มากขึ้น โปรดดูหนังสือของBarendregt [ ^{4 ]}ซึ่งทบทวนแบบจำลอง^ที่ Dana Scottคิดค้นขึ้นสำหรับตรรกะเชิงผสมในช่วงทศวรรษ 1960 และ 1970

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

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

ตรรกะเชิงการจัดเรียงสามารถตีความได้หลากหลาย บทความในช่วงแรกๆ ของ Curry แสดงให้เห็นวิธีการแปลเซตสัจพจน์สำหรับตรรกะทั่วไปเป็นสมการตรรกะเชิงการจัดเรียง^{[ 5 ]} Dana Scottในช่วงทศวรรษ 1960 และ 1970 แสดงให้เห็นวิธีการผสานทฤษฎีแบบจำลองและตรรกะเชิงการจัดเรียง

แคลคูลัสแลมบ์ดาเกี่ยวข้องกับวัตถุที่เรียกว่าเทอมแลมบ์ดาซึ่งสามารถแทนด้วยสตริงสามรูปแบบต่อไปนี้:

• ${\displaystyle v}$
• ${\displaystyle \lambda v.E_{1}}$
• ${\displaystyle (E_{1}E_{2})}$

โดยที่เป็นชื่อตัวแปรที่ถูกดึงมาจากเซตของชื่อตัวแปรที่กำหนดไว้ล่วงหน้าซึ่งไม่มีที่สิ้นสุด และและเป็นเทอมแลมบ์ดา ${\displaystyle v}$${\displaystyle E_{1}}$${\displaystyle E_{2}}$

เทอมในรูปแบบนี้เรียกว่านามธรรมตัวแปรเรียกว่าพารามิเตอร์เชิงรูปธรรมของนามธรรม และคือส่วนเนื้อหาของนามธรรม เทอมแทนฟังก์ชัน ซึ่งเมื่อนำไปใช้กับอาร์กิวเมนต์ จะผูกพารามิเตอร์เชิงรูปธรรมเข้ากับอาร์กิวเมนต์ แล้วคำนวณค่าผลลัพธ์ของ— กล่าวคือ จะคืนค่าโดยที่ทุกๆ การปรากฏของจะถูกแทนที่ด้วยอาร์กิวเมนต์ ${\displaystyle \lambda v.E_{1}}$${\displaystyle v}$${\displaystyle E_{1}}$${\displaystyle \lambda v.E_{1}}$${\displaystyle v}$${\displaystyle E_{1}}$${\displaystyle E_{1}}$${\displaystyle v}$

เทอมในรูปแบบนี้เรียกว่าแอปพลิเคชันแอปพลิเคชันจำลองการเรียกใช้หรือการดำเนินการของฟังก์ชัน: ฟังก์ชันที่แสดงโดยจะถูกเรียกใช้ โดยมีเป็นอาร์กิวเมนต์ และผลลัพธ์จะถูกคำนวณ หาก(บางครั้งเรียกว่า ตัวถูกเรียก ใช้ ) เป็นนามธรรม เทอม อาจถูกลด รูปได้ : อาร์กิวเมนต์ อาจถูกแทนที่ในส่วนเนื้อหาของแทนที่พารามิเตอร์อย่างเป็นทางการของและผลลัพธ์คือเทอมแลมบ์ดาใหม่ซึ่งเทียบเท่ากับเทอมเดิม หากเทอมแลมบ์ดาไม่มีเทอมย่อยในรูปแบบแสดงว่าไม่สามารถลดรูปได้ และอยู่ใน รูป แบบ ปกติ${\displaystyle E_{1}E_{2}}$${\displaystyle E_{1}}$${\displaystyle E_{2}}$${\displaystyle E_{1}}$${\displaystyle E_{2}}$${\displaystyle E_{1}}$${\displaystyle E_{1}}$${\displaystyle ((\lambda v.E_{1})E_{2})}$

นิพจน์นี้แสดงถึงผลลัพธ์ของการนำเทอมนั้นมาแทนที่ทุกตำแหน่งที่ปรากฏโดยอิสระด้วยดังนั้นเราจึงเขียนได้ว่า ${\displaystyle E[v:=a]}$${\displaystyle E}$${\displaystyle v}$${\displaystyle a}$

${\displaystyle ((\lambda vE)a)\Rightarrow E[v:=a]}$

ตามธรรมเนียม เราใช้คำย่อสำหรับ(เช่น การใช้งานเป็นแบบเชื่อมโยงทางซ้าย ) ${\displaystyle (abc)}$${\displaystyle ((ab)c)}$

แรงจูงใจเบื้องหลังนิยามของการลดรูปนี้คือ มันสามารถจับเอาพฤติกรรมที่สำคัญของฟังก์ชันทางคณิตศาสตร์ทั้งหมดมาไว้ได้ ตัวอย่างเช่น ลองพิจารณาฟังก์ชันที่คำนวณกำลังสองของจำนวนหนึ่ง เราอาจเขียนได้ว่า ...

กำลังสองของคือ${\displaystyle x}$${\displaystyle x*x}$

(ใช้ " " เพื่อแสดงการคูณ) นี่คือพารามิเตอร์อย่างเป็นทางการของฟังก์ชัน ในการประเมินค่ากำลังสองสำหรับค่าอาร์กิวเมนต์เฉพาะ เช่น 3 เราจะแทรกค่าดังกล่าวเข้าไปในนิยามแทนที่พารามิเตอร์อย่างเป็นทางการ: ${\displaystyle *}$${\displaystyle x}$

กำลังสองของคือ${\displaystyle 3}$${\displaystyle 3*3}$

ในการประเมินนิพจน์ที่ได้เราจะต้องใช้ความรู้เกี่ยวกับการคูณและเลข 3 เนื่องจากการคำนวณใดๆ ก็ตามเป็นเพียงการประกอบกันของการประเมินฟังก์ชันที่เหมาะสมบนอาร์กิวเมนต์พื้นฐานที่เหมาะสม หลักการแทนที่อย่างง่ายนี้จึงเพียงพอที่จะจับกลไกสำคัญของการคำนวณได้ ยิ่งไปกว่านั้น ในแคลคูลัสแลมบ์ดา แนวคิดต่างๆ เช่น '3' และ ' ' สามารถแสดงได้โดยไม่จำเป็นต้องใช้ตัวดำเนินการพื้นฐานหรือค่าคงที่ที่กำหนดจากภายนอก เป็นไปได้ที่จะระบุเทอมในแคลคูลัสแลมบ์ดา ซึ่งเมื่อตีความอย่างเหมาะสมแล้ว จะมีพฤติกรรมเหมือนเลข 3 และเหมือนตัวดำเนินการคูณ ดูการเข้ารหัสของเชิร์ช ${\displaystyle 3*3}$${\displaystyle *}$

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

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

เนื่องจากการสร้างฟังก์ชันด้วยนามธรรมเป็นวิธีเดียวในแคลคูลัสแลมบ์ดา ดังนั้นจึงต้องมีสิ่งอื่นมาแทนที่ในแคลคูลัสเชิงผสม แทนที่จะใช้การสร้างฟังก์ชันด้วยนามธรรม แคลคูลัสเชิงผสมจึงเสนอชุดฟังก์ชันพื้นฐานจำนวนจำกัด ซึ่งสามารถใช้สร้างฟังก์ชันอื่นๆ ได้

คำศัพท์เชิงผสมมีรูปแบบใดรูปแบบหนึ่งดังต่อไปนี้:

ไวยากรณ์	ชื่อ	คำอธิบาย
${\displaystyle x}$	ตัวแปร	อักขระหรือสตริงที่แทนพจน์เชิงการจัดเรียง
${\displaystyle P}$	ฟังก์ชันพื้นฐาน	หนึ่งในสัญลักษณ์ตัวรวม, , . ${\displaystyle I}$${\displaystyle K}$${\displaystyle S}$
${\displaystyle (MN)}$	แอปพลิเคชัน	การนำฟังก์ชันไปใช้กับอาร์กิวเมนต์และเป็นคำศัพท์เชิงการจัดเรียง ${\displaystyle M}$${\displaystyle N}$

ฟังก์ชันพื้นฐานคือคอมบินาเตอร์หรือฟังก์ชันที่เมื่อมองในรูปของเทอมแลมบ์ดา จะไม่มีตัวแปร อิสระ

เพื่อลดความซับซ้อนของสัญลักษณ์ โดยทั่วไปแล้วจะใช้สัญลักษณ์หรือ แทน เทอม ซึ่งเป็น ธรรมเนียมทั่วไปเดียวกัน (การเชื่อมโยงทางซ้าย) กับการประยุกต์หลายครั้งในแคลคูลัสแลมบ์ดา ${\displaystyle (E_{1}E_{2}E_{3}...E_{n})}$${\displaystyle E_{1}E_{2}E_{3}...E_{n}}$${\displaystyle (...((E_{1}E_{2})E_{3})...E_{n})}$

ในตรรกศาสตร์เชิงการจัดเรียง (combinatory logic) ตัวจัดเรียงพื้นฐานแต่ละตัวจะมีกฎการลดรูปในรูปแบบ

${\displaystyle (P\ x_{1}\dots x_{n})=E}$

โดยที่เป็นคำที่กล่าวถึงเฉพาะตัวแปรจากเซตเท่านั้นด้วยวิธีนี้ ตัวรวมเชิงดั้งเดิมจึงทำงานเหมือนฟังก์ชัน ${\displaystyle E}$${\displaystyle \{x_{1}\dots x_{n}\}}$

ตัวอย่างที่ง่ายที่สุดของคอมบินาเตอร์คือคอมบินาเตอร์เอกลักษณ์ ซึ่งกำหนดโดย ${\displaystyle I}$

${\displaystyle (I\ x)=x}$

สำหรับทุกเงื่อนไขตัวรวมฟังก์ชันแบบง่ายอีกตัวหนึ่งคือซึ่งสร้างฟังก์ชันคงที่: คือฟังก์ชันที่สำหรับอาร์กิวเมนต์ใดๆ จะส่งคืนค่าดังนั้นเราจึงกล่าวว่า ${\displaystyle x}$${\displaystyle K}$${\displaystyle (Kx)}$${\displaystyle x}$

${\displaystyle ((K\ x)\ y)=x}$

สำหรับเงื่อนไขทั้งหมดและหรือตามธรรมเนียมสำหรับการใช้งานหลายครั้ง ${\displaystyle x}$${\displaystyle y}$

${\displaystyle (K\ x\ y)=x}$

ตัวรวมฟังก์ชันตัวที่สามคือซึ่งเป็นเวอร์ชันทั่วไปของแอปพลิเคชัน: ${\displaystyle S}$

${\displaystyle (S\ x\ y\ z)=(x\ z\ (y\ z))}$

${\displaystyle S}$ใช้ได้หลังจากแทนที่ลงในแต่ละส่วนแล้ว หรือกล่าวอีกนัยหนึ่งคือ ใช้ได้ภายในสภาพแวดล้อมนั้น ${\displaystyle x}$${\displaystyle y}$${\displaystyle z}$${\displaystyle x}$${\displaystyle y}$${\displaystyle z}$

เมื่อกำหนดและแล้วสิ่งนั้นจึงไม่จำเป็น เนื่องจากสามารถสร้างขึ้นจากอีกสองสิ่งได้: ${\displaystyle S}$${\displaystyle K}$${\displaystyle I}$

${\displaystyle ((S\,K\,K)\,x)}$

${\displaystyle =(S\,K\,K)\,x}$

${\displaystyle =K\,x\,(K\,x)}$

${\displaystyle =x}$

สำหรับเทอมใดๆ ก็ตามโปรดทราบว่าถึงแม้สำหรับเทอมใดๆก็ตาม ตัวมันเองไม่เท่ากับเรากล่าวว่าเทอมเหล่านั้นเท่ากันในเชิงขยาย (extensionally equality) ความเท่ากันในเชิงขยายแสดงถึงแนวคิดทางคณิตศาสตร์ของความเท่ากันของฟังก์ชัน กล่าวคือ ฟังก์ชันสองฟังก์ชันจะถือว่าเท่ากันก็ต่อเมื่อฟังก์ชันเหล่านั้นให้ผลลัพธ์เดียวกันเสมอสำหรับอาร์กิวเมนต์เดียวกัน ในทางตรงกันข้าม เทอมเหล่านั้นเอง ร่วมกับการลดรูปของตัวรวมแบบดั้งเดิม (primitive combinators) แสดงถึงแนวคิดของ ความเท่ากันในเชิงเจตนา (intensional equality)ของฟังก์ชัน กล่าวคือ ฟังก์ชันสองฟังก์ชันจะถือว่าเท่ากันก็ต่อเมื่อมีการใช้งานที่เหมือนกันจนถึงการขยายของตัวรวมแบบดั้งเดิม มีหลายวิธีในการใช้งานฟังก์ชันเอกลักษณ์และก็เป็นหนึ่งในวิธีเหล่านั้นก็เป็นอีกวิธีหนึ่ง เราจะใช้คำว่าเทียบเท่าเพื่อหมายถึงความเท่ากันในเชิงขยาย ${\displaystyle x}$${\displaystyle ((S\,K\,K)\,x)=(Ix)}$${\displaystyle x}$${\displaystyle (S\,K\,K)}$${\displaystyle I}$${\displaystyle (S\,K\,K)}$${\displaystyle I}$${\displaystyle (S\,K\,S)}$

ตัวรวมฟังก์ชันที่น่าสนใจกว่าคือตัวรวมฟังก์ชันจุดคงที่หรือตัวรวมฟังก์ชันที่สามารถใช้ในการสร้างการเรียกซ้ำได้ ${\displaystyle Y}$

SและKสามารถนำมาประกอบกันเพื่อสร้างคอมบินาเตอร์ที่เท่ากับ เทอมแลมบ์ดา ใดๆ ในเชิงขยาย และด้วยเหตุนี้ ตามทฤษฎีบทของเชิร์ช จึงเท่ากับฟังก์ชันที่คำนวณได้ ใดๆ ก็ตาม การพิสูจน์คือการนำเสนอการแปลงT [ ]ซึ่งแปลงเทอมแลมบ์ดาใดๆ ให้เป็นคอมบินาเตอร์ที่เทียบเท่ากัน

T [ ]อาจถูกกำหนดได้ดังนี้:

1. T [ x ] ⇒ x
2. T [( E ₁ E ₂ )] ⇒ ( T [ E ₁ ] T [ E ₂ ])
3. T [ λx . E ] ⇒ ( K T [ E ]) (ถ้า xไม่ปรากฏอย่างอิสระใน E )
4. T [ λx . x ] ⇒ I
5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (ถ้า xปรากฏอย่างอิสระใน E )
6. T [ λx .( E ₁ E ₂ )] ⇒ ( S T [ λx . E ₁ ] T [ λx . E ₂ ]) (ถ้า xปรากฏอย่างอิสระใน E ₁หรือ E ₂ )

โปรดทราบว่าT [ ] ที่กำหนดมานั้นไม่ใช่ฟังก์ชันทางคณิตศาสตร์ที่มีประเภทที่ดี แต่เป็นตัวเขียนเทอมใหม่: แม้ว่าในที่สุดจะให้ผลลัพธ์เป็นตัวรวม แต่การแปลงอาจสร้างนิพจน์ตัวกลางที่ไม่ใช่ทั้งเทอมแลมบ์ดาหรือตัวรวม ตามกฎ (5)

กระบวนการนี้เรียกอีกอย่างว่าการกำจัดนามธรรม (abstraction elimination ) คำจำกัดความนี้ครอบคลุมทุกด้าน: นิพจน์แลมบ์ดาใดๆ จะอยู่ภายใต้กฎเหล่านี้เพียงข้อเดียวเท่านั้น (ดูสรุปแคลคูลัสแลมบ์ดาด้านบน)

เกี่ยวข้องกับกระบวนการนามธรรมวงเล็บซึ่งใช้การแสดงออกEที่สร้างขึ้นจากตัวแปรและการประยุกต์ใช้ และสร้างการแสดงออกตัวรวม [x]E ซึ่งตัวแปร x ไม่เป็นอิสระ โดยที่ [ x ] E x = Eเป็นจริง อัลกอริทึมที่ง่ายมากสำหรับนามธรรมวงเล็บถูกกำหนดโดยการเหนี่ยวนำบนโครงสร้างของการแสดงออกดังต่อไปนี้: ^{[ 6 ]}

1. [ x ] y  := K y
2. [ x ] x  := I
3. [ x ]( จ₁ จ₂ ) := ส ([ x ] จ₁ )([ x ] จ₂ )

การสร้างนามธรรมของวงเล็บทำให้เกิดการแปลงจากเทอมแลมบ์ดาไปเป็นนิพจน์ตัวรวม โดยการตีความนามธรรมของแลมบ์ดาโดยใช้อัลกอริทึมการสร้างนามธรรมของวงเล็บ

ตัวอย่างเช่น เราจะแปลงเทอมแลมบ์ดาλx . λy .( y x ) ให้เป็นเทอมเชิงการจัดเรียง:

T [ λx . λy .( y x )]

= T [ λx . T [ λy .( y x )]] (โดย 5)

= T [ λx .( S T [ λy . y ] T [ λy . x ])] (by 6)

= T [ λx .( SI T [ λy . x ])] (by 4)

= T [ λx .( SI ( K T [ x ]))] (by 3)

= T [ λx .( SI ( K x ))] (by 1)

= ( S T [ λx .( SI )] T [ λx .( K x )]) (by 6)

= ( S ( K ( SI )) T [ λx .( K x )]) (by 3)

= ( S ( K ( SI )) ( S T [ λx . K ] T [ λx . x ])) (by 6)

= ( S ( K ( SI )) ( S ( KK ) T [ λx . x ])) (by 3)

= ( S ( K ( SI )) ( S ( KK ) I )) (โดย 4)

ถ้าเราใช้เทอมเชิงการจัดเรียงนี้กับเทอมใดๆ สองเทอมxและy (โดยป้อนเทอมเหล่านั้นในลักษณะคล้ายคิวเข้าไปในตัวจัดเรียง 'จากด้านขวา') มันจะลดรูปได้ดังนี้:

( ส ( K ( S ฉัน )) ( ส ( KK ) ฉัน ) xy)

= ( K ( S I ) x ( S ( K K ) I x) y)

= ( S I ( S ( K K ) I x) y)

= ( I y ( S ( K K ) I xy))

= (y ( S ( K K ) I xy))

= (y ( K K x ( I x) y))

= (y ( K ( I x) y))

= (y ( I x))

= (yx)

การแสดงเชิงการจัดเรียง ( S ( K ( SI )) ( S ( KK ) I )) นั้นยาวกว่าการแสดงเป็นเทอมแลมบ์ดาλx . λy .(yx) มาก ซึ่งเป็นเรื่องปกติ โดยทั่วไปแล้ว การสร้าง T [ ] อาจขยายเทอมแลมบ์ดาที่มีความยาวnไปเป็นเทอมเชิงการจัดเรียงที่มีความยาวΘ ( n ³ ) ^{[ 7 ]}

การ แปลง T [ ] ได้รับแรงบันดาลใจจากความปรารถนาที่จะกำจัดนามธรรม กรณีพิเศษสองกรณี กฎ 3 และ 4 เป็นเรื่องเล็กน้อย: λx . xเทียบเท่ากับI อย่างชัดเจน และλx . Eเทียบเท่ากับ ( K T [ E ]) อย่างชัดเจน หากxไม่ปรากฏเป็นอิสระใน E

กฎสองข้อแรกก็ง่ายเช่นกัน: ตัวแปรจะแปลงเป็นตัวมันเอง และการประยุกต์ใช้ ซึ่งได้รับอนุญาตในแง่ของการจัดเรียง จะถูกแปลงเป็นตัวจัดเรียงโดยการแปลงตัวถูกประยุกต์และอาร์กิวเมนต์ให้เป็นตัวจัดเรียง

กฎข้อที่ 5 และ 6 เป็นสิ่งที่น่าสนใจ กฎข้อที่ 5 กล่าวอย่างง่ายๆ ว่า ในการแปลงนามธรรมที่ซับซ้อนให้เป็นคอมบินาเตอร์ เราต้องแปลงส่วนเนื้อหาของนามธรรมนั้นให้เป็นคอมบินาเตอร์ก่อน แล้วจึงกำจัดนามธรรมนั้นออกไป ส่วนกฎข้อที่ 6 นั้นกำจัดนามธรรมนั้นออกไปจริงๆ

λx .( E ₁ E ₂ ) เป็นฟังก์ชันที่รับอาร์กิวเมนต์ เช่นaและแทนที่ a ในเทอมแลมบ์ดา ( E ₁ E ₂ ) แทนที่xทำให้ได้ ( E ₁ E ₂ )[ x  : = a ] แต่การแทนที่aใน ( E ₁ E ₂ ) แทนที่xก็เหมือนกับการแทนที่ a ทั้งในE ₁และE ₂ดังนั้น

( จ₁ จ₂ )[ x  := ก ] = ( จ₁ [ x  := ก ] จ₂ [ x  := ก ])

( ladx .( E ₁ E ₂ ) a ) = (( ladx . E ₁ a ) ( ladx . E ₂ a ))

= ( S λx . E ₁ λx . E ₂ a )

= (( S λx . E ₁ λx . E ₂ ) a )

โดยความเท่าเทียมกันเชิงขยาย

แลมบ์ดา .( จ₁ จ₂ ) = ( สแลมx . จ₁ แลมx . จ₂ )

ดังนั้น เพื่อหาคอมบินาเตอร์ที่เทียบเท่ากับλx .( E ₁ E ₂ ) จึงเพียงพอที่จะหาคอมบินาเตอร์ที่เทียบเท่ากับ ( S λx . E ₁ λx . E ₂ ) และ

( S T [ λx . E ₁ ] T [ λx . E ₂ ])

เห็นได้ชัดว่าตรงตามเงื่อนไข E ₁และE ₂แต่ละอันมีจำนวนการใช้งานน้อยกว่า ( E ₁ E ₂ ) อย่างเคร่งครัด ดังนั้นการเรียกซ้ำจะต้องสิ้นสุดลงที่เทอมแลมบ์ดาที่ไม่มีการใช้งานเลย ไม่ว่าจะเป็นตัวแปรหรือเทอมในรูปแบบλx . E .

ตัวรวมที่สร้างขึ้นโดย การแปลง T [ ] สามารถทำให้เล็กลงได้หากเราคำนึงถึง กฎ การลด η :

T [ λx .( E x )] = T [ E ] (ถ้าxไม่เป็นอิสระในE )

λx .( E x) คือฟังก์ชันที่รับอาร์กิวเมนต์xและนำฟังก์ชันEไปใช้กับอาร์กิวเมนต์นั้น ซึ่งในเชิงขยายแล้ว ฟังก์ชันนี้เท่ากับฟังก์ชันEเอง ดังนั้นจึงเพียงพอที่จะแปลงEให้อยู่ในรูปแบบเชิงการจัดเรียง

เมื่อพิจารณาการลดรูปนี้ ตัวอย่างข้างต้นจึงกลายเป็น:

  T [ λx . λy .( y x )]

= ...

= ( S ( K ( SI )) T [ λx .( K x )])

= ( S ( K ( SI )) K ) (โดยการลด η)

ตัวเชื่อมนี้เทียบเท่ากับตัวเชื่อมที่ยาวกว่าก่อนหน้านี้:

  ( S ( K ( SI )) K x y )

= ( K ( SI ) x ( K x ) y )

= ( SI ( K x ) y )

= ( I y ( K x y ))

= ( y ( K x y ))

= ( yx )

ในทำนองเดียวกัน เวอร์ชันดั้งเดิมของ การแปลง T [ ] แปลงฟังก์ชันเอกลักษณ์λf . λx .( f x ) เป็น ( S ( S ( KS ) ( S ( KK ) I )) ( KI )) ด้วยกฎการลดรูป η λf . λx .( f x ) จะถูกแปลงเป็นI .

มีฐานจุดเดียวซึ่งตัวรวมทุกตัวสามารถประกอบกันได้โดยมีค่าเท่ากับ เทอมแลมบ์ดา ใดๆตัวอย่างง่ายๆ ของฐานดังกล่าวคือ { X } โดยที่:

X ≡ λx .((x S ) K )

ไม่ใช่เรื่องยากที่จะตรวจสอบว่า:

X ( X ( X X )) = ^β Kและ

X ( X ( X ( X X ))) = ^β S .

เนื่องจาก { K , S } เป็นฐาน ดังนั้น { X } ก็เป็นฐานด้วย เช่นกัน ภาษาโปรแกรม Iotaใช้Xเป็นตัวรวม (combinator) เพียงตัวเดียว

อีกหนึ่งตัวอย่างง่ายๆ ของฐานจุดเดียวคือ:

X' ≡ λx .(x K S K ) โดยที่

( X' X' ) X' = ^β Kและ

X' ( X' X' ) = ^β S

ฐานจุดเดียวที่ง่ายที่สุดเท่าที่ทราบคือการดัดแปลงเล็กน้อยของS :

S' ≡ λxλyλz . (xz) (y (λw. z))) with

S' ( S' S' ) ( S' ( S' S' ) S' S ' S ' S ' S' ) = ^β Kและ

S' ( S' ( S' S ' ( S' S' ( S' S' ))( S' ( S' ( S' S' ( S' S' )))))) S' S' = ^β S .

ในความเป็นจริง มีฐานดังกล่าวอยู่มากมายนับไม่ถ้วน^{[ 8 ]}

นอกจากSและKแล้วSchönfinkel (1924)ยังได้รวมตัวจัดเรียงสองตัวซึ่งปัจจุบันเรียกว่าBและCโดยมีการลดรูปดังต่อไปนี้:

( C f g x ) = (( f x ) g )

( B f g x ) = ( f ( g x ))

เขายังอธิบายเพิ่มเติมว่าสามารถแสดงสิ่งเหล่านี้ได้โดยใช้เพียงSและK เท่านั้น :

B = ( S ( KS ) K )

C = ( S ( S ( K ( S ( KS ) K )) S ) ( KK ))

ตัวรวมเหล่านี้มีประโยชน์อย่างยิ่งในการแปลงตรรกะเชิงประพจน์หรือแคลคูลัสแลมบ์ดาไปเป็นนิพจน์ตัวรวมCurry ก็เคยใช้ตัวรวมเหล่านี้เช่นกัน และต่อมาDavid Turner ก็ได้ใช้เช่นกัน โดย ชื่อของเขาเกี่ยวข้องกับการใช้งานทางด้านการคำนวณ โดยใช้ตัวรวมเหล่านี้ เราสามารถขยายกฎสำหรับการแปลงได้ดังนี้:

1. T [ x ] ⇒ x
2. T [( E ₁ E ₂ )] ⇒ ( T [ E ₁ ] T [ E ₂ ])
3. T [ λx . E ] ⇒ ( K T [ E ]) (ถ้า xไม่เป็นอิสระใน E )
4. T [ λx . x ] ⇒ I
5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (ถ้า xเป็นอิสระใน E )
6. T [ λx .( E ₁ E ₂ )] ⇒ ( S T [ λx . E ₁ ] T [ λx . E ₂ ]) (ถ้า xเป็นอิสระในทั้ง E ₁และ E ₂ )
7. T [ λx .( E ₁ E ₂ )] ⇒ ( C T [ λx . E ₁ ] T [ E ₂ ]) (ถ้า xเป็นอิสระใน E ₁แต่ไม่เป็น อิสระใน E ₂ )
8. T [ λx .( E ₁ E ₂ )] ⇒ ( B T [ E ₁ ] T [ λx . E ₂ ]) (ถ้า xเป็นอิสระใน E ₂แต่ไม่เป็น อิสระใน E ₁ )

เมื่อใช้ ตัวรวม BและCการแปลงของλx . λy .( y x ) จะมีลักษณะดังนี้:

  T [ λx . λy .( y x )]

= T [ λx . T [ λy .( y x )]]

= T [ λx .( C T [ λy . y ] x )] (ตามกฎข้อ 7)

= T [ λx .( C I x )]

= ( C I ) (การลด η)

${\displaystyle ={\mathsf {C}__{*}}$(สัญลักษณ์มาตรฐานแบบดั้งเดิม: )${\displaystyle {\mathsf {X}}_{*}={\mathsf {XI}}}$

${\displaystyle ={\mathsf {I}}'}$(สัญลักษณ์มาตรฐานแบบดั้งเดิม: )${\displaystyle {\mathsf {X}}'={\mathsf {CX}}}$

และแท้จริงแล้ว ( C I x y ) ลดรูปเป็น ( y x ):

  ( C I x y )

= ( I y x )

= ( y x )

แรงจูงใจในที่นี้คือBและCเป็นเวอร์ชันที่จำกัดของSโดยที่Sรับค่าและแทนที่ค่าดังกล่าวลงในทั้งตัวแปรที่ต้องการใช้และตัวแปรที่ต้องการหาค่าก่อนที่จะทำการประยุกต์ใช้ ในขณะที่C ทำการแทนที่เฉพาะในตัวแปรที่ต้องการใช้เท่านั้น และ Bทำการแทนที่เฉพาะในตัวแปรที่ต้องการหาค่าเท่านั้น

ชื่อเรียกสมัยใหม่ของคอมบินาเตอร์มาจากวิทยานิพนธ์ปริญญาเอกของHaskell Curry ในปี 1930 (ดู ระบบ B, C, K, W ) ในเอกสารต้นฉบับของ Schönfinkel สิ่งที่เราเรียกว่า S , K , I , BและC ในปัจจุบันนั้น เดิม เรียกว่าS , C , I , ZและTตามลำดับ

การลดขนาดของคอมบินาเตอร์ที่เกิดจากกฎการแปลงใหม่นั้น สามารถทำได้โดยไม่ต้องนำBและC มา ใช้ ดังที่แสดงไว้ในหัวข้อ 3.2 ของTromp (2008 )

ต้องแยกความแตกต่างระหว่างCL _Kที่อธิบายไว้ในบทความนี้กับ แคลคูลัส CL _Iความแตกต่างนี้สอดคล้องกับความแตกต่างระหว่างแคลคูลัส λ _Kและแคลคูลัส λ _Iซึ่งแตกต่างจากแคลคูลัส λ _K ตรงที่แคลคูลัส λ _Iจำกัดนามธรรมไว้เฉพาะ:

λx . Eโดยที่xมีการปรากฏอิสระอย่างน้อยหนึ่งครั้งในE .

ด้วยเหตุนี้ ตัวรวมKจึงไม่ปรากฏในแคลคูลัส λ _Iหรือใน แคลคูลัส CL _Iค่าคงที่ของCL _IคือI , B , CและSซึ่งเป็นฐานที่ สามารถนำมาประกอบกันเป็นเทอม CL _I ทั้งหมด ได้ (โดยคำนึงถึงความเท่าเทียมกัน) เทอม λ _I ทุก เทอมสามารถแปลงเป็นตัว รวม CL _I ที่เท่ากันในเชิง ขยายได้ตามกฎที่คล้ายคลึงกับกฎที่นำเสนอไว้ข้างต้นสำหรับการแปลงเทอม λ _Kเป็น ตัวรวม CL _Kดูบทที่ 9 ใน Barendregt (1984)

การแปลงL [ ] จากเทอมเชิงการจัดเรียงเป็นเทอมแลมบ์ดาเป็นเรื่องง่าย:

L [ I ] = λx . x

L [ K ] = λx . λy . x

L [ C ] = λx . λy . λz .( x z y )

L [ B ] = λx . λy . λz .( x ( y z ))

L [ S ] = λx . λy . λz .( x z ( y z ))

ลิตร [( จ₁ จ₂ )] = ( จ [ จ₁ ] จ [ จ₂ ])

อย่างไรก็ตาม โปรดทราบว่าการแปลงนี้ไม่ใช่การแปลงผกผันของT [ ] เวอร์ชันใดๆ ที่เราเคยเห็นมา

รูปแบบปกติ (Normal form)คือเทอมเชิงการจัดเรียง (combinatory term) ใดๆ ที่ตัวจัดเรียงดั้งเดิม (primitive combinators) ที่ปรากฏอยู่ (ถ้ามี) ไม่ได้ถูกนำไปใช้กับอาร์กิวเมนต์มากพอที่จะทำให้ง่ายขึ้น ไม่สามารถตัดสินได้ว่าเทอมเชิงการจัดเรียงทั่วไปมีรูปแบบปกติหรือไม่ หรือว่าเทอมเชิงการจัดเรียงสองเทอมนั้นเทียบเท่ากันหรือไม่ เป็นต้น สามารถแสดงให้เห็นได้ในทำนองเดียวกันกับปัญหาที่เกี่ยวข้องกับเทอมแลมบ์ดา (lambda terms)

ปัญหาที่ไม่สามารถตัดสินได้ข้างต้น (ความเท่าเทียมกัน การมีอยู่ของรูปแบบปกติ ฯลฯ) รับอินพุตเป็นตัวแทนทางไวยากรณ์ของคำศัพท์ภายใต้การเข้ารหัสที่เหมาะสม (เช่นการเข้ารหัสแบบ Church ) เราอาจพิจารณาแบบจำลองการคำนวณแบบง่ายๆ ที่เรา "คำนวณ" คุณสมบัติของคำศัพท์โดยใช้ตัวรวม (combinator) ที่นำไปใช้กับคำศัพท์เหล่านั้นโดยตรงในฐานะอาร์กิวเมนต์ แทนที่จะใช้กับตัวแทนทางไวยากรณ์ของคำศัพท์เหล่านั้น กล่าวคือ ให้述语( predicate ) เป็นตัวรวมที่เมื่อนำไปใช้แล้วจะส่งคืนค่าTหรือF (โดยที่TและFแทนการเข้ารหัสแบบ Church ทั่วไปของค่าจริงและเท็จλx . λy . xและλx . λy . yที่แปลงเป็นตรรกะเชิงรวม โดยเวอร์ชันเชิงรวมจะมีT = K และ F = ( K I ) ) 述语Nไม่เป็นค่าพื้นฐานหากมีอาร์กิวเมนต์สองตัวAและBที่N A = TและN B = F ตัวรวมNสมบูรณ์หากN Mมีรูปแบบปกติสำหรับทุกอาร์กิวเมนต์M ทฤษฎีบทของ Riceที่คล้ายกันสำหรับแบบจำลองของเล่นนี้กล่าวว่าภาคแสดงที่สมบูรณ์ทุกตัวเป็นภาคแสดงที่ไม่สำคัญ การพิสูจน์ทฤษฎีบทนี้ค่อนข้างง่าย^{[ 9 ]}

จากทฤษฎีบทเรื่องความไม่สามารถนิยามได้นี้ จึงสรุปได้ทันทีว่าไม่มี述语ที่สมบูรณ์ใดๆ ที่สามารถแยกแยะระหว่างคำที่มีรูปแบบปกติและคำที่ไม่มีรูปแบบปกติได้ นอกจากนี้ยังสรุปได้ว่าไม่มี述语ที่สมบูรณ์ใดๆ เช่น EQUAL ที่มีคุณสมบัติดังต่อไปนี้:

(เท่ากับAB ) = Tถ้าA = Bและ

( เท่ากับAB ) = Fถ้าA ≠ B

ถ้า EQUAL มีอยู่จริง สำหรับทุกA , λx. (EQUAL x A ) จะต้องเป็น述语ที่สมบูรณ์และไม่ใช่述语ธรรมดา

อย่างไรก็ตาม โปรดสังเกตว่าจากทฤษฎีบทเรื่องความไม่สามารถนิยามได้นี้ ยังแสดงให้เห็นโดยทันทีว่า คุณสมบัติหลายอย่างของคำศัพท์ที่เห็นได้ชัดว่าสามารถตัดสินได้นั้น ก็ไม่สามารถนิยามได้ด้วย述语ที่สมบูรณ์เช่นกัน ตัวอย่างเช่น ไม่มี述语ใดที่สามารถบอกได้ว่าตัวอักษรฟังก์ชันดั้งเดิมตัวแรกที่ปรากฏในคำศัพท์นั้นเป็นKหรือไม่ สิ่งนี้แสดงให้เห็นว่า การนิยามได้ด้วย述语นั้นไม่ใช่แบบจำลองที่สมเหตุสมผลของการตัดสินได้

เดวิด เทอร์เนอร์ ใช้คอมบินาเตอร์ของเขาในการสร้างภาษาโปรแกรม SASL

Kenneth E. Iversonใช้พรีมิทีฟที่อิงตามคอมบินาเตอร์ของ Curry ในภาษาการเขียนโปรแกรม J ของเขา ซึ่งเป็นภาษาที่สืบทอดมาจากAPLสิ่งนี้ทำให้สิ่งที่ Iverson เรียกว่าการเขียนโปรแกรมแบบแฝง (tacit programming) เป็นไปได้ นั่นคือ การเขียนโปรแกรมในนิพจน์เชิงฟังก์ชันที่ไม่มีตัวแปร พร้อมด้วยเครื่องมือที่มีประสิทธิภาพสำหรับการทำงานกับโปรแกรมดังกล่าว ปรากฏว่าการเขียนโปรแกรมแบบแฝงนั้นเป็นไปได้ในภาษาที่คล้ายกับ APL ใดๆ ที่มีตัวดำเนินการที่ผู้ใช้กำหนด^{[ 10 ]}

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

ตัว รวม KและSสอดคล้องกับสัจพจน์

AK : A → ( B → A ),

AS : ( A → ( B → C )) → (( A → B ) → ( A → C ))

และการประยุกต์ใช้ฟังก์ชันนั้นสอดคล้องกับกฎการแยก ( modus ponens )

MP : จากAและA → BอนุมานB

แคลคูลัสที่ประกอบด้วยAK , ASและMPนั้นสมบูรณ์สำหรับส่วนย่อยเชิงบ่งชี้ของตรรกะเชิงสัญชาตญาณ ซึ่งสามารถมองได้ดังต่อไปนี้ พิจารณาเซตWของเซตสูตรที่ปิดเชิงอนุมานทั้งหมด เรียงลำดับตามการรวมแล้ว จะเป็น เฟรม Kripkeเชิงสัญชาตญาณและเรากำหนดแบบจำลองในเฟรมนี้โดย ${\displaystyle \langle W,\subseteq \rangle }$${\displaystyle \Vdash }$

${\displaystyle X\Vdash A\iff A\in X.}$

นิยามนี้สอดคล้องกับเงื่อนไขความพึงพอใจของ →: ในด้านหนึ่ง ถ้าและเป็นเช่นนั้นและแล้วโดย modus ponens ในอีกด้านหนึ่ง ถ้าแล้วโดยทฤษฎีบทการหักล้างดังนั้น การปิดเชิงหักล้างของคือองค์ประกอบเช่นนั้น, , และ ${\displaystyle X\Vdash A\to B}$${\displaystyle Y\in W}$${\displaystyle Y\supseteq X}$${\displaystyle Y\Vdash A}$${\displaystyle Y\Vdash B}$${\displaystyle X\not \Vdash A\to B}$${\displaystyle X,A\not \vdash B}$${\displaystyle X\cup \{A\}}$${\displaystyle Y\in W}$${\displaystyle Y\supseteq X}$${\displaystyle Y\Vdash A}$${\displaystyle Y\not \Vdash B}$

ให้Aเป็นสูตรใดๆ ที่ไม่สามารถพิสูจน์ได้ในแคลคูลัส ดังนั้นAไม่เป็นส่วนหนึ่งของการปิดเชิงนิรนัยXของเซตว่างดังนั้นและAจึงไม่ถูกต้องตามสัญชาตญาณ ${\displaystyle X\not \Vdash A}$

• ระบบคอมพิวเตอร์ประยุกต์
• ระบบ B, C, K, W
• เครื่องจักรนามธรรมเชิงหมวดหมู่
• ไวยากรณ์เชิงหมวดหมู่แบบผสมผสาน
• การแทนที่แบบชัดเจน
• ตัวรวมจุดคงที่
• เครื่องลดกราฟ
• แคลคูลัสแลมบ์ดาและพีชคณิตทรงกระบอก แนวทางอื่นๆ ในการสร้างแบบจำลองการหาปริมาณและการกำจัดตัวแปร
• แคลคูลัสตัวรวม SKI
• ซูเปอร์คอมบินาเตอร์
• เพื่อเยาะเย้ยนกม็อกกิ้งเบิร์ด

• Barendregt, Hendrik Pieter (1984). แคลคูลัสแลมบ์ดา ไวยากรณ์และความหมายของมัน การศึกษาตรรกศาสตร์และรากฐานของคณิตศาสตร์เล่มที่ 103 สำนักพิมพ์นอร์ทฮอลแลนด์ ISBN 0-444-87508-5.
• บิมโบ, คาทาลิน (2012) ตรรกะเชิงผสม: บริสุทธิ์ ประยุกต์ และพิมพ์ไอเอสบีเอ็น 978-1-4398-0000-3.
• เชอร์ลิน, เอ็ดเวิร์ด (1991). "ฟังก์ชันบริสุทธิ์ใน APL และ J". รายงานการประชุมนานาชาติเกี่ยวกับ APL '91 - APL '91 . หน้า  88–93 . doi : 10.1145/114054.114065 . ISBN 0897914414. S2CID  25802202 .
• Curry, Haskell Brooks (1930). "Grundlagen der Kombinatorischen Logik" [รากฐานของตรรกะเชิงการจัดเรียง]. American Journal of Mathematics (ในภาษาเยอรมัน). 52 (3). สำนักพิมพ์มหาวิทยาลัยจอห์นส์ฮอปกินส์: 509– 536. doi : 10.2307/2370619 . JSTOR  2370619 .
• Curry, Haskell Brooks ; Feys, Robert (1958). ตรรกศาสตร์เชิงผสม . เล่ม 1. อัมสเตอร์ดัม: North Holland. ISBN 0-7204-2208-6.{{cite book}}: ISBN / Date incompatibility (help)
• Curry, Haskell Brooks ; Hindley, J. Roger ; Seldin, Jonathan P. (1972). ตรรกศาสตร์เชิงผสม . เล่ม 2. อัมสเตอร์ดัม: North Holland. ISBN 0-7204-2208-6.
• เอนเกเลอร์ อี. (1995) โปรแกรมผสมผสาน (PDF) . บีร์เควเซอร์. หน้า  5–6 .
• ฟิลด์, แอนโทนี เจ.; แฮร์ริสัน, ปีเตอร์ จี. (1998). การเขียนโปรแกรมเชิงฟังก์ชัน . แอดดิสัน-เวสลีย์. ISBN 0-201-19249-7.
• Goldberg, Mayer (2004). "การสร้างฐานจุดเดียวในแคลคูลัสแลมบ์ดาแบบขยาย" Information Processing Letters . 89 (6): 281– 286. doi : 10.1016/j.ipl.2003.12.005 .
• Hindley, J. Roger ; Meredith, David (1990). "Principal type-schemes and condensed detachment" . Journal of Symbolic Logic . 55 (1): 90– 105. doi : 10.2307/2274956 . JSTOR  2274956 . MR  1043546 . S2CID  6930576 .
• Hindley, J. Roger ; Seldin, Jonathan P. (2008) [1986]. แคลคูลัสแลมบ์ดาและตัวรวม: บทนำ (ฉบับที่ 2). สำนักพิมพ์มหาวิทยาลัยเคมบริดจ์ . ISBN 9780521898850.
• Lachowski, Łukasz (2018). " เกี่ยวกับความซับซ้อนของการแปลมาตรฐานของแคลคูลัสแลมบ์ดาเป็นตรรกะเชิงผสม"รายงานเกี่ยวกับตรรกะทางคณิตศาสตร์ 2018 ( 53): 19– 42. doi : 10.4467/20842589RM.18.002.8835สืบค้นเมื่อ9 กันยายน 2018
• Paulson, Lawrence C. (1995). พื้นฐานของการเขียนโปรแกรมเชิงฟังก์ชัน . มหาวิทยาลัยเคมบริดจ์.
• Quine, Willard Van Orman (1960). "Variables explained away". Proceedings of the American Philosophical Society . 104 (3): 343– 347. JSTOR  985250 . พิมพ์ซ้ำเป็นบทที่ 23 ของQuine (1996)
• Quine, Willard Van Orman (1996) [1960]. "Variables explained away". Selected Logic Papers (Enl. ed., 2. print ed.). Cambridge, Mass.: Harvard University Press . pp.  227– 235. ISBN 9780674798373.
• เชินฟินเคิล, โมเสส (1924) "Über die Bausteine ​​der mathematischen Logik" (PDF ) Mathematische Annalen (ภาษาเยอรมัน) 92 ( 3– 4): 305– 316. ดอย : 10.1007/bf01448013 . S2CID  118507515 . บทความที่ก่อตั้งตรรกะเชิงผสม แปลภาษาอังกฤษ: Schönfinkel (1967)
• เชินฟินเคิล, โมเสส (1967) [1924]. ฟาน ไฮเยนูร์ต, ฌอง (บรรณาธิการ). Über die Bausteine ​​der mathematischen Logik [ การสร้างตรรกะทางคณิตศาสตร์ ] จาก Frege ถึง Gödel: หนังสือที่มาในลอจิกคณิตศาสตร์ พ.ศ. 2422-2474 แปลโดย บาวเออร์-เมงเกลเบิร์ก, สเตฟาน เคมบริดจ์, แมสซาชูเซตส์, สหรัฐอเมริกา: สำนักพิมพ์มหาวิทยาลัยฮาร์วาร์ด . หน้า  355– 366 ไอเอสบีเอ็น 978-0674324497. OCLC  503886453 .
• เซลดิน, โจนาธาน พี. (3 มีนาคม 2551). "ตรรกะของแกงกะหรี่และเชิร์ช" (PDF) . สืบค้นเมื่อ17 กันยายน 2566 .
• สมุลลียัน, เรย์มอนด์ (1985). เพื่อล้อเลียนนกม็อกกิ้งเบิร์ดและปริศนาตรรกะอื่นๆ รวมถึงการผจญภัยอันน่าทึ่งในตรรกะเชิงผสม . นอปฟ์. ISBN 0-394-53491-3บทนำอย่างง่าย ๆ เกี่ยวกับตรรกศาสตร์เชิงการจัดเรียง นำเสนอในรูปแบบปริศนาเพื่อความ บันเทิงหลายชุด โดยใช้คำอุปมาเกี่ยวกับการดูนก
• Smullyan, Raymond (1994). การทำให้เป็นแนวทแยงและการอ้างอิงตนเองคู่มือตรรกศาสตร์อ็อกซ์ฟอร์ด เล่มที่ 27 อ็อกซ์ฟอร์ดและนิวยอร์ก: สำนักพิมพ์มหาวิทยาลัยอ็อกซ์ฟอร์ด ISBN 978-0198534501บทที่ 17–20 เป็นบทนำที่เป็นทางการมากขึ้นเกี่ยวกับตรรกศาสตร์เชิงการจัดเรียง โดยเน้นเป็นพิเศษที่ผลลัพธ์ของจุดตรึง
• Sørensen, Morten Heine B; Urzyczyn, Paweł (2006) [1999]. การบรรยายเรื่องไอโซมอร์ฟิซึมของ Curry–Howard (PDF)การศึกษาตรรกศาสตร์และรากฐานของคณิตศาสตร์ เล่มที่ 149 (ฉบับพิมพ์ครั้งที่ 1) Elsevierหน้า 442 ISBN 978-0444520777เก็บถาวรจากต้นฉบับ(PDF)เมื่อวันที่ 16 ตุลาคม 2548 เรียกดูเมื่อวันที่ 22 เมษายน 2560
• Tromp, John (2008). "แคลคูลัสแลมบ์ดาไบนารีและตรรกศาสตร์เชิงผสม" (PDF) . ใน Calude, Cristian S. (บรรณาธิการ). ความสุ่มและความซับซ้อน จากไลบ์นิซถึงไชติน . บริษัทสำนักพิมพ์วิทยาศาสตร์โลก. เก็บถาวรจากต้นฉบับ(PDF)เมื่อ 2016-03-04.
• Turner, David A. (1979). "อัลกอริทึมอีกแบบสำหรับการแยกวงเล็บ" วารสารตรรกศาสตร์เชิงสัญลักษณ์ 44 ( 2): 267– 270. doi : 10.2307/2273733 . JSTOR  2273733 . S2CID  35835482 .
• Wolfengagen, VE (2003). ตรรกะเชิงผสมในการเขียนโปรแกรม: การคำนวณด้วยวัตถุผ่านตัวอย่างและแบบฝึกหัด (ฉบับที่ 2). มอสโก: บริษัท "Center JurInfoR" จำกัด. ISBN 5-89158-101-9.
• วูลฟราม, สตีเฟน (2021). Combinators: มุมมองครบรอบร้อยปี . วูลฟราม มีเดีย . ISBN 978-1-57955-043-1เป็นการเฉลิมฉลองการพัฒนาตัวรวมสัญญาณ (combinator) ครบรอบหนึ่งร้อยปีหลังจากที่ Schönfinkel ได้คิดค้นขึ้น(1924)(อีบุ๊ก: ISBN) 978-1-57955-044-8)

• สารานุกรมปรัชญาแห่งสแตนฟอร์ด : " ตรรกศาสตร์เชิงการจัดเรียง " โดยKatalin Bimbó
• บันทึกย่อของเคอร์รีในช่วงปี ค.ศ. 1920–1931
• คีนาน, เดวิด ซี. (2001) " การผ่าตัดนกม็อกกิ้งเบิร์ด: สัญกรณ์กราฟิกสำหรับแคลคูลัสแลมบ์ดาพร้อมการลดรูปแอนิเมชัน "
• ราธแมน, คริส, " นกคอมบินาเตอร์ " ตารางที่กลั่นกรองสาระสำคัญส่วนใหญ่ของสมัลเลียน (1985)
• ตัวรวมฟังก์ชันแบบลากและวาง (แอปเพล็ต Java)
• แคลคูลัสแลมบ์ดาไบนารีและตรรกศาสตร์เชิงการจัดเรียง
• เว็บเซิร์ฟเวอร์ลดตรรกะเชิงผสม
• วูลฟราม, สตีเฟน (29 เมษายน 2020). คอมบินาเตอร์: ฉลองครบรอบ 100 ปี . โครงการฟิสิกส์วูลฟรามบนYouTube . สืบค้นเมื่อ26 กันยายน 2023 .