541 lines
31 KiB
HTML
541 lines
31 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>Assignment1: TSPL Assignment 1 | 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="Assignment1: TSPL Assignment 1" />
|
||
<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/Assignment1/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/TSPL/2019/Assignment1/" />
|
||
<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/Assignment1/","headline":"Assignment1: TSPL Assignment 1","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">Assignment1: TSPL Assignment 1</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/Assignment1.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/Assignment1/" class="Module">Assignment1</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.</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>submit tspl cw1 Assignment1.lagda.md
|
||
</code></pre></div></div>
|
||
<p>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="1249" class="Keyword">import</a> <a id="1256" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="1294" class="Symbol">as</a> <a id="1297" class="Module">Eq</a>
|
||
<a id="1300" class="Keyword">open</a> <a id="1305" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Eq</a> <a id="1308" class="Keyword">using</a> <a id="1314" class="Symbol">(</a><a id="1315" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="1318" class="Symbol">;</a> <a id="1320" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="1324" class="Symbol">;</a> <a id="1326" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a><a id="1330" class="Symbol">;</a> <a id="1332" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a><a id="1335" class="Symbol">)</a>
|
||
<a id="1337" class="Keyword">open</a> <a id="1342" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2499" class="Module">Eq.≡-Reasoning</a> <a id="1357" class="Keyword">using</a> <a id="1363" class="Symbol">(</a><a id="1364" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin_</a><a id="1370" class="Symbol">;</a> <a id="1372" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">_≡⟨⟩_</a><a id="1377" class="Symbol">;</a> <a id="1379" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">_≡⟨_⟩_</a><a id="1385" class="Symbol">;</a> <a id="1387" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">_∎</a><a id="1389" class="Symbol">)</a>
|
||
<a id="1391" class="Keyword">open</a> <a id="1396" class="Keyword">import</a> <a id="1403" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="1412" class="Keyword">using</a> <a id="1418" class="Symbol">(</a><a id="1419" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="1420" class="Symbol">;</a> <a id="1422" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="1426" class="Symbol">;</a> <a id="1428" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a><a id="1431" class="Symbol">;</a> <a id="1433" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a><a id="1436" class="Symbol">;</a> <a id="1438" href="Agda.Builtin.Nat.html#501" class="Primitive Operator">_*_</a><a id="1441" class="Symbol">;</a> <a id="1443" href="Agda.Builtin.Nat.html#388" class="Primitive Operator">_∸_</a><a id="1446" class="Symbol">;</a> <a id="1448" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#895" class="Datatype Operator">_≤_</a><a id="1451" class="Symbol">;</a> <a id="1453" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#918" class="InductiveConstructor">z≤n</a><a id="1456" class="Symbol">;</a> <a id="1458" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#960" class="InductiveConstructor">s≤s</a><a id="1461" class="Symbol">)</a>
|
||
<a id="1463" class="Keyword">open</a> <a id="1468" class="Keyword">import</a> <a id="1475" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="1495" class="Keyword">using</a> <a id="1501" class="Symbol">(</a><a id="1502" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11578" class="Function">+-assoc</a><a id="1509" class="Symbol">;</a> <a id="1511" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11734" class="Function">+-identityʳ</a><a id="1522" class="Symbol">;</a> <a id="1524" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11370" class="Function">+-suc</a><a id="1529" class="Symbol">;</a> <a id="1531" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911" class="Function">+-comm</a><a id="1537" class="Symbol">;</a>
|
||
<a id="1541" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#3632" class="Function">≤-refl</a><a id="1547" class="Symbol">;</a> <a id="1549" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#3815" class="Function">≤-trans</a><a id="1556" class="Symbol">;</a> <a id="1558" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#3682" class="Function">≤-antisym</a><a id="1567" class="Symbol">;</a> <a id="1569" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#3927" class="Function">≤-total</a><a id="1576" class="Symbol">;</a> <a id="1578" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#15619" class="Function">+-monoʳ-≤</a><a id="1587" class="Symbol">;</a> <a id="1589" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#15529" class="Function">+-monoˡ-≤</a><a id="1598" class="Symbol">;</a> <a id="1600" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#15373" class="Function">+-mono-≤</a><a id="1608" class="Symbol">)</a>
|
||
<a id="1610" class="Keyword">open</a> <a id="1615" class="Keyword">import</a> <a id="1622" href="/20.07/Relations/" class="Module">plfa.part1.Relations</a> <a id="1643" class="Keyword">using</a> <a id="1649" class="Symbol">(</a><a id="1650" href="/20.07/Relations/#18905" class="Datatype Operator">_<_</a><a id="1653" class="Symbol">;</a> <a id="1655" href="/20.07/Relations/#18932" class="InductiveConstructor">z<s</a><a id="1658" class="Symbol">;</a> <a id="1660" href="/20.07/Relations/#18989" class="InductiveConstructor">s<s</a><a id="1663" class="Symbol">;</a> <a id="1665" href="/20.07/Relations/#21658" class="InductiveConstructor">zero</a><a id="1669" class="Symbol">;</a> <a id="1671" href="/20.07/Relations/#21700" class="InductiveConstructor">suc</a><a id="1674" class="Symbol">;</a> <a id="1676" href="/20.07/Relations/#21603" class="Datatype">even</a><a id="1680" class="Symbol">;</a> <a id="1682" href="/20.07/Relations/#21623" class="Datatype">odd</a><a id="1685" class="Symbol">)</a>
|
||
</pre>
|
||
<h2 id="naturals">Naturals</h2>
|
||
|
||
<h4 id="seven">Exercise <code class="language-plaintext highlighter-rouge">seven</code> (practice)</h4>
|
||
|
||
<p>Write out <code class="language-plaintext highlighter-rouge">7</code> in longhand.</p>
|
||
|
||
<h4 id="plus-example">Exercise <code class="language-plaintext highlighter-rouge">+-example</code> (practice)</h4>
|
||
|
||
<p>Compute <code class="language-plaintext highlighter-rouge">3 + 4</code>, writing out your reasoning as a chain of equations.</p>
|
||
|
||
<h4 id="times-example">Exercise <code class="language-plaintext highlighter-rouge">*-example</code> (practice)</h4>
|
||
|
||
<p>Compute <code class="language-plaintext highlighter-rouge">3 * 4</code>, writing out your reasoning as a chain of equations.</p>
|
||
|
||
<h4 id="power">Exercise <code class="language-plaintext highlighter-rouge">_^_</code> (recommended)</h4>
|
||
|
||
<p>Define exponentiation, which is given by the following equations.</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>n ^ 0 = 1
|
||
n ^ (1 + m) = n * (n ^ m)
|
||
</code></pre></div></div>
|
||
|
||
<p>Check that <code class="language-plaintext highlighter-rouge">3 ^ 4</code> is <code class="language-plaintext highlighter-rouge">81</code>.</p>
|
||
|
||
<h4 id="monus-examples">Exercise <code class="language-plaintext highlighter-rouge">∸-examples</code> (recommended)</h4>
|
||
|
||
<p>Compute <code class="language-plaintext highlighter-rouge">5 ∸ 3</code> and <code class="language-plaintext highlighter-rouge">3 ∸ 5</code>, writing out your reasoning as a chain of equations.</p>
|
||
|
||
<h4 id="Bin">Exercise <code class="language-plaintext highlighter-rouge">Bin</code> (stretch)</h4>
|
||
|
||
<p>A more efficient representation of natural numbers uses a binary
|
||
rather than a unary system. We represent a number as a bitstring.</p>
|
||
<pre class="Agda"><a id="2541" class="Keyword">data</a> <a id="Bin"></a><a id="2546" href="/20.07/TSPL/2019/Assignment1/#2546" class="Datatype">Bin</a> <a id="2550" class="Symbol">:</a> <a id="2552" class="PrimitiveType">Set</a> <a id="2556" class="Keyword">where</a>
|
||
<a id="Bin.nil"></a><a id="2564" href="/20.07/TSPL/2019/Assignment1/#2564" class="InductiveConstructor">nil</a> <a id="2568" class="Symbol">:</a> <a id="2570" href="/20.07/TSPL/2019/Assignment1/#2546" class="Datatype">Bin</a>
|
||
<a id="Bin.x0_"></a><a id="2576" href="/20.07/TSPL/2019/Assignment1/#2576" class="InductiveConstructor Operator">x0_</a> <a id="2580" class="Symbol">:</a> <a id="2582" href="/20.07/TSPL/2019/Assignment1/#2546" class="Datatype">Bin</a> <a id="2586" class="Symbol">→</a> <a id="2588" href="/20.07/TSPL/2019/Assignment1/#2546" class="Datatype">Bin</a>
|
||
<a id="Bin.x1_"></a><a id="2594" href="/20.07/TSPL/2019/Assignment1/#2594" class="InductiveConstructor Operator">x1_</a> <a id="2598" class="Symbol">:</a> <a id="2600" href="/20.07/TSPL/2019/Assignment1/#2546" class="Datatype">Bin</a> <a id="2604" class="Symbol">→</a> <a id="2606" href="/20.07/TSPL/2019/Assignment1/#2546" class="Datatype">Bin</a>
|
||
</pre>
|
||
<p>For instance, the bitstring</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>1011
|
||
</code></pre></div></div>
|
||
|
||
<p>standing for the number eleven is encoded, right to left, as</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>x1 x1 x0 x1 nil
|
||
</code></pre></div></div>
|
||
|
||
<p>Representations are not unique due to leading zeros.
|
||
Hence, eleven is also represented by <code class="language-plaintext highlighter-rouge">001011</code>, encoded as</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>x1 x1 x0 x1 x0 x0 nil
|
||
</code></pre></div></div>
|
||
|
||
<p>Define a function</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>inc : Bin → Bin
|
||
</code></pre></div></div>
|
||
|
||
<p>that converts a bitstring to the bitstring for the next higher
|
||
number. For example, since <code class="language-plaintext highlighter-rouge">1100</code> encodes twelve, we should have</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
|
||
</code></pre></div></div>
|
||
|
||
<p>Confirm that this gives the correct answer for the bitstrings
|
||
encoding zero through four.</p>
|
||
|
||
<p>Using the above, define a pair of functions to convert
|
||
between the two representations.</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>to : ℕ → Bin
|
||
from : Bin → ℕ
|
||
</code></pre></div></div>
|
||
|
||
<p>For the former, choose the bitstring to have no leading zeros if it
|
||
represents a positive natural, and represent zero by <code class="language-plaintext highlighter-rouge">x0 nil</code>.
|
||
Confirm that these both give the correct answer for zero through four.</p>
|
||
|
||
<h2 id="induction">Induction</h2>
|
||
|
||
<h4 id="operators">Exercise <code class="language-plaintext highlighter-rouge">operators</code> (practice)</h4>
|
||
|
||
<p>Give another example of a pair of operators that have an identity
|
||
and are associative, commutative, and distribute over one another.</p>
|
||
|
||
<p>Give an example of an operator that has an identity and is
|
||
associative but is not commutative.</p>
|
||
|
||
<h4 id="finite-plus-assoc">Exercise <code class="language-plaintext highlighter-rouge">finite-+-assoc</code> (stretch)</h4>
|
||
|
||
<p>Write out what is known about associativity of addition on each of the first four
|
||
days using a finite story of creation, as
|
||
[earlier][plfa.Naturals#finite-creation]</p>
|
||
|
||
<h4 id="plus-swap">Exercise <code class="language-plaintext highlighter-rouge">+-swap</code> (recommended)</h4>
|
||
|
||
<p>Show</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + (n + p) ≡ n + (m + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>. No induction is needed,
|
||
just apply the previous results which show addition
|
||
is associative and commutative. You may need to use
|
||
the following function from the standard library:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>sym : ∀ {m n : ℕ} → m ≡ n → n ≡ m
|
||
</code></pre></div></div>
|
||
|
||
<h4 id="times-distrib-plus">Exercise <code class="language-plaintext highlighter-rouge">*-distrib-+</code> (recommended)</h4>
|
||
|
||
<p>Show multiplication distributes over addition, that is,</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(m + n) * p ≡ m * p + n * p
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>.</p>
|
||
|
||
<h4 id="times-assoc">Exercise <code class="language-plaintext highlighter-rouge">*-assoc</code> (recommended)</h4>
|
||
|
||
<p>Show multiplication is associative, that is,</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(m * n) * p ≡ m * (n * p)
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>.</p>
|
||
|
||
<h4 id="times-comm">Exercise <code class="language-plaintext highlighter-rouge">*-comm</code> (practice)</h4>
|
||
|
||
<p>Show multiplication is commutative, that is,</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m * n ≡ n * m
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>. As with commutativity of addition,
|
||
you will need to formulate and prove suitable lemmas.</p>
|
||
|
||
<h4 id="zero-monus">Exercise <code class="language-plaintext highlighter-rouge">0∸n≡0</code> (practice)</h4>
|
||
|
||
<p>Show</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>zero ∸ n ≡ zero
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">n</code>. Did your proof require induction?</p>
|
||
|
||
<h4 id="monus-plus-assoc">Exercise <code class="language-plaintext highlighter-rouge">∸-+-assoc</code> (practice)</h4>
|
||
|
||
<p>Show that monus associates with addition, that is,</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m ∸ n ∸ p ≡ m ∸ (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>.</p>
|
||
|
||
<h4 id="Bin-laws">Exercise <code class="language-plaintext highlighter-rouge">Bin-laws</code> (stretch)</h4>
|
||
|
||
<p>Recall that
|
||
Exercise [Bin][plfa.Naturals#Bin]
|
||
defines a datatype <code class="language-plaintext highlighter-rouge">Bin</code> of bitstrings representing natural numbers
|
||
and asks you to define functions</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>inc : Bin → Bin
|
||
to : ℕ → Bin
|
||
from : Bin → ℕ
|
||
</code></pre></div></div>
|
||
|
||
<p>Consider the following laws, where <code class="language-plaintext highlighter-rouge">n</code> ranges over naturals and <code class="language-plaintext highlighter-rouge">x</code>
|
||
over bitstrings.</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>from (inc x) ≡ suc (from x)
|
||
to (from n) ≡ n
|
||
from (to x) ≡ x
|
||
</code></pre></div></div>
|
||
|
||
<p>For each law: if it holds, prove; if not, give a counterexample.</p>
|
||
|
||
<h2 id="relations">Relations</h2>
|
||
|
||
<h4 id="orderings">Exercise <code class="language-plaintext highlighter-rouge">orderings</code> (practice)</h4>
|
||
|
||
<p>Give an example of a preorder that is not a partial order.</p>
|
||
|
||
<p>Give an example of a partial order that is not a preorder.</p>
|
||
|
||
<h4 id="leq-antisym-cases">Exercise <code class="language-plaintext highlighter-rouge">≤-antisym-cases</code> (practice)</h4>
|
||
|
||
<p>The above proof omits cases where one argument is <code class="language-plaintext highlighter-rouge">z≤n</code> and one
|
||
argument is <code class="language-plaintext highlighter-rouge">s≤s</code>. Why is it ok to omit them?</p>
|
||
|
||
<h4 id="exercise--mono--stretch">Exercise <code class="language-plaintext highlighter-rouge">*-mono-≤</code> (stretch)</h4>
|
||
|
||
<p>Show that multiplication is monotonic with regard to inequality.</p>
|
||
|
||
<h4 id="less-trans">Exercise <code class="language-plaintext highlighter-rouge"><-trans</code> (recommended)</h4>
|
||
|
||
<p>Show that strict inequality is transitive.</p>
|
||
|
||
<h4 id="trichotomy">Exercise <code class="language-plaintext highlighter-rouge">trichotomy</code> (practice)</h4>
|
||
|
||
<p>Show that strict inequality satisfies a weak version of trichotomy, in
|
||
the sense that for any <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code> that one of the following holds:</p>
|
||
<ul>
|
||
<li><code class="language-plaintext highlighter-rouge">m < n</code>,</li>
|
||
<li><code class="language-plaintext highlighter-rouge">m ≡ n</code>, or</li>
|
||
<li><code class="language-plaintext highlighter-rouge">m > n</code>
|
||
Define <code class="language-plaintext highlighter-rouge">m > n</code> to be the same as <code class="language-plaintext highlighter-rouge">n < m</code>.
|
||
You will need a suitable data declaration,
|
||
similar to that used for totality.
|
||
(We will show that the three cases are exclusive after we introduce
|
||
[negation][plfa.Negation].)</li>
|
||
</ul>
|
||
|
||
<h4 id="plus-mono-less">Exercise <code class="language-plaintext highlighter-rouge">+-mono-<</code></h4>
|
||
|
||
<p>Show that addition is monotonic with respect to strict inequality.
|
||
As with inequality, some additional definitions may be required.</p>
|
||
|
||
<h4 id="leq-iff-less">Exercise <code class="language-plaintext highlighter-rouge">≤-iff-<</code> (recommended)</h4>
|
||
|
||
<p>Show that <code class="language-plaintext highlighter-rouge">suc m ≤ n</code> implies <code class="language-plaintext highlighter-rouge">m < n</code>, and conversely.</p>
|
||
|
||
<h4 id="less-trans-revisited">Exercise <code class="language-plaintext highlighter-rouge"><-trans-revisited</code> (practice)</h4>
|
||
|
||
<p>Give an alternative proof that strict inequality is transitive,
|
||
using the relating between strict inequality and inequality and
|
||
the fact that inequality is transitive.</p>
|
||
|
||
<h4 id="odd-plus-odd">Exercise <code class="language-plaintext highlighter-rouge">o+o≡e</code> (stretch)</h4>
|
||
|
||
<p>Show that the sum of two odd numbers is even.</p>
|
||
|
||
<h4 id="Bin-predicates">Exercise <code class="language-plaintext highlighter-rouge">Bin-predicates</code> (stretch)</h4>
|
||
|
||
<p>Recall that
|
||
Exercise [Bin][plfa.Naturals#Bin]
|
||
defines a datatype <code class="language-plaintext highlighter-rouge">Bin</code> of bitstrings representing natural numbers.
|
||
Representations are not unique due to leading zeros.
|
||
Hence, eleven may be represented by both of the following</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>x1 x1 x0 x1 nil
|
||
x1 x1 x0 x1 x0 x0 nil
|
||
</code></pre></div></div>
|
||
|
||
<p>Define a predicate</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Can : Bin → Set
|
||
</code></pre></div></div>
|
||
|
||
<p>over all bitstrings that holds if the bitstring is canonical, meaning
|
||
it has no leading zeros; the first representation of eleven above is
|
||
canonical, and the second is not. To define it, you will need an
|
||
auxiliary predicate</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>One : Bin → Set
|
||
</code></pre></div></div>
|
||
|
||
<p>that holds only if the bistring has a leading one. A bitstring is
|
||
canonical if it has a leading one (representing a positive number) or
|
||
if it consists of a single zero (representing zero).</p>
|
||
|
||
<p>Show that increment preserves canonical bitstrings.</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Can x
|
||
------------
|
||
Can (inc x)
|
||
</code></pre></div></div>
|
||
|
||
<p>Show that converting a natural to a bitstring always yields a
|
||
canonical bitstring.</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>----------
|
||
Can (to n)
|
||
</code></pre></div></div>
|
||
|
||
<p>Show that converting a canonical bitstring to a natural
|
||
and back is the identity.</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Can x
|
||
---------------
|
||
to (from x) ≡ x
|
||
</code></pre></div></div>
|
||
|
||
<p>(Hint: For each of these, you may first need to prove related
|
||
properties of <code class="language-plaintext highlighter-rouge">One</code>.)</p>
|
||
|
||
</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/Assignment1.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>
|