Templates and program extraction from proofs in higher order systems

เทมเพลตกับการสร้างโปรแกรมจากบทพิสูจน์ในระบบอันดับสูง

Name: Pimpen Vejjajiva

LCSH: Ordered sets

Abstract: Curry-Howard terms are typed-lambda terms, which are a way of representing formal proofs in a natural deduction system. The standard approach to extracting programs from proofs is by constructing Curry-Howard terms.In carrying out mathematical proofs, the same patterns frequently recur. Therefore in extracting programs from proofs it would be helpful to formally define what a pattern, or template, is and then add it into the system so that we do not have to repeat what is essentially the same argument. Moreover, this mirrors ordinary mathematical practice. In this research, we create a new system for extracting programs from proofs by extending Crossley and Shepherdson's system (in [3]) in the language of first-order predicate calculus to second-order logic and adding templates into the extended system as new rules. We introduce two kinds of templates: induction templates and abbreviation templates. The former templates allow us to use various kinds of induction in the formal system without going through the natural numbers. The latter templates enable us to abbreviate formulae by new predicates in formal proofs. The Curry-Howard terms produced in the new system still satisfy all the basic properties including the strong normalization theorem so we can extend the extraction of programs to the greatly expanded logical system.

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

Chulalongkorn University

Address: กรุงเทพมหานคร (Bangkok)

Email: cuir@car.chula.ac.th

Name: Mark Tamthai

Role: advisor

Name: Ajchara Hamchoowong

Role: advisor

Created: 2003

Issued: 2008-01-18

Modified: 2017-06-17

วิทยานิพนธ์/Thesis

ISBN: 9741735286

eng

DegreeName: Doctor of Philosophy

Level: Doctoral Degree

Descipline: Mathematics

Grantor: Chulalongkorn University

©copyrights Chulalongkorn University

ลำดับที่.	ชื่อแฟ้มข้อมูล	ขนาดแฟ้มข้อมูล	จำนวนเข้าถึง	วัน-เวลาเข้าถึงล่าสุด
1	Pimpen.pdf	1.1 MB	21	2019-08-20 21:08:27

ใช้เวลา

0.037428 วินาที