michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
csci8980-f21/versions/19.08/Compositional/index.html

731 lines
170 KiB
HTML
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!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>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part3/Compositional.lagda.md">Source</a>
&bullet;
<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>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part3/Compositional.lagda.md">Source</a>
&bullet;
<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>
Reference in a new issue View git blame Copy permalink