PLC: Homework 4 [100 points]Due date: Wednesday, April 3rd3 extra-credit points if you turn in by Tuesday, April 2ndAbout This HomeworkFor this homework, you will start learning Agda by writing some proofs. You will first install Agdaon your computer (optional if you instead use the CS Windows lab computers), and the Iowa AgdaLibrary.How to Turn In Your SolutionYou should create a hw4 subdirectory in your github.uiowa.edu repo. You will copy files fromsubdirectories of the hw4 directory in the course repo.Partners AllowedYou may work by yourself or with one partner (no more). See the instructions from hw1 for detailson how to submit your assignment if you work with a partner.How To Get HelpYou can post questions in the hw4 section on Piazza.You are also welcome to come to our office hours. See the course’s Google Calendar, linked fromthe Resources tab of the Resources page on Piazza, for the locations and times for office hours.11 ReadingRead Chapters 2, 3, and 4 of Verified Functional Programming in Agda, available for free (oncampus or VPN) here:https://dl.acm.org/citation.cfm?id=28413162 Installing AgdaAgda is installed on the CS Windows computers. You will probably want to install it also on yourown computer. For Windows, the easiest thing is to use our installer (which we have updated nowand it works):http://homepage.cs.uiowa.edu/~astump/agda/AgdaBundle_2.5.4.2.v4.msiOtherwise, try following the directions on the Agda wiki, here:http://wiki.portal.chalmers.se/agda/pmwiki.phpEssentially you first do cabal install Agda and then agda-mode setup (the latter probablyrequires that you add ~/.cabal/bin to your path). If you install Agda this way, you should getAgda version 2.5.4.2 (any version 2.5.4.x is ok).3 Installing the IALYou clone the repo here from github:https://github.com/cedille/ial4 Configuring and testing Agda and the IAL [20 points]Finally, you need to tell Agda how to find the Iowa Agda Library. If you are using a CS Windowsmachine, then open the file h:/.emacs. Otherwise, open ~/.emacs. Add the following text, whereinstead of the word PATH, you should have the path to your copy of the IAL (wherever you put it):(custom-set-variables(agda2-program-args (quote (--include-path=PATH))))That should be a single forward tick mark on the second line of that code (might render incorrectlyin this PDF). On Windows, I found I could put backslashes if I escaped them (double backslash),like this (where Myself is, of course, your actual Windows username):C:\Users\Myself\Documents\ialTo prove that all this is working for you, open bool.agda in the IAL and type Control-c Control-lto load the file with Agda. If this succeeds you should get syntax highlighting for the file. Now2take a screenshot called ial-screenshot.YYY, capturing your Emacs window with bool.agdahighlighted. (I found that for some reason, Agda often says “Another command is currently inprogress” when I do this, and I must first type Control-c Control-x Control-r to restart Agda, andthen do Control-c Control-l.)5 Boolean theorems [30 points]In bools.agda in the hw4 directory, you will find five lemmas to prove. When you load the file withControl-c Control-l, you will see holes on the right-hand sides of the definitions of those lemmas.Remove those holes (Control-k with your cursor right before the hole will cut it out), and fill thedefinitions in with proofs. [6 points each]6 Simple equational theorems [25 points]In simple.agda you will find five problems similar to ones we did in class March 14th (see thelecture notes). They are worth 5 points each.7 Theorems about list operations [25 points]In list-todo.agda you will find definitions of two functions space-every-other and swap-pairs.After these definitions there are five holes to fill in: four proofs and one condition (in the statementof nuke-all) that has to be selected so that the last theorem is provable. The condition should bechosen so that test at the very bottom of the file type-checks without yellow highlighting. Eachhole is worth five points.3本团队核心人员组成主要包括硅谷工程师、BAT一线工程师，精通德英语！我们主要业务范围是代做编程大作业、课程设计等等。我们的方向领域：window编程 数值算法 AI人工智能 金融统计 计量分析 大数据 网络编程 WEB编程 通讯编程 游戏编程多媒体linux 外挂编程 程序API图像处理 嵌入式/单片机 数据库编程 控制台 进程与线程 网络安全 汇编语言 硬件编程 软件设计 工程标准规等。其中代写编程、代写程序、代写留学生程序作业语言或工具包括但不限于以下范围:C/C++/C#代写Java代写IT代写Python代写辅导编程作业Matlab代写Haskell代写Processing代写Linux环境搭建Rust代写Data Structure Assginment 数据结构代写MIPS代写Machine Learning 作业 代写Oracle/SQL/PostgreSQL/Pig 数据库代写/代做/辅导Web开发、网站开发、网站作业ASP.NET网站开发Finance Insurace Statistics统计、回归、迭代Prolog代写Computer Computational method代做因为专业，所以值得信赖。如有需要，请加QQ：99515681 或邮箱：99515681@qq.com 微信：codehelp
网友评论