367 lines
41 KiB
HTML
367 lines
41 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: PUC 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: PUC 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/PUC/2019/Assignment3/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/PUC/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/PUC/2019/Assignment3/","headline":"Assignment3: PUC 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: PUC 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/puc/2019/Assignment3.lagda.md">Source</a>
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<pre class="Agda"><a id="110" class="Keyword">module</a> <a id="117" href="/20.07/PUC/2019/Assignment3/" class="Module">Assignment3</a> <a id="129" 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 without a label are optional, and may be done if you want
|
||
some extra practice.</p>
|
||
|
||
<p>Please ensure your files execute correctly under Agda!</p>
|
||
|
||
<h2 id="imports">Imports</h2>
|
||
|
||
<pre class="Agda"><a id="555" class="Keyword">import</a> <a id="562" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="600" class="Symbol">as</a> <a id="603" class="Module">Eq</a>
|
||
<a id="606" class="Keyword">open</a> <a id="611" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Eq</a> <a id="614" class="Keyword">using</a> <a id="620" class="Symbol">(</a><a id="621" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="624" class="Symbol">;</a> <a id="626" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="630" class="Symbol">;</a> <a id="632" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a><a id="636" class="Symbol">;</a> <a id="638" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a><a id="641" class="Symbol">)</a>
|
||
<a id="643" class="Keyword">open</a> <a id="648" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2499" class="Module">Eq.≡-Reasoning</a> <a id="663" class="Keyword">using</a> <a id="669" class="Symbol">(</a><a id="670" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin_</a><a id="676" class="Symbol">;</a> <a id="678" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">_≡⟨⟩_</a><a id="683" class="Symbol">;</a> <a id="685" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">_≡⟨_⟩_</a><a id="691" class="Symbol">;</a> <a id="693" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">_∎</a><a id="695" class="Symbol">)</a>
|
||
<a id="697" class="Keyword">open</a> <a id="702" class="Keyword">import</a> <a id="709" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html" class="Module">Data.Bool.Base</a> <a id="724" class="Keyword">using</a> <a id="730" class="Symbol">(</a><a id="731" href="Agda.Builtin.Bool.html#135" class="Datatype">Bool</a><a id="735" class="Symbol">;</a> <a id="737" href="Agda.Builtin.Bool.html#160" class="InductiveConstructor">true</a><a id="741" class="Symbol">;</a> <a id="743" href="Agda.Builtin.Bool.html#154" class="InductiveConstructor">false</a><a id="748" class="Symbol">;</a> <a id="750" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#1480" class="Function">T</a><a id="751" class="Symbol">;</a> <a id="753" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#1015" class="Function Operator">_∧_</a><a id="756" class="Symbol">;</a> <a id="758" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#1073" class="Function Operator">_∨_</a><a id="761" class="Symbol">;</a> <a id="763" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#961" class="Function">not</a><a id="766" class="Symbol">)</a>
|
||
<a id="768" class="Keyword">open</a> <a id="773" class="Keyword">import</a> <a id="780" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="789" class="Keyword">using</a> <a id="795" class="Symbol">(</a><a id="796" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="797" class="Symbol">;</a> <a id="799" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="803" class="Symbol">;</a> <a id="805" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a><a id="808" class="Symbol">;</a> <a id="810" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a><a id="813" class="Symbol">;</a> <a id="815" href="Agda.Builtin.Nat.html#501" class="Primitive Operator">_*_</a><a id="818" class="Symbol">;</a> <a id="820" href="Agda.Builtin.Nat.html#388" class="Primitive Operator">_∸_</a><a id="823" class="Symbol">;</a> <a id="825" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#895" class="Datatype Operator">_≤_</a><a id="828" class="Symbol">;</a> <a id="830" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#960" class="InductiveConstructor">s≤s</a><a id="833" class="Symbol">;</a> <a id="835" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#918" class="InductiveConstructor">z≤n</a><a id="838" class="Symbol">)</a>
|
||
<a id="840" class="Keyword">open</a> <a id="845" class="Keyword">import</a> <a id="852" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="872" class="Keyword">using</a>
|
||
<a id="880" class="Symbol">(</a><a id="881" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11578" class="Function">+-assoc</a><a id="888" class="Symbol">;</a> <a id="890" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11679" class="Function">+-identityˡ</a><a id="901" class="Symbol">;</a> <a id="903" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11734" class="Function">+-identityʳ</a><a id="914" class="Symbol">;</a> <a id="916" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#18464" class="Function">*-assoc</a><a id="923" class="Symbol">;</a> <a id="925" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#17362" class="Function">*-identityˡ</a><a id="936" class="Symbol">;</a> <a id="938" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#17426" class="Function">*-identityʳ</a><a id="949" class="Symbol">)</a>
|
||
<a id="951" class="Keyword">open</a> <a id="956" class="Keyword">import</a> <a id="963" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="980" class="Keyword">using</a> <a id="986" class="Symbol">(</a><a id="987" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬_</a><a id="989" class="Symbol">;</a> <a id="991" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a><a id="994" class="Symbol">;</a> <a id="996" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a><a id="999" class="Symbol">;</a> <a id="1001" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a><a id="1003" class="Symbol">)</a>
|
||
<a id="1005" class="Keyword">open</a> <a id="1010" class="Keyword">import</a> <a id="1017" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html" class="Module">Data.Product</a> <a id="1030" class="Keyword">using</a> <a id="1036" class="Symbol">(</a><a id="1037" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">_×_</a><a id="1040" class="Symbol">;</a> <a id="1042" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1364" class="Function">∃</a><a id="1043" class="Symbol">;</a> <a id="1045" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃-syntax</a><a id="1053" class="Symbol">)</a> <a id="1055" class="Keyword">renaming</a> <a id="1064" class="Symbol">(</a><a id="1065" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">_,_</a> <a id="1069" class="Symbol">to</a> <a id="1072" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨_,_⟩</a><a id="1077" class="Symbol">)</a>
|
||
<a id="1079" class="Keyword">open</a> <a id="1084" class="Keyword">import</a> <a id="1091" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html" class="Module">Data.Empty</a> <a id="1102" class="Keyword">using</a> <a id="1108" class="Symbol">(</a><a id="1109" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a><a id="1110" class="Symbol">;</a> <a id="1112" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a><a id="1118" class="Symbol">)</a>
|
||
<a id="1120" class="Keyword">open</a> <a id="1125" class="Keyword">import</a> <a id="1132" href="https://agda.github.io/agda-stdlib/v1.1/Function.html" class="Module">Function</a> <a id="1141" class="Keyword">using</a> <a id="1147" class="Symbol">(</a><a id="1148" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">_∘_</a><a id="1151" class="Symbol">)</a>
|
||
<a id="1153" class="Keyword">open</a> <a id="1158" class="Keyword">import</a> <a id="1165" href="https://agda.github.io/agda-stdlib/v1.1/Algebra.Structures.html" class="Module">Algebra.Structures</a> <a id="1184" class="Keyword">using</a> <a id="1190" class="Symbol">(</a><a id="1191" href="https://agda.github.io/agda-stdlib/v1.1/Algebra.Structures.html#2215" class="Record">IsMonoid</a><a id="1199" class="Symbol">)</a>
|
||
<a id="1201" class="Keyword">open</a> <a id="1206" class="Keyword">import</a> <a id="1213" href="https://agda.github.io/agda-stdlib/v1.1/Level.html" class="Module">Level</a> <a id="1219" class="Keyword">using</a> <a id="1225" class="Symbol">(</a><a id="1226" href="Agda.Primitive.html#408" class="Postulate">Level</a><a id="1231" class="Symbol">)</a>
|
||
<a id="1233" class="Keyword">open</a> <a id="1238" class="Keyword">import</a> <a id="1245" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Unary.html" class="Module">Relation.Unary</a> <a id="1260" class="Keyword">using</a> <a id="1266" class="Symbol">(</a><a id="1267" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Unary.html#3474" class="Function">Decidable</a><a id="1276" class="Symbol">)</a>
|
||
<a id="1278" class="Keyword">open</a> <a id="1283" class="Keyword">import</a> <a id="1290" href="/20.07/Relations/" class="Module">plfa.part1.Relations</a> <a id="1311" class="Keyword">using</a> <a id="1317" class="Symbol">(</a><a id="1318" href="/20.07/Relations/#18905" class="Datatype Operator">_<_</a><a id="1321" class="Symbol">;</a> <a id="1323" href="/20.07/Relations/#18932" class="InductiveConstructor">z<s</a><a id="1326" class="Symbol">;</a> <a id="1328" href="/20.07/Relations/#18989" class="InductiveConstructor">s<s</a><a id="1331" class="Symbol">)</a>
|
||
<a id="1333" class="Keyword">open</a> <a id="1338" class="Keyword">import</a> <a id="1345" href="/20.07/Isomorphism/" class="Module">plfa.part1.Isomorphism</a> <a id="1368" class="Keyword">using</a> <a id="1374" class="Symbol">(</a><a id="1375" href="/20.07/Isomorphism/#4365" class="Record Operator">_≃_</a><a id="1378" class="Symbol">;</a> <a id="1380" href="/20.07/Isomorphism/#7107" class="Function">≃-sym</a><a id="1385" class="Symbol">;</a> <a id="1387" href="/20.07/Isomorphism/#7432" class="Function">≃-trans</a><a id="1394" class="Symbol">;</a> <a id="1396" href="/20.07/Isomorphism/#9281" class="Record Operator">_≲_</a><a id="1399" class="Symbol">;</a> <a id="1401" href="/20.07/Isomorphism/#2684" class="Postulate">extensionality</a><a id="1415" class="Symbol">)</a>
|
||
<a id="1417" class="Keyword">open</a> <a id="1422" href="/20.07/Isomorphism/#8516" class="Module">plfa.part1.Isomorphism.≃-Reasoning</a>
|
||
<a id="1457" class="Keyword">open</a> <a id="1462" class="Keyword">import</a> <a id="1469" href="/20.07/Lists/" class="Module">plfa.part1.Lists</a> <a id="1486" class="Keyword">using</a> <a id="1492" class="Symbol">(</a><a id="1493" href="/20.07/Lists/#1067" class="Datatype">List</a><a id="1497" class="Symbol">;</a> <a id="1499" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="1501" class="Symbol">;</a> <a id="1503" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">_∷_</a><a id="1506" class="Symbol">;</a> <a id="1508" href="/20.07/Lists/#2827" class="Operator">[_]</a><a id="1511" class="Symbol">;</a> <a id="1513" href="/20.07/Lists/#2850" class="Operator">[_,_]</a><a id="1518" class="Symbol">;</a> <a id="1520" href="/20.07/Lists/#2881" class="Operator">[_,_,_]</a><a id="1527" class="Symbol">;</a> <a id="1529" href="/20.07/Lists/#2920" class="Operator">[_,_,_,_]</a><a id="1538" class="Symbol">;</a>
|
||
<a id="1542" href="/20.07/Lists/#3467" class="Function Operator">_++_</a><a id="1546" class="Symbol">;</a> <a id="1548" href="/20.07/Lists/#8318" class="Function">reverse</a><a id="1555" class="Symbol">;</a> <a id="1557" href="/20.07/Lists/#12865" class="Function">map</a><a id="1560" class="Symbol">;</a> <a id="1562" href="/20.07/Lists/#15291" class="Function">foldr</a><a id="1567" class="Symbol">;</a> <a id="1569" href="/20.07/Lists/#16254" class="Function">sum</a><a id="1572" class="Symbol">;</a> <a id="1574" href="/20.07/Lists/#21529" class="Datatype">All</a><a id="1577" class="Symbol">;</a> <a id="1579" href="/20.07/Lists/#22982" class="Datatype">Any</a><a id="1582" class="Symbol">;</a> <a id="1584" href="/20.07/Lists/#23033" class="InductiveConstructor">here</a><a id="1588" class="Symbol">;</a> <a id="1590" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a><a id="1595" class="Symbol">;</a> <a id="1597" href="/20.07/Lists/#23404" class="Function Operator">_∈_</a><a id="1600" class="Symbol">)</a>
|
||
<a id="1602" class="Keyword">open</a> <a id="1607" class="Keyword">import</a> <a id="1614" href="/20.07/Lambda/" class="Module">plfa.part2.Lambda</a> <a id="1632" class="Keyword">hiding</a> <a id="1639" class="Symbol">(</a><a id="1640" href="/20.07/Lambda/#7592" class="Function Operator">ƛ′_⇒_</a><a id="1645" class="Symbol">;</a> <a id="1647" href="/20.07/Lambda/#7713" class="Function Operator">case′_[zero⇒_|suc_⇒_]</a><a id="1668" class="Symbol">;</a> <a id="1670" href="/20.07/Lambda/#7927" class="Function Operator">μ′_⇒_</a><a id="1675" class="Symbol">;</a> <a id="1677" href="/20.07/Lambda/#8681" class="Function">plus′</a><a id="1682" class="Symbol">)</a>
|
||
<a id="1684" class="Keyword">open</a> <a id="1689" class="Keyword">import</a> <a id="1696" href="/20.07/Properties/" class="Module">plfa.part2.Properties</a> <a id="1718" class="Keyword">hiding</a> <a id="1725" class="Symbol">(</a><a id="1726" href="/20.07/Properties/#11767" class="Postulate">value?</a><a id="1732" class="Symbol">;</a> <a id="1734" href="/20.07/Properties/#42067" class="Postulate">unstuck</a><a id="1741" class="Symbol">;</a> <a id="1743" href="/20.07/Properties/#42267" class="Postulate">preserves</a><a id="1752" class="Symbol">;</a> <a id="1754" href="/20.07/Properties/#42504" class="Postulate">wttdgs</a><a id="1760" 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.</p>
|
||
|
||
<h4 id="exercise-primed-stretch">Exercise <code class="language-plaintext highlighter-rouge">primed</code> (stretch)</h4>
|
||
|
||
<p>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="2033" href="/20.07/PUC/2019/Assignment3/#2033" class="Function Operator">ƛ′_⇒_</a> <a id="2039" class="Symbol">:</a> <a id="2041" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="2046" class="Symbol">→</a> <a id="2048" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="2053" class="Symbol">→</a> <a id="2055" href="/20.07/Lambda/#4005" class="Datatype">Term</a>
|
||
<a id="2060" href="/20.07/PUC/2019/Assignment3/#2033" class="Function Operator">ƛ′</a> <a id="2063" class="Symbol">(</a><a id="2064" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="2066" href="/20.07/PUC/2019/Assignment3/#2066" class="Bound">x</a><a id="2067" class="Symbol">)</a> <a id="2069" href="/20.07/PUC/2019/Assignment3/#2033" class="Function Operator">⇒</a> <a id="2071" href="/20.07/PUC/2019/Assignment3/#2071" class="Bound">N</a> <a id="2074" class="Symbol">=</a> <a id="2077" href="/20.07/Lambda/#4063" class="InductiveConstructor Operator">ƛ</a> <a id="2079" href="/20.07/PUC/2019/Assignment3/#2066" class="Bound">x</a> <a id="2081" href="/20.07/Lambda/#4063" class="InductiveConstructor Operator">⇒</a> <a id="2083" href="/20.07/PUC/2019/Assignment3/#2071" class="Bound">N</a>
|
||
<a id="2085" href="/20.07/PUC/2019/Assignment3/#2033" class="CatchallClause Function Operator">ƛ′</a><a id="2087" class="CatchallClause"> </a><a id="2088" class="CatchallClause Symbol">_</a><a id="2089" class="CatchallClause"> </a><a id="2090" href="/20.07/PUC/2019/Assignment3/#2033" class="CatchallClause Function Operator">⇒</a><a id="2091" class="CatchallClause"> </a><a id="2092" class="CatchallClause Symbol">_</a> <a id="2099" class="Symbol">=</a> <a id="2102" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="2109" href="/20.07/PUC/2019/Assignment3/#2138" class="Postulate">impossible</a>
|
||
<a id="2122" class="Keyword">where</a> <a id="2128" class="Keyword">postulate</a> <a id="2138" href="/20.07/PUC/2019/Assignment3/#2138" class="Postulate">impossible</a> <a id="2149" class="Symbol">:</a> <a id="2151" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a>
|
||
|
||
<a id="case′_[zero⇒_|suc_⇒_]"></a><a id="2154" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">case′_[zero⇒_|suc_⇒_]</a> <a id="2176" class="Symbol">:</a> <a id="2178" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="2183" class="Symbol">→</a> <a id="2185" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="2190" class="Symbol">→</a> <a id="2192" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="2197" class="Symbol">→</a> <a id="2199" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="2204" class="Symbol">→</a> <a id="2206" href="/20.07/Lambda/#4005" class="Datatype">Term</a>
|
||
<a id="2211" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">case′</a> <a id="2217" href="/20.07/PUC/2019/Assignment3/#2217" class="Bound">L</a> <a id="2219" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">[zero⇒</a> <a id="2226" href="/20.07/PUC/2019/Assignment3/#2226" class="Bound">M</a> <a id="2228" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">|suc</a> <a id="2233" class="Symbol">(</a><a id="2234" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="2236" href="/20.07/PUC/2019/Assignment3/#2236" class="Bound">x</a><a id="2237" class="Symbol">)</a> <a id="2239" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">⇒</a> <a id="2241" href="/20.07/PUC/2019/Assignment3/#2241" class="Bound">N</a> <a id="2243" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">]</a> <a id="2246" class="Symbol">=</a> <a id="2249" href="/20.07/Lambda/#4232" class="InductiveConstructor Operator">case</a> <a id="2254" href="/20.07/PUC/2019/Assignment3/#2217" class="Bound">L</a> <a id="2256" href="/20.07/Lambda/#4232" class="InductiveConstructor Operator">[zero⇒</a> <a id="2263" href="/20.07/PUC/2019/Assignment3/#2226" class="Bound">M</a> <a id="2265" href="/20.07/Lambda/#4232" class="InductiveConstructor Operator">|suc</a> <a id="2270" href="/20.07/PUC/2019/Assignment3/#2236" class="Bound">x</a> <a id="2272" href="/20.07/Lambda/#4232" class="InductiveConstructor Operator">⇒</a> <a id="2274" href="/20.07/PUC/2019/Assignment3/#2241" class="Bound">N</a> <a id="2276" href="/20.07/Lambda/#4232" class="InductiveConstructor Operator">]</a>
|
||
<a id="2278" href="/20.07/PUC/2019/Assignment3/#2154" class="CatchallClause Function Operator">case′</a><a id="2283" class="CatchallClause"> </a><a id="2284" class="CatchallClause Symbol">_</a><a id="2285" class="CatchallClause"> </a><a id="2286" href="/20.07/PUC/2019/Assignment3/#2154" class="CatchallClause Function Operator">[zero⇒</a><a id="2292" class="CatchallClause"> </a><a id="2293" class="CatchallClause Symbol">_</a><a id="2294" class="CatchallClause"> </a><a id="2295" href="/20.07/PUC/2019/Assignment3/#2154" class="CatchallClause Function Operator">|suc</a><a id="2299" class="CatchallClause"> </a><a id="2300" class="CatchallClause Symbol">_</a><a id="2301" class="CatchallClause"> </a><a id="2302" href="/20.07/PUC/2019/Assignment3/#2154" class="CatchallClause Function Operator">⇒</a><a id="2303" class="CatchallClause"> </a><a id="2304" class="CatchallClause Symbol">_</a><a id="2305" class="CatchallClause"> </a><a id="2306" href="/20.07/PUC/2019/Assignment3/#2154" class="CatchallClause Function Operator">]</a> <a id="2313" class="Symbol">=</a> <a id="2316" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="2323" href="/20.07/PUC/2019/Assignment3/#2352" class="Postulate">impossible</a>
|
||
<a id="2336" class="Keyword">where</a> <a id="2342" class="Keyword">postulate</a> <a id="2352" href="/20.07/PUC/2019/Assignment3/#2352" class="Postulate">impossible</a> <a id="2363" class="Symbol">:</a> <a id="2365" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a>
|
||
|
||
<a id="μ′_⇒_"></a><a id="2368" href="/20.07/PUC/2019/Assignment3/#2368" class="Function Operator">μ′_⇒_</a> <a id="2374" class="Symbol">:</a> <a id="2376" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="2381" class="Symbol">→</a> <a id="2383" href="/20.07/Lambda/#4005" class="Datatype">Term</a> <a id="2388" class="Symbol">→</a> <a id="2390" href="/20.07/Lambda/#4005" class="Datatype">Term</a>
|
||
<a id="2395" href="/20.07/PUC/2019/Assignment3/#2368" class="Function Operator">μ′</a> <a id="2398" class="Symbol">(</a><a id="2399" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="2401" href="/20.07/PUC/2019/Assignment3/#2401" class="Bound">x</a><a id="2402" class="Symbol">)</a> <a id="2404" href="/20.07/PUC/2019/Assignment3/#2368" class="Function Operator">⇒</a> <a id="2406" href="/20.07/PUC/2019/Assignment3/#2406" class="Bound">N</a> <a id="2409" class="Symbol">=</a> <a id="2412" href="/20.07/Lambda/#4292" class="InductiveConstructor Operator">μ</a> <a id="2414" href="/20.07/PUC/2019/Assignment3/#2401" class="Bound">x</a> <a id="2416" href="/20.07/Lambda/#4292" class="InductiveConstructor Operator">⇒</a> <a id="2418" href="/20.07/PUC/2019/Assignment3/#2406" class="Bound">N</a>
|
||
<a id="2420" href="/20.07/PUC/2019/Assignment3/#2368" class="CatchallClause Function Operator">μ′</a><a id="2422" class="CatchallClause"> </a><a id="2423" class="CatchallClause Symbol">_</a><a id="2424" class="CatchallClause"> </a><a id="2425" href="/20.07/PUC/2019/Assignment3/#2368" class="CatchallClause Function Operator">⇒</a><a id="2426" class="CatchallClause"> </a><a id="2427" class="CatchallClause Symbol">_</a> <a id="2434" class="Symbol">=</a> <a id="2437" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="2444" href="/20.07/PUC/2019/Assignment3/#2473" class="Postulate">impossible</a>
|
||
<a id="2457" class="Keyword">where</a> <a id="2463" class="Keyword">postulate</a> <a id="2473" href="/20.07/PUC/2019/Assignment3/#2473" class="Postulate">impossible</a> <a id="2484" class="Symbol">:</a> <a id="2486" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a>
|
||
</pre>
|
||
<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="2552" href="/20.07/PUC/2019/Assignment3/#2552" class="Function">plus′</a> <a id="2558" class="Symbol">:</a> <a id="2560" href="/20.07/Lambda/#4005" class="Datatype">Term</a>
|
||
<a id="2565" href="/20.07/PUC/2019/Assignment3/#2552" class="Function">plus′</a> <a id="2571" class="Symbol">=</a> <a id="2573" href="/20.07/PUC/2019/Assignment3/#2368" class="Function Operator">μ′</a> <a id="2576" href="/20.07/PUC/2019/Assignment3/#2683" class="Function">+</a> <a id="2578" href="/20.07/PUC/2019/Assignment3/#2368" class="Function Operator">⇒</a> <a id="2580" href="/20.07/PUC/2019/Assignment3/#2033" class="Function Operator">ƛ′</a> <a id="2583" href="/20.07/PUC/2019/Assignment3/#2697" class="Function">m</a> <a id="2585" href="/20.07/PUC/2019/Assignment3/#2033" class="Function Operator">⇒</a> <a id="2587" href="/20.07/PUC/2019/Assignment3/#2033" class="Function Operator">ƛ′</a> <a id="2590" href="/20.07/PUC/2019/Assignment3/#2711" class="Function">n</a> <a id="2592" href="/20.07/PUC/2019/Assignment3/#2033" class="Function Operator">⇒</a>
|
||
<a id="2604" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">case′</a> <a id="2610" href="/20.07/PUC/2019/Assignment3/#2697" class="Function">m</a>
|
||
<a id="2624" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">[zero⇒</a> <a id="2631" href="/20.07/PUC/2019/Assignment3/#2711" class="Function">n</a>
|
||
<a id="2645" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">|suc</a> <a id="2650" href="/20.07/PUC/2019/Assignment3/#2697" class="Function">m</a> <a id="2652" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">⇒</a> <a id="2654" href="/20.07/Lambda/#4191" class="InductiveConstructor Operator">`suc</a> <a id="2659" class="Symbol">(</a><a id="2660" href="/20.07/PUC/2019/Assignment3/#2683" class="Function">+</a> <a id="2662" href="/20.07/Lambda/#4109" class="InductiveConstructor Operator">·</a> <a id="2664" href="/20.07/PUC/2019/Assignment3/#2697" class="Function">m</a> <a id="2666" href="/20.07/Lambda/#4109" class="InductiveConstructor Operator">·</a> <a id="2668" href="/20.07/PUC/2019/Assignment3/#2711" class="Function">n</a><a id="2669" class="Symbol">)</a> <a id="2671" href="/20.07/PUC/2019/Assignment3/#2154" class="Function Operator">]</a>
|
||
<a id="2675" class="Keyword">where</a>
|
||
<a id="2683" href="/20.07/PUC/2019/Assignment3/#2683" class="Function">+</a> <a id="2686" class="Symbol">=</a> <a id="2689" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="2691" class="String">"+"</a>
|
||
<a id="2697" href="/20.07/PUC/2019/Assignment3/#2697" class="Function">m</a> <a id="2700" class="Symbol">=</a> <a id="2703" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="2705" class="String">"m"</a>
|
||
<a id="2711" href="/20.07/PUC/2019/Assignment3/#2711" class="Function">n</a> <a id="2714" class="Symbol">=</a> <a id="2717" href="/20.07/Lambda/#4024" class="InductiveConstructor Operator">`</a> <a id="2719" 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 with 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>
|
||
|
||
<h4 id="exercise-">Exercise <code class="language-plaintext highlighter-rouge">—↠≲—↠′</code></h4>
|
||
|
||
<p>Show that the first notion of reflexive and transitive closure
|
||
above embeds into the second. Why are they not isomorphic?</p>
|
||
|
||
<h4 id="exercise-plus-example">Exercise <code class="language-plaintext highlighter-rouge">plus-example</code></h4>
|
||
|
||
<p>Write out the reduction sequence demonstrating that one plus one is two.</p>
|
||
|
||
<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>
|
||
|
||
<h2 id="properties">Properties</h2>
|
||
|
||
<h4 id="exercise-progress-">Exercise <code class="language-plaintext highlighter-rouge">Progress-≃</code></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>
|
||
|
||
<h4 id="exercise-progress">Exercise <code class="language-plaintext highlighter-rouge">progress′</code></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>
|
||
|
||
<h4 id="exercise-value">Exercise <code class="language-plaintext highlighter-rouge">value?</code></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="3862" class="Keyword">postulate</a>
|
||
<a id="value?"></a><a id="3874" href="/20.07/PUC/2019/Assignment3/#3874" class="Postulate">value?</a> <a id="3881" class="Symbol">:</a> <a id="3883" class="Symbol">∀</a> <a id="3885" class="Symbol">{</a><a id="3886" href="/20.07/PUC/2019/Assignment3/#3886" class="Bound">A</a> <a id="3888" href="/20.07/PUC/2019/Assignment3/#3888" class="Bound">M</a><a id="3889" class="Symbol">}</a> <a id="3891" class="Symbol">→</a> <a id="3893" href="/20.07/Lambda/#31868" class="InductiveConstructor">∅</a> <a id="3895" href="/20.07/Lambda/#34792" class="Datatype Operator">⊢</a> <a id="3897" href="/20.07/PUC/2019/Assignment3/#3888" class="Bound">M</a> <a id="3899" href="/20.07/Lambda/#34792" class="Datatype Operator">⦂</a> <a id="3901" href="/20.07/PUC/2019/Assignment3/#3886" class="Bound">A</a> <a id="3903" class="Symbol">→</a> <a id="3905" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a> <a id="3909" class="Symbol">(</a><a id="3910" href="/20.07/Lambda/#12384" class="Datatype">Value</a> <a id="3916" href="/20.07/PUC/2019/Assignment3/#3888" class="Bound">M</a><a id="3917" 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>
|
||
|
||
<h4 id="exercise-mul-example-recommended">Exercise <code class="language-plaintext highlighter-rouge">mul-example</code> (recommended)</h4>
|
||
|
||
<p>Using the evaluator, confirm that two times two is four.</p>
|
||
|
||
<h4 id="exercise-progress-preservation">Exercise: <code class="language-plaintext highlighter-rouge">progress-preservation</code></h4>
|
||
|
||
<p>Without peeking at their statements above, write down the progress
|
||
and preservation theorems for the simply typed lambda-calculus.</p>
|
||
|
||
<h4 id="exercise-subject-expansion">Exercise <code class="language-plaintext highlighter-rouge">subject-expansion</code></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>,
|
||
and conversely that <code class="language-plaintext highlighter-rouge">M</code> <em>expands</em> to <code class="language-plaintext highlighter-rouge">N</code> if <code class="language-plaintext highlighter-rouge">N —→ 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>
|
||
|
||
<h4 id="exercise-stuck">Exercise <code class="language-plaintext highlighter-rouge">stuck</code></h4>
|
||
|
||
<p>Give an example of an ill-typed term that does get stuck.</p>
|
||
|
||
<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>
|
||
|
||
</div>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/courses/puc/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>
|