全國中小學科展

Imperative Programming程式碼與Functional Programming程式碼的等價性與其證明,使用Agda

科展類別

臺灣國際科展作品

屆次

2021年

科別

電腦科學與資訊工程

得獎情形

三等獎

學校名稱

國立臺灣師範大學附屬高級中學

指導老師

李柏翰

作者

陳立凡

關鍵字

程式語言、程式證明、函數式程式設計

摘要或動機

本研究主要考慮在盡量保留可讀性的情況下,找出將 Imperative Programming 程式碼對應的 Functional Programming 的程式碼並證明。 結果如下: 一、if statement 等價於由 ifte 函數所構成的程式碼,其中函數ifte定義在本文內 二、某些 for-loop statement 等價於由 foldl 函數所構成的程式碼 三、某些 for-loop statement 等價於由 map 函數所構成的程式碼

TISF2021-190035.pdf

Adobe Reader(Pdf)檔案