Chulalongkorn University Theses and Dissertations (Chula ETD)

Lambda-calculus with patterns

Other Title (Parallel Title in Other Language of ETD)

แคลคูลัสแลมบ์ดาที่มีแพทเทอร์น

Year (A.D.)

1997

Document Type

Thesis

First Advisor

Ajchara Harnchoowong

Second Advisor

Hall, Mark Edwin

Faculty/College

Graduate School (บัณฑิตวิทยาลัย)

Degree Name

Master of Science

Degree Level

Master's Degree

Degree Discipline

Mathematics

DOI

10.58837/CHULA.THE.1997.1257

Abstract

The original lambed-calculus can be used to represent a function, via a lambda-term, and to interpret the result of applying a function to an argument. However, there are some functions which cannot be represented by lambda-terms. By adding patterns, which will be used to specify the form of the argument accepted, and to extract subterms of the argument, and by modifying the definition of terms to allow a kind of "definition by cases" we can construct a new lambda-calculus. This new lambda-calculus can describe a larger class of functions, yet still satisfies all the basic properties of the original lambda-calculus, including the Church-Rosser theorem.

Other Abstract (Other language abstract of ETD)

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

Link to Full Text

Share

COinS