673 lines
72 KiB
HTML
673 lines
72 KiB
HTML
<!DOCTYPE html>
|
||
<html lang="en"><head>
|
||
<meta charset="utf-8">
|
||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1">
|
||
<title>Assignment3: TSPL Assignment 3 | Programming Language Foundations in Agda
|
||
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
|
||
<meta name="generator" content="Jekyll v3.9.0" />
|
||
<meta property="og:title" content="Assignment3: TSPL Assignment 3" />
|
||
<meta property="og:locale" content="en_US" />
|
||
<meta name="description" content="Programming Language Foundations in Agda" />
|
||
<meta property="og:description" content="Programming Language Foundations in Agda" />
|
||
<link rel="canonical" href="https://plfa.github.io/20.07/TSPL/2019/Assignment3/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/TSPL/2019/Assignment3/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/20.07/TSPL/2019/Assignment3/","headline":"Assignment3: TSPL Assignment 3","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
|
||
<!-- End Jekyll SEO tag -->
|
||
<link rel="stylesheet" href="/20.07/assets/main.css"></head>
|
||
<body><header class="site-header" role="banner">
|
||
|
||
<div class="wrapper">
|
||
|
||
<a class="site-title" href="/20.07/">Programming Language Foundations in Agda
|
||
</a>
|
||
|
||
<nav class="site-nav">
|
||
<span class="menu-icon">
|
||
<svg viewBox="0 0 18 15" width="18px" height="15px">
|
||
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
|
||
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
|
||
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
|
||
</svg>
|
||
</span>
|
||
|
||
<div class="trigger">
|
||
<a class="page-link" href="/20.07/">The Book</a>
|
||
<a class="page-link" href="/20.07/Announcements/">Announcements</a>
|
||
<a class="page-link" href="/20.07/GettingStarted/">Getting Started</a>
|
||
<a class="page-link" href="/20.07/Citing/">Citing</a>
|
||
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
|
||
</div>
|
||
</nav>
|
||
|
||
</div>
|
||
|
||
</header>
|
||
<main class="page-content" aria-label="Content">
|
||
<div class="wrapper">
|
||
<article class="post">
|
||
|
||
<header class="post-header">
|
||
<h1 class="post-title">Assignment3: TSPL Assignment 3</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/courses/tspl/2019/Assignment3.lagda.md">Source</a>
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<pre class="Agda"><a id="112" class="Keyword">module</a> <a id="119" href="/20.07/TSPL/2019/Assignment3/" class="Module">Assignment3</a> <a id="131" class="Keyword">where</a>
|
||
</pre>
|
||
<h2 id="your-name-and-email-goes-here">YOUR NAME AND EMAIL GOES HERE</h2>
|
||
|
||
<h2 id="introduction">Introduction</h2>
|
||
|
||
<p>You must do <em>all</em> the exercises labelled “(recommended)”.</p>
|
||
|
||
<p>Exercises labelled “(stretch)” are there to provide an extra challenge.
|
||
You don’t need to do all of these, but should attempt at least a few.</p>
|
||
|
||
<p>Exercises labelled “(practice)” are included for those who want extra practice.</p>
|
||
|
||
<p>Submit your homework using the “submit” command.
|
||
Please ensure your files execute correctly under Agda!</p>
|
||
|
||
<h2 id="good-scholarly-practice">Good Scholarly Practice.</h2>
|
||
|
||
<p>Please remember the University requirement as
|
||
regards all assessed work. Details about this can be found at:</p>
|
||
|
||
<blockquote>
|
||
<p><a href="http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct">http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct</a></p>
|
||
</blockquote>
|
||
|
||
<p>Furthermore, you are required to take reasonable measures to protect
|
||
your assessed work from unauthorised access. For example, if you put
|
||
any such work on a public repository then you must set access
|
||
permissions appropriately (generally permitting access only to
|
||
yourself, or your group in the case of group practicals).</p>
|
||
|
||
<h2 id="imports">Imports</h2>
|
||
|
||
<pre class="Agda"><a id="1198" class="Keyword">import</a> <a id="1205" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="1243" class="Symbol">as</a> <a id="1246" class="Module">Eq</a>
|
||
<a id="1249" class="Keyword">open</a> <a id="1254" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Eq</a> <a id="1257" class="Keyword">using</a> <a id="1263" class="Symbol">(</a><a id="1264" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="1267" class="Symbol">;</a> <a id="1269" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="1273" class="Symbol">;</a> <a id="1275" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a><a id="1279" class="Symbol">;</a> <a id="1281" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a><a id="1284" class="Symbol">)</a>
|
||
<a id="1286" class="Keyword">open</a> <a id="1291" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2499" class="Module">Eq.≡-Reasoning</a> <a id="1306" class="Keyword">using</a> <a id="1312" class="Symbol">(</a><a id="1313" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin_</a><a id="1319" class="Symbol">;</a> <a id="1321" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">_≡⟨⟩_</a><a id="1326" class="Symbol">;</a> <a id="1328" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">_≡⟨_⟩_</a><a id="1334" class="Symbol">;</a> <a id="1336" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">_∎</a><a id="1338" class="Symbol">)</a>
|
||
<a id="1340" class="Keyword">open</a> <a id="1345" class="Keyword">import</a> <a id="1352" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html" class="Module">Data.Bool.Base</a> <a id="1367" class="Keyword">using</a> <a id="1373" class="Symbol">(</a><a id="1374" href="Agda.Builtin.Bool.html#135" class="Datatype">Bool</a><a id="1378" class="Symbol">;</a> <a id="1380" href="Agda.Builtin.Bool.html#160" class="InductiveConstructor">true</a><a id="1384" class="Symbol">;</a> <a id="1386" href="Agda.Builtin.Bool.html#154" class="InductiveConstructor">false</a><a id="1391" class="Symbol">;</a> <a id="1393" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#1480" class="Function">T</a><a id="1394" class="Symbol">;</a> <a id="1396" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#1015" class="Function Operator">_∧_</a><a id="1399" class="Symbol">;</a> <a id="1401" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#1073" class="Function Operator">_∨_</a><a id="1404" class="Symbol">;</a> <a id="1406" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#961" class="Function">not</a><a id="1409" class="Symbol">)</a>
|
||
<a id="1411" class="Keyword">open</a> <a id="1416" class="Keyword">import</a> <a id="1423" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="1432" class="Keyword">using</a> <a id="1438" class="Symbol">(</a><a id="1439" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="1440" class="Symbol">;</a> <a id="1442" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="1446" class="Symbol">;</a> <a id="1448" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a><a id="1451" class="Symbol">;</a> <a id="1453" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a><a id="1456" class="Symbol">;</a> <a id="1458" href="Agda.Builtin.Nat.html#501" class="Primitive Operator">_*_</a><a id="1461" class="Symbol">;</a> <a id="1463" href="Agda.Builtin.Nat.html#388" class="Primitive Operator">_∸_</a><a id="1466" class="Symbol">;</a> <a id="1468" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#895" class="Datatype Operator">_≤_</a><a id="1471" class="Symbol">;</a> <a id="1473" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#960" class="InductiveConstructor">s≤s</a><a id="1476" class="Symbol">;</a> <a id="1478" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#918" class="InductiveConstructor">z≤n</a><a id="1481" class="Symbol">)</a>
|
||
<a id="1483" class="Keyword">open</a> <a id="1488" class="Keyword">import</a> <a id="1495" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="1515" class="Keyword">using</a>
|
||
<a id="1523" class="Symbol">(</a><a id="1524" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11578" class="Function">+-assoc</a><a id="1531" class="Symbol">;</a> <a id="1533" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11679" class="Function">+-identityˡ</a><a id="1544" class="Symbol">;</a> <a id="1546" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11734" class="Function">+-identityʳ</a><a id="1557" class="Symbol">;</a> <a id="1559" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#18464" class="Function">*-assoc</a><a id="1566" class="Symbol">;</a> <a id="1568" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#17362" class="Function">*-identityˡ</a><a id="1579" class="Symbol">;</a> <a id="1581" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#17426" class="Function">*-identityʳ</a><a id="1592" class="Symbol">)</a>
|
||
<a id="1594" class="Keyword">open</a> <a id="1599" class="Keyword">import</a> <a id="1606" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="1623" class="Keyword">using</a> <a id="1629" class="Symbol">(</a><a id="1630" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬_</a><a id="1632" class="Symbol">;</a> <a id="1634" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a><a id="1637" class="Symbol">;</a> <a id="1639" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a><a id="1642" class="Symbol">;</a> <a id="1644" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a><a id="1646" class="Symbol">)</a>
|
||
<a id="1648" class="Keyword">open</a> <a id="1653" class="Keyword">import</a> <a id="1660" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html" class="Module">Data.Product</a> <a id="1673" class="Keyword">using</a> <a id="1679" class="Symbol">(</a><a id="1680" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">_×_</a><a id="1683" class="Symbol">;</a> <a id="1685" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1364" class="Function">∃</a><a id="1686" class="Symbol">;</a> <a id="1688" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃-syntax</a><a id="1696" class="Symbol">)</a> <a id="1698" class="Keyword">renaming</a> <a id="1707" class="Symbol">(</a><a id="1708" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">_,_</a> <a id="1712" class="Symbol">to</a> <a id="1715" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨_,_⟩</a><a id="1720" class="Symbol">)</a>
|
||
<a id="1722" class="Keyword">open</a> <a id="1727" class="Keyword">import</a> <a id="1734" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html" class="Module">Data.Empty</a> <a id="1745" class="Keyword">using</a> <a id="1751" class="Symbol">(</a><a id="1752" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a><a id="1753" class="Symbol">;</a> <a id="1755" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a><a id="1761" class="Symbol">)</a>
|
||
<a id="1763" class="Keyword">open</a> <a id="1768" class="Keyword">import</a> <a id="1775" href="https://agda.github.io/agda-stdlib/v1.1/Function.html" class="Module">Function</a> <a id="1784" class="Keyword">using</a> <a id="1790" class="Symbol">(</a><a id="1791" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">_∘_</a><a id="1794" class="Symbol">)</a>
|
||
<a id="1796" class="Keyword">open</a> <a id="1801" class="Keyword">import</a> <a id="1808" href="https://agda.github.io/agda-stdlib/v1.1/Algebra.Structures.html" class="Module">Algebra.Structures</a> <a id="1827" class="Keyword">using</a> <a id="1833" class="Symbol">(</a><a id="1834" href="https://agda.github.io/agda-stdlib/v1.1/Algebra.Structures.html#2215" class="Record">IsMonoid</a><a id="1842" class="Symbol">)</a>
|
||
<a id="1844" class="Keyword">open</a> <a id="1849" class="Keyword">import</a> <a id="1856" href="https://agda.github.io/agda-stdlib/v1.1/Level.html" class="Module">Level</a> <a id="1862" class="Keyword">using</a> <a id="1868" class="Symbol">(</a><a id="1869" href="Agda.Primitive.html#408" class="Postulate">Level</a><a id="1874" class="Symbol">)</a>
|
||
<a id="1876" class="Keyword">open</a> <a id="1881" class="Keyword">import</a> <a id="1888" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Unary.html" class="Module">Relation.Unary</a> <a id="1903" class="Keyword">using</a> <a id="1909" class="Symbol">(</a><a id="1910" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Unary.html#3474" class="Function">Decidable</a><a id="1919" class="Symbol">)</a>
|
||
<a id="1921" class="Keyword">open</a> <a id="1926" class="Keyword">import</a> <a id="1933" href="/20.07/Relations/" class="Module">plfa.part1.Relations</a> <a id="1954" class="Keyword">using</a> <a id="1960" class="Symbol">(</a><a id="1961" href="/20.07/Relations/#18905" class="Datatype Operator">_<_</a><a id="1964" class="Symbol">;</a> <a id="1966" href="/20.07/Relations/#18932" class="InductiveConstructor">z<s</a><a id="1969" class="Symbol">;</a> <a id="1971" href="/20.07/Relations/#18989" class="InductiveConstructor">s<s</a><a id="1974" class="Symbol">)</a>
|
||
<a id="1976" class="Keyword">open</a> <a id="1981" class="Keyword">import</a> <a id="1988" href="/20.07/Isomorphism/" class="Module">plfa.part1.Isomorphism</a> <a id="2011" class="Keyword">using</a> <a id="2017" class="Symbol">(</a><a id="2018" href="/20.07/Isomorphism/#4365" class="Record Operator">_≃_</a><a id="2021" class="Symbol">;</a> <a id="2023" href="/20.07/Isomorphism/#7107" class="Function">≃-sym</a><a id="2028" class="Symbol">;</a> <a id="2030" href="/20.07/Isomorphism/#7432" class="Function">≃-trans</a><a id="2037" class="Symbol">;</a> <a id="2039" href="/20.07/Isomorphism/#9281" class="Record Operator">_≲_</a><a id="2042" class="Symbol">;</a> <a id="2044" href="/20.07/Isomorphism/#2684" class="Postulate">extensionality</a><a id="2058" class="Symbol">)</a>
|
||
<a id="2060" class="Keyword">open</a> <a id="2065" href="/20.07/Isomorphism/#8516" class="Module">plfa.part1.Isomorphism.≃-Reasoning</a>
|
||
<a id="2100" class="Keyword">open</a> <a id="2105" class="Keyword">import</a> <a id="2112" href="/20.07/Lists/" class="Module">plfa.part1.Lists</a> <a id="2129" class="Keyword">using</a> <a id="2135" class="Symbol">(</a><a id="2136" href="/20.07/Lists/#1067" class="Datatype">List</a><a id="2140" class="Symbol">;</a> <a id="2142" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="2144" class="Symbol">;</a> <a id="2146" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">_∷_</a><a id="2149" class="Symbol">;</a> <a id="2151" href="/20.07/Lists/#2827" class="Operator">[_]</a><a id="2154" class="Symbol">;</a> <a id="2156" href="/20.07/Lists/#2850" class="Operator">[_,_]</a><a id="2161" class="Symbol">;</a> <a id="2163" href="/20.07/Lists/#2881" class="Operator">[_,_,_]</a><a id="2170" class="Symbol">;</a> <a id="2172" href="/20.07/Lists/#2920" class="Operator">[_,_,_,_]</a><a id="2181" class="Symbol">;</a>
|
||
<a id="2185" href="/20.07/Lists/#3467" class="Function Operator">_++_</a><a id="2189" class="Symbol">;</a> <a id="2191" href="/20.07/Lists/#8318" class="Function">reverse</a><a id="2198" class="Symbol">;</a> <a id="2200" href="/20.07/Lists/#12865" class="Function">map</a><a id="2203" class="Symbol">;</a> <a id="2205" href="/20.07/Lists/#15291" class="Function">foldr</a><a id="2210" class="Symbol">;</a> <a id="2212" href="/20.07/Lists/#16254" class="Function">sum</a><a id="2215" class="Symbol">;</a> <a id="2217" href="/20.07/Lists/#21529" class="Datatype">All</a><a id="2220" class="Symbol">;</a> <a id="2222" href="/20.07/Lists/#22982" class="Datatype">Any</a><a id="2225" class="Symbol">;</a> <a id="2227" href="/20.07/Lists/#23033" class="InductiveConstructor">here</a><a id="2231" class="Symbol">;</a> <a id="2233" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a><a id="2238" class="Symbol">;</a> <a id="2240" href="/20.07/Lists/#23404" class="Function Operator">_∈_</a><a id="2243" class="Symbol">)</a>
|
||
<a id="2245" class="Keyword">open</a> <a id="2250" class="Keyword">import</a> <a id="2257" href="/20.07/Lambda/" class="Module">plfa.part2.Lambda</a> <a id="2275" class="Keyword">hiding</a> <a id="2282" class="Symbol">(</a><a id="2283" href="/20.07/Lambda/#7592" class="Function Operator">ƛ′_⇒_</a><a id="2288" class="Symbol">;</a> <a id="2290" href="/20.07/Lambda/#7713" class="Function Operator">case′_[zero⇒_|suc_⇒_]</a><a id="2311" class="Symbol">;</a> <a id="2313" href="/20.07/Lambda/#7927" class="Function Operator">μ′_⇒_</a><a id="2318" class="Symbol">;</a> <a id="2320" href="/20.07/Lambda/#8681" class="Function">plus′</a><a id="2325" class="Symbol">)</a>
|
||
<a id="2327" class="Keyword">open</a> <a id="2332" class="Keyword">import</a> <a id="2339" href="/20.07/Properties/" class="Module">plfa.part2.Properties</a> <a id="2361" class="Keyword">hiding</a> <a id="2368" class="Symbol">(</a><a id="2369" href="/20.07/Properties/#11767" class="Postulate">value?</a><a id="2375" class="Symbol">;</a> <a id="2377" href="/20.07/Properties/#42067" class="Postulate">unstuck</a><a id="2384" class="Symbol">;</a> <a id="2386" href="/20.07/Properties/#42267" class="Postulate">preserves</a><a id="2395" class="Symbol">;</a> <a id="2397" href="/20.07/Properties/#42504" class="Postulate">wttdgs</a><a id="2403" class="Symbol">)</a>
|
||
</pre>
|
||
|
||
<h2 id="lists">Lists</h2>
|
||
|
||
<h4 id="exercise-reverse--distrib-recommended">Exercise <code class="language-plaintext highlighter-rouge">reverse-++-distrib</code> (recommended)</h4>
|
||
|
||
<p>Show that the reverse of one list appended to another is the
|
||
reverse of the second appended to the reverse of the first:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
|
||
</code></pre></div></div>
|
||
|
||
<h4 id="exercise-reverse-involutive-recommended">Exercise <code class="language-plaintext highlighter-rouge">reverse-involutive</code> (recommended)</h4>
|
||
|
||
<p>A function is an <em>involution</em> if when applied twice it acts
|
||
as the identity function. Show that reverse is an involution:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>reverse (reverse xs) ≡ xs
|
||
</code></pre></div></div>
|
||
|
||
<h4 id="exercise-map-compose-practice">Exercise <code class="language-plaintext highlighter-rouge">map-compose</code> (practice)</h4>
|
||
|
||
<p>Prove that the map of a composition is equal to the composition of two maps:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>map (g ∘ f) ≡ map g ∘ map f
|
||
</code></pre></div></div>
|
||
|
||
<p>The last step of the proof requires extensionality.</p>
|
||
|
||
<h4 id="exercise-map--distribute-practice">Exercise <code class="language-plaintext highlighter-rouge">map-++-distribute</code> (practice)</h4>
|
||
|
||
<p>Prove the following relationship between map and append:</p>
|
||
|
||
<p>map f (xs ++ ys) ≡ map f xs ++ map f ys</p>
|
||
|
||
<h4 id="exercise-map-tree-practice">Exercise <code class="language-plaintext highlighter-rouge">map-Tree</code> (practice)</h4>
|
||
|
||
<p>Define a type of trees with leaves of type <code class="language-plaintext highlighter-rouge">A</code> and internal
|
||
nodes of type <code class="language-plaintext highlighter-rouge">B</code>:</p>
|
||
<pre class="Agda"><a id="3323" class="Keyword">data</a> <a id="Tree"></a><a id="3328" href="/20.07/TSPL/2019/Assignment3/#3328" class="Datatype">Tree</a> <a id="3333" class="Symbol">(</a><a id="3334" href="/20.07/TSPL/2019/Assignment3/#3334" class="Bound">A</a> <a id="3336" href="/20.07/TSPL/2019/Assignment3/#3336" class="Bound">B</a> <a id="3338" class="Symbol">:</a> <a id="3340" class="PrimitiveType">Set</a><a id="3343" class="Symbol">)</a> <a id="3345" class="Symbol">:</a> <a id="3347" class="PrimitiveType">Set</a> <a id="3351" class="Keyword">where</a>
|
||
<a id="Tree.leaf"></a><a id="3359" href="/20.07/TSPL/2019/Assignment3/#3359" class="InductiveConstructor">leaf</a> <a id="3364" class="Symbol">:</a> <a id="3366" href="/20.07/TSPL/2019/Assignment3/#3334" class="Bound">A</a> <a id="3368" class="Symbol">→</a> <a id="3370" href="/20.07/TSPL/2019/Assignment3/#3328" class="Datatype">Tree</a> <a id="3375" href="/20.07/TSPL/2019/Assignment3/#3334" class="Bound">A</a> <a id="3377" href="/20.07/TSPL/2019/Assignment3/#3336" class="Bound">B</a>
|
||
<a id="Tree.node"></a><a id="3381" href="/20.07/TSPL/2019/Assignment3/#3381" class="InductiveConstructor">node</a> <a id="3386" class="Symbol">:</a> <a id="3388" href="/20.07/TSPL/2019/Assignment3/#3328" class="Datatype">Tree</a> <a id="3393" href="/20.07/TSPL/2019/Assignment3/#3334" class="Bound">A</a> <a id="3395" href="/20.07/TSPL/2019/Assignment3/#3336" class="Bound">B</a> <a id="3397" class="Symbol">→</a> <a id="3399" href="/20.07/TSPL/2019/Assignment3/#3336" class="Bound">B</a> <a id="3401" class="Symbol">→</a> <a id="3403" href="/20.07/TSPL/2019/Assignment3/#3328" class="Datatype">Tree</a> <a id="3408" href="/20.07/TSPL/2019/Assignment3/#3334" class="Bound">A</a> <a id="3410" href="/20.07/TSPL/2019/Assignment3/#3336" class="Bound">B</a> <a id="3412" class="Symbol">→</a> <a id="3414" href="/20.07/TSPL/2019/Assignment3/#3328" class="Datatype">Tree</a> <a id="3419" href="/20.07/TSPL/2019/Assignment3/#3334" class="Bound">A</a> <a id="3421" href="/20.07/TSPL/2019/Assignment3/#3336" class="Bound">B</a>
|
||
</pre>
|
||
<p>Define a suitable map operator over trees:</p>
|
||
<pre class="Agda"><a id="3474" class="Keyword">postulate</a>
|
||
<a id="map-Tree"></a><a id="3486" href="/20.07/TSPL/2019/Assignment3/#3486" class="Postulate">map-Tree</a> <a id="3495" class="Symbol">:</a> <a id="3497" class="Symbol">∀</a> <a id="3499" class="Symbol">{</a><a id="3500" href="/20.07/TSPL/2019/Assignment3/#3500" class="Bound">A</a> <a id="3502" href="/20.07/TSPL/2019/Assignment3/#3502" class="Bound">B</a> <a id="3504" href="/20.07/TSPL/2019/Assignment3/#3504" class="Bound">C</a> <a id="3506" href="/20.07/TSPL/2019/Assignment3/#3506" class="Bound">D</a> <a id="3508" class="Symbol">:</a> <a id="3510" class="PrimitiveType">Set</a><a id="3513" class="Symbol">}</a>
|
||
<a id="3519" class="Symbol">→</a> <a id="3521" class="Symbol">(</a><a id="3522" href="/20.07/TSPL/2019/Assignment3/#3500" class="Bound">A</a> <a id="3524" class="Symbol">→</a> <a id="3526" href="/20.07/TSPL/2019/Assignment3/#3504" class="Bound">C</a><a id="3527" class="Symbol">)</a> <a id="3529" class="Symbol">→</a> <a id="3531" class="Symbol">(</a><a id="3532" href="/20.07/TSPL/2019/Assignment3/#3502" class="Bound">B</a> <a id="3534" class="Symbol">→</a> <a id="3536" href="/20.07/TSPL/2019/Assignment3/#3506" class="Bound">D</a><a id="3537" class="Symbol">)</a> <a id="3539" class="Symbol">→</a> <a id="3541" href="/20.07/TSPL/2019/Assignment3/#3328" class="Datatype">Tree</a> <a id="3546" href="/20.07/TSPL/2019/Assignment3/#3500" class="Bound">A</a> <a id="3548" href="/20.07/TSPL/2019/Assignment3/#3502" class="Bound">B</a> <a id="3550" class="Symbol">→</a> <a id="3552" href="/20.07/TSPL/2019/Assignment3/#3328" class="Datatype">Tree</a> <a id="3557" href="/20.07/TSPL/2019/Assignment3/#3504" class="Bound">C</a> <a id="3559" href="/20.07/TSPL/2019/Assignment3/#3506" class="Bound">D</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-product-recommended">Exercise <code class="language-plaintext highlighter-rouge">product</code> (recommended)</h4>
|
||
|
||
<p>Use fold to define a function to find the product of a list of numbers.
|
||
For example:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>product [ 1 , 2 , 3 , 4 ] ≡ 24
|
||
</code></pre></div></div>
|
||
|
||
<pre class="Agda"><a id="3732" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="exercise-foldr--recommended">Exercise <code class="language-plaintext highlighter-rouge">foldr-++</code> (recommended)</h4>
|
||
|
||
<p>Show that fold and append are related as follows:</p>
|
||
<pre class="Agda"><a id="3854" class="Keyword">postulate</a>
|
||
<a id="foldr-++"></a><a id="3866" href="/20.07/TSPL/2019/Assignment3/#3866" class="Postulate">foldr-++</a> <a id="3875" class="Symbol">:</a> <a id="3877" class="Symbol">∀</a> <a id="3879" class="Symbol">{</a><a id="3880" href="/20.07/TSPL/2019/Assignment3/#3880" class="Bound">A</a> <a id="3882" href="/20.07/TSPL/2019/Assignment3/#3882" class="Bound">B</a> <a id="3884" class="Symbol">:</a> <a id="3886" class="PrimitiveType">Set</a><a id="3889" class="Symbol">}</a> <a id="3891" class="Symbol">(</a><a id="3892" href="/20.07/TSPL/2019/Assignment3/#3892" class="Bound Operator">_⊗_</a> <a id="3896" class="Symbol">:</a> <a id="3898" href="/20.07/TSPL/2019/Assignment3/#3880" class="Bound">A</a> <a id="3900" class="Symbol">→</a> <a id="3902" href="/20.07/TSPL/2019/Assignment3/#3882" class="Bound">B</a> <a id="3904" class="Symbol">→</a> <a id="3906" href="/20.07/TSPL/2019/Assignment3/#3882" class="Bound">B</a><a id="3907" class="Symbol">)</a> <a id="3909" class="Symbol">(</a><a id="3910" href="/20.07/TSPL/2019/Assignment3/#3910" class="Bound">e</a> <a id="3912" class="Symbol">:</a> <a id="3914" href="/20.07/TSPL/2019/Assignment3/#3882" class="Bound">B</a><a id="3915" class="Symbol">)</a> <a id="3917" class="Symbol">(</a><a id="3918" href="/20.07/TSPL/2019/Assignment3/#3918" class="Bound">xs</a> <a id="3921" href="/20.07/TSPL/2019/Assignment3/#3921" class="Bound">ys</a> <a id="3924" class="Symbol">:</a> <a id="3926" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="3931" href="/20.07/TSPL/2019/Assignment3/#3880" class="Bound">A</a><a id="3932" class="Symbol">)</a> <a id="3934" class="Symbol">→</a>
|
||
<a id="3940" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="3946" href="/20.07/TSPL/2019/Assignment3/#3892" class="Bound Operator">_⊗_</a> <a id="3950" href="/20.07/TSPL/2019/Assignment3/#3910" class="Bound">e</a> <a id="3952" class="Symbol">(</a><a id="3953" href="/20.07/TSPL/2019/Assignment3/#3918" class="Bound">xs</a> <a id="3956" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="3959" href="/20.07/TSPL/2019/Assignment3/#3921" class="Bound">ys</a><a id="3961" class="Symbol">)</a> <a id="3963" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="3965" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="3971" href="/20.07/TSPL/2019/Assignment3/#3892" class="Bound Operator">_⊗_</a> <a id="3975" class="Symbol">(</a><a id="3976" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="3982" href="/20.07/TSPL/2019/Assignment3/#3892" class="Bound Operator">_⊗_</a> <a id="3986" href="/20.07/TSPL/2019/Assignment3/#3910" class="Bound">e</a> <a id="3988" href="/20.07/TSPL/2019/Assignment3/#3921" class="Bound">ys</a><a id="3990" class="Symbol">)</a> <a id="3992" href="/20.07/TSPL/2019/Assignment3/#3918" class="Bound">xs</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-map-is-foldr-practice">Exercise <code class="language-plaintext highlighter-rouge">map-is-foldr</code> (practice)</h4>
|
||
|
||
<p>Show that map can be defined using fold:</p>
|
||
<pre class="Agda"><a id="4087" class="Keyword">postulate</a>
|
||
<a id="map-is-foldr"></a><a id="4099" href="/20.07/TSPL/2019/Assignment3/#4099" class="Postulate">map-is-foldr</a> <a id="4112" class="Symbol">:</a> <a id="4114" class="Symbol">∀</a> <a id="4116" class="Symbol">{</a><a id="4117" href="/20.07/TSPL/2019/Assignment3/#4117" class="Bound">A</a> <a id="4119" href="/20.07/TSPL/2019/Assignment3/#4119" class="Bound">B</a> <a id="4121" class="Symbol">:</a> <a id="4123" class="PrimitiveType">Set</a><a id="4126" class="Symbol">}</a> <a id="4128" class="Symbol">{</a><a id="4129" href="/20.07/TSPL/2019/Assignment3/#4129" class="Bound">f</a> <a id="4131" class="Symbol">:</a> <a id="4133" href="/20.07/TSPL/2019/Assignment3/#4117" class="Bound">A</a> <a id="4135" class="Symbol">→</a> <a id="4137" href="/20.07/TSPL/2019/Assignment3/#4119" class="Bound">B</a><a id="4138" class="Symbol">}</a> <a id="4140" class="Symbol">→</a>
|
||
<a id="4146" href="/20.07/Lists/#12865" class="Function">map</a> <a id="4150" href="/20.07/TSPL/2019/Assignment3/#4129" class="Bound">f</a> <a id="4152" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4154" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="4160" class="Symbol">(λ</a> <a id="4163" href="/20.07/TSPL/2019/Assignment3/#4163" class="Bound">x</a> <a id="4165" href="/20.07/TSPL/2019/Assignment3/#4165" class="Bound">xs</a> <a id="4168" class="Symbol">→</a> <a id="4170" href="/20.07/TSPL/2019/Assignment3/#4129" class="Bound">f</a> <a id="4172" href="/20.07/TSPL/2019/Assignment3/#4163" class="Bound">x</a> <a id="4174" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4176" href="/20.07/TSPL/2019/Assignment3/#4165" class="Bound">xs</a><a id="4178" class="Symbol">)</a> <a id="4180" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
|
||
</pre>
|
||
<p>This requires extensionality.</p>
|
||
|
||
<h4 id="exercise-fold-tree-practice">Exercise <code class="language-plaintext highlighter-rouge">fold-Tree</code> (practice)</h4>
|
||
|
||
<p>Define a suitable fold function for the type of trees given earlier:</p>
|
||
<pre class="Agda"><a id="4329" class="Keyword">postulate</a>
|
||
<a id="fold-Tree"></a><a id="4341" href="/20.07/TSPL/2019/Assignment3/#4341" class="Postulate">fold-Tree</a> <a id="4351" class="Symbol">:</a> <a id="4353" class="Symbol">∀</a> <a id="4355" class="Symbol">{</a><a id="4356" href="/20.07/TSPL/2019/Assignment3/#4356" class="Bound">A</a> <a id="4358" href="/20.07/TSPL/2019/Assignment3/#4358" class="Bound">B</a> <a id="4360" href="/20.07/TSPL/2019/Assignment3/#4360" class="Bound">C</a> <a id="4362" class="Symbol">:</a> <a id="4364" class="PrimitiveType">Set</a><a id="4367" class="Symbol">}</a>
|
||
<a id="4373" class="Symbol">→</a> <a id="4375" class="Symbol">(</a><a id="4376" href="/20.07/TSPL/2019/Assignment3/#4356" class="Bound">A</a> <a id="4378" class="Symbol">→</a> <a id="4380" href="/20.07/TSPL/2019/Assignment3/#4360" class="Bound">C</a><a id="4381" class="Symbol">)</a> <a id="4383" class="Symbol">→</a> <a id="4385" class="Symbol">(</a><a id="4386" href="/20.07/TSPL/2019/Assignment3/#4360" class="Bound">C</a> <a id="4388" class="Symbol">→</a> <a id="4390" href="/20.07/TSPL/2019/Assignment3/#4358" class="Bound">B</a> <a id="4392" class="Symbol">→</a> <a id="4394" href="/20.07/TSPL/2019/Assignment3/#4360" class="Bound">C</a> <a id="4396" class="Symbol">→</a> <a id="4398" href="/20.07/TSPL/2019/Assignment3/#4360" class="Bound">C</a><a id="4399" class="Symbol">)</a> <a id="4401" class="Symbol">→</a> <a id="4403" href="/20.07/TSPL/2019/Assignment3/#3328" class="Datatype">Tree</a> <a id="4408" href="/20.07/TSPL/2019/Assignment3/#4356" class="Bound">A</a> <a id="4410" href="/20.07/TSPL/2019/Assignment3/#4358" class="Bound">B</a> <a id="4412" class="Symbol">→</a> <a id="4414" href="/20.07/TSPL/2019/Assignment3/#4360" class="Bound">C</a>
|
||
</pre>
|
||
<pre class="Agda"><a id="4425" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="exercise-map-is-fold-tree-practice">Exercise <code class="language-plaintext highlighter-rouge">map-is-fold-Tree</code> (practice)</h4>
|
||
|
||
<p>Demonstrate an analogue of <code class="language-plaintext highlighter-rouge">map-is-foldr</code> for the type of trees.</p>
|
||
|
||
<pre class="Agda"><a id="4568" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="exercise-sum-downfrom-stretch">Exercise <code class="language-plaintext highlighter-rouge">sum-downFrom</code> (stretch)</h4>
|
||
|
||
<p>Define a function that counts down as follows:</p>
|
||
<pre class="Agda"><a id="downFrom"></a><a id="4687" href="/20.07/TSPL/2019/Assignment3/#4687" class="Function">downFrom</a> <a id="4696" class="Symbol">:</a> <a id="4698" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="4700" class="Symbol">→</a> <a id="4702" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="4707" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
|
||
<a id="4709" href="/20.07/TSPL/2019/Assignment3/#4687" class="Function">downFrom</a> <a id="4718" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="4727" class="Symbol">=</a> <a id="4730" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
|
||
<a id="4733" href="/20.07/TSPL/2019/Assignment3/#4687" class="Function">downFrom</a> <a id="4742" class="Symbol">(</a><a id="4743" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="4747" href="/20.07/TSPL/2019/Assignment3/#4747" class="Bound">n</a><a id="4748" class="Symbol">)</a> <a id="4751" class="Symbol">=</a> <a id="4754" href="/20.07/TSPL/2019/Assignment3/#4747" class="Bound">n</a> <a id="4756" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4758" href="/20.07/TSPL/2019/Assignment3/#4687" class="Function">downFrom</a> <a id="4767" href="/20.07/TSPL/2019/Assignment3/#4747" class="Bound">n</a>
|
||
</pre>
|
||
<p>For example:</p>
|
||
<pre class="Agda"><a id="4790" href="/20.07/TSPL/2019/Assignment3/#4790" class="Function">_</a> <a id="4792" class="Symbol">:</a> <a id="4794" href="/20.07/TSPL/2019/Assignment3/#4687" class="Function">downFrom</a> <a id="4803" class="Number">3</a> <a id="4805" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4807" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="4809" class="Number">2</a> <a id="4811" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="4813" class="Number">1</a> <a id="4815" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="4817" class="Number">0</a> <a id="4819" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
|
||
<a id="4821" class="Symbol">_</a> <a id="4823" class="Symbol">=</a> <a id="4825" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
</pre>
|
||
<p>Prove that the sum of the numbers <code class="language-plaintext highlighter-rouge">(n - 1) + ⋯ + 0</code> is
|
||
equal to <code class="language-plaintext highlighter-rouge">n * (n ∸ 1) / 2</code>:</p>
|
||
<pre class="Agda"><a id="4921" class="Keyword">postulate</a>
|
||
<a id="sum-downFrom"></a><a id="4933" href="/20.07/TSPL/2019/Assignment3/#4933" class="Postulate">sum-downFrom</a> <a id="4946" class="Symbol">:</a> <a id="4948" class="Symbol">∀</a> <a id="4950" class="Symbol">(</a><a id="4951" href="/20.07/TSPL/2019/Assignment3/#4951" class="Bound">n</a> <a id="4953" class="Symbol">:</a> <a id="4955" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="4956" class="Symbol">)</a>
|
||
<a id="4962" class="Symbol">→</a> <a id="4964" href="/20.07/Lists/#16254" class="Function">sum</a> <a id="4968" class="Symbol">(</a><a id="4969" href="/20.07/TSPL/2019/Assignment3/#4687" class="Function">downFrom</a> <a id="4978" href="/20.07/TSPL/2019/Assignment3/#4951" class="Bound">n</a><a id="4979" class="Symbol">)</a> <a id="4981" href="Agda.Builtin.Nat.html#501" class="Primitive Operator">*</a> <a id="4983" class="Number">2</a> <a id="4985" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4987" href="/20.07/TSPL/2019/Assignment3/#4951" class="Bound">n</a> <a id="4989" href="Agda.Builtin.Nat.html#501" class="Primitive Operator">*</a> <a id="4991" class="Symbol">(</a><a id="4992" href="/20.07/TSPL/2019/Assignment3/#4951" class="Bound">n</a> <a id="4994" href="Agda.Builtin.Nat.html#388" class="Primitive Operator">∸</a> <a id="4996" class="Number">1</a><a id="4997" class="Symbol">)</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-foldl-practice">Exercise <code class="language-plaintext highlighter-rouge">foldl</code> (practice)</h4>
|
||
|
||
<p>Define a function <code class="language-plaintext highlighter-rouge">foldl</code> which is analogous to <code class="language-plaintext highlighter-rouge">foldr</code>, but where
|
||
operations associate to the left rather than the right. For example:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>foldr _⊗_ e [ x , y , z ] = x ⊗ (y ⊗ (z ⊗ e))
|
||
foldl _⊗_ e [ x , y , z ] = ((e ⊗ x) ⊗ y) ⊗ z
|
||
</code></pre></div></div>
|
||
|
||
<pre class="Agda"><a id="5286" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-foldr-monoid-foldl-practice">Exercise <code class="language-plaintext highlighter-rouge">foldr-monoid-foldl</code> (practice)</h4>
|
||
|
||
<p>Show that if <code class="language-plaintext highlighter-rouge">_⊗_</code> and <code class="language-plaintext highlighter-rouge">e</code> form a monoid, then <code class="language-plaintext highlighter-rouge">foldr _⊗_ e</code> and
|
||
<code class="language-plaintext highlighter-rouge">foldl _⊗_ e</code> always compute the same result.</p>
|
||
|
||
<pre class="Agda"><a id="5478" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-any---recommended">Exercise <code class="language-plaintext highlighter-rouge">Any-++-⇔</code> (recommended)</h4>
|
||
|
||
<p>Prove a result similar to <code class="language-plaintext highlighter-rouge">All-++-⇔</code>, but with <code class="language-plaintext highlighter-rouge">Any</code> in place of <code class="language-plaintext highlighter-rouge">All</code>, and a suitable
|
||
replacement for <code class="language-plaintext highlighter-rouge">_×_</code>. As a consequence, demonstrate an equivalence relating
|
||
<code class="language-plaintext highlighter-rouge">_∈_</code> and <code class="language-plaintext highlighter-rouge">_++_</code>.</p>
|
||
|
||
<pre class="Agda"><a id="5735" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-all---stretch">Exercise <code class="language-plaintext highlighter-rouge">All-++-≃</code> (stretch)</h4>
|
||
|
||
<p>Show that the equivalence <code class="language-plaintext highlighter-rouge">All-++-⇔</code> can be extended to an isomorphism.</p>
|
||
|
||
<pre class="Agda"><a id="5877" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-anyall-recommended">Exercise <code class="language-plaintext highlighter-rouge">¬Any⇔All¬</code> (recommended)</h4>
|
||
|
||
<p>Show that <code class="language-plaintext highlighter-rouge">Any</code> and <code class="language-plaintext highlighter-rouge">All</code> satisfy a version of De Morgan’s Law:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs
|
||
</code></pre></div></div>
|
||
|
||
<p>(Can you see why it is important that here <code class="language-plaintext highlighter-rouge">_∘_</code> is generalised
|
||
to arbitrary levels, as described in the section on
|
||
<a href="/20.07/Equality/#unipoly">universe polymorphism</a>?)</p>
|
||
|
||
<p>Do we also have the following?</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs
|
||
</code></pre></div></div>
|
||
|
||
<p>If so, prove; if not, explain why.</p>
|
||
|
||
<pre class="Agda"><a id="6344" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-anyall-stretch">Exercise <code class="language-plaintext highlighter-rouge">¬Any≃All¬</code> (stretch)</h4>
|
||
|
||
<p>Show that the equivalence <code class="language-plaintext highlighter-rouge">¬Any⇔All¬</code> can be extended to an isomorphism.
|
||
You will need to use extensionality.</p>
|
||
|
||
<pre class="Agda"><a id="6525" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-all--practice">Exercise <code class="language-plaintext highlighter-rouge">All-∀</code> (practice)</h4>
|
||
|
||
<p>Show that <code class="language-plaintext highlighter-rouge">All P xs</code> is isomorphic to <code class="language-plaintext highlighter-rouge">∀ {x} → x ∈ xs → P x</code>.</p>
|
||
|
||
<pre class="Agda"><a id="6655" class="Comment">-- You code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-any--practice">Exercise <code class="language-plaintext highlighter-rouge">Any-∃</code> (practice)</h4>
|
||
|
||
<p>Show that <code class="language-plaintext highlighter-rouge">Any P xs</code> is isomorphic to <code class="language-plaintext highlighter-rouge">∃[ x ] (x ∈ xs × P x)</code>.</p>
|
||
|
||
<pre class="Agda"><a id="6785" class="Comment">-- You code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-any-stretch">Exercise <code class="language-plaintext highlighter-rouge">any?</code> (stretch)</h4>
|
||
|
||
<p>Just as <code class="language-plaintext highlighter-rouge">All</code> has analogues <code class="language-plaintext highlighter-rouge">all</code> and <code class="language-plaintext highlighter-rouge">All?</code> which determine whether a
|
||
predicate holds for every element of a list, so does <code class="language-plaintext highlighter-rouge">Any</code> have
|
||
analogues <code class="language-plaintext highlighter-rouge">any</code> and <code class="language-plaintext highlighter-rouge">Any?</code> which determine whether a predicate holds
|
||
for some element of a list. Give their definitions.</p>
|
||
|
||
<pre class="Agda"><a id="7107" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-filter-stretch">Exercise <code class="language-plaintext highlighter-rouge">filter?</code> (stretch)</h4>
|
||
|
||
<p>Define the following variant of the traditional <code class="language-plaintext highlighter-rouge">filter</code> function on lists,
|
||
which given a decidable predicate and a list returns all elements of the
|
||
list satisfying the predicate:</p>
|
||
<pre class="Agda"><a id="7355" class="Keyword">postulate</a>
|
||
<a id="filter?"></a><a id="7367" href="/20.07/TSPL/2019/Assignment3/#7367" class="Postulate">filter?</a> <a id="7375" class="Symbol">:</a> <a id="7377" class="Symbol">∀</a> <a id="7379" class="Symbol">{</a><a id="7380" href="/20.07/TSPL/2019/Assignment3/#7380" class="Bound">A</a> <a id="7382" class="Symbol">:</a> <a id="7384" class="PrimitiveType">Set</a><a id="7387" class="Symbol">}</a> <a id="7389" class="Symbol">{</a><a id="7390" href="/20.07/TSPL/2019/Assignment3/#7390" class="Bound">P</a> <a id="7392" class="Symbol">:</a> <a id="7394" href="/20.07/TSPL/2019/Assignment3/#7380" class="Bound">A</a> <a id="7396" class="Symbol">→</a> <a id="7398" class="PrimitiveType">Set</a><a id="7401" class="Symbol">}</a>
|
||
<a id="7407" class="Symbol">→</a> <a id="7409" class="Symbol">(</a><a id="7410" href="/20.07/TSPL/2019/Assignment3/#7410" class="Bound">P?</a> <a id="7413" class="Symbol">:</a> <a id="7415" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Unary.html#3474" class="Function">Decidable</a> <a id="7425" href="/20.07/TSPL/2019/Assignment3/#7390" class="Bound">P</a><a id="7426" class="Symbol">)</a> <a id="7428" class="Symbol">→</a> <a id="7430" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="7435" href="/20.07/TSPL/2019/Assignment3/#7380" class="Bound">A</a> <a id="7437" class="Symbol">→</a> <a id="7439" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃[</a> <a id="7442" href="/20.07/TSPL/2019/Assignment3/#7442" class="Bound">ys</a> <a id="7445" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">]</a><a id="7446" class="Symbol">(</a> <a id="7448" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="7452" href="/20.07/TSPL/2019/Assignment3/#7390" class="Bound">P</a> <a id="7454" href="/20.07/TSPL/2019/Assignment3/#7442" class="Bound">ys</a> <a id="7457" class="Symbol">)</a>
|
||
</pre>
|
||
|
||
<h2 id="lambda">Lambda</h2>
|
||
|
||
<h4 id="exercise-mul-recommended">Exercise <code class="language-plaintext highlighter-rouge">mul</code> (recommended)</h4>
|
||
|
||
<p>Write out the definition of a lambda term that multiplies
|
||
two natural numbers. Your definition may use <code class="language-plaintext highlighter-rouge">plus</code> as
|
||
defined earlier.</p>
|
||
|
||
<pre class="Agda"><a id="7648" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-mulᶜ-practice">Exercise <code class="language-plaintext highlighter-rouge">mulᶜ</code> (practice)</h4>
|
||
|
||
<p>Write out the definition of a lambda term that multiplies
|
||
two natural numbers represented as Church numerals. Your
|
||
definition may use <code class="language-plaintext highlighter-rouge">plusᶜ</code> as defined earlier (or may not
|
||
— there are nice definitions both ways).</p>
|
||
|
||
<pre class="Agda"><a id="7929" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="primed">Exercise <code class="language-plaintext highlighter-rouge">primed</code> (stretch)</h4>
|
||
|
||
<p>Some people find it annoying to write <code class="language-plaintext highlighter-rouge">` "x"</code> instead of <code class="language-plaintext highlighter-rouge">x</code>.
|
||
We can make examples with lambda terms slightly easier to write
|
||
by adding the following definitions:</p>
|
||
<pre class="Agda"><a id="ƛ′_⇒_"></a><a id="8173" href="/20.07/TSPL/2019/Assignment3/#8173" class="Function Operator">ƛ′_⇒_</a> <a id="8179" class="Symbol">:</a> <a id="8181" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="8186" class="Symbol">→</a> <a id="8188" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="8193" class="Symbol">→</a> <a id="8195" href="/20.07/Lambda/#4005" class="Datatype">Term</a>
|
||
<a id="8200" href="/20.07/TSPL/2019/Assignment3/#8173" class="Function Operator">ƛ′</a> <a id="8203" class="Symbol">(</a><a id="8204" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="8206" href="/20.07/TSPL/2019/Assignment3/#8206" class="Bound">x</a><a id="8207" class="Symbol">)</a> <a id="8209" href="/20.07/TSPL/2019/Assignment3/#8173" class="Function Operator">⇒</a> <a id="8211" href="/20.07/TSPL/2019/Assignment3/#8211" class="Bound">N</a> <a id="8214" class="Symbol">=</a> <a id="8217" href="/20.07/Lambda/#4063" class="InductiveConstructor Operator">ƛ</a> <a id="8219" href="/20.07/TSPL/2019/Assignment3/#8206" class="Bound">x</a> <a id="8221" href="/20.07/Lambda/#4063" class="InductiveConstructor Operator">⇒</a> <a id="8223" href="/20.07/TSPL/2019/Assignment3/#8211" class="Bound">N</a>
|
||
<a id="8225" href="/20.07/TSPL/2019/Assignment3/#8173" class="CatchallClause Function Operator">ƛ′</a><a id="8227" class="CatchallClause"> </a><a id="8228" class="CatchallClause Symbol">_</a><a id="8229" class="CatchallClause"> </a><a id="8230" href="/20.07/TSPL/2019/Assignment3/#8173" class="CatchallClause Function Operator">⇒</a><a id="8231" class="CatchallClause"> </a><a id="8232" class="CatchallClause Symbol">_</a> <a id="8239" class="Symbol">=</a> <a id="8242" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="8249" href="/20.07/TSPL/2019/Assignment3/#8278" class="Postulate">impossible</a>
|
||
<a id="8262" class="Keyword">where</a> <a id="8268" class="Keyword">postulate</a> <a id="8278" href="/20.07/TSPL/2019/Assignment3/#8278" class="Postulate">impossible</a> <a id="8289" class="Symbol">:</a> <a id="8291" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a>
|
||
|
||
<a id="case′_[zero⇒_|suc_⇒_]"></a><a id="8294" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">case′_[zero⇒_|suc_⇒_]</a> <a id="8316" class="Symbol">:</a> <a id="8318" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="8323" class="Symbol">→</a> <a id="8325" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="8330" class="Symbol">→</a> <a id="8332" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="8337" class="Symbol">→</a> <a id="8339" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="8344" class="Symbol">→</a> <a id="8346" href="/20.07/Lambda/#4005" class="Datatype">Term</a>
|
||
<a id="8351" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">case′</a> <a id="8357" href="/20.07/TSPL/2019/Assignment3/#8357" class="Bound">L</a> <a id="8359" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">[zero⇒</a> <a id="8366" href="/20.07/TSPL/2019/Assignment3/#8366" class="Bound">M</a> <a id="8368" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">|suc</a> <a id="8373" class="Symbol">(</a><a id="8374" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="8376" href="/20.07/TSPL/2019/Assignment3/#8376" class="Bound">x</a><a id="8377" class="Symbol">)</a> <a id="8379" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">⇒</a> <a id="8381" href="/20.07/TSPL/2019/Assignment3/#8381" class="Bound">N</a> <a id="8383" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">]</a> <a id="8386" class="Symbol">=</a> <a id="8389" href="/20.07/Lambda/#4232" class="InductiveConstructor Operator">case</a> <a id="8394" href="/20.07/TSPL/2019/Assignment3/#8357" class="Bound">L</a> <a id="8396" href="/20.07/Lambda/#4232" class="InductiveConstructor Operator">[zero⇒</a> <a id="8403" href="/20.07/TSPL/2019/Assignment3/#8366" class="Bound">M</a> <a id="8405" href="/20.07/Lambda/#4232" class="InductiveConstructor Operator">|suc</a> <a id="8410" href="/20.07/TSPL/2019/Assignment3/#8376" class="Bound">x</a> <a id="8412" href="/20.07/Lambda/#4232" class="InductiveConstructor Operator">⇒</a> <a id="8414" href="/20.07/TSPL/2019/Assignment3/#8381" class="Bound">N</a> <a id="8416" href="/20.07/Lambda/#4232" class="InductiveConstructor Operator">]</a>
|
||
<a id="8418" href="/20.07/TSPL/2019/Assignment3/#8294" class="CatchallClause Function Operator">case′</a><a id="8423" class="CatchallClause"> </a><a id="8424" class="CatchallClause Symbol">_</a><a id="8425" class="CatchallClause"> </a><a id="8426" href="/20.07/TSPL/2019/Assignment3/#8294" class="CatchallClause Function Operator">[zero⇒</a><a id="8432" class="CatchallClause"> </a><a id="8433" class="CatchallClause Symbol">_</a><a id="8434" class="CatchallClause"> </a><a id="8435" href="/20.07/TSPL/2019/Assignment3/#8294" class="CatchallClause Function Operator">|suc</a><a id="8439" class="CatchallClause"> </a><a id="8440" class="CatchallClause Symbol">_</a><a id="8441" class="CatchallClause"> </a><a id="8442" href="/20.07/TSPL/2019/Assignment3/#8294" class="CatchallClause Function Operator">⇒</a><a id="8443" class="CatchallClause"> </a><a id="8444" class="CatchallClause Symbol">_</a><a id="8445" class="CatchallClause"> </a><a id="8446" href="/20.07/TSPL/2019/Assignment3/#8294" class="CatchallClause Function Operator">]</a> <a id="8453" class="Symbol">=</a> <a id="8456" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="8463" href="/20.07/TSPL/2019/Assignment3/#8492" class="Postulate">impossible</a>
|
||
<a id="8476" class="Keyword">where</a> <a id="8482" class="Keyword">postulate</a> <a id="8492" href="/20.07/TSPL/2019/Assignment3/#8492" class="Postulate">impossible</a> <a id="8503" class="Symbol">:</a> <a id="8505" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a>
|
||
|
||
<a id="μ′_⇒_"></a><a id="8508" href="/20.07/TSPL/2019/Assignment3/#8508" class="Function Operator">μ′_⇒_</a> <a id="8514" class="Symbol">:</a> <a id="8516" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="8521" class="Symbol">→</a> <a id="8523" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="8528" class="Symbol">→</a> <a id="8530" href="/20.07/Lambda/#4005" class="Datatype">Term</a>
|
||
<a id="8535" href="/20.07/TSPL/2019/Assignment3/#8508" class="Function Operator">μ′</a> <a id="8538" class="Symbol">(</a><a id="8539" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="8541" href="/20.07/TSPL/2019/Assignment3/#8541" class="Bound">x</a><a id="8542" class="Symbol">)</a> <a id="8544" href="/20.07/TSPL/2019/Assignment3/#8508" class="Function Operator">⇒</a> <a id="8546" href="/20.07/TSPL/2019/Assignment3/#8546" class="Bound">N</a> <a id="8549" class="Symbol">=</a> <a id="8552" href="/20.07/Lambda/#4292" class="InductiveConstructor Operator">μ</a> <a id="8554" href="/20.07/TSPL/2019/Assignment3/#8541" class="Bound">x</a> <a id="8556" href="/20.07/Lambda/#4292" class="InductiveConstructor Operator">⇒</a> <a id="8558" href="/20.07/TSPL/2019/Assignment3/#8546" class="Bound">N</a>
|
||
<a id="8560" href="/20.07/TSPL/2019/Assignment3/#8508" class="CatchallClause Function Operator">μ′</a><a id="8562" class="CatchallClause"> </a><a id="8563" class="CatchallClause Symbol">_</a><a id="8564" class="CatchallClause"> </a><a id="8565" href="/20.07/TSPL/2019/Assignment3/#8508" class="CatchallClause Function Operator">⇒</a><a id="8566" class="CatchallClause"> </a><a id="8567" class="CatchallClause Symbol">_</a> <a id="8574" class="Symbol">=</a> <a id="8577" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="8584" href="/20.07/TSPL/2019/Assignment3/#8613" class="Postulate">impossible</a>
|
||
<a id="8597" class="Keyword">where</a> <a id="8603" class="Keyword">postulate</a> <a id="8613" href="/20.07/TSPL/2019/Assignment3/#8613" class="Postulate">impossible</a> <a id="8624" class="Symbol">:</a> <a id="8626" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a>
|
||
</pre>
|
||
<p>We intend to apply the function only when the first term is a variable, which we
|
||
indicate by postulating a term <code class="language-plaintext highlighter-rouge">impossible</code> of the empty type <code class="language-plaintext highlighter-rouge">⊥</code>. If we use
|
||
C-c C-n to normalise the term</p>
|
||
|
||
<p>ƛ′ two ⇒ two</p>
|
||
|
||
<p>Agda will return an answer warning us that the impossible has occurred:</p>
|
||
|
||
<p>⊥-elim (plfa.part2.Lambda.impossible (<code class="language-plaintext highlighter-rouge">`suc (`suc `zero)) (`suc (`suc `zero))</code>)</p>
|
||
|
||
<p>While postulating the impossible is a useful technique, it must be
|
||
used with care, since such postulation could allow us to provide
|
||
evidence of <em>any</em> proposition whatsoever, regardless of its truth.</p>
|
||
|
||
<p>The definition of <code class="language-plaintext highlighter-rouge">plus</code> can now be written as follows:</p>
|
||
<pre class="Agda"><a id="plus′"></a><a id="9258" href="/20.07/TSPL/2019/Assignment3/#9258" class="Function">plus′</a> <a id="9264" class="Symbol">:</a> <a id="9266" href="/20.07/Lambda/#4005" class="Datatype">Term</a>
|
||
<a id="9271" href="/20.07/TSPL/2019/Assignment3/#9258" class="Function">plus′</a> <a id="9277" class="Symbol">=</a> <a id="9279" href="/20.07/TSPL/2019/Assignment3/#8508" class="Function Operator">μ′</a> <a id="9282" href="/20.07/TSPL/2019/Assignment3/#9389" class="Function">+</a> <a id="9284" href="/20.07/TSPL/2019/Assignment3/#8508" class="Function Operator">⇒</a> <a id="9286" href="/20.07/TSPL/2019/Assignment3/#8173" class="Function Operator">ƛ′</a> <a id="9289" href="/20.07/TSPL/2019/Assignment3/#9403" class="Function">m</a> <a id="9291" href="/20.07/TSPL/2019/Assignment3/#8173" class="Function Operator">⇒</a> <a id="9293" href="/20.07/TSPL/2019/Assignment3/#8173" class="Function Operator">ƛ′</a> <a id="9296" href="/20.07/TSPL/2019/Assignment3/#9417" class="Function">n</a> <a id="9298" href="/20.07/TSPL/2019/Assignment3/#8173" class="Function Operator">⇒</a>
|
||
<a id="9310" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">case′</a> <a id="9316" href="/20.07/TSPL/2019/Assignment3/#9403" class="Function">m</a>
|
||
<a id="9330" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">[zero⇒</a> <a id="9337" href="/20.07/TSPL/2019/Assignment3/#9417" class="Function">n</a>
|
||
<a id="9351" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">|suc</a> <a id="9356" href="/20.07/TSPL/2019/Assignment3/#9403" class="Function">m</a> <a id="9358" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">⇒</a> <a id="9360" href="/20.07/Lambda/#4191" class="InductiveConstructor Operator">`suc</a> <a id="9365" class="Symbol">(</a><a id="9366" href="/20.07/TSPL/2019/Assignment3/#9389" class="Function">+</a> <a id="9368" href="/20.07/Lambda/#4109" class="InductiveConstructor Operator">·</a> <a id="9370" href="/20.07/TSPL/2019/Assignment3/#9403" class="Function">m</a> <a id="9372" href="/20.07/Lambda/#4109" class="InductiveConstructor Operator">·</a> <a id="9374" href="/20.07/TSPL/2019/Assignment3/#9417" class="Function">n</a><a id="9375" class="Symbol">)</a> <a id="9377" href="/20.07/TSPL/2019/Assignment3/#8294" class="Function Operator">]</a>
|
||
<a id="9381" class="Keyword">where</a>
|
||
<a id="9389" href="/20.07/TSPL/2019/Assignment3/#9389" class="Function">+</a> <a id="9392" class="Symbol">=</a> <a id="9395" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="9397" class="String">"+"</a>
|
||
<a id="9403" href="/20.07/TSPL/2019/Assignment3/#9403" class="Function">m</a> <a id="9406" class="Symbol">=</a> <a id="9409" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="9411" class="String">"m"</a>
|
||
<a id="9417" href="/20.07/TSPL/2019/Assignment3/#9417" class="Function">n</a> <a id="9420" class="Symbol">=</a> <a id="9423" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="9425" class="String">"n"</a>
|
||
</pre>
|
||
<p>Write out the definition of multiplication in the same style.</p>
|
||
|
||
<h4 id="exercise-___-stretch">Exercise <code class="language-plaintext highlighter-rouge">_[_:=_]′</code> (stretch)</h4>
|
||
|
||
<p>The definition of substitution above has three clauses (<code class="language-plaintext highlighter-rouge">ƛ</code>, <code class="language-plaintext highlighter-rouge">case</code>,
|
||
and <code class="language-plaintext highlighter-rouge">μ</code>) that invoke a <code class="language-plaintext highlighter-rouge">with</code> clause to deal with bound variables.
|
||
Rewrite the definition to factor the common part of these three
|
||
clauses into a single function, defined by mutual recursion with
|
||
substitution.</p>
|
||
|
||
<pre class="Agda"><a id="9817" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise--practice">Exercise <code class="language-plaintext highlighter-rouge">—↠≲—↠′</code> (practice)</h4>
|
||
|
||
<p>Show that the first notion of reflexive and transitive closure
|
||
above embeds into the second. Why are they not isomorphic?</p>
|
||
|
||
<pre class="Agda"><a id="10008" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="exercise-plus-example-practice">Exercise <code class="language-plaintext highlighter-rouge">plus-example</code> (practice)</h4>
|
||
|
||
<p>Write out the reduction sequence demonstrating that one plus one is two.</p>
|
||
|
||
<pre class="Agda"><a id="10155" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-context--practice">Exercise <code class="language-plaintext highlighter-rouge">Context-≃</code> (practice)</h4>
|
||
|
||
<p>Show that <code class="language-plaintext highlighter-rouge">Context</code> is isomorphic to <code class="language-plaintext highlighter-rouge">List (Id × Type)</code>.
|
||
For instance, the isomorphism relates the context</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ
|
||
</code></pre></div></div>
|
||
|
||
<p>to the list</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>[ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ]
|
||
</code></pre></div></div>
|
||
|
||
<pre class="Agda"><a id="10423" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="exercise-mul-type-recommended">Exercise <code class="language-plaintext highlighter-rouge">mul-type</code> (recommended)</h4>
|
||
|
||
<p>Using the term <code class="language-plaintext highlighter-rouge">mul</code> you defined earlier, write out the derivation
|
||
showing that it is well typed.</p>
|
||
|
||
<pre class="Agda"><a id="10594" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-mulᶜ-type-practice">Exercise <code class="language-plaintext highlighter-rouge">mulᶜ-type</code> (practice)</h4>
|
||
|
||
<p>Using the term <code class="language-plaintext highlighter-rouge">mulᶜ</code> you defined earlier, write out the derivation
|
||
showing that it is well typed.</p>
|
||
|
||
<pre class="Agda"><a id="10765" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h2 id="properties">Properties</h2>
|
||
|
||
<h4 id="exercise-progress--practice">Exercise <code class="language-plaintext highlighter-rouge">Progress-≃</code> (practice)</h4>
|
||
|
||
<p>Show that <code class="language-plaintext highlighter-rouge">Progress M</code> is isomorphic to <code class="language-plaintext highlighter-rouge">Value M ⊎ ∃[ N ](M —→ N)</code>.</p>
|
||
|
||
<pre class="Agda"><a id="10922" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="exercise-progress-practice">Exercise <code class="language-plaintext highlighter-rouge">progress′</code> (practice)</h4>
|
||
|
||
<p>Write out the proof of <code class="language-plaintext highlighter-rouge">progress′</code> in full, and compare it to the
|
||
proof of <code class="language-plaintext highlighter-rouge">progress</code> above.</p>
|
||
|
||
<pre class="Agda"><a id="11086" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="exercise-value-practice">Exercise <code class="language-plaintext highlighter-rouge">value?</code> (practice)</h4>
|
||
|
||
<p>Combine <code class="language-plaintext highlighter-rouge">progress</code> and <code class="language-plaintext highlighter-rouge">—→¬V</code> to write a program that decides
|
||
whether a well-typed term is a value:</p>
|
||
<pre class="Agda"><a id="11253" class="Keyword">postulate</a>
|
||
<a id="value?"></a><a id="11265" href="/20.07/TSPL/2019/Assignment3/#11265" class="Postulate">value?</a> <a id="11272" class="Symbol">:</a> <a id="11274" class="Symbol">∀</a> <a id="11276" class="Symbol">{</a><a id="11277" href="/20.07/TSPL/2019/Assignment3/#11277" class="Bound">A</a> <a id="11279" href="/20.07/TSPL/2019/Assignment3/#11279" class="Bound">M</a><a id="11280" class="Symbol">}</a> <a id="11282" class="Symbol">→</a> <a id="11284" href="/20.07/Lambda/#31868" class="InductiveConstructor">∅</a> <a id="11286" href="/20.07/Lambda/#34792" class="Datatype Operator">⊢</a> <a id="11288" href="/20.07/TSPL/2019/Assignment3/#11279" class="Bound">M</a> <a id="11290" href="/20.07/Lambda/#34792" class="Datatype Operator">⦂</a> <a id="11292" href="/20.07/TSPL/2019/Assignment3/#11277" class="Bound">A</a> <a id="11294" class="Symbol">→</a> <a id="11296" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a> <a id="11300" class="Symbol">(</a><a id="11301" href="/20.07/Lambda/#12384" class="Datatype">Value</a> <a id="11307" href="/20.07/TSPL/2019/Assignment3/#11279" class="Bound">M</a><a id="11308" class="Symbol">)</a>
|
||
</pre>
|
||
<h4 id="exercise-subst-stretch">Exercise <code class="language-plaintext highlighter-rouge">subst′</code> (stretch)</h4>
|
||
|
||
<p>Rewrite <code class="language-plaintext highlighter-rouge">subst</code> to work with the modified definition <code class="language-plaintext highlighter-rouge">_[_:=_]′</code>
|
||
from the exercise in the previous chapter. As before, this
|
||
should factor dealing with bound variables into a single function,
|
||
defined by mutual recursion with the proof that substitution
|
||
preserves types.</p>
|
||
|
||
<pre class="Agda"><a id="11623" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-mul-eval-recommended">Exercise <code class="language-plaintext highlighter-rouge">mul-eval</code> (recommended)</h4>
|
||
|
||
<p>Using the evaluator, confirm that two times two is four.</p>
|
||
|
||
<pre class="Agda"><a id="11754" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-progress-preservation-practice">Exercise: <code class="language-plaintext highlighter-rouge">progress-preservation</code> (practice)</h4>
|
||
|
||
<p>Without peeking at their statements above, write down the progress
|
||
and preservation theorems for the simply typed lambda-calculus.</p>
|
||
|
||
<pre class="Agda"><a id="11970" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-subject_expansion-practice">Exercise <code class="language-plaintext highlighter-rouge">subject_expansion</code> (practice)</h4>
|
||
|
||
<p>We say that <code class="language-plaintext highlighter-rouge">M</code> <em>reduces</em> to <code class="language-plaintext highlighter-rouge">N</code> if <code class="language-plaintext highlighter-rouge">M —→ N</code>,
|
||
but we can also describe the same situation by saying
|
||
that <code class="language-plaintext highlighter-rouge">N</code> <em>expands</em> to <code class="language-plaintext highlighter-rouge">M</code>.
|
||
The preservation property is sometimes called <em>subject reduction</em>.
|
||
Its opposite is <em>subject expansion</em>, which holds if
|
||
<code class="language-plaintext highlighter-rouge">M —→ N</code> and <code class="language-plaintext highlighter-rouge">∅ ⊢ N ⦂ A</code> imply <code class="language-plaintext highlighter-rouge">∅ ⊢ M ⦂ A</code>.
|
||
Find two counter-examples to subject expansion, one
|
||
with case expressions and one not involving case expressions.</p>
|
||
|
||
<pre class="Agda"><a id="12454" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-stuck-practice">Exercise <code class="language-plaintext highlighter-rouge">stuck</code> (practice)</h4>
|
||
|
||
<p>Give an example of an ill-typed term that does get stuck.</p>
|
||
|
||
<pre class="Agda"><a id="12580" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="exercise-unstuck-recommended">Exercise <code class="language-plaintext highlighter-rouge">unstuck</code> (recommended)</h4>
|
||
|
||
<p>Provide proofs of the three postulates, <code class="language-plaintext highlighter-rouge">unstuck</code>, <code class="language-plaintext highlighter-rouge">preserves</code>, and <code class="language-plaintext highlighter-rouge">wttdgs</code> above.</p>
|
||
|
||
<pre class="Agda"><a id="12736" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
</div>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/courses/tspl/2019/Assignment3.lagda.md">Source</a>
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
</article>
|
||
|
||
</div>
|
||
</main><footer class="site-footer h-card">
|
||
<data class="u-url" href="/20.07/"></data>
|
||
|
||
<div class="wrapper">
|
||
|
||
<h2 class="footer-heading">Programming Language Foundations in Agda
|
||
</h2><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Philip Wadler</li>
|
||
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Wen Kokke</li>
|
||
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Jeremy G. Siek</li>
|
||
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
|
||
</div>
|
||
</footer>
|
||
<!-- Import jQuery -->
|
||
<script type="text/javascript" src="/20.07/assets/jquery.js"></script>
|
||
|
||
<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
|
||
<script type="text/javascript">
|
||
anchors.add();
|
||
</script>
|
||
|
||
<script type="text/javascript">
|
||
|
||
// Makes sandwhich menu works
|
||
$('.menu-icon').click(function(){
|
||
$('.trigger').toggle();
|
||
});
|
||
|
||
// Script which allows for foldable code blocks
|
||
$('div.foldable pre').each(function(){
|
||
var autoHeight = $(this).height();
|
||
var lineHeight = parseFloat($(this).css('line-height'));
|
||
|
||
var plus = $("<div></div>");
|
||
var horLine = $("<div></div>");
|
||
var verLine = $("<div></div>");
|
||
$(this).prepend(plus);
|
||
plus.css({
|
||
'position' : 'relative',
|
||
'float' : 'right',
|
||
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'width' : lineHeight,
|
||
'height' : lineHeight});
|
||
verLine.css({
|
||
'position' : 'relative',
|
||
'height' : lineHeight,
|
||
'width' : '3px',
|
||
'background-color' : '#C1E0FF'});
|
||
horLine.css({
|
||
'position' : 'relative',
|
||
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
|
||
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'height' : '3px',
|
||
'width' : lineHeight,
|
||
'background-color' : '#C1E0FF'});
|
||
plus.append(verLine);
|
||
plus.append(horLine);
|
||
|
||
$(this).height(2.0 * lineHeight);
|
||
$(this).css('overflow','hidden');
|
||
|
||
$(this).click(function(){
|
||
if ($(this).height() == autoHeight) {
|
||
$(this).height(2.0 * lineHeight);
|
||
plus.show();
|
||
}
|
||
else {
|
||
$(this).height('auto');
|
||
plus.hide();
|
||
}
|
||
});
|
||
});
|
||
</script>
|
||
|
||
<!-- Import KaTeX -->
|
||
<script type="text/javascript" src="/20.07/assets/katex.js"></script>
|
||
|
||
<!-- Script which renders TeX using KaTeX -->
|
||
<script type="text/javascript">
|
||
$("script[type='math/tex']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text();
|
||
return "<span class=\"inline-equation\">" +
|
||
katex.renderToString(tex) +
|
||
"</span>";
|
||
});
|
||
$("script[type='math/tex; mode=display']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
|
||
return "<div class=\"equation\">" +
|
||
katex.renderToString("\\displaystyle "+tex) +
|
||
"</div>";
|
||
});
|
||
</script>
|
||
</body>
|
||
|
||
</html>
|