731 lines
170 KiB
HTML
731 lines
170 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>Compositional: The denotational semantics is compositional 🚧 | 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="Compositional: The denotational semantics is compositional 🚧" />
|
||
<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/19.08/Compositional/" />
|
||
<meta property="og:url" content="https://plfa.github.io/19.08/Compositional/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/19.08/Compositional/","headline":"Compositional: The denotational semantics is compositional 🚧","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
|
||
<!-- End Jekyll SEO tag -->
|
||
<link rel="stylesheet" href="/19.08/assets/main.css"></head>
|
||
<body><header class="site-header" role="banner">
|
||
|
||
<div class="wrapper">
|
||
|
||
<a class="site-title" href="/19.08/">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="/19.08/">The Book</a>
|
||
<a class="page-link" href="/19.08/Announcements/">Announcements</a>
|
||
<a class="page-link" href="/19.08/GettingStarted/">Getting Started</a>
|
||
<a class="page-link" href="/19.08/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">Compositional: The denotational semantics is compositional 🚧</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
<a alt="Previous chapter" href="/19.08/Denotational/">Prev</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part3/Compositional.lagda.md">Source</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Next chapter" href="/19.08/Soundness/">Next</a>
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<pre class="Agda"><a id="185" class="Keyword">module</a> <a id="192" href="/19.08/Compositional/" class="Module">plfa.part3.Compositional</a> <a id="217" class="Keyword">where</a>
|
||
</pre>
|
||
<h2 id="introduction">Introduction</h2>
|
||
|
||
<p>In this chapter we prove that the denotational semantics is compositional,
|
||
which means we fill in the ellipses in the following equations.</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ℰ (` x) ≃ ...
|
||
ℰ (ƛ M) ≃ ... ℰ M ...
|
||
ℰ (M · N) ≃ ... ℰ M ... ℰ N ...
|
||
</code></pre></div></div>
|
||
|
||
<p>Such equations would imply that the denotational semantics could be
|
||
instead defined as a recursive function. Indeed, we end this chapter
|
||
with such a definition and prove that it is equivalent to ℰ.</p>
|
||
|
||
<h2 id="imports">Imports</h2>
|
||
|
||
<pre class="Agda"><a id="682" class="Keyword">open</a> <a id="687" class="Keyword">import</a> <a id="694" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html" class="Module">Data.Product</a> <a id="707" class="Keyword">using</a> <a id="713" class="Symbol">(</a><a id="714" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">_×_</a><a id="717" class="Symbol">;</a> <a id="719" href="Agda.Builtin.Sigma.html#139" class="Record">Σ</a><a id="720" class="Symbol">;</a> <a id="722" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ-syntax</a><a id="730" class="Symbol">;</a> <a id="732" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1364" class="Function">∃</a><a id="733" class="Symbol">;</a> <a id="735" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃-syntax</a><a id="743" class="Symbol">;</a> <a id="745" href="Agda.Builtin.Sigma.html#225" class="Field">proj₁</a><a id="750" class="Symbol">;</a> <a id="752" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a><a id="757" class="Symbol">)</a>
|
||
<a id="761" class="Keyword">renaming</a> <a id="770" class="Symbol">(</a><a id="771" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">_,_</a> <a id="775" class="Symbol">to</a> <a id="778" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨_,_⟩</a><a id="783" class="Symbol">)</a>
|
||
<a id="785" class="Keyword">open</a> <a id="790" class="Keyword">import</a> <a id="797" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.html" class="Module">Data.Sum</a> <a id="806" class="Keyword">using</a> <a id="812" class="Symbol">(</a><a id="813" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#612" class="Datatype Operator">_⊎_</a><a id="816" class="Symbol">;</a> <a id="818" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a><a id="822" class="Symbol">;</a> <a id="824" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a><a id="828" class="Symbol">)</a>
|
||
<a id="830" class="Keyword">open</a> <a id="835" class="Keyword">import</a> <a id="842" href="https://agda.github.io/agda-stdlib/v1.1/Data.Unit.html" class="Module">Data.Unit</a> <a id="852" class="Keyword">using</a> <a id="858" class="Symbol">(</a><a id="859" href="Agda.Builtin.Unit.html#137" class="Record">⊤</a><a id="860" class="Symbol">;</a> <a id="862" href="Agda.Builtin.Unit.html#174" class="InductiveConstructor">tt</a><a id="864" class="Symbol">)</a>
|
||
<a id="866" class="Keyword">open</a> <a id="871" class="Keyword">import</a> <a id="878" href="/19.08/Untyped/" class="Module">plfa.part2.Untyped</a>
|
||
<a id="899" class="Keyword">using</a> <a id="905" class="Symbol">(</a><a id="906" href="/19.08/Untyped/#3153" class="Datatype">Context</a><a id="913" class="Symbol">;</a> <a id="915" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">_,_</a><a id="918" class="Symbol">;</a> <a id="920" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="921" class="Symbol">;</a> <a id="923" href="plfa.part2.Untyped.html#3521" class="Datatype Operator">_∋_</a><a id="926" class="Symbol">;</a> <a id="928" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">_⊢_</a><a id="931" class="Symbol">;</a> <a id="933" href="plfa.part2.Untyped.html#4330" class="InductiveConstructor Operator">`_</a><a id="935" class="Symbol">;</a> <a id="937" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ_</a><a id="939" class="Symbol">;</a> <a id="941" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">_·_</a><a id="944" class="Symbol">)</a>
|
||
<a id="946" class="Keyword">open</a> <a id="951" class="Keyword">import</a> <a id="958" href="/19.08/Denotational/" class="Module">plfa.part3.Denotational</a>
|
||
<a id="984" class="Keyword">using</a> <a id="990" class="Symbol">(</a><a id="991" href="/19.08/Denotational/#4070" class="Datatype">Value</a><a id="996" class="Symbol">;</a> <a id="998" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">_↦_</a><a id="1001" class="Symbol">;</a> <a id="1003" href="plfa.part3.Denotational.html#7364" class="Function Operator">_`,_</a><a id="1007" class="Symbol">;</a> <a id="1009" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">_⊔_</a><a id="1012" class="Symbol">;</a> <a id="1014" href="plfa.part3.Denotational.html#4090" class="InductiveConstructor">⊥</a><a id="1015" class="Symbol">;</a> <a id="1017" href="plfa.part3.Denotational.html#4427" class="Datatype Operator">_⊑_</a><a id="1020" class="Symbol">;</a> <a id="1022" href="plfa.part3.Denotational.html#9417" class="Datatype Operator">_⊢_↓_</a><a id="1027" class="Symbol">;</a>
|
||
<a id="1038" href="/19.08/Denotational/#4462" class="InductiveConstructor">⊑-bot</a><a id="1043" class="Symbol">;</a> <a id="1045" href="plfa.part3.Denotational.html#4788" class="InductiveConstructor">⊑-fun</a><a id="1050" class="Symbol">;</a> <a id="1052" href="plfa.part3.Denotational.html#4487" class="InductiveConstructor">⊑-conj-L</a><a id="1060" class="Symbol">;</a> <a id="1062" href="plfa.part3.Denotational.html#4571" class="InductiveConstructor">⊑-conj-R1</a><a id="1071" class="Symbol">;</a> <a id="1073" href="plfa.part3.Denotational.html#4644" class="InductiveConstructor">⊑-conj-R2</a><a id="1082" class="Symbol">;</a>
|
||
<a id="1093" href="/19.08/Denotational/#4891" class="InductiveConstructor">⊑-dist</a><a id="1099" class="Symbol">;</a> <a id="1101" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a><a id="1107" class="Symbol">;</a> <a id="1109" href="plfa.part3.Denotational.html#4717" class="InductiveConstructor">⊑-trans</a><a id="1116" class="Symbol">;</a> <a id="1118" href="plfa.part3.Denotational.html#6192" class="Function">⊔↦⊔-dist</a><a id="1126" class="Symbol">;</a>
|
||
<a id="1137" href="/19.08/Denotational/#9471" class="InductiveConstructor">var</a><a id="1140" class="Symbol">;</a> <a id="1142" href="plfa.part3.Denotational.html#9668" class="InductiveConstructor">↦-intro</a><a id="1149" class="Symbol">;</a> <a id="1151" href="plfa.part3.Denotational.html#9546" class="InductiveConstructor">↦-elim</a><a id="1157" class="Symbol">;</a> <a id="1159" href="plfa.part3.Denotational.html#9847" class="InductiveConstructor">⊔-intro</a><a id="1166" class="Symbol">;</a> <a id="1168" href="plfa.part3.Denotational.html#9780" class="InductiveConstructor">⊥-intro</a><a id="1175" class="Symbol">;</a> <a id="1177" href="plfa.part3.Denotational.html#9962" class="InductiveConstructor">sub</a><a id="1180" class="Symbol">;</a>
|
||
<a id="1191" href="/19.08/Denotational/#26297" class="Function">up-env</a><a id="1197" class="Symbol">;</a> <a id="1199" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a><a id="1200" class="Symbol">;</a> <a id="1202" href="plfa.part3.Denotational.html#17698" class="Function Operator">_≃_</a><a id="1205" class="Symbol">;</a> <a id="1207" href="plfa.part3.Denotational.html#17970" class="Function">≃-sym</a><a id="1212" class="Symbol">;</a> <a id="1214" href="plfa.part3.Denotational.html#17303" class="Function">Denotation</a><a id="1224" class="Symbol">;</a> <a id="1226" href="plfa.part3.Denotational.html#7207" class="Function">Env</a><a id="1229" class="Symbol">)</a>
|
||
<a id="1231" class="Keyword">open</a> <a id="1236" href="/19.08/Denotational/#19098" class="Module">plfa.part3.Denotational.≃-Reasoning</a>
|
||
</pre>
|
||
<h2 id="equation-for-lambda-abstraction">Equation for lambda abstraction</h2>
|
||
|
||
<p>Regarding the first equation</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ℰ (ƛ M) ≃ ... ℰ M ...
|
||
</code></pre></div></div>
|
||
|
||
<p>we need to define a function that maps a <code class="language-plaintext highlighter-rouge">Denotation (Γ , ★)</code> to a
|
||
<code class="language-plaintext highlighter-rouge">Denotation Γ</code>. This function, let us name it <code class="language-plaintext highlighter-rouge">ℱ</code>, should mimic the
|
||
non-recursive part of the semantics when applied to a lambda term. In
|
||
particular, we need to consider the rules <code class="language-plaintext highlighter-rouge">↦-intro</code>, <code class="language-plaintext highlighter-rouge">⊥-intro</code>, and
|
||
<code class="language-plaintext highlighter-rouge">⊔-intro</code>. So <code class="language-plaintext highlighter-rouge">ℱ</code> has three parameters, the denotation <code class="language-plaintext highlighter-rouge">D</code> of the
|
||
subterm <code class="language-plaintext highlighter-rouge">M</code>, an environment <code class="language-plaintext highlighter-rouge">γ</code>, and a value <code class="language-plaintext highlighter-rouge">v</code>. If we define <code class="language-plaintext highlighter-rouge">ℱ</code> by
|
||
recursion on the value <code class="language-plaintext highlighter-rouge">v</code>, then it matches up nicely with the three
|
||
rules <code class="language-plaintext highlighter-rouge">↦-intro</code>, <code class="language-plaintext highlighter-rouge">⊥-intro</code>, and <code class="language-plaintext highlighter-rouge">⊔-intro</code>.</p>
|
||
|
||
<pre class="Agda"><a id="ℱ"></a><a id="1898" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="1900" class="Symbol">:</a> <a id="1902" class="Symbol">∀{</a><a id="1904" href="plfa.part3.Compositional.html#1904" class="Bound">Γ</a><a id="1905" class="Symbol">}</a> <a id="1907" class="Symbol">→</a> <a id="1909" href="/19.08/Denotational/#17303" class="Function">Denotation</a> <a id="1920" class="Symbol">(</a><a id="1921" href="plfa.part3.Compositional.html#1904" class="Bound">Γ</a> <a id="1923" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="1925" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="1926" class="Symbol">)</a> <a id="1928" class="Symbol">→</a> <a id="1930" href="plfa.part3.Denotational.html#17303" class="Function">Denotation</a> <a id="1941" href="plfa.part3.Compositional.html#1904" class="Bound">Γ</a>
|
||
<a id="1943" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="1945" href="plfa.part3.Compositional.html#1945" class="Bound">D</a> <a id="1947" href="plfa.part3.Compositional.html#1947" class="Bound">γ</a> <a id="1949" class="Symbol">(</a><a id="1950" href="plfa.part3.Compositional.html#1950" class="Bound">v</a> <a id="1952" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="1954" href="plfa.part3.Compositional.html#1954" class="Bound">w</a><a id="1955" class="Symbol">)</a> <a id="1957" class="Symbol">=</a> <a id="1959" href="plfa.part3.Compositional.html#1945" class="Bound">D</a> <a id="1961" class="Symbol">(</a><a id="1962" href="plfa.part3.Compositional.html#1947" class="Bound">γ</a> <a id="1964" href="plfa.part3.Denotational.html#7364" class="Function Operator">`,</a> <a id="1967" href="plfa.part3.Compositional.html#1950" class="Bound">v</a><a id="1968" class="Symbol">)</a> <a id="1970" href="plfa.part3.Compositional.html#1954" class="Bound">w</a>
|
||
<a id="1972" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="1974" href="plfa.part3.Compositional.html#1974" class="Bound">D</a> <a id="1976" href="plfa.part3.Compositional.html#1976" class="Bound">γ</a> <a id="1978" href="/19.08/Denotational/#4090" class="InductiveConstructor">⊥</a> <a id="1980" class="Symbol">=</a> <a id="1982" href="Agda.Builtin.Unit.html#137" class="Record">⊤</a>
|
||
<a id="1984" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="1986" href="plfa.part3.Compositional.html#1986" class="Bound">D</a> <a id="1988" href="plfa.part3.Compositional.html#1988" class="Bound">γ</a> <a id="1990" class="Symbol">(</a><a id="1991" href="plfa.part3.Compositional.html#1991" class="Bound">u</a> <a id="1993" href="/19.08/Denotational/#4132" class="InductiveConstructor Operator">⊔</a> <a id="1995" href="plfa.part3.Compositional.html#1995" class="Bound">v</a><a id="1996" class="Symbol">)</a> <a id="1998" class="Symbol">=</a> <a id="2000" class="Symbol">(</a><a id="2001" href="plfa.part3.Compositional.html#1898" class="Function">ℱ</a> <a id="2003" href="plfa.part3.Compositional.html#1986" class="Bound">D</a> <a id="2005" href="plfa.part3.Compositional.html#1988" class="Bound">γ</a> <a id="2007" href="plfa.part3.Compositional.html#1991" class="Bound">u</a><a id="2008" class="Symbol">)</a> <a id="2010" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="2012" class="Symbol">(</a><a id="2013" href="plfa.part3.Compositional.html#1898" class="Function">ℱ</a> <a id="2015" href="plfa.part3.Compositional.html#1986" class="Bound">D</a> <a id="2017" href="plfa.part3.Compositional.html#1988" class="Bound">γ</a> <a id="2019" href="plfa.part3.Compositional.html#1995" class="Bound">v</a><a id="2020" class="Symbol">)</a>
|
||
</pre>
|
||
<p>If one squints hard enough, the <code class="language-plaintext highlighter-rouge">ℱ</code> function starts to look like the
|
||
<code class="language-plaintext highlighter-rouge">curry</code> operation familar to functional programmers. It turns a
|
||
function that expects a tuple of length <code class="language-plaintext highlighter-rouge">n + 1</code> (the environment <code class="language-plaintext highlighter-rouge">Γ ,
|
||
★</code>) into a function that expects a tuple of length <code class="language-plaintext highlighter-rouge">n</code> and returns a
|
||
function of one parameter.</p>
|
||
|
||
<p>Using this <code class="language-plaintext highlighter-rouge">ℱ</code>, we hope to prove that</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ℰ (ƛ N) ≃ ℱ (ℰ N)
|
||
</code></pre></div></div>
|
||
|
||
<p>The function <code class="language-plaintext highlighter-rouge">ℱ</code> is preserved when going from a larger value <code class="language-plaintext highlighter-rouge">v</code> to a
|
||
smaller value <code class="language-plaintext highlighter-rouge">u</code>. The proof is a straightforward induction on the
|
||
derivation of <code class="language-plaintext highlighter-rouge">u ⊑ v</code>, using the <code class="language-plaintext highlighter-rouge">up-env</code> lemma in the case for the
|
||
<code class="language-plaintext highlighter-rouge">⊑-fun</code> rule.</p>
|
||
|
||
<pre class="Agda"><a id="sub-ℱ"></a><a id="2613" href="/19.08/Compositional/#2613" class="Function">sub-ℱ</a> <a id="2619" class="Symbol">:</a> <a id="2621" class="Symbol">∀{</a><a id="2623" href="plfa.part3.Compositional.html#2623" class="Bound">Γ</a><a id="2624" class="Symbol">}{</a><a id="2626" href="plfa.part3.Compositional.html#2626" class="Bound">N</a> <a id="2628" class="Symbol">:</a> <a id="2630" href="plfa.part3.Compositional.html#2623" class="Bound">Γ</a> <a id="2632" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="2634" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="2636" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="2638" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="2639" class="Symbol">}{</a><a id="2641" href="plfa.part3.Compositional.html#2641" class="Bound">γ</a> <a id="2643" href="plfa.part3.Compositional.html#2643" class="Bound">v</a> <a id="2645" href="plfa.part3.Compositional.html#2645" class="Bound">u</a><a id="2646" class="Symbol">}</a>
|
||
<a id="2650" class="Symbol">→</a> <a id="2652" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="2654" class="Symbol">(</a><a id="2655" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="2657" href="plfa.part3.Compositional.html#2626" class="Bound">N</a><a id="2658" class="Symbol">)</a> <a id="2660" href="plfa.part3.Compositional.html#2641" class="Bound">γ</a> <a id="2662" href="plfa.part3.Compositional.html#2643" class="Bound">v</a>
|
||
<a id="2666" class="Symbol">→</a> <a id="2668" href="/19.08/Compositional/#2645" class="Bound">u</a> <a id="2670" href="/19.08/Denotational/#4427" class="Datatype Operator">⊑</a> <a id="2672" href="plfa.part3.Compositional.html#2643" class="Bound">v</a>
|
||
<a id="2678" class="Comment">------------</a>
|
||
<a id="2693" class="Symbol">→</a> <a id="2695" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="2697" class="Symbol">(</a><a id="2698" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="2700" href="plfa.part3.Compositional.html#2626" class="Bound">N</a><a id="2701" class="Symbol">)</a> <a id="2703" href="plfa.part3.Compositional.html#2641" class="Bound">γ</a> <a id="2705" href="plfa.part3.Compositional.html#2645" class="Bound">u</a>
|
||
<a id="2707" href="/19.08/Compositional/#2613" class="Function">sub-ℱ</a> <a id="2713" href="plfa.part3.Compositional.html#2713" class="Bound">d</a> <a id="2715" href="/19.08/Denotational/#4462" class="InductiveConstructor">⊑-bot</a> <a id="2721" class="Symbol">=</a> <a id="2723" href="Agda.Builtin.Unit.html#174" class="InductiveConstructor">tt</a>
|
||
<a id="2726" href="/19.08/Compositional/#2613" class="Function">sub-ℱ</a> <a id="2732" href="plfa.part3.Compositional.html#2732" class="Bound">d</a> <a id="2734" class="Symbol">(</a><a id="2735" href="/19.08/Denotational/#4788" class="InductiveConstructor">⊑-fun</a> <a id="2741" href="plfa.part3.Compositional.html#2741" class="Bound">lt</a> <a id="2744" href="plfa.part3.Compositional.html#2744" class="Bound">lt′</a><a id="2747" class="Symbol">)</a> <a id="2749" class="Symbol">=</a> <a id="2751" href="plfa.part3.Denotational.html#9962" class="InductiveConstructor">sub</a> <a id="2755" class="Symbol">(</a><a id="2756" href="plfa.part3.Denotational.html#26297" class="Function">up-env</a> <a id="2763" href="plfa.part3.Compositional.html#2732" class="Bound">d</a> <a id="2765" href="plfa.part3.Compositional.html#2741" class="Bound">lt</a><a id="2767" class="Symbol">)</a> <a id="2769" href="plfa.part3.Compositional.html#2744" class="Bound">lt′</a>
|
||
<a id="2773" href="/19.08/Compositional/#2613" class="Function">sub-ℱ</a> <a id="2779" href="plfa.part3.Compositional.html#2779" class="Bound">d</a> <a id="2781" class="Symbol">(</a><a id="2782" href="/19.08/Denotational/#4487" class="InductiveConstructor">⊑-conj-L</a> <a id="2791" href="plfa.part3.Compositional.html#2791" class="Bound">lt</a> <a id="2794" href="plfa.part3.Compositional.html#2794" class="Bound">lt₁</a><a id="2797" class="Symbol">)</a> <a id="2799" class="Symbol">=</a> <a id="2801" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="2803" href="plfa.part3.Compositional.html#2613" class="Function">sub-ℱ</a> <a id="2809" href="plfa.part3.Compositional.html#2779" class="Bound">d</a> <a id="2811" href="plfa.part3.Compositional.html#2791" class="Bound">lt</a> <a id="2814" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="2816" href="plfa.part3.Compositional.html#2613" class="Function">sub-ℱ</a> <a id="2822" href="plfa.part3.Compositional.html#2779" class="Bound">d</a> <a id="2824" href="plfa.part3.Compositional.html#2794" class="Bound">lt₁</a> <a id="2828" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="2830" href="/19.08/Compositional/#2613" class="Function">sub-ℱ</a> <a id="2836" href="plfa.part3.Compositional.html#2836" class="Bound">d</a> <a id="2838" class="Symbol">(</a><a id="2839" href="/19.08/Denotational/#4571" class="InductiveConstructor">⊑-conj-R1</a> <a id="2849" href="plfa.part3.Compositional.html#2849" class="Bound">lt</a><a id="2851" class="Symbol">)</a> <a id="2853" class="Symbol">=</a> <a id="2855" href="plfa.part3.Compositional.html#2613" class="Function">sub-ℱ</a> <a id="2861" class="Symbol">(</a><a id="2862" href="Agda.Builtin.Sigma.html#225" class="Field">proj₁</a> <a id="2868" href="plfa.part3.Compositional.html#2836" class="Bound">d</a><a id="2869" class="Symbol">)</a> <a id="2871" href="plfa.part3.Compositional.html#2849" class="Bound">lt</a>
|
||
<a id="2874" href="/19.08/Compositional/#2613" class="Function">sub-ℱ</a> <a id="2880" href="plfa.part3.Compositional.html#2880" class="Bound">d</a> <a id="2882" class="Symbol">(</a><a id="2883" href="/19.08/Denotational/#4644" class="InductiveConstructor">⊑-conj-R2</a> <a id="2893" href="plfa.part3.Compositional.html#2893" class="Bound">lt</a><a id="2895" class="Symbol">)</a> <a id="2897" class="Symbol">=</a> <a id="2899" href="plfa.part3.Compositional.html#2613" class="Function">sub-ℱ</a> <a id="2905" class="Symbol">(</a><a id="2906" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a> <a id="2912" href="plfa.part3.Compositional.html#2880" class="Bound">d</a><a id="2913" class="Symbol">)</a> <a id="2915" href="plfa.part3.Compositional.html#2893" class="Bound">lt</a>
|
||
<a id="2918" href="/19.08/Compositional/#2613" class="Function">sub-ℱ</a> <a id="2924" class="Symbol">{</a><a id="2925" class="Argument">v</a> <a id="2927" class="Symbol">=</a> <a id="2929" href="plfa.part3.Compositional.html#2929" class="Bound">v₁</a> <a id="2932" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="2934" href="plfa.part3.Compositional.html#2934" class="Bound">v₂</a> <a id="2937" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="2939" href="plfa.part3.Compositional.html#2929" class="Bound">v₁</a> <a id="2942" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="2944" href="plfa.part3.Compositional.html#2944" class="Bound">v₃</a><a id="2946" class="Symbol">}</a> <a id="2948" class="Symbol">{</a><a id="2949" href="plfa.part3.Compositional.html#2929" class="Bound">v₁</a> <a id="2952" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="2954" class="Symbol">(</a><a id="2955" href="plfa.part3.Compositional.html#2934" class="Bound">v₂</a> <a id="2958" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="2960" href="plfa.part3.Compositional.html#2944" class="Bound">v₃</a><a id="2962" class="Symbol">)}</a> <a id="2965" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="2967" href="plfa.part3.Compositional.html#2967" class="Bound">N2</a> <a id="2970" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="2972" href="plfa.part3.Compositional.html#2972" class="Bound">N3</a> <a id="2975" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="2977" href="plfa.part3.Denotational.html#4891" class="InductiveConstructor">⊑-dist</a> <a id="2984" class="Symbol">=</a>
|
||
<a id="2989" href="/19.08/Denotational/#9847" class="InductiveConstructor">⊔-intro</a> <a id="2997" href="/19.08/Compositional/#2967" class="Bound">N2</a> <a id="3000" href="plfa.part3.Compositional.html#2972" class="Bound">N3</a>
|
||
<a id="3003" href="/19.08/Compositional/#2613" class="Function">sub-ℱ</a> <a id="3009" href="plfa.part3.Compositional.html#3009" class="Bound">d</a> <a id="3011" class="Symbol">(</a><a id="3012" href="/19.08/Denotational/#4717" class="InductiveConstructor">⊑-trans</a> <a id="3020" href="plfa.part3.Compositional.html#3020" class="Bound">x₁</a> <a id="3023" href="plfa.part3.Compositional.html#3023" class="Bound">x₂</a><a id="3025" class="Symbol">)</a> <a id="3027" class="Symbol">=</a> <a id="3029" href="plfa.part3.Compositional.html#2613" class="Function">sub-ℱ</a> <a id="3035" class="Symbol">(</a><a id="3036" href="plfa.part3.Compositional.html#2613" class="Function">sub-ℱ</a> <a id="3042" href="plfa.part3.Compositional.html#3009" class="Bound">d</a> <a id="3044" href="plfa.part3.Compositional.html#3023" class="Bound">x₂</a><a id="3046" class="Symbol">)</a> <a id="3048" href="plfa.part3.Compositional.html#3020" class="Bound">x₁</a>
|
||
</pre>
|
||
<!--
|
||
[PLW:
|
||
If denotations were strengthened to be downward closed,
|
||
we could rewrite the signature replacing (ℰ N) by d : Denotation (Γ , ★)]
|
||
[JGS: I'll look into this.]
|
||
-->
|
||
|
||
<p>With this subsumption property in hand, we can prove the forward
|
||
direction of the semantic equation for lambda. The proof is by
|
||
induction on the semantics, using <code class="language-plaintext highlighter-rouge">sub-ℱ</code> in the case for the <code class="language-plaintext highlighter-rouge">sub</code>
|
||
rule.</p>
|
||
|
||
<pre class="Agda"><a id="ℰƛ→ℱℰ"></a><a id="3442" href="/19.08/Compositional/#3442" class="Function">ℰƛ→ℱℰ</a> <a id="3448" class="Symbol">:</a> <a id="3450" class="Symbol">∀{</a><a id="3452" href="plfa.part3.Compositional.html#3452" class="Bound">Γ</a><a id="3453" class="Symbol">}{</a><a id="3455" href="plfa.part3.Compositional.html#3455" class="Bound">γ</a> <a id="3457" class="Symbol">:</a> <a id="3459" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="3463" href="plfa.part3.Compositional.html#3452" class="Bound">Γ</a><a id="3464" class="Symbol">}{</a><a id="3466" href="plfa.part3.Compositional.html#3466" class="Bound">N</a> <a id="3468" class="Symbol">:</a> <a id="3470" href="plfa.part3.Compositional.html#3452" class="Bound">Γ</a> <a id="3472" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="3474" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="3476" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="3478" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="3479" class="Symbol">}{</a><a id="3481" href="plfa.part3.Compositional.html#3481" class="Bound">v</a> <a id="3483" class="Symbol">:</a> <a id="3485" href="plfa.part3.Denotational.html#4070" class="Datatype">Value</a><a id="3490" class="Symbol">}</a>
|
||
<a id="3494" class="Symbol">→</a> <a id="3496" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="3498" class="Symbol">(</a><a id="3499" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="3501" href="/19.08/Compositional/#3466" class="Bound">N</a><a id="3502" class="Symbol">)</a> <a id="3504" href="plfa.part3.Compositional.html#3455" class="Bound">γ</a> <a id="3506" href="plfa.part3.Compositional.html#3481" class="Bound">v</a>
|
||
<a id="3512" class="Comment">------------</a>
|
||
<a id="3527" class="Symbol">→</a> <a id="3529" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="3531" class="Symbol">(</a><a id="3532" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="3534" href="plfa.part3.Compositional.html#3466" class="Bound">N</a><a id="3535" class="Symbol">)</a> <a id="3537" href="plfa.part3.Compositional.html#3455" class="Bound">γ</a> <a id="3539" href="plfa.part3.Compositional.html#3481" class="Bound">v</a>
|
||
<a id="3541" href="/19.08/Compositional/#3442" class="Function">ℰƛ→ℱℰ</a> <a id="3547" class="Symbol">(</a><a id="3548" href="/19.08/Denotational/#9668" class="InductiveConstructor">↦-intro</a> <a id="3556" href="plfa.part3.Compositional.html#3556" class="Bound">d</a><a id="3557" class="Symbol">)</a> <a id="3559" class="Symbol">=</a> <a id="3561" href="plfa.part3.Compositional.html#3556" class="Bound">d</a>
|
||
<a id="3563" href="/19.08/Compositional/#3442" class="Function">ℰƛ→ℱℰ</a> <a id="3569" href="/19.08/Denotational/#9780" class="InductiveConstructor">⊥-intro</a> <a id="3577" class="Symbol">=</a> <a id="3579" href="Agda.Builtin.Unit.html#174" class="InductiveConstructor">tt</a>
|
||
<a id="3582" href="/19.08/Compositional/#3442" class="Function">ℰƛ→ℱℰ</a> <a id="3588" class="Symbol">(</a><a id="3589" href="/19.08/Denotational/#9847" class="InductiveConstructor">⊔-intro</a> <a id="3597" href="plfa.part3.Compositional.html#3597" class="Bound">d₁</a> <a id="3600" href="plfa.part3.Compositional.html#3600" class="Bound">d₂</a><a id="3602" class="Symbol">)</a> <a id="3604" class="Symbol">=</a> <a id="3606" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="3608" href="plfa.part3.Compositional.html#3442" class="Function">ℰƛ→ℱℰ</a> <a id="3614" href="plfa.part3.Compositional.html#3597" class="Bound">d₁</a> <a id="3617" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="3619" href="plfa.part3.Compositional.html#3442" class="Function">ℰƛ→ℱℰ</a> <a id="3625" href="plfa.part3.Compositional.html#3600" class="Bound">d₂</a> <a id="3628" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="3630" href="/19.08/Compositional/#3442" class="Function">ℰƛ→ℱℰ</a> <a id="3636" class="Symbol">(</a><a id="3637" href="/19.08/Denotational/#9962" class="InductiveConstructor">sub</a> <a id="3641" href="plfa.part3.Compositional.html#3641" class="Bound">d</a> <a id="3643" href="plfa.part3.Compositional.html#3643" class="Bound">lt</a><a id="3645" class="Symbol">)</a> <a id="3647" class="Symbol">=</a> <a id="3649" href="plfa.part3.Compositional.html#2613" class="Function">sub-ℱ</a> <a id="3655" class="Symbol">(</a><a id="3656" href="plfa.part3.Compositional.html#3442" class="Function">ℰƛ→ℱℰ</a> <a id="3662" href="plfa.part3.Compositional.html#3641" class="Bound">d</a><a id="3663" class="Symbol">)</a> <a id="3665" href="plfa.part3.Compositional.html#3643" class="Bound">lt</a>
|
||
</pre>
|
||
<p>The “inversion lemma” for lambda abstraction is a special case of the
|
||
above. The inversion lemma is useful in proving that denotations are
|
||
preserved by reduction.</p>
|
||
|
||
<pre class="Agda"><a id="lambda-inversion"></a><a id="3841" href="/19.08/Compositional/#3841" class="Function">lambda-inversion</a> <a id="3858" class="Symbol">:</a> <a id="3860" class="Symbol">∀{</a><a id="3862" href="plfa.part3.Compositional.html#3862" class="Bound">Γ</a><a id="3863" class="Symbol">}{</a><a id="3865" href="plfa.part3.Compositional.html#3865" class="Bound">γ</a> <a id="3867" class="Symbol">:</a> <a id="3869" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="3873" href="plfa.part3.Compositional.html#3862" class="Bound">Γ</a><a id="3874" class="Symbol">}{</a><a id="3876" href="plfa.part3.Compositional.html#3876" class="Bound">N</a> <a id="3878" class="Symbol">:</a> <a id="3880" href="plfa.part3.Compositional.html#3862" class="Bound">Γ</a> <a id="3882" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="3884" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="3886" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="3888" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="3889" class="Symbol">}{</a><a id="3891" href="plfa.part3.Compositional.html#3891" class="Bound">v₁</a> <a id="3894" href="plfa.part3.Compositional.html#3894" class="Bound">v₂</a> <a id="3897" class="Symbol">:</a> <a id="3899" href="plfa.part3.Denotational.html#4070" class="Datatype">Value</a><a id="3904" class="Symbol">}</a>
|
||
<a id="3908" class="Symbol">→</a> <a id="3910" href="/19.08/Compositional/#3865" class="Bound">γ</a> <a id="3912" href="/19.08/Denotational/#9417" class="Datatype Operator">⊢</a> <a id="3914" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="3916" href="plfa.part3.Compositional.html#3876" class="Bound">N</a> <a id="3918" href="plfa.part3.Denotational.html#9417" class="Datatype Operator">↓</a> <a id="3920" href="plfa.part3.Compositional.html#3891" class="Bound">v₁</a> <a id="3923" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="3925" href="plfa.part3.Compositional.html#3894" class="Bound">v₂</a>
|
||
<a id="3932" class="Comment">-----------------</a>
|
||
<a id="3952" class="Symbol">→</a> <a id="3954" class="Symbol">(</a><a id="3955" href="/19.08/Compositional/#3865" class="Bound">γ</a> <a id="3957" href="/19.08/Denotational/#7364" class="Function Operator">`,</a> <a id="3960" href="plfa.part3.Compositional.html#3891" class="Bound">v₁</a><a id="3962" class="Symbol">)</a> <a id="3964" href="plfa.part3.Denotational.html#9417" class="Datatype Operator">⊢</a> <a id="3966" href="plfa.part3.Compositional.html#3876" class="Bound">N</a> <a id="3968" href="plfa.part3.Denotational.html#9417" class="Datatype Operator">↓</a> <a id="3970" href="plfa.part3.Compositional.html#3894" class="Bound">v₂</a>
|
||
<a id="3973" href="/19.08/Compositional/#3841" class="Function">lambda-inversion</a><a id="3989" class="Symbol">{</a><a id="3990" class="Argument">v₁</a> <a id="3993" class="Symbol">=</a> <a id="3995" href="plfa.part3.Compositional.html#3995" class="Bound">v₁</a><a id="3997" class="Symbol">}{</a><a id="3999" class="Argument">v₂</a> <a id="4002" class="Symbol">=</a> <a id="4004" href="plfa.part3.Compositional.html#4004" class="Bound">v₂</a><a id="4006" class="Symbol">}</a> <a id="4008" href="plfa.part3.Compositional.html#4008" class="Bound">d</a> <a id="4010" class="Symbol">=</a> <a id="4012" href="plfa.part3.Compositional.html#3442" class="Function">ℰƛ→ℱℰ</a><a id="4017" class="Symbol">{</a><a id="4018" class="Argument">v</a> <a id="4020" class="Symbol">=</a> <a id="4022" href="plfa.part3.Compositional.html#3995" class="Bound">v₁</a> <a id="4025" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="4027" href="plfa.part3.Compositional.html#4004" class="Bound">v₂</a><a id="4029" class="Symbol">}</a> <a id="4031" href="plfa.part3.Compositional.html#4008" class="Bound">d</a>
|
||
</pre>
|
||
<p>The backward direction of the semantic equation for lambda is even
|
||
easier to prove than the forward direction. We proceed by induction on
|
||
the value v.</p>
|
||
|
||
<pre class="Agda"><a id="ℱℰ→ℰƛ"></a><a id="4194" href="/19.08/Compositional/#4194" class="Function">ℱℰ→ℰƛ</a> <a id="4200" class="Symbol">:</a> <a id="4202" class="Symbol">∀{</a><a id="4204" href="plfa.part3.Compositional.html#4204" class="Bound">Γ</a><a id="4205" class="Symbol">}{</a><a id="4207" href="plfa.part3.Compositional.html#4207" class="Bound">γ</a> <a id="4209" class="Symbol">:</a> <a id="4211" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="4215" href="plfa.part3.Compositional.html#4204" class="Bound">Γ</a><a id="4216" class="Symbol">}{</a><a id="4218" href="plfa.part3.Compositional.html#4218" class="Bound">N</a> <a id="4220" class="Symbol">:</a> <a id="4222" href="plfa.part3.Compositional.html#4204" class="Bound">Γ</a> <a id="4224" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="4226" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="4228" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="4230" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="4231" class="Symbol">}{</a><a id="4233" href="plfa.part3.Compositional.html#4233" class="Bound">v</a> <a id="4235" class="Symbol">:</a> <a id="4237" href="plfa.part3.Denotational.html#4070" class="Datatype">Value</a><a id="4242" class="Symbol">}</a>
|
||
<a id="4246" class="Symbol">→</a> <a id="4248" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="4250" class="Symbol">(</a><a id="4251" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="4253" href="plfa.part3.Compositional.html#4218" class="Bound">N</a><a id="4254" class="Symbol">)</a> <a id="4256" href="plfa.part3.Compositional.html#4207" class="Bound">γ</a> <a id="4258" href="plfa.part3.Compositional.html#4233" class="Bound">v</a>
|
||
<a id="4264" class="Comment">------------</a>
|
||
<a id="4279" class="Symbol">→</a> <a id="4281" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="4283" class="Symbol">(</a><a id="4284" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="4286" href="/19.08/Compositional/#4218" class="Bound">N</a><a id="4287" class="Symbol">)</a> <a id="4289" href="plfa.part3.Compositional.html#4207" class="Bound">γ</a> <a id="4291" href="plfa.part3.Compositional.html#4233" class="Bound">v</a>
|
||
<a id="4293" href="/19.08/Compositional/#4194" class="Function">ℱℰ→ℰƛ</a> <a id="4299" class="Symbol">{</a><a id="4300" class="Argument">v</a> <a id="4302" class="Symbol">=</a> <a id="4304" href="/19.08/Denotational/#4090" class="InductiveConstructor">⊥</a><a id="4305" class="Symbol">}</a> <a id="4307" href="plfa.part3.Compositional.html#4307" class="Bound">d</a> <a id="4309" class="Symbol">=</a> <a id="4311" href="plfa.part3.Denotational.html#9780" class="InductiveConstructor">⊥-intro</a>
|
||
<a id="4319" href="/19.08/Compositional/#4194" class="Function">ℱℰ→ℰƛ</a> <a id="4325" class="Symbol">{</a><a id="4326" class="Argument">v</a> <a id="4328" class="Symbol">=</a> <a id="4330" href="plfa.part3.Compositional.html#4330" class="Bound">v₁</a> <a id="4333" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="4335" href="plfa.part3.Compositional.html#4335" class="Bound">v₂</a><a id="4337" class="Symbol">}</a> <a id="4339" href="plfa.part3.Compositional.html#4339" class="Bound">d</a> <a id="4341" class="Symbol">=</a> <a id="4343" href="plfa.part3.Denotational.html#9668" class="InductiveConstructor">↦-intro</a> <a id="4351" href="plfa.part3.Compositional.html#4339" class="Bound">d</a>
|
||
<a id="4353" href="/19.08/Compositional/#4194" class="Function">ℱℰ→ℰƛ</a> <a id="4359" class="Symbol">{</a><a id="4360" class="Argument">v</a> <a id="4362" class="Symbol">=</a> <a id="4364" href="plfa.part3.Compositional.html#4364" class="Bound">v₁</a> <a id="4367" href="/19.08/Denotational/#4132" class="InductiveConstructor Operator">⊔</a> <a id="4369" href="plfa.part3.Compositional.html#4369" class="Bound">v₂</a><a id="4371" class="Symbol">}</a> <a id="4373" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4375" href="plfa.part3.Compositional.html#4375" class="Bound">d1</a> <a id="4378" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4380" href="plfa.part3.Compositional.html#4380" class="Bound">d2</a> <a id="4383" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4385" class="Symbol">=</a> <a id="4387" href="plfa.part3.Denotational.html#9847" class="InductiveConstructor">⊔-intro</a> <a id="4395" class="Symbol">(</a><a id="4396" href="plfa.part3.Compositional.html#4194" class="Function">ℱℰ→ℰƛ</a> <a id="4402" href="plfa.part3.Compositional.html#4375" class="Bound">d1</a><a id="4404" class="Symbol">)</a> <a id="4406" class="Symbol">(</a><a id="4407" href="plfa.part3.Compositional.html#4194" class="Function">ℱℰ→ℰƛ</a> <a id="4413" href="plfa.part3.Compositional.html#4380" class="Bound">d2</a><a id="4415" class="Symbol">)</a>
|
||
</pre>
|
||
<p>So indeed, the denotational semantics is compositional with respect
|
||
to lambda abstraction, as witnessed by the function <code class="language-plaintext highlighter-rouge">ℱ</code>.</p>
|
||
|
||
<pre class="Agda"><a id="lam-equiv"></a><a id="4552" href="/19.08/Compositional/#4552" class="Function">lam-equiv</a> <a id="4562" class="Symbol">:</a> <a id="4564" class="Symbol">∀{</a><a id="4566" href="plfa.part3.Compositional.html#4566" class="Bound">Γ</a><a id="4567" class="Symbol">}{</a><a id="4569" href="plfa.part3.Compositional.html#4569" class="Bound">N</a> <a id="4571" class="Symbol">:</a> <a id="4573" href="plfa.part3.Compositional.html#4566" class="Bound">Γ</a> <a id="4575" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="4577" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="4579" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="4581" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="4582" class="Symbol">}</a>
|
||
<a id="4586" class="Symbol">→</a> <a id="4588" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="4590" class="Symbol">(</a><a id="4591" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="4593" href="/19.08/Compositional/#4569" class="Bound">N</a><a id="4594" class="Symbol">)</a> <a id="4596" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="4598" href="plfa.part3.Compositional.html#1898" class="Function">ℱ</a> <a id="4600" class="Symbol">(</a><a id="4601" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="4603" href="plfa.part3.Compositional.html#4569" class="Bound">N</a><a id="4604" class="Symbol">)</a>
|
||
<a id="4606" href="/19.08/Compositional/#4552" class="Function">lam-equiv</a> <a id="4616" href="plfa.part3.Compositional.html#4616" class="Bound">γ</a> <a id="4618" href="plfa.part3.Compositional.html#4618" class="Bound">v</a> <a id="4620" class="Symbol">=</a> <a id="4622" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4624" href="plfa.part3.Compositional.html#3442" class="Function">ℰƛ→ℱℰ</a> <a id="4630" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4632" href="plfa.part3.Compositional.html#4194" class="Function">ℱℰ→ℰƛ</a> <a id="4638" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
</pre>
|
||
|
||
<h2 id="equation-for-function-application">Equation for function application</h2>
|
||
|
||
<p>Next we fill in the ellipses for the equation concerning function
|
||
application.</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ℰ (M · N) ≃ ... ℰ M ... ℰ N ...
|
||
</code></pre></div></div>
|
||
|
||
<p>For this we need to define a function that takes two denotations, both
|
||
in context <code class="language-plaintext highlighter-rouge">Γ</code>, and produces another one in context <code class="language-plaintext highlighter-rouge">Γ</code>. This
|
||
function, let us name it <code class="language-plaintext highlighter-rouge">●</code>, needs to mimic the non-recursive aspects
|
||
of the semantics of an application <code class="language-plaintext highlighter-rouge">L · M</code>. We cannot proceed as
|
||
easily as for <code class="language-plaintext highlighter-rouge">ℱ</code> and define the function by recursion on value <code class="language-plaintext highlighter-rouge">v</code>
|
||
because, for example, the rule <code class="language-plaintext highlighter-rouge">↦-elim</code> applies to any value. Instead
|
||
we shall define <code class="language-plaintext highlighter-rouge">●</code> in a way that directly deals with the <code class="language-plaintext highlighter-rouge">↦-elim</code> and
|
||
<code class="language-plaintext highlighter-rouge">⊥-intro</code> rules but ignores <code class="language-plaintext highlighter-rouge">⊔-intro</code>. This makes the forward
|
||
direction of the proof more difficult, and the case for <code class="language-plaintext highlighter-rouge">⊔-intro</code>
|
||
demonstrates why the <code class="language-plaintext highlighter-rouge">⊑-dist</code> rule is important.</p>
|
||
|
||
<p>So we define the application of <code class="language-plaintext highlighter-rouge">D₁</code> to <code class="language-plaintext highlighter-rouge">D₂</code>, written <code class="language-plaintext highlighter-rouge">D₁ ● D₂</code>, to include
|
||
any value <code class="language-plaintext highlighter-rouge">w</code> equivalent to <code class="language-plaintext highlighter-rouge">⊥</code>, for the <code class="language-plaintext highlighter-rouge">⊥-intro</code> rule, and to include any
|
||
value <code class="language-plaintext highlighter-rouge">w</code> that is the output of an entry <code class="language-plaintext highlighter-rouge">v ↦ w</code> in <code class="language-plaintext highlighter-rouge">D₁</code>, provided the
|
||
input <code class="language-plaintext highlighter-rouge">v</code> is in <code class="language-plaintext highlighter-rouge">D₂</code>, for the <code class="language-plaintext highlighter-rouge">↦-elim</code> rule.</p>
|
||
|
||
<pre class="Agda"><a id="5731" class="Keyword">infixl</a> <a id="5738" class="Number">7</a> <a id="5740" href="/19.08/Compositional/#5745" class="Function Operator">_●_</a>
|
||
|
||
<a id="_●_"></a><a id="5745" href="/19.08/Compositional/#5745" class="Function Operator">_●_</a> <a id="5749" class="Symbol">:</a> <a id="5751" class="Symbol">∀{</a><a id="5753" href="plfa.part3.Compositional.html#5753" class="Bound">Γ</a><a id="5754" class="Symbol">}</a> <a id="5756" class="Symbol">→</a> <a id="5758" href="/19.08/Denotational/#17303" class="Function">Denotation</a> <a id="5769" href="plfa.part3.Compositional.html#5753" class="Bound">Γ</a> <a id="5771" class="Symbol">→</a> <a id="5773" href="plfa.part3.Denotational.html#17303" class="Function">Denotation</a> <a id="5784" href="plfa.part3.Compositional.html#5753" class="Bound">Γ</a> <a id="5786" class="Symbol">→</a> <a id="5788" href="plfa.part3.Denotational.html#17303" class="Function">Denotation</a> <a id="5799" href="plfa.part3.Compositional.html#5753" class="Bound">Γ</a>
|
||
<a id="5801" class="Symbol">(</a><a id="5802" href="/19.08/Compositional/#5802" class="Bound">D₁</a> <a id="5805" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="5807" href="plfa.part3.Compositional.html#5807" class="Bound">D₂</a><a id="5809" class="Symbol">)</a> <a id="5811" href="plfa.part3.Compositional.html#5811" class="Bound">γ</a> <a id="5813" href="plfa.part3.Compositional.html#5813" class="Bound">w</a> <a id="5815" class="Symbol">=</a> <a id="5817" href="plfa.part3.Compositional.html#5813" class="Bound">w</a> <a id="5819" href="/19.08/Denotational/#4427" class="Datatype Operator">⊑</a> <a id="5821" href="plfa.part3.Denotational.html#4090" class="InductiveConstructor">⊥</a> <a id="5823" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#612" class="Datatype Operator">⊎</a> <a id="5825" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="5828" href="plfa.part3.Compositional.html#5828" class="Bound">v</a> <a id="5830" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="5832" href="plfa.part3.Denotational.html#4070" class="Datatype">Value</a> <a id="5838" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a><a id="5839" class="Symbol">(</a> <a id="5841" href="plfa.part3.Compositional.html#5802" class="Bound">D₁</a> <a id="5844" href="plfa.part3.Compositional.html#5811" class="Bound">γ</a> <a id="5846" class="Symbol">(</a><a id="5847" href="plfa.part3.Compositional.html#5828" class="Bound">v</a> <a id="5849" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="5851" href="plfa.part3.Compositional.html#5813" class="Bound">w</a><a id="5852" class="Symbol">)</a> <a id="5854" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="5856" href="plfa.part3.Compositional.html#5807" class="Bound">D₂</a> <a id="5859" href="plfa.part3.Compositional.html#5811" class="Bound">γ</a> <a id="5861" href="plfa.part3.Compositional.html#5828" class="Bound">v</a> <a id="5863" class="Symbol">)</a>
|
||
</pre>
|
||
<p>If one squints hard enough, the <code class="language-plaintext highlighter-rouge">_●_</code> operator starts to look
|
||
like the <code class="language-plaintext highlighter-rouge">apply</code> operation familiar to functional programmers.
|
||
It takes two parameters and applies the first to the second.</p>
|
||
|
||
<p>Next we consider the inversion lemma for application, which is also
|
||
the forward direction of the semantic equation for application. We
|
||
describe the proof below.</p>
|
||
|
||
<pre class="Agda"><a id="ℰ·→●ℰ"></a><a id="6224" href="/19.08/Compositional/#6224" class="Function">ℰ·→●ℰ</a> <a id="6230" class="Symbol">:</a> <a id="6232" class="Symbol">∀{</a><a id="6234" href="plfa.part3.Compositional.html#6234" class="Bound">Γ</a><a id="6235" class="Symbol">}{</a><a id="6237" href="plfa.part3.Compositional.html#6237" class="Bound">γ</a> <a id="6239" class="Symbol">:</a> <a id="6241" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="6245" href="plfa.part3.Compositional.html#6234" class="Bound">Γ</a><a id="6246" class="Symbol">}{</a><a id="6248" href="plfa.part3.Compositional.html#6248" class="Bound">L</a> <a id="6250" href="plfa.part3.Compositional.html#6250" class="Bound">M</a> <a id="6252" class="Symbol">:</a> <a id="6254" href="plfa.part3.Compositional.html#6234" class="Bound">Γ</a> <a id="6256" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="6258" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="6259" class="Symbol">}{</a><a id="6261" href="plfa.part3.Compositional.html#6261" class="Bound">v</a> <a id="6263" class="Symbol">:</a> <a id="6265" href="plfa.part3.Denotational.html#4070" class="Datatype">Value</a><a id="6270" class="Symbol">}</a>
|
||
<a id="6274" class="Symbol">→</a> <a id="6276" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="6278" class="Symbol">(</a><a id="6279" href="/19.08/Compositional/#6248" class="Bound">L</a> <a id="6281" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="6283" href="plfa.part3.Compositional.html#6250" class="Bound">M</a><a id="6284" class="Symbol">)</a> <a id="6286" href="plfa.part3.Compositional.html#6237" class="Bound">γ</a> <a id="6288" href="plfa.part3.Compositional.html#6261" class="Bound">v</a>
|
||
<a id="6294" class="Comment">----------------</a>
|
||
<a id="6313" class="Symbol">→</a> <a id="6315" class="Symbol">(</a><a id="6316" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="6318" href="/19.08/Compositional/#6248" class="Bound">L</a> <a id="6320" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="6322" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="6324" href="plfa.part3.Compositional.html#6250" class="Bound">M</a><a id="6325" class="Symbol">)</a> <a id="6327" href="plfa.part3.Compositional.html#6237" class="Bound">γ</a> <a id="6329" href="plfa.part3.Compositional.html#6261" class="Bound">v</a>
|
||
<a id="6331" href="/19.08/Compositional/#6224" class="Function">ℰ·→●ℰ</a> <a id="6337" class="Symbol">(</a><a id="6338" href="/19.08/Denotational/#9546" class="InductiveConstructor">↦-elim</a><a id="6344" class="Symbol">{</a><a id="6345" class="Argument">v</a> <a id="6347" class="Symbol">=</a> <a id="6349" href="plfa.part3.Compositional.html#6349" class="Bound">v′</a><a id="6351" class="Symbol">}</a> <a id="6353" href="plfa.part3.Compositional.html#6353" class="Bound">d₁</a> <a id="6356" href="plfa.part3.Compositional.html#6356" class="Bound">d₂</a><a id="6358" class="Symbol">)</a> <a id="6360" class="Symbol">=</a> <a id="6362" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="6367" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6369" href="plfa.part3.Compositional.html#6349" class="Bound">v′</a> <a id="6372" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6374" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6376" href="plfa.part3.Compositional.html#6353" class="Bound">d₁</a> <a id="6379" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6381" href="plfa.part3.Compositional.html#6356" class="Bound">d₂</a> <a id="6384" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6386" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="6388" href="/19.08/Compositional/#6224" class="Function">ℰ·→●ℰ</a> <a id="6394" class="Symbol">{</a><a id="6395" class="Argument">v</a> <a id="6397" class="Symbol">=</a> <a id="6399" href="/19.08/Denotational/#4090" class="InductiveConstructor">⊥</a><a id="6400" class="Symbol">}</a> <a id="6402" href="plfa.part3.Denotational.html#9780" class="InductiveConstructor">⊥-intro</a> <a id="6410" class="Symbol">=</a> <a id="6412" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="6417" href="plfa.part3.Denotational.html#4462" class="InductiveConstructor">⊑-bot</a>
|
||
<a id="6423" href="/19.08/Compositional/#6224" class="Function">ℰ·→●ℰ</a> <a id="6429" class="Symbol">{</a><a id="6430" href="plfa.part3.Compositional.html#6430" class="Bound">Γ</a><a id="6431" class="Symbol">}{</a><a id="6433" href="plfa.part3.Compositional.html#6433" class="Bound">γ</a><a id="6434" class="Symbol">}{</a><a id="6436" href="plfa.part3.Compositional.html#6436" class="Bound">L</a><a id="6437" class="Symbol">}{</a><a id="6439" href="plfa.part3.Compositional.html#6439" class="Bound">M</a><a id="6440" class="Symbol">}{</a><a id="6442" href="plfa.part3.Compositional.html#6442" class="Bound">v</a><a id="6443" class="Symbol">}</a> <a id="6445" class="Symbol">(</a><a id="6446" href="/19.08/Denotational/#9847" class="InductiveConstructor">⊔-intro</a><a id="6453" class="Symbol">{</a><a id="6454" class="Argument">v</a> <a id="6456" class="Symbol">=</a> <a id="6458" href="plfa.part3.Compositional.html#6458" class="Bound">v₁</a><a id="6460" class="Symbol">}{</a><a id="6462" class="Argument">w</a> <a id="6464" class="Symbol">=</a> <a id="6466" href="plfa.part3.Compositional.html#6466" class="Bound">v₂</a><a id="6468" class="Symbol">}</a> <a id="6470" href="plfa.part3.Compositional.html#6470" class="Bound">d₁</a> <a id="6473" href="plfa.part3.Compositional.html#6473" class="Bound">d₂</a><a id="6475" class="Symbol">)</a>
|
||
<a id="6481" class="Keyword">with</a> <a id="6486" href="/19.08/Compositional/#6224" class="Function">ℰ·→●ℰ</a> <a id="6492" href="plfa.part3.Compositional.html#6470" class="Bound">d₁</a> <a id="6495" class="Symbol">|</a> <a id="6497" href="plfa.part3.Compositional.html#6224" class="Function">ℰ·→●ℰ</a> <a id="6503" href="plfa.part3.Compositional.html#6473" class="Bound">d₂</a>
|
||
<a id="6506" class="Symbol">...</a> <a id="6510" class="Symbol">|</a> <a id="6512" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="6517" href="/19.08/Compositional/#6517" class="Bound">lt1</a> <a id="6521" class="Symbol">|</a> <a id="6523" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="6528" href="plfa.part3.Compositional.html#6528" class="Bound">lt2</a> <a id="6532" class="Symbol">=</a> <a id="6534" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="6539" class="Symbol">(</a><a id="6540" href="/19.08/Denotational/#4487" class="InductiveConstructor">⊑-conj-L</a> <a id="6549" href="plfa.part3.Compositional.html#6517" class="Bound">lt1</a> <a id="6553" href="plfa.part3.Compositional.html#6528" class="Bound">lt2</a><a id="6556" class="Symbol">)</a>
|
||
<a id="6558" class="Symbol">...</a> <a id="6562" class="Symbol">|</a> <a id="6564" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="6569" href="/19.08/Compositional/#6569" class="Bound">lt1</a> <a id="6573" class="Symbol">|</a> <a id="6575" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="6580" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6582" href="plfa.part3.Compositional.html#6582" class="Bound">v₁′</a> <a id="6586" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6588" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6590" href="plfa.part3.Compositional.html#6590" class="Bound">L↓v12</a> <a id="6596" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6598" href="plfa.part3.Compositional.html#6598" class="Bound">M↓v3</a> <a id="6603" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6605" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6607" class="Symbol">=</a>
|
||
<a id="6615" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="6620" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6622" href="/19.08/Compositional/#6582" class="Bound">v₁′</a> <a id="6626" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6628" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6630" href="/19.08/Denotational/#9962" class="InductiveConstructor">sub</a> <a id="6634" href="plfa.part3.Compositional.html#6590" class="Bound">L↓v12</a> <a id="6640" href="plfa.part3.Compositional.html#6666" class="Function">lt</a> <a id="6643" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6645" href="plfa.part3.Compositional.html#6598" class="Bound">M↓v3</a> <a id="6650" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6652" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="6660" class="Keyword">where</a> <a id="6666" href="/19.08/Compositional/#6666" class="Function">lt</a> <a id="6669" class="Symbol">:</a> <a id="6671" href="plfa.part3.Compositional.html#6582" class="Bound">v₁′</a> <a id="6675" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="6677" class="Symbol">(</a><a id="6678" class="Bound">v₁</a> <a id="6681" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="6683" class="Bound">v₂</a><a id="6685" class="Symbol">)</a> <a id="6687" href="plfa.part3.Denotational.html#4427" class="Datatype Operator">⊑</a> <a id="6689" href="plfa.part3.Compositional.html#6582" class="Bound">v₁′</a> <a id="6693" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="6695" class="Bound">v₂</a>
|
||
<a id="6710" href="/19.08/Compositional/#6666" class="Function">lt</a> <a id="6713" class="Symbol">=</a> <a id="6715" class="Symbol">(</a><a id="6716" href="/19.08/Denotational/#4788" class="InductiveConstructor">⊑-fun</a> <a id="6722" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a> <a id="6729" class="Symbol">(</a><a id="6730" href="plfa.part3.Denotational.html#4487" class="InductiveConstructor">⊑-conj-L</a> <a id="6739" class="Symbol">(</a><a id="6740" href="plfa.part3.Denotational.html#4717" class="InductiveConstructor">⊑-trans</a> <a id="6748" href="plfa.part3.Compositional.html#6569" class="Bound">lt1</a> <a id="6752" href="plfa.part3.Denotational.html#4462" class="InductiveConstructor">⊑-bot</a><a id="6757" class="Symbol">)</a> <a id="6759" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a><a id="6765" class="Symbol">))</a>
|
||
<a id="6768" class="Symbol">...</a> <a id="6772" class="Symbol">|</a> <a id="6774" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="6779" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6781" href="/19.08/Compositional/#6781" class="Bound">v₁′</a> <a id="6785" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6787" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6789" href="plfa.part3.Compositional.html#6789" class="Bound">L↓v12</a> <a id="6795" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6797" href="plfa.part3.Compositional.html#6797" class="Bound">M↓v3</a> <a id="6802" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6804" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6806" class="Symbol">|</a> <a id="6808" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="6813" href="plfa.part3.Compositional.html#6813" class="Bound">lt2</a> <a id="6817" class="Symbol">=</a>
|
||
<a id="6825" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="6830" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6832" href="/19.08/Compositional/#6781" class="Bound">v₁′</a> <a id="6836" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6838" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6840" href="/19.08/Denotational/#9962" class="InductiveConstructor">sub</a> <a id="6844" href="plfa.part3.Compositional.html#6789" class="Bound">L↓v12</a> <a id="6850" href="plfa.part3.Compositional.html#6876" class="Function">lt</a> <a id="6853" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6855" href="plfa.part3.Compositional.html#6797" class="Bound">M↓v3</a> <a id="6860" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6862" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="6870" class="Keyword">where</a> <a id="6876" href="/19.08/Compositional/#6876" class="Function">lt</a> <a id="6879" class="Symbol">:</a> <a id="6881" href="plfa.part3.Compositional.html#6781" class="Bound">v₁′</a> <a id="6885" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="6887" class="Symbol">(</a><a id="6888" class="Bound">v₁</a> <a id="6891" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="6893" class="Bound">v₂</a><a id="6895" class="Symbol">)</a> <a id="6897" href="plfa.part3.Denotational.html#4427" class="Datatype Operator">⊑</a> <a id="6899" href="plfa.part3.Compositional.html#6781" class="Bound">v₁′</a> <a id="6903" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="6905" class="Bound">v₁</a>
|
||
<a id="6920" href="/19.08/Compositional/#6876" class="Function">lt</a> <a id="6923" class="Symbol">=</a> <a id="6925" class="Symbol">(</a><a id="6926" href="/19.08/Denotational/#4788" class="InductiveConstructor">⊑-fun</a> <a id="6932" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a> <a id="6939" class="Symbol">(</a><a id="6940" href="plfa.part3.Denotational.html#4487" class="InductiveConstructor">⊑-conj-L</a> <a id="6949" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a> <a id="6956" class="Symbol">(</a><a id="6957" href="plfa.part3.Denotational.html#4717" class="InductiveConstructor">⊑-trans</a> <a id="6965" href="plfa.part3.Compositional.html#6813" class="Bound">lt2</a> <a id="6969" href="plfa.part3.Denotational.html#4462" class="InductiveConstructor">⊑-bot</a><a id="6974" class="Symbol">)))</a>
|
||
<a id="6978" class="Symbol">...</a> <a id="6982" class="Symbol">|</a> <a id="6984" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="6989" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6991" href="/19.08/Compositional/#6991" class="Bound">v₁′</a> <a id="6995" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6997" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6999" href="plfa.part3.Compositional.html#6999" class="Bound">L↓v12</a> <a id="7005" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7007" href="plfa.part3.Compositional.html#7007" class="Bound">M↓v3</a> <a id="7012" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7014" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7016" class="Symbol">|</a> <a id="7018" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="7023" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7025" href="plfa.part3.Compositional.html#7025" class="Bound">v₁′′</a> <a id="7030" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7032" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7034" href="plfa.part3.Compositional.html#7034" class="Bound">L↓v12′</a> <a id="7041" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7043" href="plfa.part3.Compositional.html#7043" class="Bound">M↓v3′</a> <a id="7049" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7051" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7053" class="Symbol">=</a>
|
||
<a id="7061" class="Keyword">let</a> <a id="7065" href="/19.08/Compositional/#7065" class="Bound">L↓⊔</a> <a id="7069" class="Symbol">=</a> <a id="7071" href="/19.08/Denotational/#9847" class="InductiveConstructor">⊔-intro</a> <a id="7079" href="plfa.part3.Compositional.html#6999" class="Bound">L↓v12</a> <a id="7085" href="plfa.part3.Compositional.html#7034" class="Bound">L↓v12′</a> <a id="7092" class="Keyword">in</a>
|
||
<a id="7101" class="Keyword">let</a> <a id="7105" href="/19.08/Compositional/#7105" class="Bound">M↓⊔</a> <a id="7109" class="Symbol">=</a> <a id="7111" href="/19.08/Denotational/#9847" class="InductiveConstructor">⊔-intro</a> <a id="7119" href="plfa.part3.Compositional.html#7007" class="Bound">M↓v3</a> <a id="7124" href="plfa.part3.Compositional.html#7043" class="Bound">M↓v3′</a> <a id="7130" class="Keyword">in</a>
|
||
<a id="7139" class="Keyword">let</a> <a id="7143" href="/19.08/Compositional/#7143" class="Bound">x</a> <a id="7145" class="Symbol">=</a> <a id="7147" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="7152" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7154" href="plfa.part3.Compositional.html#6991" class="Bound">v₁′</a> <a id="7158" href="/19.08/Denotational/#4132" class="InductiveConstructor Operator">⊔</a> <a id="7160" href="plfa.part3.Compositional.html#7025" class="Bound">v₁′′</a> <a id="7165" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7167" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7169" href="plfa.part3.Denotational.html#9962" class="InductiveConstructor">sub</a> <a id="7173" href="plfa.part3.Compositional.html#7065" class="Bound">L↓⊔</a> <a id="7177" href="plfa.part3.Denotational.html#6192" class="Function">⊔↦⊔-dist</a> <a id="7186" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7188" href="plfa.part3.Compositional.html#7105" class="Bound">M↓⊔</a> <a id="7192" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7194" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7196" class="Keyword">in</a>
|
||
<a id="7205" href="/19.08/Compositional/#7143" class="Bound">x</a>
|
||
<a id="7207" href="/19.08/Compositional/#6224" class="Function">ℰ·→●ℰ</a> <a id="7213" class="Symbol">{</a><a id="7214" href="plfa.part3.Compositional.html#7214" class="Bound">Γ</a><a id="7215" class="Symbol">}{</a><a id="7217" href="plfa.part3.Compositional.html#7217" class="Bound">γ</a><a id="7218" class="Symbol">}{</a><a id="7220" href="plfa.part3.Compositional.html#7220" class="Bound">L</a><a id="7221" class="Symbol">}{</a><a id="7223" href="plfa.part3.Compositional.html#7223" class="Bound">M</a><a id="7224" class="Symbol">}{</a><a id="7226" href="plfa.part3.Compositional.html#7226" class="Bound">v</a><a id="7227" class="Symbol">}</a> <a id="7229" class="Symbol">(</a><a id="7230" href="/19.08/Denotational/#9962" class="InductiveConstructor">sub</a> <a id="7234" href="plfa.part3.Compositional.html#7234" class="Bound">d</a> <a id="7236" href="plfa.part3.Compositional.html#7236" class="Bound">lt</a><a id="7238" class="Symbol">)</a>
|
||
<a id="7244" class="Keyword">with</a> <a id="7249" href="/19.08/Compositional/#6224" class="Function">ℰ·→●ℰ</a> <a id="7255" href="plfa.part3.Compositional.html#7234" class="Bound">d</a>
|
||
<a id="7257" class="Symbol">...</a> <a id="7261" class="Symbol">|</a> <a id="7263" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="7268" href="/19.08/Compositional/#7268" class="Bound">lt2</a> <a id="7272" class="Symbol">=</a> <a id="7274" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="7279" class="Symbol">(</a><a id="7280" href="/19.08/Denotational/#4717" class="InductiveConstructor">⊑-trans</a> <a id="7288" class="Bound">lt</a> <a id="7291" href="plfa.part3.Compositional.html#7268" class="Bound">lt2</a><a id="7294" class="Symbol">)</a>
|
||
<a id="7296" class="Symbol">...</a> <a id="7300" class="Symbol">|</a> <a id="7302" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="7307" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7309" href="/19.08/Compositional/#7309" class="Bound">v₁</a> <a id="7312" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7314" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7316" href="plfa.part3.Compositional.html#7316" class="Bound">L↓v12</a> <a id="7322" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7324" href="plfa.part3.Compositional.html#7324" class="Bound">M↓v3</a> <a id="7329" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7331" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7333" class="Symbol">=</a>
|
||
<a id="7341" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="7346" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7348" href="/19.08/Compositional/#7309" class="Bound">v₁</a> <a id="7351" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7353" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7355" href="/19.08/Denotational/#9962" class="InductiveConstructor">sub</a> <a id="7359" href="plfa.part3.Compositional.html#7316" class="Bound">L↓v12</a> <a id="7365" class="Symbol">(</a><a id="7366" href="plfa.part3.Denotational.html#4788" class="InductiveConstructor">⊑-fun</a> <a id="7372" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a> <a id="7379" class="Bound">lt</a><a id="7381" class="Symbol">)</a> <a id="7383" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7385" href="plfa.part3.Compositional.html#7324" class="Bound">M↓v3</a> <a id="7390" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7392" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
</pre>
|
||
<p>We proceed by induction on the semantics.</p>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>In case <code class="language-plaintext highlighter-rouge">↦-elim</code> we have <code class="language-plaintext highlighter-rouge">γ ⊢ L ↓ (v′ ↦ v)</code> and <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v′</code>,
|
||
which is all we need to show <code class="language-plaintext highlighter-rouge">(ℰ L ● ℰ M) γ v</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>In case <code class="language-plaintext highlighter-rouge">⊥-intro</code> we have <code class="language-plaintext highlighter-rouge">v = ⊥</code>. We conclude that <code class="language-plaintext highlighter-rouge">v ⊑ ⊥</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>In case <code class="language-plaintext highlighter-rouge">⊔-intro</code> we have <code class="language-plaintext highlighter-rouge">ℰ (L · M) γ v₁</code> and <code class="language-plaintext highlighter-rouge">ℰ (L · M) γ v₂</code>
|
||
and need to show <code class="language-plaintext highlighter-rouge">(ℰ L ● ℰ M) γ (v₁ ⊔ v₂)</code>. By the induction
|
||
hypothesis, we have <code class="language-plaintext highlighter-rouge">(ℰ L ● ℰ M) γ v₁</code> and <code class="language-plaintext highlighter-rouge">(ℰ L ● ℰ M) γ v₂</code>.
|
||
We have four subcases to consider.</p>
|
||
|
||
<ul>
|
||
<li>Suppose <code class="language-plaintext highlighter-rouge">v₁ ⊑ ⊥</code> and <code class="language-plaintext highlighter-rouge">v₂ ⊑ ⊥</code>. Then <code class="language-plaintext highlighter-rouge">v₁ ⊔ v₂ ⊑ ⊥</code>.</li>
|
||
<li>Suppose <code class="language-plaintext highlighter-rouge">v₁ ⊑ ⊥</code>, <code class="language-plaintext highlighter-rouge">γ ⊢ L ↓ v₁′ ↦ v₂</code>, and <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v₁′</code>.
|
||
We have <code class="language-plaintext highlighter-rouge">γ ⊢ L ↓ v₁′ ↦ (v₁ ⊔ v₂)</code> by rule <code class="language-plaintext highlighter-rouge">sub</code>
|
||
because <code class="language-plaintext highlighter-rouge">v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₂</code>.</li>
|
||
<li>Suppose <code class="language-plaintext highlighter-rouge">γ ⊢ L ↓ v₁′ ↦ v₁</code>, <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v₁′</code>, and <code class="language-plaintext highlighter-rouge">v₂ ⊑ ⊥</code>.
|
||
We have <code class="language-plaintext highlighter-rouge">γ ⊢ L ↓ v₁′ ↦ (v₁ ⊔ v₂)</code> by rule <code class="language-plaintext highlighter-rouge">sub</code>
|
||
because <code class="language-plaintext highlighter-rouge">v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₁</code>.</li>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">γ ⊢ L ↓ v₁′′ ↦ v₁, γ ⊢ M ↓ v₁′′</code>,
|
||
<code class="language-plaintext highlighter-rouge">γ ⊢ L ↓ v₁′ ↦ v₂</code>, and <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v₁′</code>.
|
||
This case is the most interesting.
|
||
By two uses of the rule <code class="language-plaintext highlighter-rouge">⊔-intro</code> we have
|
||
<code class="language-plaintext highlighter-rouge">γ ⊢ L ↓ (v₁′ ↦ v₂) ⊔ (v₁′′ ↦ v₁)</code> and
|
||
<code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ (v₁′ ⊔ v₁′′)</code>. But this does not yet match
|
||
what we need for <code class="language-plaintext highlighter-rouge">ℰ L ● ℰ M</code> because the result of
|
||
<code class="language-plaintext highlighter-rouge">L</code> must be an <code class="language-plaintext highlighter-rouge">↦</code> whose input entry is <code class="language-plaintext highlighter-rouge">v₁′ ⊔ v₁′′</code>.
|
||
So we use the <code class="language-plaintext highlighter-rouge">sub</code> rule to obtain
|
||
<code class="language-plaintext highlighter-rouge">γ ⊢ L ↓ (v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂)</code>,
|
||
using the <code class="language-plaintext highlighter-rouge">⊔↦⊔-dist</code> lemma (thanks to the <code class="language-plaintext highlighter-rouge">⊑-dist</code> rule) to
|
||
show that</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> (v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂) ⊑ (v₁′ ↦ v₂) ⊔ (v₁′′ ↦ v₁)
|
||
</code></pre></div> </div>
|
||
|
||
<p>So we have proved what is needed for this case.</p>
|
||
</li>
|
||
</ul>
|
||
</li>
|
||
<li>
|
||
<p>In case <code class="language-plaintext highlighter-rouge">sub</code> we have <code class="language-plaintext highlighter-rouge">Γ ⊢ L · M ↓ v₁</code> and <code class="language-plaintext highlighter-rouge">v ⊑ v₁</code>.
|
||
By the induction hypothesis, we have <code class="language-plaintext highlighter-rouge">(ℰ L ● ℰ M) γ v₁</code>.
|
||
We have two subcases to consider.</p>
|
||
|
||
<ul>
|
||
<li>Suppose <code class="language-plaintext highlighter-rouge">v₁ ⊑ ⊥</code>. We conclude that <code class="language-plaintext highlighter-rouge">v ⊑ ⊥</code>.</li>
|
||
<li>Suppose <code class="language-plaintext highlighter-rouge">Γ ⊢ L ↓ v′ → v₁</code> and <code class="language-plaintext highlighter-rouge">Γ ⊢ M ↓ v′</code>.
|
||
We conclude with <code class="language-plaintext highlighter-rouge">Γ ⊢ L ↓ v′ → v</code> by rule <code class="language-plaintext highlighter-rouge">sub</code>, because
|
||
<code class="language-plaintext highlighter-rouge">v′ → v ⊑ v′ → v₁</code>.</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
|
||
<p>The forward direction is proved by cases on the premise <code class="language-plaintext highlighter-rouge">(ℰ L ● ℰ M) γ v</code>.
|
||
In case <code class="language-plaintext highlighter-rouge">v ⊑ ⊥</code>, we obtain <code class="language-plaintext highlighter-rouge">Γ ⊢ L · M ↓ ⊥</code> by rule <code class="language-plaintext highlighter-rouge">⊥-intro</code>.
|
||
Otherwise, we conclude immediately by rule <code class="language-plaintext highlighter-rouge">↦-elim</code>.</p>
|
||
|
||
<pre class="Agda"><a id="●ℰ→ℰ·"></a><a id="9458" href="/19.08/Compositional/#9458" class="Function">●ℰ→ℰ·</a> <a id="9464" class="Symbol">:</a> <a id="9466" class="Symbol">∀{</a><a id="9468" href="plfa.part3.Compositional.html#9468" class="Bound">Γ</a><a id="9469" class="Symbol">}{</a><a id="9471" href="plfa.part3.Compositional.html#9471" class="Bound">γ</a> <a id="9473" class="Symbol">:</a> <a id="9475" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="9479" href="plfa.part3.Compositional.html#9468" class="Bound">Γ</a><a id="9480" class="Symbol">}{</a><a id="9482" href="plfa.part3.Compositional.html#9482" class="Bound">L</a> <a id="9484" href="plfa.part3.Compositional.html#9484" class="Bound">M</a> <a id="9486" class="Symbol">:</a> <a id="9488" href="plfa.part3.Compositional.html#9468" class="Bound">Γ</a> <a id="9490" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="9492" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="9493" class="Symbol">}{</a><a id="9495" href="plfa.part3.Compositional.html#9495" class="Bound">v</a><a id="9496" class="Symbol">}</a>
|
||
<a id="9500" class="Symbol">→</a> <a id="9502" class="Symbol">(</a><a id="9503" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="9505" href="/19.08/Compositional/#9482" class="Bound">L</a> <a id="9507" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="9509" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="9511" href="plfa.part3.Compositional.html#9484" class="Bound">M</a><a id="9512" class="Symbol">)</a> <a id="9514" href="plfa.part3.Compositional.html#9471" class="Bound">γ</a> <a id="9516" href="plfa.part3.Compositional.html#9495" class="Bound">v</a>
|
||
<a id="9522" class="Comment">----------------</a>
|
||
<a id="9541" class="Symbol">→</a> <a id="9543" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="9545" class="Symbol">(</a><a id="9546" href="/19.08/Compositional/#9482" class="Bound">L</a> <a id="9548" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="9550" href="plfa.part3.Compositional.html#9484" class="Bound">M</a><a id="9551" class="Symbol">)</a> <a id="9553" href="plfa.part3.Compositional.html#9471" class="Bound">γ</a> <a id="9555" href="plfa.part3.Compositional.html#9495" class="Bound">v</a>
|
||
<a id="9557" href="/19.08/Compositional/#9458" class="Function">●ℰ→ℰ·</a> <a id="9563" class="Symbol">{</a><a id="9564" href="plfa.part3.Compositional.html#9564" class="Bound">γ</a><a id="9565" class="Symbol">}{</a><a id="9567" href="plfa.part3.Compositional.html#9567" class="Bound">v</a><a id="9568" class="Symbol">}</a> <a id="9570" class="Symbol">(</a><a id="9571" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="9576" href="plfa.part3.Compositional.html#9576" class="Bound">lt</a><a id="9578" class="Symbol">)</a> <a id="9580" class="Symbol">=</a> <a id="9582" href="/19.08/Denotational/#9962" class="InductiveConstructor">sub</a> <a id="9586" href="plfa.part3.Denotational.html#9780" class="InductiveConstructor">⊥-intro</a> <a id="9594" href="plfa.part3.Compositional.html#9576" class="Bound">lt</a>
|
||
<a id="9597" href="/19.08/Compositional/#9458" class="Function">●ℰ→ℰ·</a> <a id="9603" class="Symbol">{</a><a id="9604" href="plfa.part3.Compositional.html#9604" class="Bound">γ</a><a id="9605" class="Symbol">}{</a><a id="9607" href="plfa.part3.Compositional.html#9607" class="Bound">v</a><a id="9608" class="Symbol">}</a> <a id="9610" class="Symbol">(</a><a id="9611" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="9616" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="9618" href="plfa.part3.Compositional.html#9618" class="Bound">v₁</a> <a id="9621" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="9623" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="9625" href="plfa.part3.Compositional.html#9625" class="Bound">d1</a> <a id="9628" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="9630" href="plfa.part3.Compositional.html#9630" class="Bound">d2</a> <a id="9633" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="9635" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a><a id="9636" class="Symbol">)</a> <a id="9638" class="Symbol">=</a> <a id="9640" href="/19.08/Denotational/#9546" class="InductiveConstructor">↦-elim</a> <a id="9647" href="plfa.part3.Compositional.html#9625" class="Bound">d1</a> <a id="9650" href="plfa.part3.Compositional.html#9630" class="Bound">d2</a>
|
||
</pre>
|
||
<p>So we have proved that the semantics is compositional with respect to
|
||
function application, as witnessed by the <code class="language-plaintext highlighter-rouge">●</code> function.</p>
|
||
|
||
<pre class="Agda"><a id="app-equiv"></a><a id="9789" href="/19.08/Compositional/#9789" class="Function">app-equiv</a> <a id="9799" class="Symbol">:</a> <a id="9801" class="Symbol">∀{</a><a id="9803" href="plfa.part3.Compositional.html#9803" class="Bound">Γ</a><a id="9804" class="Symbol">}{</a><a id="9806" href="plfa.part3.Compositional.html#9806" class="Bound">L</a> <a id="9808" href="plfa.part3.Compositional.html#9808" class="Bound">M</a> <a id="9810" class="Symbol">:</a> <a id="9812" href="plfa.part3.Compositional.html#9803" class="Bound">Γ</a> <a id="9814" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="9816" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="9817" class="Symbol">}</a>
|
||
<a id="9821" class="Symbol">→</a> <a id="9823" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="9825" class="Symbol">(</a><a id="9826" href="/19.08/Compositional/#9806" class="Bound">L</a> <a id="9828" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="9830" href="plfa.part3.Compositional.html#9808" class="Bound">M</a><a id="9831" class="Symbol">)</a> <a id="9833" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="9835" class="Symbol">(</a><a id="9836" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="9838" href="plfa.part3.Compositional.html#9806" class="Bound">L</a><a id="9839" class="Symbol">)</a> <a id="9841" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="9843" class="Symbol">(</a><a id="9844" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="9846" href="plfa.part3.Compositional.html#9808" class="Bound">M</a><a id="9847" class="Symbol">)</a>
|
||
<a id="9849" href="/19.08/Compositional/#9789" class="Function">app-equiv</a> <a id="9859" href="plfa.part3.Compositional.html#9859" class="Bound">γ</a> <a id="9861" href="plfa.part3.Compositional.html#9861" class="Bound">v</a> <a id="9863" class="Symbol">=</a> <a id="9865" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="9867" href="plfa.part3.Compositional.html#6224" class="Function">ℰ·→●ℰ</a> <a id="9873" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="9875" href="plfa.part3.Compositional.html#9458" class="Function">●ℰ→ℰ·</a> <a id="9881" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
</pre>
|
||
<p>We also need an inversion lemma for variables.
|
||
If <code class="language-plaintext highlighter-rouge">Γ ⊢ x ↓ v</code>, then <code class="language-plaintext highlighter-rouge">v ⊑ γ x</code>. The proof is a straightforward
|
||
induction on the semantics.</p>
|
||
|
||
<pre class="Agda"><a id="var-inv"></a><a id="10031" href="/19.08/Compositional/#10031" class="Function">var-inv</a> <a id="10039" class="Symbol">:</a> <a id="10041" class="Symbol">∀</a> <a id="10043" class="Symbol">{</a><a id="10044" href="plfa.part3.Compositional.html#10044" class="Bound">Γ</a> <a id="10046" href="plfa.part3.Compositional.html#10046" class="Bound">v</a> <a id="10048" href="plfa.part3.Compositional.html#10048" class="Bound">x</a><a id="10049" class="Symbol">}</a> <a id="10051" class="Symbol">{</a><a id="10052" href="plfa.part3.Compositional.html#10052" class="Bound">γ</a> <a id="10054" class="Symbol">:</a> <a id="10056" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="10060" href="plfa.part3.Compositional.html#10044" class="Bound">Γ</a><a id="10061" class="Symbol">}</a>
|
||
<a id="10065" class="Symbol">→</a> <a id="10067" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="10069" class="Symbol">(</a><a id="10070" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="10072" href="/19.08/Compositional/#10048" class="Bound">x</a><a id="10073" class="Symbol">)</a> <a id="10075" href="plfa.part3.Compositional.html#10052" class="Bound">γ</a> <a id="10077" href="plfa.part3.Compositional.html#10046" class="Bound">v</a>
|
||
<a id="10083" class="Comment">-------------------</a>
|
||
<a id="10105" class="Symbol">→</a> <a id="10107" href="/19.08/Compositional/#10046" class="Bound">v</a> <a id="10109" href="/19.08/Denotational/#4427" class="Datatype Operator">⊑</a> <a id="10111" href="plfa.part3.Compositional.html#10052" class="Bound">γ</a> <a id="10113" href="plfa.part3.Compositional.html#10048" class="Bound">x</a>
|
||
<a id="10115" href="/19.08/Compositional/#10031" class="Function">var-inv</a> <a id="10123" class="Symbol">(</a><a id="10124" href="/19.08/Denotational/#9471" class="InductiveConstructor">var</a><a id="10127" class="Symbol">)</a> <a id="10129" class="Symbol">=</a> <a id="10131" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a>
|
||
<a id="10138" href="/19.08/Compositional/#10031" class="Function">var-inv</a> <a id="10146" class="Symbol">(</a><a id="10147" href="/19.08/Denotational/#9847" class="InductiveConstructor">⊔-intro</a> <a id="10155" href="plfa.part3.Compositional.html#10155" class="Bound">d₁</a> <a id="10158" href="plfa.part3.Compositional.html#10158" class="Bound">d₂</a><a id="10160" class="Symbol">)</a> <a id="10162" class="Symbol">=</a> <a id="10164" href="plfa.part3.Denotational.html#4487" class="InductiveConstructor">⊑-conj-L</a> <a id="10173" class="Symbol">(</a><a id="10174" href="plfa.part3.Compositional.html#10031" class="Function">var-inv</a> <a id="10182" href="plfa.part3.Compositional.html#10155" class="Bound">d₁</a><a id="10184" class="Symbol">)</a> <a id="10186" class="Symbol">(</a><a id="10187" href="plfa.part3.Compositional.html#10031" class="Function">var-inv</a> <a id="10195" href="plfa.part3.Compositional.html#10158" class="Bound">d₂</a><a id="10197" class="Symbol">)</a>
|
||
<a id="10199" href="/19.08/Compositional/#10031" class="Function">var-inv</a> <a id="10207" class="Symbol">(</a><a id="10208" href="/19.08/Denotational/#9962" class="InductiveConstructor">sub</a> <a id="10212" href="plfa.part3.Compositional.html#10212" class="Bound">d</a> <a id="10214" href="plfa.part3.Compositional.html#10214" class="Bound">lt</a><a id="10216" class="Symbol">)</a> <a id="10218" class="Symbol">=</a> <a id="10220" href="plfa.part3.Denotational.html#4717" class="InductiveConstructor">⊑-trans</a> <a id="10228" href="plfa.part3.Compositional.html#10214" class="Bound">lt</a> <a id="10231" class="Symbol">(</a><a id="10232" href="plfa.part3.Compositional.html#10031" class="Function">var-inv</a> <a id="10240" href="plfa.part3.Compositional.html#10212" class="Bound">d</a><a id="10241" class="Symbol">)</a>
|
||
<a id="10243" href="/19.08/Compositional/#10031" class="Function">var-inv</a> <a id="10251" href="/19.08/Denotational/#9780" class="InductiveConstructor">⊥-intro</a> <a id="10259" class="Symbol">=</a> <a id="10261" href="plfa.part3.Denotational.html#4462" class="InductiveConstructor">⊑-bot</a>
|
||
</pre>
|
||
<p>To round-out the semantic equations, we establish the following one
|
||
for variables.</p>
|
||
|
||
<pre class="Agda"><a id="var-equiv"></a><a id="10360" href="/19.08/Compositional/#10360" class="Function">var-equiv</a> <a id="10370" class="Symbol">:</a> <a id="10372" class="Symbol">∀{</a><a id="10374" href="plfa.part3.Compositional.html#10374" class="Bound">Γ</a><a id="10375" class="Symbol">}{</a><a id="10377" href="plfa.part3.Compositional.html#10377" class="Bound">x</a> <a id="10379" class="Symbol">:</a> <a id="10381" href="plfa.part3.Compositional.html#10374" class="Bound">Γ</a> <a id="10383" href="/19.08/Untyped/#3521" class="Datatype Operator">∋</a> <a id="10385" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="10386" class="Symbol">}</a> <a id="10388" class="Symbol">→</a> <a id="10390" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="10392" class="Symbol">(</a><a id="10393" href="plfa.part2.Untyped.html#4330" class="InductiveConstructor Operator">`</a> <a id="10395" href="plfa.part3.Compositional.html#10377" class="Bound">x</a><a id="10396" class="Symbol">)</a> <a id="10398" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="10400" class="Symbol">(λ</a> <a id="10403" href="plfa.part3.Compositional.html#10403" class="Bound">γ</a> <a id="10405" href="plfa.part3.Compositional.html#10405" class="Bound">v</a> <a id="10407" class="Symbol">→</a> <a id="10409" href="plfa.part3.Compositional.html#10405" class="Bound">v</a> <a id="10411" href="plfa.part3.Denotational.html#4427" class="Datatype Operator">⊑</a> <a id="10413" href="plfa.part3.Compositional.html#10403" class="Bound">γ</a> <a id="10415" href="plfa.part3.Compositional.html#10377" class="Bound">x</a><a id="10416" class="Symbol">)</a>
|
||
<a id="10418" href="/19.08/Compositional/#10360" class="Function">var-equiv</a> <a id="10428" href="plfa.part3.Compositional.html#10428" class="Bound">γ</a> <a id="10430" href="plfa.part3.Compositional.html#10430" class="Bound">v</a> <a id="10432" class="Symbol">=</a> <a id="10434" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="10436" href="plfa.part3.Compositional.html#10031" class="Function">var-inv</a> <a id="10444" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="10446" class="Symbol">(λ</a> <a id="10449" href="plfa.part3.Compositional.html#10449" class="Bound">lt</a> <a id="10452" class="Symbol">→</a> <a id="10454" href="/19.08/Denotational/#9962" class="InductiveConstructor">sub</a> <a id="10458" href="plfa.part3.Denotational.html#9471" class="InductiveConstructor">var</a> <a id="10462" href="plfa.part3.Compositional.html#10449" class="Bound">lt</a><a id="10464" class="Symbol">)</a> <a id="10466" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
</pre>
|
||
|
||
<h2 id="congruence">Congruence</h2>
|
||
|
||
<p>The main work of this chapter is complete: we have established
|
||
semantic equations that show how the denotational semantics is
|
||
compositional. In this section and the next we make use of these
|
||
equations to prove some corollaries: that denotational equality is a
|
||
<em>congruence</em> and to prove the <em>compositionality property</em>, which states
|
||
that surrounding two denotationally-equal terms in the same context
|
||
produces two programs that are denotationally equal.</p>
|
||
|
||
<p>We begin by showing that denotational equality is a congruence with
|
||
respect to lambda abstraction: that <code class="language-plaintext highlighter-rouge">ℰ N ≃ ℰ N′</code> implies <code class="language-plaintext highlighter-rouge">ℰ (ƛ N) ≃ ℰ
|
||
(ƛ N′)</code>. We shall use the <code class="language-plaintext highlighter-rouge">lam-equiv</code> equation to reduce this question to
|
||
whether <code class="language-plaintext highlighter-rouge">ℱ</code> is a congruence.</p>
|
||
|
||
<pre class="Agda"><a id="ℱ-cong"></a><a id="11190" href="/19.08/Compositional/#11190" class="Function">ℱ-cong</a> <a id="11197" class="Symbol">:</a> <a id="11199" class="Symbol">∀{</a><a id="11201" href="plfa.part3.Compositional.html#11201" class="Bound">Γ</a><a id="11202" class="Symbol">}{</a><a id="11204" href="plfa.part3.Compositional.html#11204" class="Bound">D</a> <a id="11206" href="plfa.part3.Compositional.html#11206" class="Bound">D′</a> <a id="11209" class="Symbol">:</a> <a id="11211" href="/19.08/Denotational/#17303" class="Function">Denotation</a> <a id="11222" class="Symbol">(</a><a id="11223" href="plfa.part3.Compositional.html#11201" class="Bound">Γ</a> <a id="11225" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="11227" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="11228" class="Symbol">)}</a>
|
||
<a id="11233" class="Symbol">→</a> <a id="11235" href="/19.08/Compositional/#11204" class="Bound">D</a> <a id="11237" href="/19.08/Denotational/#17698" class="Function Operator">≃</a> <a id="11239" href="plfa.part3.Compositional.html#11206" class="Bound">D′</a>
|
||
<a id="11246" class="Comment">-----------</a>
|
||
<a id="11260" class="Symbol">→</a> <a id="11262" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="11264" href="plfa.part3.Compositional.html#11204" class="Bound">D</a> <a id="11266" href="/19.08/Denotational/#17698" class="Function Operator">≃</a> <a id="11268" href="plfa.part3.Compositional.html#1898" class="Function">ℱ</a> <a id="11270" href="plfa.part3.Compositional.html#11206" class="Bound">D′</a>
|
||
<a id="11273" href="/19.08/Compositional/#11190" class="Function">ℱ-cong</a><a id="11279" class="Symbol">{</a><a id="11280" href="plfa.part3.Compositional.html#11280" class="Bound">Γ</a><a id="11281" class="Symbol">}</a> <a id="11283" href="plfa.part3.Compositional.html#11283" class="Bound">D≃D′</a> <a id="11288" href="plfa.part3.Compositional.html#11288" class="Bound">γ</a> <a id="11290" href="plfa.part3.Compositional.html#11290" class="Bound">v</a> <a id="11292" class="Symbol">=</a>
|
||
<a id="11296" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11298" class="Symbol">(λ</a> <a id="11301" href="/19.08/Compositional/#11301" class="Bound">x</a> <a id="11303" class="Symbol">→</a> <a id="11305" href="plfa.part3.Compositional.html#11368" class="Function">ℱ≃</a><a id="11307" class="Symbol">{</a><a id="11308" href="plfa.part3.Compositional.html#11288" class="Bound">γ</a><a id="11309" class="Symbol">}{</a><a id="11311" href="plfa.part3.Compositional.html#11290" class="Bound">v</a><a id="11312" class="Symbol">}</a> <a id="11314" href="plfa.part3.Compositional.html#11301" class="Bound">x</a> <a id="11316" href="plfa.part3.Compositional.html#11283" class="Bound">D≃D′</a><a id="11320" class="Symbol">)</a> <a id="11322" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11324" class="Symbol">(λ</a> <a id="11327" href="plfa.part3.Compositional.html#11327" class="Bound">x</a> <a id="11329" class="Symbol">→</a> <a id="11331" href="plfa.part3.Compositional.html#11368" class="Function">ℱ≃</a><a id="11333" class="Symbol">{</a><a id="11334" href="plfa.part3.Compositional.html#11288" class="Bound">γ</a><a id="11335" class="Symbol">}{</a><a id="11337" href="plfa.part3.Compositional.html#11290" class="Bound">v</a><a id="11338" class="Symbol">}</a> <a id="11340" href="plfa.part3.Compositional.html#11327" class="Bound">x</a> <a id="11342" class="Symbol">(</a><a id="11343" href="/19.08/Denotational/#17970" class="Function">≃-sym</a> <a id="11349" href="plfa.part3.Compositional.html#11283" class="Bound">D≃D′</a><a id="11353" class="Symbol">))</a> <a id="11356" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="11360" class="Keyword">where</a>
|
||
<a id="11368" href="/19.08/Compositional/#11368" class="Function">ℱ≃</a> <a id="11371" class="Symbol">:</a> <a id="11373" class="Symbol">∀{</a><a id="11375" href="plfa.part3.Compositional.html#11375" class="Bound">γ</a> <a id="11377" class="Symbol">:</a> <a id="11379" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="11383" href="plfa.part3.Compositional.html#11280" class="Bound">Γ</a><a id="11384" class="Symbol">}{</a><a id="11386" href="plfa.part3.Compositional.html#11386" class="Bound">v</a><a id="11387" class="Symbol">}{</a><a id="11389" href="plfa.part3.Compositional.html#11389" class="Bound">D</a> <a id="11391" href="plfa.part3.Compositional.html#11391" class="Bound">D′</a> <a id="11394" class="Symbol">:</a> <a id="11396" href="plfa.part3.Denotational.html#17303" class="Function">Denotation</a> <a id="11407" class="Symbol">(</a><a id="11408" href="plfa.part3.Compositional.html#11280" class="Bound">Γ</a> <a id="11410" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="11412" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="11413" class="Symbol">)}</a>
|
||
<a id="11420" class="Symbol">→</a> <a id="11422" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="11424" href="plfa.part3.Compositional.html#11389" class="Bound">D</a> <a id="11426" href="plfa.part3.Compositional.html#11375" class="Bound">γ</a> <a id="11428" href="plfa.part3.Compositional.html#11386" class="Bound">v</a> <a id="11431" class="Symbol">→</a> <a id="11434" href="plfa.part3.Compositional.html#11389" class="Bound">D</a> <a id="11436" href="/19.08/Denotational/#17698" class="Function Operator">≃</a> <a id="11438" href="plfa.part3.Compositional.html#11391" class="Bound">D′</a> <a id="11441" class="Symbol">→</a> <a id="11443" href="plfa.part3.Compositional.html#1898" class="Function">ℱ</a> <a id="11445" href="plfa.part3.Compositional.html#11391" class="Bound">D′</a> <a id="11448" href="plfa.part3.Compositional.html#11375" class="Bound">γ</a> <a id="11450" href="plfa.part3.Compositional.html#11386" class="Bound">v</a>
|
||
<a id="11454" href="/19.08/Compositional/#11368" class="Function">ℱ≃</a> <a id="11457" class="Symbol">{</a><a id="11458" class="Argument">v</a> <a id="11460" class="Symbol">=</a> <a id="11462" href="/19.08/Denotational/#4090" class="InductiveConstructor">⊥</a><a id="11463" class="Symbol">}</a> <a id="11465" href="plfa.part3.Compositional.html#11465" class="Bound">fd</a> <a id="11468" href="plfa.part3.Compositional.html#11468" class="Bound">dd′</a> <a id="11472" class="Symbol">=</a> <a id="11474" href="Agda.Builtin.Unit.html#174" class="InductiveConstructor">tt</a>
|
||
<a id="11479" href="/19.08/Compositional/#11368" class="Function">ℱ≃</a> <a id="11482" class="Symbol">{</a><a id="11483" href="plfa.part3.Compositional.html#11483" class="Bound">γ</a><a id="11484" class="Symbol">}{</a><a id="11486" href="plfa.part3.Compositional.html#11486" class="Bound">v</a> <a id="11488" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="11490" href="plfa.part3.Compositional.html#11490" class="Bound">w</a><a id="11491" class="Symbol">}</a> <a id="11493" href="plfa.part3.Compositional.html#11493" class="Bound">fd</a> <a id="11496" href="plfa.part3.Compositional.html#11496" class="Bound">dd′</a> <a id="11500" class="Symbol">=</a> <a id="11502" href="Agda.Builtin.Sigma.html#225" class="Field">proj₁</a> <a id="11508" class="Symbol">(</a><a id="11509" href="plfa.part3.Compositional.html#11496" class="Bound">dd′</a> <a id="11513" class="Symbol">(</a><a id="11514" href="plfa.part3.Compositional.html#11483" class="Bound">γ</a> <a id="11516" href="plfa.part3.Denotational.html#7364" class="Function Operator">`,</a> <a id="11519" href="plfa.part3.Compositional.html#11486" class="Bound">v</a><a id="11520" class="Symbol">)</a> <a id="11522" href="plfa.part3.Compositional.html#11490" class="Bound">w</a><a id="11523" class="Symbol">)</a> <a id="11525" href="plfa.part3.Compositional.html#11493" class="Bound">fd</a>
|
||
<a id="11530" href="/19.08/Compositional/#11368" class="Function">ℱ≃</a> <a id="11533" class="Symbol">{</a><a id="11534" href="plfa.part3.Compositional.html#11534" class="Bound">γ</a><a id="11535" class="Symbol">}{</a><a id="11537" href="plfa.part3.Compositional.html#11537" class="Bound">u</a> <a id="11539" href="/19.08/Denotational/#4132" class="InductiveConstructor Operator">⊔</a> <a id="11541" href="plfa.part3.Compositional.html#11541" class="Bound">w</a><a id="11542" class="Symbol">}</a> <a id="11544" href="plfa.part3.Compositional.html#11544" class="Bound">fd</a> <a id="11547" href="plfa.part3.Compositional.html#11547" class="Bound">dd′</a> <a id="11551" class="Symbol">=</a> <a id="11553" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11555" href="plfa.part3.Compositional.html#11368" class="Function">ℱ≃</a><a id="11557" class="Symbol">{</a><a id="11558" href="plfa.part3.Compositional.html#11534" class="Bound">γ</a><a id="11559" class="Symbol">}{</a><a id="11561" href="plfa.part3.Compositional.html#11537" class="Bound">u</a><a id="11562" class="Symbol">}</a> <a id="11564" class="Symbol">(</a><a id="11565" href="Agda.Builtin.Sigma.html#225" class="Field">proj₁</a> <a id="11571" href="plfa.part3.Compositional.html#11544" class="Bound">fd</a><a id="11573" class="Symbol">)</a> <a id="11575" href="plfa.part3.Compositional.html#11547" class="Bound">dd′</a> <a id="11579" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11581" href="plfa.part3.Compositional.html#11368" class="Function">ℱ≃</a><a id="11583" class="Symbol">{</a><a id="11584" href="plfa.part3.Compositional.html#11534" class="Bound">γ</a><a id="11585" class="Symbol">}{</a><a id="11587" href="plfa.part3.Compositional.html#11541" class="Bound">w</a><a id="11588" class="Symbol">}</a> <a id="11590" class="Symbol">(</a><a id="11591" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a> <a id="11597" href="plfa.part3.Compositional.html#11544" class="Bound">fd</a><a id="11599" class="Symbol">)</a> <a id="11601" href="plfa.part3.Compositional.html#11547" class="Bound">dd′</a> <a id="11605" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
</pre>
|
||
<p>The proof of <code class="language-plaintext highlighter-rouge">ℱ-cong</code> uses the lemma <code class="language-plaintext highlighter-rouge">ℱ≃</code> to handle both directions of
|
||
the if-and-only-if. That lemma is proved by a straightforward
|
||
induction on the value <code class="language-plaintext highlighter-rouge">v</code>.</p>
|
||
|
||
<p>We now prove that lambda abstraction is a congruence by direct
|
||
equational reasoning.</p>
|
||
|
||
<pre class="Agda"><a id="lam-cong"></a><a id="11864" href="/19.08/Compositional/#11864" class="Function">lam-cong</a> <a id="11873" class="Symbol">:</a> <a id="11875" class="Symbol">∀{</a><a id="11877" href="plfa.part3.Compositional.html#11877" class="Bound">Γ</a><a id="11878" class="Symbol">}{</a><a id="11880" href="plfa.part3.Compositional.html#11880" class="Bound">N</a> <a id="11882" href="plfa.part3.Compositional.html#11882" class="Bound">N′</a> <a id="11885" class="Symbol">:</a> <a id="11887" href="plfa.part3.Compositional.html#11877" class="Bound">Γ</a> <a id="11889" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="11891" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="11893" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="11895" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="11896" class="Symbol">}</a>
|
||
<a id="11900" class="Symbol">→</a> <a id="11902" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="11904" href="/19.08/Compositional/#11880" class="Bound">N</a> <a id="11906" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="11908" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="11910" href="plfa.part3.Compositional.html#11882" class="Bound">N′</a>
|
||
<a id="11917" class="Comment">-----------------</a>
|
||
<a id="11937" class="Symbol">→</a> <a id="11939" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="11941" class="Symbol">(</a><a id="11942" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="11944" href="/19.08/Compositional/#11880" class="Bound">N</a><a id="11945" class="Symbol">)</a> <a id="11947" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="11949" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="11951" class="Symbol">(</a><a id="11952" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="11954" href="plfa.part3.Compositional.html#11882" class="Bound">N′</a><a id="11956" class="Symbol">)</a>
|
||
<a id="11958" href="/19.08/Compositional/#11864" class="Function">lam-cong</a> <a id="11967" class="Symbol">{</a><a id="11968" href="plfa.part3.Compositional.html#11968" class="Bound">Γ</a><a id="11969" class="Symbol">}{</a><a id="11971" href="plfa.part3.Compositional.html#11971" class="Bound">N</a><a id="11972" class="Symbol">}{</a><a id="11974" href="plfa.part3.Compositional.html#11974" class="Bound">N′</a><a id="11976" class="Symbol">}</a> <a id="11978" href="plfa.part3.Compositional.html#11978" class="Bound">N≃N′</a> <a id="11983" class="Symbol">=</a>
|
||
<a id="11987" href="/19.08/Denotational/#19190" class="Function Operator">start</a>
|
||
<a id="11997" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="11999" class="Symbol">(</a><a id="12000" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="12002" href="/19.08/Compositional/#11971" class="Bound">N</a><a id="12003" class="Symbol">)</a>
|
||
<a id="12007" href="/19.08/Denotational/#19281" class="Function Operator">≃⟨</a> <a id="12010" href="/19.08/Compositional/#4552" class="Function">lam-equiv</a> <a id="12020" href="plfa.part3.Denotational.html#19281" class="Function Operator">⟩</a>
|
||
<a id="12026" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="12028" class="Symbol">(</a><a id="12029" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="12031" href="plfa.part3.Compositional.html#11971" class="Bound">N</a><a id="12032" class="Symbol">)</a>
|
||
<a id="12036" href="/19.08/Denotational/#19281" class="Function Operator">≃⟨</a> <a id="12039" href="/19.08/Compositional/#11190" class="Function">ℱ-cong</a> <a id="12046" href="plfa.part3.Compositional.html#11978" class="Bound">N≃N′</a> <a id="12051" href="plfa.part3.Denotational.html#19281" class="Function Operator">⟩</a>
|
||
<a id="12057" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="12059" class="Symbol">(</a><a id="12060" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="12062" href="plfa.part3.Compositional.html#11974" class="Bound">N′</a><a id="12064" class="Symbol">)</a>
|
||
<a id="12068" href="/19.08/Denotational/#19281" class="Function Operator">≃⟨</a> <a id="12071" href="plfa.part3.Denotational.html#17970" class="Function">≃-sym</a> <a id="12077" href="/19.08/Compositional/#4552" class="Function">lam-equiv</a> <a id="12087" href="plfa.part3.Denotational.html#19281" class="Function Operator">⟩</a>
|
||
<a id="12093" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="12095" class="Symbol">(</a><a id="12096" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="12098" href="/19.08/Compositional/#11974" class="Bound">N′</a><a id="12100" class="Symbol">)</a>
|
||
<a id="12104" href="/19.08/Denotational/#19528" class="Function Operator">☐</a>
|
||
</pre>
|
||
<p>Next we prove that denotational equality is a congruence for
|
||
application: that <code class="language-plaintext highlighter-rouge">ℰ L ≃ ℰ L′</code> and <code class="language-plaintext highlighter-rouge">ℰ M ≃ ℰ M′</code> imply
|
||
<code class="language-plaintext highlighter-rouge">ℰ (L · M) ≃ ℰ (L′ · M′)</code>. The <code class="language-plaintext highlighter-rouge">app-equiv</code> equation
|
||
reduces this to the question of whether the <code class="language-plaintext highlighter-rouge">●</code> operator
|
||
is a congruence.</p>
|
||
|
||
<pre class="Agda"><a id="●-cong"></a><a id="12357" href="/19.08/Compositional/#12357" class="Function">●-cong</a> <a id="12364" class="Symbol">:</a> <a id="12366" class="Symbol">∀{</a><a id="12368" href="plfa.part3.Compositional.html#12368" class="Bound">Γ</a><a id="12369" class="Symbol">}{</a><a id="12371" href="plfa.part3.Compositional.html#12371" class="Bound">D₁</a> <a id="12374" href="plfa.part3.Compositional.html#12374" class="Bound">D₁′</a> <a id="12378" href="plfa.part3.Compositional.html#12378" class="Bound">D₂</a> <a id="12381" href="plfa.part3.Compositional.html#12381" class="Bound">D₂′</a> <a id="12385" class="Symbol">:</a> <a id="12387" href="/19.08/Denotational/#17303" class="Function">Denotation</a> <a id="12398" href="plfa.part3.Compositional.html#12368" class="Bound">Γ</a><a id="12399" class="Symbol">}</a>
|
||
<a id="12403" class="Symbol">→</a> <a id="12405" href="/19.08/Compositional/#12371" class="Bound">D₁</a> <a id="12408" href="/19.08/Denotational/#17698" class="Function Operator">≃</a> <a id="12410" href="plfa.part3.Compositional.html#12374" class="Bound">D₁′</a> <a id="12414" class="Symbol">→</a> <a id="12416" href="plfa.part3.Compositional.html#12378" class="Bound">D₂</a> <a id="12419" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="12421" href="plfa.part3.Compositional.html#12381" class="Bound">D₂′</a>
|
||
<a id="12427" class="Symbol">→</a> <a id="12429" class="Symbol">(</a><a id="12430" href="/19.08/Compositional/#12371" class="Bound">D₁</a> <a id="12433" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="12435" href="plfa.part3.Compositional.html#12378" class="Bound">D₂</a><a id="12437" class="Symbol">)</a> <a id="12439" href="/19.08/Denotational/#17698" class="Function Operator">≃</a> <a id="12441" class="Symbol">(</a><a id="12442" href="plfa.part3.Compositional.html#12374" class="Bound">D₁′</a> <a id="12446" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="12448" href="plfa.part3.Compositional.html#12381" class="Bound">D₂′</a><a id="12451" class="Symbol">)</a>
|
||
<a id="12453" href="/19.08/Compositional/#12357" class="Function">●-cong</a> <a id="12460" class="Symbol">{</a><a id="12461" href="plfa.part3.Compositional.html#12461" class="Bound">Γ</a><a id="12462" class="Symbol">}</a> <a id="12464" href="plfa.part3.Compositional.html#12464" class="Bound">d1</a> <a id="12467" href="plfa.part3.Compositional.html#12467" class="Bound">d2</a> <a id="12470" href="plfa.part3.Compositional.html#12470" class="Bound">γ</a> <a id="12472" href="plfa.part3.Compositional.html#12472" class="Bound">v</a> <a id="12474" class="Symbol">=</a> <a id="12476" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12478" class="Symbol">(λ</a> <a id="12481" href="plfa.part3.Compositional.html#12481" class="Bound">x</a> <a id="12483" class="Symbol">→</a> <a id="12485" href="plfa.part3.Compositional.html#12571" class="Function">●≃</a> <a id="12488" href="plfa.part3.Compositional.html#12481" class="Bound">x</a> <a id="12490" href="plfa.part3.Compositional.html#12464" class="Bound">d1</a> <a id="12493" href="plfa.part3.Compositional.html#12467" class="Bound">d2</a><a id="12495" class="Symbol">)</a> <a id="12497" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a>
|
||
<a id="12524" class="Symbol">(λ</a> <a id="12527" href="/19.08/Compositional/#12527" class="Bound">x</a> <a id="12529" class="Symbol">→</a> <a id="12531" href="plfa.part3.Compositional.html#12571" class="Function">●≃</a> <a id="12534" href="plfa.part3.Compositional.html#12527" class="Bound">x</a> <a id="12536" class="Symbol">(</a><a id="12537" href="/19.08/Denotational/#17970" class="Function">≃-sym</a> <a id="12543" href="plfa.part3.Compositional.html#12464" class="Bound">d1</a><a id="12545" class="Symbol">)</a> <a id="12547" class="Symbol">(</a><a id="12548" href="plfa.part3.Denotational.html#17970" class="Function">≃-sym</a> <a id="12554" href="plfa.part3.Compositional.html#12467" class="Bound">d2</a><a id="12556" class="Symbol">))</a> <a id="12559" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="12563" class="Keyword">where</a>
|
||
<a id="12571" href="/19.08/Compositional/#12571" class="Function">●≃</a> <a id="12574" class="Symbol">:</a> <a id="12576" class="Symbol">∀{</a><a id="12578" href="plfa.part3.Compositional.html#12578" class="Bound">γ</a> <a id="12580" class="Symbol">:</a> <a id="12582" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="12586" href="plfa.part3.Compositional.html#12461" class="Bound">Γ</a><a id="12587" class="Symbol">}{</a><a id="12589" href="plfa.part3.Compositional.html#12589" class="Bound">v</a><a id="12590" class="Symbol">}{</a><a id="12592" href="plfa.part3.Compositional.html#12592" class="Bound">D₁</a> <a id="12595" href="plfa.part3.Compositional.html#12595" class="Bound">D₁′</a> <a id="12599" href="plfa.part3.Compositional.html#12599" class="Bound">D₂</a> <a id="12602" href="plfa.part3.Compositional.html#12602" class="Bound">D₂′</a> <a id="12606" class="Symbol">:</a> <a id="12608" href="plfa.part3.Denotational.html#17303" class="Function">Denotation</a> <a id="12619" href="plfa.part3.Compositional.html#12461" class="Bound">Γ</a><a id="12620" class="Symbol">}</a>
|
||
<a id="12626" class="Symbol">→</a> <a id="12628" class="Symbol">(</a><a id="12629" href="/19.08/Compositional/#12592" class="Bound">D₁</a> <a id="12632" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="12634" href="plfa.part3.Compositional.html#12599" class="Bound">D₂</a><a id="12636" class="Symbol">)</a> <a id="12638" href="plfa.part3.Compositional.html#12578" class="Bound">γ</a> <a id="12640" href="plfa.part3.Compositional.html#12589" class="Bound">v</a> <a id="12643" class="Symbol">→</a> <a id="12646" href="plfa.part3.Compositional.html#12592" class="Bound">D₁</a> <a id="12649" href="/19.08/Denotational/#17698" class="Function Operator">≃</a> <a id="12651" href="plfa.part3.Compositional.html#12595" class="Bound">D₁′</a> <a id="12656" class="Symbol">→</a> <a id="12659" href="plfa.part3.Compositional.html#12599" class="Bound">D₂</a> <a id="12662" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="12664" href="plfa.part3.Compositional.html#12602" class="Bound">D₂′</a>
|
||
<a id="12672" class="Symbol">→</a> <a id="12674" class="Symbol">(</a><a id="12675" href="/19.08/Compositional/#12595" class="Bound">D₁′</a> <a id="12679" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="12681" href="plfa.part3.Compositional.html#12602" class="Bound">D₂′</a><a id="12684" class="Symbol">)</a> <a id="12686" href="plfa.part3.Compositional.html#12578" class="Bound">γ</a> <a id="12688" href="plfa.part3.Compositional.html#12589" class="Bound">v</a>
|
||
<a id="12692" href="/19.08/Compositional/#12571" class="Function">●≃</a> <a id="12695" class="Symbol">(</a><a id="12696" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="12701" href="plfa.part3.Compositional.html#12701" class="Bound">v⊑⊥</a><a id="12704" class="Symbol">)</a> <a id="12706" href="plfa.part3.Compositional.html#12706" class="Bound">eq₁</a> <a id="12710" href="plfa.part3.Compositional.html#12710" class="Bound">eq₂</a> <a id="12714" class="Symbol">=</a> <a id="12716" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="12721" href="plfa.part3.Compositional.html#12701" class="Bound">v⊑⊥</a>
|
||
<a id="12727" href="/19.08/Compositional/#12571" class="Function">●≃</a> <a id="12730" class="Symbol">{</a><a id="12731" href="plfa.part3.Compositional.html#12731" class="Bound">γ</a><a id="12732" class="Symbol">}</a> <a id="12734" class="Symbol">{</a><a id="12735" href="plfa.part3.Compositional.html#12735" class="Bound">w</a><a id="12736" class="Symbol">}</a> <a id="12738" class="Symbol">(</a><a id="12739" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="12744" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12746" href="plfa.part3.Compositional.html#12746" class="Bound">v</a> <a id="12748" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12750" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12752" href="plfa.part3.Compositional.html#12752" class="Bound">Dv↦w</a> <a id="12757" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12759" href="plfa.part3.Compositional.html#12759" class="Bound">Dv</a> <a id="12762" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12764" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a><a id="12765" class="Symbol">)</a> <a id="12767" href="plfa.part3.Compositional.html#12767" class="Bound">eq₁</a> <a id="12771" href="plfa.part3.Compositional.html#12771" class="Bound">eq₂</a> <a id="12775" class="Symbol">=</a>
|
||
<a id="12781" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="12786" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12788" href="/19.08/Compositional/#12746" class="Bound">v</a> <a id="12790" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12792" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12794" href="Agda.Builtin.Sigma.html#225" class="Field">proj₁</a> <a id="12800" class="Symbol">(</a><a id="12801" href="plfa.part3.Compositional.html#12767" class="Bound">eq₁</a> <a id="12805" href="plfa.part3.Compositional.html#12731" class="Bound">γ</a> <a id="12807" class="Symbol">(</a><a id="12808" href="plfa.part3.Compositional.html#12746" class="Bound">v</a> <a id="12810" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="12812" href="plfa.part3.Compositional.html#12735" class="Bound">w</a><a id="12813" class="Symbol">))</a> <a id="12816" href="plfa.part3.Compositional.html#12752" class="Bound">Dv↦w</a> <a id="12821" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12823" href="Agda.Builtin.Sigma.html#225" class="Field">proj₁</a> <a id="12829" class="Symbol">(</a><a id="12830" href="plfa.part3.Compositional.html#12771" class="Bound">eq₂</a> <a id="12834" href="plfa.part3.Compositional.html#12731" class="Bound">γ</a> <a id="12836" href="plfa.part3.Compositional.html#12746" class="Bound">v</a><a id="12837" class="Symbol">)</a> <a id="12839" href="plfa.part3.Compositional.html#12759" class="Bound">Dv</a> <a id="12842" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12844" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
</pre>
|
||
<p>Again, both directions of the if-and-only-if are proved via a lemma.
|
||
This time the lemma is proved by cases on <code class="language-plaintext highlighter-rouge">(D₁ ● D₂) γ v</code>.</p>
|
||
|
||
<p>With the congruence of <code class="language-plaintext highlighter-rouge">●</code>, we can prove that application is a
|
||
congruence by direct equational reasoning.</p>
|
||
|
||
<pre class="Agda"><a id="app-cong"></a><a id="13091" href="/19.08/Compositional/#13091" class="Function">app-cong</a> <a id="13100" class="Symbol">:</a> <a id="13102" class="Symbol">∀{</a><a id="13104" href="plfa.part3.Compositional.html#13104" class="Bound">Γ</a><a id="13105" class="Symbol">}{</a><a id="13107" href="plfa.part3.Compositional.html#13107" class="Bound">L</a> <a id="13109" href="plfa.part3.Compositional.html#13109" class="Bound">L′</a> <a id="13112" href="plfa.part3.Compositional.html#13112" class="Bound">M</a> <a id="13114" href="plfa.part3.Compositional.html#13114" class="Bound">M′</a> <a id="13117" class="Symbol">:</a> <a id="13119" href="plfa.part3.Compositional.html#13104" class="Bound">Γ</a> <a id="13121" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="13123" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="13124" class="Symbol">}</a>
|
||
<a id="13128" class="Symbol">→</a> <a id="13130" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="13132" href="/19.08/Compositional/#13107" class="Bound">L</a> <a id="13134" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="13136" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="13138" href="plfa.part3.Compositional.html#13109" class="Bound">L′</a>
|
||
<a id="13143" class="Symbol">→</a> <a id="13145" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="13147" href="/19.08/Compositional/#13112" class="Bound">M</a> <a id="13149" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="13151" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="13153" href="plfa.part3.Compositional.html#13114" class="Bound">M′</a>
|
||
<a id="13160" class="Comment">-------------------------</a>
|
||
<a id="13188" class="Symbol">→</a> <a id="13190" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="13192" class="Symbol">(</a><a id="13193" href="/19.08/Compositional/#13107" class="Bound">L</a> <a id="13195" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="13197" href="plfa.part3.Compositional.html#13112" class="Bound">M</a><a id="13198" class="Symbol">)</a> <a id="13200" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="13202" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="13204" class="Symbol">(</a><a id="13205" href="plfa.part3.Compositional.html#13109" class="Bound">L′</a> <a id="13208" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="13210" href="plfa.part3.Compositional.html#13114" class="Bound">M′</a><a id="13212" class="Symbol">)</a>
|
||
<a id="13214" href="/19.08/Compositional/#13091" class="Function">app-cong</a> <a id="13223" class="Symbol">{</a><a id="13224" href="plfa.part3.Compositional.html#13224" class="Bound">Γ</a><a id="13225" class="Symbol">}{</a><a id="13227" href="plfa.part3.Compositional.html#13227" class="Bound">L</a><a id="13228" class="Symbol">}{</a><a id="13230" href="plfa.part3.Compositional.html#13230" class="Bound">L′</a><a id="13232" class="Symbol">}{</a><a id="13234" href="plfa.part3.Compositional.html#13234" class="Bound">M</a><a id="13235" class="Symbol">}{</a><a id="13237" href="plfa.part3.Compositional.html#13237" class="Bound">M′</a><a id="13239" class="Symbol">}</a> <a id="13241" href="plfa.part3.Compositional.html#13241" class="Bound">L≅L′</a> <a id="13246" href="plfa.part3.Compositional.html#13246" class="Bound">M≅M′</a> <a id="13251" class="Symbol">=</a>
|
||
<a id="13255" href="/19.08/Denotational/#19190" class="Function Operator">start</a>
|
||
<a id="13265" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="13267" class="Symbol">(</a><a id="13268" href="/19.08/Compositional/#13227" class="Bound">L</a> <a id="13270" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="13272" href="plfa.part3.Compositional.html#13234" class="Bound">M</a><a id="13273" class="Symbol">)</a>
|
||
<a id="13277" href="/19.08/Denotational/#19281" class="Function Operator">≃⟨</a> <a id="13280" href="/19.08/Compositional/#9789" class="Function">app-equiv</a> <a id="13290" href="plfa.part3.Denotational.html#19281" class="Function Operator">⟩</a>
|
||
<a id="13296" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="13298" href="/19.08/Compositional/#13227" class="Bound">L</a> <a id="13300" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="13302" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="13304" href="plfa.part3.Compositional.html#13234" class="Bound">M</a>
|
||
<a id="13308" href="/19.08/Denotational/#19281" class="Function Operator">≃⟨</a> <a id="13311" href="/19.08/Compositional/#12357" class="Function">●-cong</a> <a id="13318" href="plfa.part3.Compositional.html#13241" class="Bound">L≅L′</a> <a id="13323" href="plfa.part3.Compositional.html#13246" class="Bound">M≅M′</a> <a id="13328" href="plfa.part3.Denotational.html#19281" class="Function Operator">⟩</a>
|
||
<a id="13334" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="13336" href="/19.08/Compositional/#13230" class="Bound">L′</a> <a id="13339" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="13341" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="13343" href="plfa.part3.Compositional.html#13237" class="Bound">M′</a>
|
||
<a id="13348" href="/19.08/Denotational/#19281" class="Function Operator">≃⟨</a> <a id="13351" href="plfa.part3.Denotational.html#17970" class="Function">≃-sym</a> <a id="13357" href="/19.08/Compositional/#9789" class="Function">app-equiv</a> <a id="13367" href="plfa.part3.Denotational.html#19281" class="Function Operator">⟩</a>
|
||
<a id="13373" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="13375" class="Symbol">(</a><a id="13376" href="/19.08/Compositional/#13230" class="Bound">L′</a> <a id="13379" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="13381" href="plfa.part3.Compositional.html#13237" class="Bound">M′</a><a id="13383" class="Symbol">)</a>
|
||
<a id="13387" href="/19.08/Denotational/#19528" class="Function Operator">☐</a>
|
||
</pre>
|
||
|
||
<h2 id="compositionality">Compositionality</h2>
|
||
|
||
<p>The <em>compositionality property</em> states that surrounding two terms that
|
||
are denotationally equal in the same context produces two programs
|
||
that are denotationally equal. To make this precise, we define what we
|
||
mean by “context” and “surround”.</p>
|
||
|
||
<p>A <em>context</em> is a program with one hole in it. The following data
|
||
definition <code class="language-plaintext highlighter-rouge">Ctx</code> makes this idea explicit. We index the <code class="language-plaintext highlighter-rouge">Ctx</code> data
|
||
type with two contexts for variables: one for the the hole and one for
|
||
terms that result from filling the hole.</p>
|
||
|
||
<pre class="Agda"><a id="13909" class="Keyword">data</a> <a id="Ctx"></a><a id="13914" href="/19.08/Compositional/#13914" class="Datatype">Ctx</a> <a id="13918" class="Symbol">:</a> <a id="13920" href="/19.08/Untyped/#3153" class="Datatype">Context</a> <a id="13928" class="Symbol">→</a> <a id="13930" href="plfa.part2.Untyped.html#3153" class="Datatype">Context</a> <a id="13938" class="Symbol">→</a> <a id="13940" class="PrimitiveType">Set</a> <a id="13944" class="Keyword">where</a>
|
||
<a id="Ctx.ctx-hole"></a><a id="13952" href="/19.08/Compositional/#13952" class="InductiveConstructor">ctx-hole</a> <a id="13961" class="Symbol">:</a> <a id="13963" class="Symbol">∀{</a><a id="13965" href="plfa.part3.Compositional.html#13965" class="Bound">Γ</a><a id="13966" class="Symbol">}</a> <a id="13968" class="Symbol">→</a> <a id="13970" href="plfa.part3.Compositional.html#13914" class="Datatype">Ctx</a> <a id="13974" href="plfa.part3.Compositional.html#13965" class="Bound">Γ</a> <a id="13976" href="plfa.part3.Compositional.html#13965" class="Bound">Γ</a>
|
||
<a id="Ctx.ctx-lam"></a><a id="13980" href="/19.08/Compositional/#13980" class="InductiveConstructor">ctx-lam</a> <a id="13988" class="Symbol">:</a> <a id="13991" class="Symbol">∀{</a><a id="13993" href="plfa.part3.Compositional.html#13993" class="Bound">Γ</a> <a id="13995" href="plfa.part3.Compositional.html#13995" class="Bound">Δ</a><a id="13996" class="Symbol">}</a> <a id="13998" class="Symbol">→</a> <a id="14000" href="plfa.part3.Compositional.html#13914" class="Datatype">Ctx</a> <a id="14004" class="Symbol">(</a><a id="14005" href="plfa.part3.Compositional.html#13993" class="Bound">Γ</a> <a id="14007" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="14009" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="14010" class="Symbol">)</a> <a id="14012" class="Symbol">(</a><a id="14013" href="plfa.part3.Compositional.html#13995" class="Bound">Δ</a> <a id="14015" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">,</a> <a id="14017" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="14018" class="Symbol">)</a> <a id="14020" class="Symbol">→</a> <a id="14022" href="plfa.part3.Compositional.html#13914" class="Datatype">Ctx</a> <a id="14026" class="Symbol">(</a><a id="14027" href="plfa.part3.Compositional.html#13993" class="Bound">Γ</a> <a id="14029" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">,</a> <a id="14031" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="14032" class="Symbol">)</a> <a id="14034" href="plfa.part3.Compositional.html#13995" class="Bound">Δ</a>
|
||
<a id="Ctx.ctx-app-L"></a><a id="14038" href="/19.08/Compositional/#14038" class="InductiveConstructor">ctx-app-L</a> <a id="14048" class="Symbol">:</a> <a id="14050" class="Symbol">∀{</a><a id="14052" href="plfa.part3.Compositional.html#14052" class="Bound">Γ</a> <a id="14054" href="plfa.part3.Compositional.html#14054" class="Bound">Δ</a><a id="14055" class="Symbol">}</a> <a id="14057" class="Symbol">→</a> <a id="14059" href="plfa.part3.Compositional.html#13914" class="Datatype">Ctx</a> <a id="14063" href="plfa.part3.Compositional.html#14052" class="Bound">Γ</a> <a id="14065" href="plfa.part3.Compositional.html#14054" class="Bound">Δ</a> <a id="14067" class="Symbol">→</a> <a id="14069" href="plfa.part3.Compositional.html#14054" class="Bound">Δ</a> <a id="14071" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="14073" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="14075" class="Symbol">→</a> <a id="14077" href="plfa.part3.Compositional.html#13914" class="Datatype">Ctx</a> <a id="14081" href="plfa.part3.Compositional.html#14052" class="Bound">Γ</a> <a id="14083" href="plfa.part3.Compositional.html#14054" class="Bound">Δ</a>
|
||
<a id="Ctx.ctx-app-R"></a><a id="14087" href="/19.08/Compositional/#14087" class="InductiveConstructor">ctx-app-R</a> <a id="14097" class="Symbol">:</a> <a id="14099" class="Symbol">∀{</a><a id="14101" href="plfa.part3.Compositional.html#14101" class="Bound">Γ</a> <a id="14103" href="plfa.part3.Compositional.html#14103" class="Bound">Δ</a><a id="14104" class="Symbol">}</a> <a id="14106" class="Symbol">→</a> <a id="14108" href="plfa.part3.Compositional.html#14103" class="Bound">Δ</a> <a id="14110" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="14112" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="14114" class="Symbol">→</a> <a id="14116" href="plfa.part3.Compositional.html#13914" class="Datatype">Ctx</a> <a id="14120" href="plfa.part3.Compositional.html#14101" class="Bound">Γ</a> <a id="14122" href="plfa.part3.Compositional.html#14103" class="Bound">Δ</a> <a id="14124" class="Symbol">→</a> <a id="14126" href="plfa.part3.Compositional.html#13914" class="Datatype">Ctx</a> <a id="14130" href="plfa.part3.Compositional.html#14101" class="Bound">Γ</a> <a id="14132" href="plfa.part3.Compositional.html#14103" class="Bound">Δ</a>
|
||
</pre>
|
||
<ul>
|
||
<li>
|
||
<p>The constructor <code class="language-plaintext highlighter-rouge">ctx-hole</code> represents the hole, and in this case the
|
||
variable context for the hole is the same as the variable context
|
||
for the term that results from filling the hole.</p>
|
||
</li>
|
||
<li>
|
||
<p>The constructor <code class="language-plaintext highlighter-rouge">ctx-lam</code> takes a <code class="language-plaintext highlighter-rouge">Ctx</code> and produces a larger one that
|
||
adds a lambda abstraction at the top. The variable context of the
|
||
hole stays the same, whereas we remove one variable from the context
|
||
of the resulting term because it is bound by this lambda
|
||
abstraction.</p>
|
||
</li>
|
||
<li>
|
||
<p>There are two constructions for application, <code class="language-plaintext highlighter-rouge">ctx-app-L</code> and
|
||
<code class="language-plaintext highlighter-rouge">ctx-app-R</code>. The <code class="language-plaintext highlighter-rouge">ctx-app-L</code> is for when the hole is inside the left-hand
|
||
term (the operator) and the later is when the hole is inside the
|
||
right-hand term (the operand).</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<p>The action of surrounding a term with a context is defined by the
|
||
following <code class="language-plaintext highlighter-rouge">plug</code> function. It is defined by recursion on the context.</p>
|
||
|
||
<pre class="Agda"><a id="plug"></a><a id="14998" href="/19.08/Compositional/#14998" class="Function">plug</a> <a id="15003" class="Symbol">:</a> <a id="15005" class="Symbol">∀{</a><a id="15007" href="plfa.part3.Compositional.html#15007" class="Bound">Γ</a><a id="15008" class="Symbol">}{</a><a id="15010" href="plfa.part3.Compositional.html#15010" class="Bound">Δ</a><a id="15011" class="Symbol">}</a> <a id="15013" class="Symbol">→</a> <a id="15015" href="plfa.part3.Compositional.html#13914" class="Datatype">Ctx</a> <a id="15019" href="plfa.part3.Compositional.html#15007" class="Bound">Γ</a> <a id="15021" href="plfa.part3.Compositional.html#15010" class="Bound">Δ</a> <a id="15023" class="Symbol">→</a> <a id="15025" href="plfa.part3.Compositional.html#15007" class="Bound">Γ</a> <a id="15027" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="15029" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="15031" class="Symbol">→</a> <a id="15033" href="plfa.part3.Compositional.html#15010" class="Bound">Δ</a> <a id="15035" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="15037" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a>
|
||
<a id="15039" href="/19.08/Compositional/#14998" class="Function">plug</a> <a id="15044" href="plfa.part3.Compositional.html#13952" class="InductiveConstructor">ctx-hole</a> <a id="15053" href="plfa.part3.Compositional.html#15053" class="Bound">M</a> <a id="15055" class="Symbol">=</a> <a id="15057" href="plfa.part3.Compositional.html#15053" class="Bound">M</a>
|
||
<a id="15059" href="/19.08/Compositional/#14998" class="Function">plug</a> <a id="15064" class="Symbol">(</a><a id="15065" href="plfa.part3.Compositional.html#13980" class="InductiveConstructor">ctx-lam</a> <a id="15073" href="plfa.part3.Compositional.html#15073" class="Bound">C</a><a id="15074" class="Symbol">)</a> <a id="15076" href="plfa.part3.Compositional.html#15076" class="Bound">N</a> <a id="15078" class="Symbol">=</a> <a id="15080" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="15082" href="plfa.part3.Compositional.html#14998" class="Function">plug</a> <a id="15087" href="plfa.part3.Compositional.html#15073" class="Bound">C</a> <a id="15089" href="plfa.part3.Compositional.html#15076" class="Bound">N</a>
|
||
<a id="15091" href="/19.08/Compositional/#14998" class="Function">plug</a> <a id="15096" class="Symbol">(</a><a id="15097" href="plfa.part3.Compositional.html#14038" class="InductiveConstructor">ctx-app-L</a> <a id="15107" href="plfa.part3.Compositional.html#15107" class="Bound">C</a> <a id="15109" href="plfa.part3.Compositional.html#15109" class="Bound">N</a><a id="15110" class="Symbol">)</a> <a id="15112" href="plfa.part3.Compositional.html#15112" class="Bound">L</a> <a id="15114" class="Symbol">=</a> <a id="15116" class="Symbol">(</a><a id="15117" href="plfa.part3.Compositional.html#14998" class="Function">plug</a> <a id="15122" href="plfa.part3.Compositional.html#15107" class="Bound">C</a> <a id="15124" href="plfa.part3.Compositional.html#15112" class="Bound">L</a><a id="15125" class="Symbol">)</a> <a id="15127" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="15129" href="plfa.part3.Compositional.html#15109" class="Bound">N</a>
|
||
<a id="15131" href="/19.08/Compositional/#14998" class="Function">plug</a> <a id="15136" class="Symbol">(</a><a id="15137" href="plfa.part3.Compositional.html#14087" class="InductiveConstructor">ctx-app-R</a> <a id="15147" href="plfa.part3.Compositional.html#15147" class="Bound">L</a> <a id="15149" href="plfa.part3.Compositional.html#15149" class="Bound">C</a><a id="15150" class="Symbol">)</a> <a id="15152" href="plfa.part3.Compositional.html#15152" class="Bound">M</a> <a id="15154" class="Symbol">=</a> <a id="15156" href="plfa.part3.Compositional.html#15147" class="Bound">L</a> <a id="15158" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="15160" class="Symbol">(</a><a id="15161" href="plfa.part3.Compositional.html#14998" class="Function">plug</a> <a id="15166" href="plfa.part3.Compositional.html#15149" class="Bound">C</a> <a id="15168" href="plfa.part3.Compositional.html#15152" class="Bound">M</a><a id="15169" class="Symbol">)</a>
|
||
</pre>
|
||
<p>We are ready to state and prove the compositionality principle. Given
|
||
two terms <code class="language-plaintext highlighter-rouge">M</code> and <code class="language-plaintext highlighter-rouge">N</code> that are denotationally equal, plugging them both
|
||
into an arbitrary context <code class="language-plaintext highlighter-rouge">C</code> produces two programs that are
|
||
denotationally equal.</p>
|
||
|
||
<pre class="Agda"><a id="compositionality"></a><a id="15407" href="/19.08/Compositional/#15407" class="Function">compositionality</a> <a id="15424" class="Symbol">:</a> <a id="15426" class="Symbol">∀{</a><a id="15428" href="plfa.part3.Compositional.html#15428" class="Bound">Γ</a> <a id="15430" href="plfa.part3.Compositional.html#15430" class="Bound">Δ</a><a id="15431" class="Symbol">}{</a><a id="15433" href="plfa.part3.Compositional.html#15433" class="Bound">C</a> <a id="15435" class="Symbol">:</a> <a id="15437" href="plfa.part3.Compositional.html#13914" class="Datatype">Ctx</a> <a id="15441" href="plfa.part3.Compositional.html#15428" class="Bound">Γ</a> <a id="15443" href="plfa.part3.Compositional.html#15430" class="Bound">Δ</a><a id="15444" class="Symbol">}</a> <a id="15446" class="Symbol">{</a><a id="15447" href="plfa.part3.Compositional.html#15447" class="Bound">M</a> <a id="15449" href="plfa.part3.Compositional.html#15449" class="Bound">N</a> <a id="15451" class="Symbol">:</a> <a id="15453" href="plfa.part3.Compositional.html#15428" class="Bound">Γ</a> <a id="15455" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="15457" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="15458" class="Symbol">}</a>
|
||
<a id="15462" class="Symbol">→</a> <a id="15464" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="15466" href="/19.08/Compositional/#15447" class="Bound">M</a> <a id="15468" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="15470" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="15472" href="plfa.part3.Compositional.html#15449" class="Bound">N</a>
|
||
<a id="15478" class="Comment">---------------------------</a>
|
||
<a id="15508" class="Symbol">→</a> <a id="15510" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="15512" class="Symbol">(</a><a id="15513" href="/19.08/Compositional/#14998" class="Function">plug</a> <a id="15518" href="plfa.part3.Compositional.html#15433" class="Bound">C</a> <a id="15520" href="plfa.part3.Compositional.html#15447" class="Bound">M</a><a id="15521" class="Symbol">)</a> <a id="15523" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="15525" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="15527" class="Symbol">(</a><a id="15528" href="plfa.part3.Compositional.html#14998" class="Function">plug</a> <a id="15533" href="plfa.part3.Compositional.html#15433" class="Bound">C</a> <a id="15535" href="plfa.part3.Compositional.html#15449" class="Bound">N</a><a id="15536" class="Symbol">)</a>
|
||
<a id="15538" href="/19.08/Compositional/#15407" class="Function">compositionality</a> <a id="15555" class="Symbol">{</a><a id="15556" class="Argument">C</a> <a id="15558" class="Symbol">=</a> <a id="15560" href="plfa.part3.Compositional.html#13952" class="InductiveConstructor">ctx-hole</a><a id="15568" class="Symbol">}</a> <a id="15570" href="plfa.part3.Compositional.html#15570" class="Bound">M≃N</a> <a id="15574" class="Symbol">=</a>
|
||
<a id="15578" href="/19.08/Compositional/#15570" class="Bound">M≃N</a>
|
||
<a id="15582" href="/19.08/Compositional/#15407" class="Function">compositionality</a> <a id="15599" class="Symbol">{</a><a id="15600" class="Argument">C</a> <a id="15602" class="Symbol">=</a> <a id="15604" href="plfa.part3.Compositional.html#13980" class="InductiveConstructor">ctx-lam</a> <a id="15612" href="plfa.part3.Compositional.html#15612" class="Bound">C′</a><a id="15614" class="Symbol">}</a> <a id="15616" href="plfa.part3.Compositional.html#15616" class="Bound">M≃N</a> <a id="15620" class="Symbol">=</a>
|
||
<a id="15624" href="/19.08/Compositional/#11864" class="Function">lam-cong</a> <a id="15633" class="Symbol">(</a><a id="15634" href="plfa.part3.Compositional.html#15407" class="Function">compositionality</a> <a id="15651" class="Symbol">{</a><a id="15652" class="Argument">C</a> <a id="15654" class="Symbol">=</a> <a id="15656" href="plfa.part3.Compositional.html#15612" class="Bound">C′</a><a id="15658" class="Symbol">}</a> <a id="15660" href="plfa.part3.Compositional.html#15616" class="Bound">M≃N</a><a id="15663" class="Symbol">)</a>
|
||
<a id="15665" href="/19.08/Compositional/#15407" class="Function">compositionality</a> <a id="15682" class="Symbol">{</a><a id="15683" class="Argument">C</a> <a id="15685" class="Symbol">=</a> <a id="15687" href="plfa.part3.Compositional.html#14038" class="InductiveConstructor">ctx-app-L</a> <a id="15697" href="plfa.part3.Compositional.html#15697" class="Bound">C′</a> <a id="15700" href="plfa.part3.Compositional.html#15700" class="Bound">L</a><a id="15701" class="Symbol">}</a> <a id="15703" href="plfa.part3.Compositional.html#15703" class="Bound">M≃N</a> <a id="15707" class="Symbol">=</a>
|
||
<a id="15711" href="/19.08/Compositional/#13091" class="Function">app-cong</a> <a id="15720" class="Symbol">(</a><a id="15721" href="plfa.part3.Compositional.html#15407" class="Function">compositionality</a> <a id="15738" class="Symbol">{</a><a id="15739" class="Argument">C</a> <a id="15741" class="Symbol">=</a> <a id="15743" href="plfa.part3.Compositional.html#15697" class="Bound">C′</a><a id="15745" class="Symbol">}</a> <a id="15747" href="plfa.part3.Compositional.html#15703" class="Bound">M≃N</a><a id="15750" class="Symbol">)</a> <a id="15752" class="Symbol">λ</a> <a id="15754" href="plfa.part3.Compositional.html#15754" class="Bound">γ</a> <a id="15756" href="plfa.part3.Compositional.html#15756" class="Bound">v</a> <a id="15758" class="Symbol">→</a> <a id="15760" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="15762" class="Symbol">(λ</a> <a id="15765" href="plfa.part3.Compositional.html#15765" class="Bound">x</a> <a id="15767" class="Symbol">→</a> <a id="15769" href="plfa.part3.Compositional.html#15765" class="Bound">x</a><a id="15770" class="Symbol">)</a> <a id="15772" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15774" class="Symbol">(λ</a> <a id="15777" href="plfa.part3.Compositional.html#15777" class="Bound">x</a> <a id="15779" class="Symbol">→</a> <a id="15781" href="plfa.part3.Compositional.html#15777" class="Bound">x</a><a id="15782" class="Symbol">)</a> <a id="15784" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="15786" href="/19.08/Compositional/#15407" class="Function">compositionality</a> <a id="15803" class="Symbol">{</a><a id="15804" class="Argument">C</a> <a id="15806" class="Symbol">=</a> <a id="15808" href="plfa.part3.Compositional.html#14087" class="InductiveConstructor">ctx-app-R</a> <a id="15818" href="plfa.part3.Compositional.html#15818" class="Bound">L</a> <a id="15820" href="plfa.part3.Compositional.html#15820" class="Bound">C′</a><a id="15822" class="Symbol">}</a> <a id="15824" href="plfa.part3.Compositional.html#15824" class="Bound">M≃N</a> <a id="15828" class="Symbol">=</a>
|
||
<a id="15832" href="/19.08/Compositional/#13091" class="Function">app-cong</a> <a id="15841" class="Symbol">(λ</a> <a id="15844" href="plfa.part3.Compositional.html#15844" class="Bound">γ</a> <a id="15846" href="plfa.part3.Compositional.html#15846" class="Bound">v</a> <a id="15848" class="Symbol">→</a> <a id="15850" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="15852" class="Symbol">(λ</a> <a id="15855" href="plfa.part3.Compositional.html#15855" class="Bound">x</a> <a id="15857" class="Symbol">→</a> <a id="15859" href="plfa.part3.Compositional.html#15855" class="Bound">x</a><a id="15860" class="Symbol">)</a> <a id="15862" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15864" class="Symbol">(λ</a> <a id="15867" href="plfa.part3.Compositional.html#15867" class="Bound">x</a> <a id="15869" class="Symbol">→</a> <a id="15871" href="plfa.part3.Compositional.html#15867" class="Bound">x</a><a id="15872" class="Symbol">)</a> <a id="15874" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a><a id="15875" class="Symbol">)</a> <a id="15877" class="Symbol">(</a><a id="15878" href="plfa.part3.Compositional.html#15407" class="Function">compositionality</a> <a id="15895" class="Symbol">{</a><a id="15896" class="Argument">C</a> <a id="15898" class="Symbol">=</a> <a id="15900" href="plfa.part3.Compositional.html#15820" class="Bound">C′</a><a id="15902" class="Symbol">}</a> <a id="15904" href="plfa.part3.Compositional.html#15824" class="Bound">M≃N</a><a id="15907" class="Symbol">)</a>
|
||
</pre>
|
||
<p>The proof is a straightforward induction on the context <code class="language-plaintext highlighter-rouge">C</code>, using the
|
||
congruence properties <code class="language-plaintext highlighter-rouge">lam-cong</code> and <code class="language-plaintext highlighter-rouge">app-cong</code> that we established
|
||
above.</p>
|
||
|
||
<h2 id="the-denotational-semantics-defined-as-a-function">The denotational semantics defined as a function</h2>
|
||
|
||
<p>Having established the three equations <code class="language-plaintext highlighter-rouge">var-equiv</code>, <code class="language-plaintext highlighter-rouge">lam-equiv</code>, and
|
||
<code class="language-plaintext highlighter-rouge">app-equiv</code>, one should be able to define the denotational semantics
|
||
as a recursive function over the input term <code class="language-plaintext highlighter-rouge">M</code>. Indeed, we define the
|
||
following function <code class="language-plaintext highlighter-rouge">⟦ M ⟧</code> that maps terms to denotations, using the
|
||
auxiliary curry <code class="language-plaintext highlighter-rouge">ℱ</code> and apply <code class="language-plaintext highlighter-rouge">●</code> functions in the cases for lambda
|
||
and application, respectively.</p>
|
||
|
||
<pre class="Agda"><a id="⟦_⟧"></a><a id="16496" href="/19.08/Compositional/#16496" class="Function Operator">⟦_⟧</a> <a id="16500" class="Symbol">:</a> <a id="16502" class="Symbol">∀{</a><a id="16504" href="plfa.part3.Compositional.html#16504" class="Bound">Γ</a><a id="16505" class="Symbol">}</a> <a id="16507" class="Symbol">→</a> <a id="16509" class="Symbol">(</a><a id="16510" href="plfa.part3.Compositional.html#16510" class="Bound">M</a> <a id="16512" class="Symbol">:</a> <a id="16514" href="plfa.part3.Compositional.html#16504" class="Bound">Γ</a> <a id="16516" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="16518" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="16519" class="Symbol">)</a> <a id="16521" class="Symbol">→</a> <a id="16523" href="/19.08/Denotational/#17303" class="Function">Denotation</a> <a id="16534" href="plfa.part3.Compositional.html#16504" class="Bound">Γ</a>
|
||
<a id="16536" href="/19.08/Compositional/#16496" class="Function Operator">⟦</a> <a id="16538" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="16540" href="plfa.part3.Compositional.html#16540" class="Bound">x</a> <a id="16542" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a> <a id="16544" href="plfa.part3.Compositional.html#16544" class="Bound">γ</a> <a id="16546" href="plfa.part3.Compositional.html#16546" class="Bound">v</a> <a id="16548" class="Symbol">=</a> <a id="16550" href="plfa.part3.Compositional.html#16546" class="Bound">v</a> <a id="16552" href="/19.08/Denotational/#4427" class="Datatype Operator">⊑</a> <a id="16554" href="plfa.part3.Compositional.html#16544" class="Bound">γ</a> <a id="16556" href="plfa.part3.Compositional.html#16540" class="Bound">x</a>
|
||
<a id="16558" href="/19.08/Compositional/#16496" class="Function Operator">⟦</a> <a id="16560" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="16562" href="plfa.part3.Compositional.html#16562" class="Bound">N</a> <a id="16564" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a> <a id="16566" class="Symbol">=</a> <a id="16568" href="plfa.part3.Compositional.html#1898" class="Function">ℱ</a> <a id="16570" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟦</a> <a id="16572" href="plfa.part3.Compositional.html#16562" class="Bound">N</a> <a id="16574" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a>
|
||
<a id="16576" href="/19.08/Compositional/#16496" class="Function Operator">⟦</a> <a id="16578" href="plfa.part3.Compositional.html#16578" class="Bound">L</a> <a id="16580" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="16582" href="plfa.part3.Compositional.html#16582" class="Bound">M</a> <a id="16584" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a> <a id="16586" class="Symbol">=</a> <a id="16588" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟦</a> <a id="16590" href="plfa.part3.Compositional.html#16578" class="Bound">L</a> <a id="16592" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a> <a id="16594" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="16596" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟦</a> <a id="16598" href="plfa.part3.Compositional.html#16582" class="Bound">M</a> <a id="16600" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a>
|
||
</pre>
|
||
<p>The proof that <code class="language-plaintext highlighter-rouge">ℰ M</code> is denotationally equal to <code class="language-plaintext highlighter-rouge">⟦ M ⟧</code> is a
|
||
straightforward induction, using the three equations
|
||
<code class="language-plaintext highlighter-rouge">var-equiv</code>, <code class="language-plaintext highlighter-rouge">lam-equiv</code>, and <code class="language-plaintext highlighter-rouge">app-equiv</code> together
|
||
with the congruence lemmas for <code class="language-plaintext highlighter-rouge">ℱ</code> and <code class="language-plaintext highlighter-rouge">●</code>.</p>
|
||
|
||
<pre class="Agda"><a id="ℰ≃⟦⟧"></a><a id="16821" href="/19.08/Compositional/#16821" class="Function">ℰ≃⟦⟧</a> <a id="16826" class="Symbol">:</a> <a id="16828" class="Symbol">∀</a> <a id="16830" class="Symbol">{</a><a id="16831" href="plfa.part3.Compositional.html#16831" class="Bound">Γ</a><a id="16832" class="Symbol">}</a> <a id="16834" class="Symbol">{</a><a id="16835" href="plfa.part3.Compositional.html#16835" class="Bound">M</a> <a id="16837" class="Symbol">:</a> <a id="16839" href="plfa.part3.Compositional.html#16831" class="Bound">Γ</a> <a id="16841" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="16843" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="16844" class="Symbol">}</a> <a id="16846" class="Symbol">→</a> <a id="16848" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="16850" href="plfa.part3.Compositional.html#16835" class="Bound">M</a> <a id="16852" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="16854" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟦</a> <a id="16856" href="plfa.part3.Compositional.html#16835" class="Bound">M</a> <a id="16858" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a>
|
||
<a id="16860" href="/19.08/Compositional/#16821" class="Function">ℰ≃⟦⟧</a> <a id="16865" class="Symbol">{</a><a id="16866" href="plfa.part3.Compositional.html#16866" class="Bound">Γ</a><a id="16867" class="Symbol">}</a> <a id="16869" class="Symbol">{</a><a id="16870" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="16872" href="plfa.part3.Compositional.html#16872" class="Bound">x</a><a id="16873" class="Symbol">}</a> <a id="16875" class="Symbol">=</a> <a id="16877" href="plfa.part3.Compositional.html#10360" class="Function">var-equiv</a>
|
||
<a id="16887" href="/19.08/Compositional/#16821" class="Function">ℰ≃⟦⟧</a> <a id="16892" class="Symbol">{</a><a id="16893" href="plfa.part3.Compositional.html#16893" class="Bound">Γ</a><a id="16894" class="Symbol">}</a> <a id="16896" class="Symbol">{</a><a id="16897" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="16899" href="plfa.part3.Compositional.html#16899" class="Bound">N</a><a id="16900" class="Symbol">}</a> <a id="16902" class="Symbol">=</a>
|
||
<a id="16906" class="Keyword">let</a> <a id="16910" href="/19.08/Compositional/#16910" class="Bound">ih</a> <a id="16913" class="Symbol">=</a> <a id="16915" href="plfa.part3.Compositional.html#16821" class="Function">ℰ≃⟦⟧</a> <a id="16920" class="Symbol">{</a><a id="16921" class="Argument">M</a> <a id="16923" class="Symbol">=</a> <a id="16925" href="plfa.part3.Compositional.html#16899" class="Bound">N</a><a id="16926" class="Symbol">}</a> <a id="16928" class="Keyword">in</a>
|
||
<a id="16935" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="16937" class="Symbol">(</a><a id="16938" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="16940" href="/19.08/Compositional/#16899" class="Bound">N</a><a id="16941" class="Symbol">)</a>
|
||
<a id="16945" href="/19.08/Denotational/#19281" class="Function Operator">≃⟨</a> <a id="16948" href="/19.08/Compositional/#4552" class="Function">lam-equiv</a> <a id="16958" href="plfa.part3.Denotational.html#19281" class="Function Operator">⟩</a>
|
||
<a id="16964" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="16966" class="Symbol">(</a><a id="16967" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="16969" href="plfa.part3.Compositional.html#16899" class="Bound">N</a><a id="16970" class="Symbol">)</a>
|
||
<a id="16974" href="/19.08/Denotational/#19281" class="Function Operator">≃⟨</a> <a id="16977" href="/19.08/Compositional/#11190" class="Function">ℱ-cong</a> <a id="16984" class="Symbol">(</a><a id="16985" href="plfa.part3.Compositional.html#16821" class="Function">ℰ≃⟦⟧</a> <a id="16990" class="Symbol">{</a><a id="16991" class="Argument">M</a> <a id="16993" class="Symbol">=</a> <a id="16995" href="plfa.part3.Compositional.html#16899" class="Bound">N</a><a id="16996" class="Symbol">})</a> <a id="16999" href="plfa.part3.Denotational.html#19281" class="Function Operator">⟩</a>
|
||
<a id="17005" href="/19.08/Compositional/#1898" class="Function">ℱ</a> <a id="17007" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟦</a> <a id="17009" href="plfa.part3.Compositional.html#16899" class="Bound">N</a> <a id="17011" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a>
|
||
<a id="17015" href="/19.08/Denotational/#19421" class="Function Operator">≃⟨⟩</a>
|
||
<a id="17023" href="/19.08/Compositional/#16496" class="Function Operator">⟦</a> <a id="17025" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="17027" href="plfa.part3.Compositional.html#16899" class="Bound">N</a> <a id="17029" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a>
|
||
<a id="17033" href="/19.08/Denotational/#19528" class="Function Operator">☐</a>
|
||
<a id="17035" href="/19.08/Compositional/#16821" class="Function">ℰ≃⟦⟧</a> <a id="17040" class="Symbol">{</a><a id="17041" href="plfa.part3.Compositional.html#17041" class="Bound">Γ</a><a id="17042" class="Symbol">}</a> <a id="17044" class="Symbol">{</a><a id="17045" href="plfa.part3.Compositional.html#17045" class="Bound">L</a> <a id="17047" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="17049" href="plfa.part3.Compositional.html#17049" class="Bound">M</a><a id="17050" class="Symbol">}</a> <a id="17052" class="Symbol">=</a>
|
||
<a id="17057" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="17059" class="Symbol">(</a><a id="17060" href="/19.08/Compositional/#17045" class="Bound">L</a> <a id="17062" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="17064" href="plfa.part3.Compositional.html#17049" class="Bound">M</a><a id="17065" class="Symbol">)</a>
|
||
<a id="17069" href="/19.08/Denotational/#19281" class="Function Operator">≃⟨</a> <a id="17072" href="/19.08/Compositional/#9789" class="Function">app-equiv</a> <a id="17082" href="plfa.part3.Denotational.html#19281" class="Function Operator">⟩</a>
|
||
<a id="17087" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="17089" href="/19.08/Compositional/#17045" class="Bound">L</a> <a id="17091" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="17093" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="17095" href="plfa.part3.Compositional.html#17049" class="Bound">M</a>
|
||
<a id="17099" href="/19.08/Denotational/#19281" class="Function Operator">≃⟨</a> <a id="17102" href="/19.08/Compositional/#12357" class="Function">●-cong</a> <a id="17109" class="Symbol">(</a><a id="17110" href="plfa.part3.Compositional.html#16821" class="Function">ℰ≃⟦⟧</a> <a id="17115" class="Symbol">{</a><a id="17116" class="Argument">M</a> <a id="17118" class="Symbol">=</a> <a id="17120" href="plfa.part3.Compositional.html#17045" class="Bound">L</a><a id="17121" class="Symbol">})</a> <a id="17124" class="Symbol">(</a><a id="17125" href="plfa.part3.Compositional.html#16821" class="Function">ℰ≃⟦⟧</a> <a id="17130" class="Symbol">{</a><a id="17131" class="Argument">M</a> <a id="17133" class="Symbol">=</a> <a id="17135" href="plfa.part3.Compositional.html#17049" class="Bound">M</a><a id="17136" class="Symbol">})</a> <a id="17139" href="plfa.part3.Denotational.html#19281" class="Function Operator">⟩</a>
|
||
<a id="17144" href="/19.08/Compositional/#16496" class="Function Operator">⟦</a> <a id="17146" href="plfa.part3.Compositional.html#17045" class="Bound">L</a> <a id="17148" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a> <a id="17150" href="plfa.part3.Compositional.html#5745" class="Function Operator">●</a> <a id="17152" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟦</a> <a id="17154" href="plfa.part3.Compositional.html#17049" class="Bound">M</a> <a id="17156" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a>
|
||
<a id="17160" href="/19.08/Denotational/#19421" class="Function Operator">≃⟨⟩</a>
|
||
<a id="17168" href="/19.08/Compositional/#16496" class="Function Operator">⟦</a> <a id="17170" href="plfa.part3.Compositional.html#17045" class="Bound">L</a> <a id="17172" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="17174" href="plfa.part3.Compositional.html#17049" class="Bound">M</a> <a id="17176" href="plfa.part3.Compositional.html#16496" class="Function Operator">⟧</a>
|
||
<a id="17180" href="/19.08/Denotational/#19528" class="Function Operator">☐</a>
|
||
</pre>
|
||
|
||
<h2 id="unicode">Unicode</h2>
|
||
|
||
<p>This chapter uses the following unicode:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ℱ U+2131 SCRIPT CAPITAL F (\McF)
|
||
● U+2131 BLACK CIRCLE (\cib)
|
||
</code></pre></div></div>
|
||
|
||
</div>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
<a alt="Previous chapter" href="/19.08/Denotational/">Prev</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part3/Compositional.lagda.md">Source</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Next chapter" href="/19.08/Soundness/">Next</a>
|
||
|
||
</p>
|
||
|
||
|
||
</article>
|
||
|
||
</div>
|
||
</main><footer class="site-footer h-card">
|
||
<data class="u-url" href="/19.08/"></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="/19.08/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="/19.08/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="/19.08/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 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="/19.08/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="/19.08/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="/19.08/assets/jquery.js"></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="/19.08/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>
|