<!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/20.07/Compositional/" /> <meta property="og:url" content="https://plfa.github.io/20.07/Compositional/" /> <meta property="og:site_name" content="Programming Language Foundations in Agda" /> <script type="application/ld+json"> {"url":"https://plfa.github.io/20.07/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="/20.07/assets/main.css"></head> <body><header class="site-header" role="banner"> <div class="wrapper"> <a class="site-title" href="/20.07/">Programming Language Foundations in Agda </a> <nav class="site-nav"> <span class="menu-icon"> <svg viewBox="0 0 18 15" width="18px" height="15px"> <path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/> <path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/> <path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/> </svg> </span> <div class="trigger"> <a class="page-link" href="/20.07/">The Book</a> <a class="page-link" href="/20.07/Announcements/">Announcements</a> <a class="page-link" href="/20.07/GettingStarted/">Getting Started</a> <a class="page-link" href="/20.07/Citing/">Citing</a> <a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">δΈζ</a> </div> </nav> </div> </header> <main class="page-content" aria-label="Content"> <div class="wrapper"> <article class="post"> <header class="post-header"> <h1 class="post-title">Compositional: The denotational semantics is compositional π§</h1> </header> <p style="text-align:center;"> <a alt="Previous chapter" href="/20.07/Denotational/">Prev</a> • <a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part3/Compositional.lagda.md">Source</a> • <a alt="Next chapter" href="/20.07/Soundness/">Next</a> </p> <div class="post-content"> <pre class="Agda"><a id="185" class="Keyword">module</a> <a id="192" href="/20.07/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="/20.07/Untyped/" class="Module">plfa.part2.Untyped</a> <a id="899" class="Keyword">using</a> <a id="905" class="Symbol">(</a><a id="906" href="/20.07/Untyped/#3153" class="Datatype">Context</a><a id="913" class="Symbol">;</a> <a id="915" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">_,_</a><a id="918" class="Symbol">;</a> <a id="920" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="921" class="Symbol">;</a> <a id="923" href="/20.07/Untyped/#3521" class="Datatype Operator">_β_</a><a id="926" class="Symbol">;</a> <a id="928" href="/20.07/Untyped/#4294" class="Datatype Operator">_β’_</a><a id="931" class="Symbol">;</a> <a id="933" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`_</a><a id="935" class="Symbol">;</a> <a id="937" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ_</a><a id="939" class="Symbol">;</a> <a id="941" href="/20.07/Untyped/#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="/20.07/Denotational/" class="Module">plfa.part3.Denotational</a> <a id="984" class="Keyword">using</a> <a id="990" class="Symbol">(</a><a id="991" href="/20.07/Denotational/#4151" class="Datatype">Value</a><a id="996" class="Symbol">;</a> <a id="998" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">_β¦_</a><a id="1001" class="Symbol">;</a> <a id="1003" href="/20.07/Denotational/#7445" class="Function Operator">_`,_</a><a id="1007" class="Symbol">;</a> <a id="1009" href="/20.07/Denotational/#4213" class="InductiveConstructor Operator">_β_</a><a id="1012" class="Symbol">;</a> <a id="1014" href="/20.07/Denotational/#4171" class="InductiveConstructor">β₯</a><a id="1015" class="Symbol">;</a> <a id="1017" href="/20.07/Denotational/#4508" class="Datatype Operator">_β_</a><a id="1020" class="Symbol">;</a> <a id="1022" href="/20.07/Denotational/#9346" class="Datatype Operator">_β’_β_</a><a id="1027" class="Symbol">;</a> <a id="1038" href="/20.07/Denotational/#4543" class="InductiveConstructor">β-bot</a><a id="1043" class="Symbol">;</a> <a id="1045" href="/20.07/Denotational/#4869" class="InductiveConstructor">β-fun</a><a id="1050" class="Symbol">;</a> <a id="1052" href="/20.07/Denotational/#4568" class="InductiveConstructor">β-conj-L</a><a id="1060" class="Symbol">;</a> <a id="1062" href="/20.07/Denotational/#4652" class="InductiveConstructor">β-conj-R1</a><a id="1071" class="Symbol">;</a> <a id="1073" href="/20.07/Denotational/#4725" class="InductiveConstructor">β-conj-R2</a><a id="1082" class="Symbol">;</a> <a id="1093" href="/20.07/Denotational/#4972" class="InductiveConstructor">β-dist</a><a id="1099" class="Symbol">;</a> <a id="1101" href="/20.07/Denotational/#5638" class="Function">β-refl</a><a id="1107" class="Symbol">;</a> <a id="1109" href="/20.07/Denotational/#4798" class="InductiveConstructor">β-trans</a><a id="1116" class="Symbol">;</a> <a id="1118" href="/20.07/Denotational/#6273" class="Function">ββ¦β-dist</a><a id="1126" class="Symbol">;</a> <a id="1137" href="/20.07/Denotational/#9400" class="InductiveConstructor">var</a><a id="1140" class="Symbol">;</a> <a id="1142" href="/20.07/Denotational/#9597" class="InductiveConstructor">β¦-intro</a><a id="1149" class="Symbol">;</a> <a id="1151" href="/20.07/Denotational/#9475" class="InductiveConstructor">β¦-elim</a><a id="1157" class="Symbol">;</a> <a id="1159" href="/20.07/Denotational/#9776" class="InductiveConstructor">β-intro</a><a id="1166" class="Symbol">;</a> <a id="1168" href="/20.07/Denotational/#9709" class="InductiveConstructor">β₯-intro</a><a id="1175" class="Symbol">;</a> <a id="1177" href="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a><a id="1180" class="Symbol">;</a> <a id="1191" href="/20.07/Denotational/#26158" class="Function">up-env</a><a id="1197" class="Symbol">;</a> <a id="1199" href="/20.07/Denotational/#17486" class="Function">β°</a><a id="1200" class="Symbol">;</a> <a id="1202" href="/20.07/Denotational/#17668" class="Function Operator">_β_</a><a id="1205" class="Symbol">;</a> <a id="1207" href="/20.07/Denotational/#17940" class="Function">β-sym</a><a id="1212" class="Symbol">;</a> <a id="1214" href="/20.07/Denotational/#17273" class="Function">Denotation</a><a id="1224" class="Symbol">;</a> <a id="1226" href="/20.07/Denotational/#7288" class="Function">Env</a><a id="1229" class="Symbol">)</a> <a id="1231" class="Keyword">open</a> <a id="1236" href="/20.07/Denotational/#19068" 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="/20.07/Compositional/#1898" class="Function">β±</a> <a id="1900" class="Symbol">:</a> <a id="1902" class="Symbol">β{</a><a id="1904" href="/20.07/Compositional/#1904" class="Bound">Ξ</a><a id="1905" class="Symbol">}</a> <a id="1907" class="Symbol">β</a> <a id="1909" href="/20.07/Denotational/#17273" class="Function">Denotation</a> <a id="1920" class="Symbol">(</a><a id="1921" href="/20.07/Compositional/#1904" class="Bound">Ξ</a> <a id="1923" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="1925" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="1926" class="Symbol">)</a> <a id="1928" class="Symbol">β</a> <a id="1930" href="/20.07/Denotational/#17273" class="Function">Denotation</a> <a id="1941" href="/20.07/Compositional/#1904" class="Bound">Ξ</a> <a id="1943" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="1945" href="/20.07/Compositional/#1945" class="Bound">D</a> <a id="1947" href="/20.07/Compositional/#1947" class="Bound">Ξ³</a> <a id="1949" class="Symbol">(</a><a id="1950" href="/20.07/Compositional/#1950" class="Bound">v</a> <a id="1952" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="1954" href="/20.07/Compositional/#1954" class="Bound">w</a><a id="1955" class="Symbol">)</a> <a id="1957" class="Symbol">=</a> <a id="1959" href="/20.07/Compositional/#1945" class="Bound">D</a> <a id="1961" class="Symbol">(</a><a id="1962" href="/20.07/Compositional/#1947" class="Bound">Ξ³</a> <a id="1964" href="/20.07/Denotational/#7445" class="Function Operator">`,</a> <a id="1967" href="/20.07/Compositional/#1950" class="Bound">v</a><a id="1968" class="Symbol">)</a> <a id="1970" href="/20.07/Compositional/#1954" class="Bound">w</a> <a id="1972" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="1974" href="/20.07/Compositional/#1974" class="Bound">D</a> <a id="1976" href="/20.07/Compositional/#1976" class="Bound">Ξ³</a> <a id="1978" href="/20.07/Denotational/#4171" 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="/20.07/Compositional/#1898" class="Function">β±</a> <a id="1986" href="/20.07/Compositional/#1986" class="Bound">D</a> <a id="1988" href="/20.07/Compositional/#1988" class="Bound">Ξ³</a> <a id="1990" class="Symbol">(</a><a id="1991" href="/20.07/Compositional/#1991" class="Bound">u</a> <a id="1993" href="/20.07/Denotational/#4213" class="InductiveConstructor Operator">β</a> <a id="1995" href="/20.07/Compositional/#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="/20.07/Compositional/#1898" class="Function">β±</a> <a id="2003" href="/20.07/Compositional/#1986" class="Bound">D</a> <a id="2005" href="/20.07/Compositional/#1988" class="Bound">Ξ³</a> <a id="2007" href="/20.07/Compositional/#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="/20.07/Compositional/#1898" class="Function">β±</a> <a id="2015" href="/20.07/Compositional/#1986" class="Bound">D</a> <a id="2017" href="/20.07/Compositional/#1988" class="Bound">Ξ³</a> <a id="2019" href="/20.07/Compositional/#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="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="2619" class="Symbol">:</a> <a id="2621" class="Symbol">β{</a><a id="2623" href="/20.07/Compositional/#2623" class="Bound">Ξ</a><a id="2624" class="Symbol">}{</a><a id="2626" href="/20.07/Compositional/#2626" class="Bound">N</a> <a id="2628" class="Symbol">:</a> <a id="2630" href="/20.07/Compositional/#2623" class="Bound">Ξ</a> <a id="2632" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="2634" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a> <a id="2636" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="2638" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="2639" class="Symbol">}{</a><a id="2641" href="/20.07/Compositional/#2641" class="Bound">Ξ³</a> <a id="2643" href="/20.07/Compositional/#2643" class="Bound">v</a> <a id="2645" href="/20.07/Compositional/#2645" class="Bound">u</a><a id="2646" class="Symbol">}</a> <a id="2650" class="Symbol">β</a> <a id="2652" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="2654" class="Symbol">(</a><a id="2655" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="2657" href="/20.07/Compositional/#2626" class="Bound">N</a><a id="2658" class="Symbol">)</a> <a id="2660" href="/20.07/Compositional/#2641" class="Bound">Ξ³</a> <a id="2662" href="/20.07/Compositional/#2643" class="Bound">v</a> <a id="2666" class="Symbol">β</a> <a id="2668" href="/20.07/Compositional/#2645" class="Bound">u</a> <a id="2670" href="/20.07/Denotational/#4508" class="Datatype Operator">β</a> <a id="2672" href="/20.07/Compositional/#2643" class="Bound">v</a> <a id="2678" class="Comment">------------</a> <a id="2693" class="Symbol">β</a> <a id="2695" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="2697" class="Symbol">(</a><a id="2698" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="2700" href="/20.07/Compositional/#2626" class="Bound">N</a><a id="2701" class="Symbol">)</a> <a id="2703" href="/20.07/Compositional/#2641" class="Bound">Ξ³</a> <a id="2705" href="/20.07/Compositional/#2645" class="Bound">u</a> <a id="2707" href="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="2713" href="/20.07/Compositional/#2713" class="Bound">d</a> <a id="2715" href="/20.07/Denotational/#4543" 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="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="2732" href="/20.07/Compositional/#2732" class="Bound">d</a> <a id="2734" class="Symbol">(</a><a id="2735" href="/20.07/Denotational/#4869" class="InductiveConstructor">β-fun</a> <a id="2741" href="/20.07/Compositional/#2741" class="Bound">lt</a> <a id="2744" href="/20.07/Compositional/#2744" class="Bound">ltβ²</a><a id="2747" class="Symbol">)</a> <a id="2749" class="Symbol">=</a> <a id="2751" href="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a> <a id="2755" class="Symbol">(</a><a id="2756" href="/20.07/Denotational/#26158" class="Function">up-env</a> <a id="2763" href="/20.07/Compositional/#2732" class="Bound">d</a> <a id="2765" href="/20.07/Compositional/#2741" class="Bound">lt</a><a id="2767" class="Symbol">)</a> <a id="2769" href="/20.07/Compositional/#2744" class="Bound">ltβ²</a> <a id="2773" href="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="2779" href="/20.07/Compositional/#2779" class="Bound">d</a> <a id="2781" class="Symbol">(</a><a id="2782" href="/20.07/Denotational/#4568" class="InductiveConstructor">β-conj-L</a> <a id="2791" href="/20.07/Compositional/#2791" class="Bound">lt</a> <a id="2794" href="/20.07/Compositional/#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="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="2809" href="/20.07/Compositional/#2779" class="Bound">d</a> <a id="2811" href="/20.07/Compositional/#2791" class="Bound">lt</a> <a id="2814" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="2816" href="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="2822" href="/20.07/Compositional/#2779" class="Bound">d</a> <a id="2824" href="/20.07/Compositional/#2794" class="Bound">ltβ</a> <a id="2828" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="2830" href="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="2836" href="/20.07/Compositional/#2836" class="Bound">d</a> <a id="2838" class="Symbol">(</a><a id="2839" href="/20.07/Denotational/#4652" class="InductiveConstructor">β-conj-R1</a> <a id="2849" href="/20.07/Compositional/#2849" class="Bound">lt</a><a id="2851" class="Symbol">)</a> <a id="2853" class="Symbol">=</a> <a id="2855" href="/20.07/Compositional/#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="/20.07/Compositional/#2836" class="Bound">d</a><a id="2869" class="Symbol">)</a> <a id="2871" href="/20.07/Compositional/#2849" class="Bound">lt</a> <a id="2874" href="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="2880" href="/20.07/Compositional/#2880" class="Bound">d</a> <a id="2882" class="Symbol">(</a><a id="2883" href="/20.07/Denotational/#4725" class="InductiveConstructor">β-conj-R2</a> <a id="2893" href="/20.07/Compositional/#2893" class="Bound">lt</a><a id="2895" class="Symbol">)</a> <a id="2897" class="Symbol">=</a> <a id="2899" href="/20.07/Compositional/#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="/20.07/Compositional/#2880" class="Bound">d</a><a id="2913" class="Symbol">)</a> <a id="2915" href="/20.07/Compositional/#2893" class="Bound">lt</a> <a id="2918" href="/20.07/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="/20.07/Compositional/#2929" class="Bound">vβ</a> <a id="2932" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="2934" href="/20.07/Compositional/#2934" class="Bound">vβ</a> <a id="2937" href="/20.07/Denotational/#4213" class="InductiveConstructor Operator">β</a> <a id="2939" href="/20.07/Compositional/#2929" class="Bound">vβ</a> <a id="2942" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="2944" href="/20.07/Compositional/#2944" class="Bound">vβ</a><a id="2946" class="Symbol">}</a> <a id="2948" class="Symbol">{</a><a id="2949" href="/20.07/Compositional/#2929" class="Bound">vβ</a> <a id="2952" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="2954" class="Symbol">(</a><a id="2955" href="/20.07/Compositional/#2934" class="Bound">vβ</a> <a id="2958" href="/20.07/Denotational/#4213" class="InductiveConstructor Operator">β</a> <a id="2960" href="/20.07/Compositional/#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="/20.07/Compositional/#2967" class="Bound">N2</a> <a id="2970" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="2972" href="/20.07/Compositional/#2972" class="Bound">N3</a> <a id="2975" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="2977" href="/20.07/Denotational/#4972" class="InductiveConstructor">β-dist</a> <a id="2984" class="Symbol">=</a> <a id="2989" href="/20.07/Denotational/#9776" class="InductiveConstructor">β-intro</a> <a id="2997" href="/20.07/Compositional/#2967" class="Bound">N2</a> <a id="3000" href="/20.07/Compositional/#2972" class="Bound">N3</a> <a id="3003" href="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="3009" href="/20.07/Compositional/#3009" class="Bound">d</a> <a id="3011" class="Symbol">(</a><a id="3012" href="/20.07/Denotational/#4798" class="InductiveConstructor">β-trans</a> <a id="3020" href="/20.07/Compositional/#3020" class="Bound">xβ</a> <a id="3023" href="/20.07/Compositional/#3023" class="Bound">xβ</a><a id="3025" class="Symbol">)</a> <a id="3027" class="Symbol">=</a> <a id="3029" href="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="3035" class="Symbol">(</a><a id="3036" href="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="3042" href="/20.07/Compositional/#3009" class="Bound">d</a> <a id="3044" href="/20.07/Compositional/#3023" class="Bound">xβ</a><a id="3046" class="Symbol">)</a> <a id="3048" href="/20.07/Compositional/#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="/20.07/Compositional/#3442" class="Function">β°Ζββ±β°</a> <a id="3448" class="Symbol">:</a> <a id="3450" class="Symbol">β{</a><a id="3452" href="/20.07/Compositional/#3452" class="Bound">Ξ</a><a id="3453" class="Symbol">}{</a><a id="3455" href="/20.07/Compositional/#3455" class="Bound">Ξ³</a> <a id="3457" class="Symbol">:</a> <a id="3459" href="/20.07/Denotational/#7288" class="Function">Env</a> <a id="3463" href="/20.07/Compositional/#3452" class="Bound">Ξ</a><a id="3464" class="Symbol">}{</a><a id="3466" href="/20.07/Compositional/#3466" class="Bound">N</a> <a id="3468" class="Symbol">:</a> <a id="3470" href="/20.07/Compositional/#3452" class="Bound">Ξ</a> <a id="3472" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="3474" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a> <a id="3476" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="3478" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="3479" class="Symbol">}{</a><a id="3481" href="/20.07/Compositional/#3481" class="Bound">v</a> <a id="3483" class="Symbol">:</a> <a id="3485" href="/20.07/Denotational/#4151" class="Datatype">Value</a><a id="3490" class="Symbol">}</a> <a id="3494" class="Symbol">β</a> <a id="3496" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="3498" class="Symbol">(</a><a id="3499" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="3501" href="/20.07/Compositional/#3466" class="Bound">N</a><a id="3502" class="Symbol">)</a> <a id="3504" href="/20.07/Compositional/#3455" class="Bound">Ξ³</a> <a id="3506" href="/20.07/Compositional/#3481" class="Bound">v</a> <a id="3512" class="Comment">------------</a> <a id="3527" class="Symbol">β</a> <a id="3529" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="3531" class="Symbol">(</a><a id="3532" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="3534" href="/20.07/Compositional/#3466" class="Bound">N</a><a id="3535" class="Symbol">)</a> <a id="3537" href="/20.07/Compositional/#3455" class="Bound">Ξ³</a> <a id="3539" href="/20.07/Compositional/#3481" class="Bound">v</a> <a id="3541" href="/20.07/Compositional/#3442" class="Function">β°Ζββ±β°</a> <a id="3547" class="Symbol">(</a><a id="3548" href="/20.07/Denotational/#9597" class="InductiveConstructor">β¦-intro</a> <a id="3556" href="/20.07/Compositional/#3556" class="Bound">d</a><a id="3557" class="Symbol">)</a> <a id="3559" class="Symbol">=</a> <a id="3561" href="/20.07/Compositional/#3556" class="Bound">d</a> <a id="3563" href="/20.07/Compositional/#3442" class="Function">β°Ζββ±β°</a> <a id="3569" href="/20.07/Denotational/#9709" 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="/20.07/Compositional/#3442" class="Function">β°Ζββ±β°</a> <a id="3588" class="Symbol">(</a><a id="3589" href="/20.07/Denotational/#9776" class="InductiveConstructor">β-intro</a> <a id="3597" href="/20.07/Compositional/#3597" class="Bound">dβ</a> <a id="3600" href="/20.07/Compositional/#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="/20.07/Compositional/#3442" class="Function">β°Ζββ±β°</a> <a id="3614" href="/20.07/Compositional/#3597" class="Bound">dβ</a> <a id="3617" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="3619" href="/20.07/Compositional/#3442" class="Function">β°Ζββ±β°</a> <a id="3625" href="/20.07/Compositional/#3600" class="Bound">dβ</a> <a id="3628" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="3630" href="/20.07/Compositional/#3442" class="Function">β°Ζββ±β°</a> <a id="3636" class="Symbol">(</a><a id="3637" href="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a> <a id="3641" href="/20.07/Compositional/#3641" class="Bound">d</a> <a id="3643" href="/20.07/Compositional/#3643" class="Bound">lt</a><a id="3645" class="Symbol">)</a> <a id="3647" class="Symbol">=</a> <a id="3649" href="/20.07/Compositional/#2613" class="Function">sub-β±</a> <a id="3655" class="Symbol">(</a><a id="3656" href="/20.07/Compositional/#3442" class="Function">β°Ζββ±β°</a> <a id="3662" href="/20.07/Compositional/#3641" class="Bound">d</a><a id="3663" class="Symbol">)</a> <a id="3665" href="/20.07/Compositional/#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="/20.07/Compositional/#3841" class="Function">lambda-inversion</a> <a id="3858" class="Symbol">:</a> <a id="3860" class="Symbol">β{</a><a id="3862" href="/20.07/Compositional/#3862" class="Bound">Ξ</a><a id="3863" class="Symbol">}{</a><a id="3865" href="/20.07/Compositional/#3865" class="Bound">Ξ³</a> <a id="3867" class="Symbol">:</a> <a id="3869" href="/20.07/Denotational/#7288" class="Function">Env</a> <a id="3873" href="/20.07/Compositional/#3862" class="Bound">Ξ</a><a id="3874" class="Symbol">}{</a><a id="3876" href="/20.07/Compositional/#3876" class="Bound">N</a> <a id="3878" class="Symbol">:</a> <a id="3880" href="/20.07/Compositional/#3862" class="Bound">Ξ</a> <a id="3882" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="3884" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a> <a id="3886" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="3888" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="3889" class="Symbol">}{</a><a id="3891" href="/20.07/Compositional/#3891" class="Bound">vβ</a> <a id="3894" href="/20.07/Compositional/#3894" class="Bound">vβ</a> <a id="3897" class="Symbol">:</a> <a id="3899" href="/20.07/Denotational/#4151" class="Datatype">Value</a><a id="3904" class="Symbol">}</a> <a id="3908" class="Symbol">β</a> <a id="3910" href="/20.07/Compositional/#3865" class="Bound">Ξ³</a> <a id="3912" href="/20.07/Denotational/#9346" class="Datatype Operator">β’</a> <a id="3914" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="3916" href="/20.07/Compositional/#3876" class="Bound">N</a> <a id="3918" href="/20.07/Denotational/#9346" class="Datatype Operator">β</a> <a id="3920" href="/20.07/Compositional/#3891" class="Bound">vβ</a> <a id="3923" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="3925" href="/20.07/Compositional/#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="/20.07/Compositional/#3865" class="Bound">Ξ³</a> <a id="3957" href="/20.07/Denotational/#7445" class="Function Operator">`,</a> <a id="3960" href="/20.07/Compositional/#3891" class="Bound">vβ</a><a id="3962" class="Symbol">)</a> <a id="3964" href="/20.07/Denotational/#9346" class="Datatype Operator">β’</a> <a id="3966" href="/20.07/Compositional/#3876" class="Bound">N</a> <a id="3968" href="/20.07/Denotational/#9346" class="Datatype Operator">β</a> <a id="3970" href="/20.07/Compositional/#3894" class="Bound">vβ</a> <a id="3973" href="/20.07/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="/20.07/Compositional/#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="/20.07/Compositional/#4004" class="Bound">vβ</a><a id="4006" class="Symbol">}</a> <a id="4008" href="/20.07/Compositional/#4008" class="Bound">d</a> <a id="4010" class="Symbol">=</a> <a id="4012" href="/20.07/Compositional/#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="/20.07/Compositional/#3995" class="Bound">vβ</a> <a id="4025" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="4027" href="/20.07/Compositional/#4004" class="Bound">vβ</a><a id="4029" class="Symbol">}</a> <a id="4031" href="/20.07/Compositional/#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="/20.07/Compositional/#4194" class="Function">β±β°ββ°Ζ</a> <a id="4200" class="Symbol">:</a> <a id="4202" class="Symbol">β{</a><a id="4204" href="/20.07/Compositional/#4204" class="Bound">Ξ</a><a id="4205" class="Symbol">}{</a><a id="4207" href="/20.07/Compositional/#4207" class="Bound">Ξ³</a> <a id="4209" class="Symbol">:</a> <a id="4211" href="/20.07/Denotational/#7288" class="Function">Env</a> <a id="4215" href="/20.07/Compositional/#4204" class="Bound">Ξ</a><a id="4216" class="Symbol">}{</a><a id="4218" href="/20.07/Compositional/#4218" class="Bound">N</a> <a id="4220" class="Symbol">:</a> <a id="4222" href="/20.07/Compositional/#4204" class="Bound">Ξ</a> <a id="4224" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="4226" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a> <a id="4228" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="4230" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="4231" class="Symbol">}{</a><a id="4233" href="/20.07/Compositional/#4233" class="Bound">v</a> <a id="4235" class="Symbol">:</a> <a id="4237" href="/20.07/Denotational/#4151" class="Datatype">Value</a><a id="4242" class="Symbol">}</a> <a id="4246" class="Symbol">β</a> <a id="4248" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="4250" class="Symbol">(</a><a id="4251" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="4253" href="/20.07/Compositional/#4218" class="Bound">N</a><a id="4254" class="Symbol">)</a> <a id="4256" href="/20.07/Compositional/#4207" class="Bound">Ξ³</a> <a id="4258" href="/20.07/Compositional/#4233" class="Bound">v</a> <a id="4264" class="Comment">------------</a> <a id="4279" class="Symbol">β</a> <a id="4281" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="4283" class="Symbol">(</a><a id="4284" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="4286" href="/20.07/Compositional/#4218" class="Bound">N</a><a id="4287" class="Symbol">)</a> <a id="4289" href="/20.07/Compositional/#4207" class="Bound">Ξ³</a> <a id="4291" href="/20.07/Compositional/#4233" class="Bound">v</a> <a id="4293" href="/20.07/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="/20.07/Denotational/#4171" class="InductiveConstructor">β₯</a><a id="4305" class="Symbol">}</a> <a id="4307" href="/20.07/Compositional/#4307" class="Bound">d</a> <a id="4309" class="Symbol">=</a> <a id="4311" href="/20.07/Denotational/#9709" class="InductiveConstructor">β₯-intro</a> <a id="4319" href="/20.07/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="/20.07/Compositional/#4330" class="Bound">vβ</a> <a id="4333" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="4335" href="/20.07/Compositional/#4335" class="Bound">vβ</a><a id="4337" class="Symbol">}</a> <a id="4339" href="/20.07/Compositional/#4339" class="Bound">d</a> <a id="4341" class="Symbol">=</a> <a id="4343" href="/20.07/Denotational/#9597" class="InductiveConstructor">β¦-intro</a> <a id="4351" href="/20.07/Compositional/#4339" class="Bound">d</a> <a id="4353" href="/20.07/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="/20.07/Compositional/#4364" class="Bound">vβ</a> <a id="4367" href="/20.07/Denotational/#4213" class="InductiveConstructor Operator">β</a> <a id="4369" href="/20.07/Compositional/#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="/20.07/Compositional/#4375" class="Bound">d1</a> <a id="4378" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4380" href="/20.07/Compositional/#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="/20.07/Denotational/#9776" class="InductiveConstructor">β-intro</a> <a id="4395" class="Symbol">(</a><a id="4396" href="/20.07/Compositional/#4194" class="Function">β±β°ββ°Ζ</a> <a id="4402" href="/20.07/Compositional/#4375" class="Bound">d1</a><a id="4404" class="Symbol">)</a> <a id="4406" class="Symbol">(</a><a id="4407" href="/20.07/Compositional/#4194" class="Function">β±β°ββ°Ζ</a> <a id="4413" href="/20.07/Compositional/#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="/20.07/Compositional/#4552" class="Function">lam-equiv</a> <a id="4562" class="Symbol">:</a> <a id="4564" class="Symbol">β{</a><a id="4566" href="/20.07/Compositional/#4566" class="Bound">Ξ</a><a id="4567" class="Symbol">}{</a><a id="4569" href="/20.07/Compositional/#4569" class="Bound">N</a> <a id="4571" class="Symbol">:</a> <a id="4573" href="/20.07/Compositional/#4566" class="Bound">Ξ</a> <a id="4575" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="4577" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a> <a id="4579" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="4581" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="4582" class="Symbol">}</a> <a id="4586" class="Symbol">β</a> <a id="4588" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="4590" class="Symbol">(</a><a id="4591" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="4593" href="/20.07/Compositional/#4569" class="Bound">N</a><a id="4594" class="Symbol">)</a> <a id="4596" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="4598" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="4600" class="Symbol">(</a><a id="4601" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="4603" href="/20.07/Compositional/#4569" class="Bound">N</a><a id="4604" class="Symbol">)</a> <a id="4606" href="/20.07/Compositional/#4552" class="Function">lam-equiv</a> <a id="4616" href="/20.07/Compositional/#4616" class="Bound">Ξ³</a> <a id="4618" href="/20.07/Compositional/#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="/20.07/Compositional/#3442" class="Function">β°Ζββ±β°</a> <a id="4630" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4632" href="/20.07/Compositional/#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="/20.07/Compositional/#5745" class="Function Operator">_β_</a> <a id="_β_"></a><a id="5745" href="/20.07/Compositional/#5745" class="Function Operator">_β_</a> <a id="5749" class="Symbol">:</a> <a id="5751" class="Symbol">β{</a><a id="5753" href="/20.07/Compositional/#5753" class="Bound">Ξ</a><a id="5754" class="Symbol">}</a> <a id="5756" class="Symbol">β</a> <a id="5758" href="/20.07/Denotational/#17273" class="Function">Denotation</a> <a id="5769" href="/20.07/Compositional/#5753" class="Bound">Ξ</a> <a id="5771" class="Symbol">β</a> <a id="5773" href="/20.07/Denotational/#17273" class="Function">Denotation</a> <a id="5784" href="/20.07/Compositional/#5753" class="Bound">Ξ</a> <a id="5786" class="Symbol">β</a> <a id="5788" href="/20.07/Denotational/#17273" class="Function">Denotation</a> <a id="5799" href="/20.07/Compositional/#5753" class="Bound">Ξ</a> <a id="5801" class="Symbol">(</a><a id="5802" href="/20.07/Compositional/#5802" class="Bound">Dβ</a> <a id="5805" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="5807" href="/20.07/Compositional/#5807" class="Bound">Dβ</a><a id="5809" class="Symbol">)</a> <a id="5811" href="/20.07/Compositional/#5811" class="Bound">Ξ³</a> <a id="5813" href="/20.07/Compositional/#5813" class="Bound">w</a> <a id="5815" class="Symbol">=</a> <a id="5817" href="/20.07/Compositional/#5813" class="Bound">w</a> <a id="5819" href="/20.07/Denotational/#4508" class="Datatype Operator">β</a> <a id="5821" href="/20.07/Denotational/#4171" 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="/20.07/Compositional/#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="/20.07/Denotational/#4151" 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="/20.07/Compositional/#5802" class="Bound">Dβ</a> <a id="5844" href="/20.07/Compositional/#5811" class="Bound">Ξ³</a> <a id="5846" class="Symbol">(</a><a id="5847" href="/20.07/Compositional/#5828" class="Bound">v</a> <a id="5849" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="5851" href="/20.07/Compositional/#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="/20.07/Compositional/#5807" class="Bound">Dβ</a> <a id="5859" href="/20.07/Compositional/#5811" class="Bound">Ξ³</a> <a id="5861" href="/20.07/Compositional/#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="/20.07/Compositional/#6224" class="Function">β°Β·βββ°</a> <a id="6230" class="Symbol">:</a> <a id="6232" class="Symbol">β{</a><a id="6234" href="/20.07/Compositional/#6234" class="Bound">Ξ</a><a id="6235" class="Symbol">}{</a><a id="6237" href="/20.07/Compositional/#6237" class="Bound">Ξ³</a> <a id="6239" class="Symbol">:</a> <a id="6241" href="/20.07/Denotational/#7288" class="Function">Env</a> <a id="6245" href="/20.07/Compositional/#6234" class="Bound">Ξ</a><a id="6246" class="Symbol">}{</a><a id="6248" href="/20.07/Compositional/#6248" class="Bound">L</a> <a id="6250" href="/20.07/Compositional/#6250" class="Bound">M</a> <a id="6252" class="Symbol">:</a> <a id="6254" href="/20.07/Compositional/#6234" class="Bound">Ξ</a> <a id="6256" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="6258" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="6259" class="Symbol">}{</a><a id="6261" href="/20.07/Compositional/#6261" class="Bound">v</a> <a id="6263" class="Symbol">:</a> <a id="6265" href="/20.07/Denotational/#4151" class="Datatype">Value</a><a id="6270" class="Symbol">}</a> <a id="6274" class="Symbol">β</a> <a id="6276" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="6278" class="Symbol">(</a><a id="6279" href="/20.07/Compositional/#6248" class="Bound">L</a> <a id="6281" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="6283" href="/20.07/Compositional/#6250" class="Bound">M</a><a id="6284" class="Symbol">)</a> <a id="6286" href="/20.07/Compositional/#6237" class="Bound">Ξ³</a> <a id="6288" href="/20.07/Compositional/#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="/20.07/Denotational/#17486" class="Function">β°</a> <a id="6318" href="/20.07/Compositional/#6248" class="Bound">L</a> <a id="6320" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="6322" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="6324" href="/20.07/Compositional/#6250" class="Bound">M</a><a id="6325" class="Symbol">)</a> <a id="6327" href="/20.07/Compositional/#6237" class="Bound">Ξ³</a> <a id="6329" href="/20.07/Compositional/#6261" class="Bound">v</a> <a id="6331" href="/20.07/Compositional/#6224" class="Function">β°Β·βββ°</a> <a id="6337" class="Symbol">(</a><a id="6338" href="/20.07/Denotational/#9475" 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="/20.07/Compositional/#6349" class="Bound">vβ²</a><a id="6351" class="Symbol">}</a> <a id="6353" href="/20.07/Compositional/#6353" class="Bound">dβ</a> <a id="6356" href="/20.07/Compositional/#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="/20.07/Compositional/#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="/20.07/Compositional/#6353" class="Bound">dβ</a> <a id="6379" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6381" href="/20.07/Compositional/#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="/20.07/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="/20.07/Denotational/#4171" class="InductiveConstructor">β₯</a><a id="6400" class="Symbol">}</a> <a id="6402" href="/20.07/Denotational/#9709" 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="/20.07/Denotational/#4543" class="InductiveConstructor">β-bot</a> <a id="6423" href="/20.07/Compositional/#6224" class="Function">β°Β·βββ°</a> <a id="6429" class="Symbol">{</a><a id="6430" href="/20.07/Compositional/#6430" class="Bound">Ξ</a><a id="6431" class="Symbol">}{</a><a id="6433" href="/20.07/Compositional/#6433" class="Bound">Ξ³</a><a id="6434" class="Symbol">}{</a><a id="6436" href="/20.07/Compositional/#6436" class="Bound">L</a><a id="6437" class="Symbol">}{</a><a id="6439" href="/20.07/Compositional/#6439" class="Bound">M</a><a id="6440" class="Symbol">}{</a><a id="6442" href="/20.07/Compositional/#6442" class="Bound">v</a><a id="6443" class="Symbol">}</a> <a id="6445" class="Symbol">(</a><a id="6446" href="/20.07/Denotational/#9776" 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="/20.07/Compositional/#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="/20.07/Compositional/#6466" class="Bound">vβ</a><a id="6468" class="Symbol">}</a> <a id="6470" href="/20.07/Compositional/#6470" class="Bound">dβ</a> <a id="6473" href="/20.07/Compositional/#6473" class="Bound">dβ</a><a id="6475" class="Symbol">)</a> <a id="6481" class="Keyword">with</a> <a id="6486" href="/20.07/Compositional/#6224" class="Function">β°Β·βββ°</a> <a id="6492" href="/20.07/Compositional/#6470" class="Bound">dβ</a> <a id="6495" class="Symbol">|</a> <a id="6497" href="/20.07/Compositional/#6224" class="Function">β°Β·βββ°</a> <a id="6503" href="/20.07/Compositional/#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="/20.07/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="/20.07/Compositional/#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="/20.07/Denotational/#4568" class="InductiveConstructor">β-conj-L</a> <a id="6549" href="/20.07/Compositional/#6517" class="Bound">lt1</a> <a id="6553" href="/20.07/Compositional/#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="/20.07/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="/20.07/Compositional/#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="/20.07/Compositional/#6590" class="Bound">Lβv12</a> <a id="6596" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6598" href="/20.07/Compositional/#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="/20.07/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="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a> <a id="6634" href="/20.07/Compositional/#6590" class="Bound">Lβv12</a> <a id="6640" href="/20.07/Compositional/#6666" class="Function">lt</a> <a id="6643" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6645" href="/20.07/Compositional/#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="/20.07/Compositional/#6666" class="Function">lt</a> <a id="6669" class="Symbol">:</a> <a id="6671" href="/20.07/Compositional/#6582" class="Bound">vββ²</a> <a id="6675" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="6677" class="Symbol">(</a><a id="6678" class="Bound">vβ</a> <a id="6681" href="/20.07/Denotational/#4213" class="InductiveConstructor Operator">β</a> <a id="6683" class="Bound">vβ</a><a id="6685" class="Symbol">)</a> <a id="6687" href="/20.07/Denotational/#4508" class="Datatype Operator">β</a> <a id="6689" href="/20.07/Compositional/#6582" class="Bound">vββ²</a> <a id="6693" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="6695" class="Bound">vβ</a> <a id="6710" href="/20.07/Compositional/#6666" class="Function">lt</a> <a id="6713" class="Symbol">=</a> <a id="6715" class="Symbol">(</a><a id="6716" href="/20.07/Denotational/#4869" class="InductiveConstructor">β-fun</a> <a id="6722" href="/20.07/Denotational/#5638" class="Function">β-refl</a> <a id="6729" class="Symbol">(</a><a id="6730" href="/20.07/Denotational/#4568" class="InductiveConstructor">β-conj-L</a> <a id="6739" class="Symbol">(</a><a id="6740" href="/20.07/Denotational/#4798" class="InductiveConstructor">β-trans</a> <a id="6748" href="/20.07/Compositional/#6569" class="Bound">lt1</a> <a id="6752" href="/20.07/Denotational/#4543" class="InductiveConstructor">β-bot</a><a id="6757" class="Symbol">)</a> <a id="6759" href="/20.07/Denotational/#5638" 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="/20.07/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="/20.07/Compositional/#6789" class="Bound">Lβv12</a> <a id="6795" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6797" href="/20.07/Compositional/#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="/20.07/Compositional/#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="/20.07/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="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a> <a id="6844" href="/20.07/Compositional/#6789" class="Bound">Lβv12</a> <a id="6850" href="/20.07/Compositional/#6876" class="Function">lt</a> <a id="6853" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6855" href="/20.07/Compositional/#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="/20.07/Compositional/#6876" class="Function">lt</a> <a id="6879" class="Symbol">:</a> <a id="6881" href="/20.07/Compositional/#6781" class="Bound">vββ²</a> <a id="6885" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="6887" class="Symbol">(</a><a id="6888" class="Bound">vβ</a> <a id="6891" href="/20.07/Denotational/#4213" class="InductiveConstructor Operator">β</a> <a id="6893" class="Bound">vβ</a><a id="6895" class="Symbol">)</a> <a id="6897" href="/20.07/Denotational/#4508" class="Datatype Operator">β</a> <a id="6899" href="/20.07/Compositional/#6781" class="Bound">vββ²</a> <a id="6903" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="6905" class="Bound">vβ</a> <a id="6920" href="/20.07/Compositional/#6876" class="Function">lt</a> <a id="6923" class="Symbol">=</a> <a id="6925" class="Symbol">(</a><a id="6926" href="/20.07/Denotational/#4869" class="InductiveConstructor">β-fun</a> <a id="6932" href="/20.07/Denotational/#5638" class="Function">β-refl</a> <a id="6939" class="Symbol">(</a><a id="6940" href="/20.07/Denotational/#4568" class="InductiveConstructor">β-conj-L</a> <a id="6949" href="/20.07/Denotational/#5638" class="Function">β-refl</a> <a id="6956" class="Symbol">(</a><a id="6957" href="/20.07/Denotational/#4798" class="InductiveConstructor">β-trans</a> <a id="6965" href="/20.07/Compositional/#6813" class="Bound">lt2</a> <a id="6969" href="/20.07/Denotational/#4543" 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="/20.07/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="/20.07/Compositional/#6999" class="Bound">Lβv12</a> <a id="7005" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7007" href="/20.07/Compositional/#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="/20.07/Compositional/#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="/20.07/Compositional/#7034" class="Bound">Lβv12β²</a> <a id="7041" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7043" href="/20.07/Compositional/#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="/20.07/Compositional/#7065" class="Bound">Lββ</a> <a id="7069" class="Symbol">=</a> <a id="7071" href="/20.07/Denotational/#9776" class="InductiveConstructor">β-intro</a> <a id="7079" href="/20.07/Compositional/#6999" class="Bound">Lβv12</a> <a id="7085" href="/20.07/Compositional/#7034" class="Bound">Lβv12β²</a> <a id="7092" class="Keyword">in</a> <a id="7101" class="Keyword">let</a> <a id="7105" href="/20.07/Compositional/#7105" class="Bound">Mββ</a> <a id="7109" class="Symbol">=</a> <a id="7111" href="/20.07/Denotational/#9776" class="InductiveConstructor">β-intro</a> <a id="7119" href="/20.07/Compositional/#7007" class="Bound">Mβv3</a> <a id="7124" href="/20.07/Compositional/#7043" class="Bound">Mβv3β²</a> <a id="7130" class="Keyword">in</a> <a id="7139" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">injβ</a> <a id="7144" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="7146" href="/20.07/Compositional/#6991" class="Bound">vββ²</a> <a id="7150" href="/20.07/Denotational/#4213" class="InductiveConstructor Operator">β</a> <a id="7152" href="/20.07/Compositional/#7025" class="Bound">vββ²β²</a> <a id="7157" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7159" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="7161" href="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a> <a id="7165" href="/20.07/Compositional/#7065" class="Bound">Lββ</a> <a id="7169" href="/20.07/Denotational/#6273" class="Function">ββ¦β-dist</a> <a id="7178" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7180" href="/20.07/Compositional/#7105" class="Bound">Mββ</a> <a id="7184" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="7186" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="7188" href="/20.07/Compositional/#6224" class="Function">β°Β·βββ°</a> <a id="7194" class="Symbol">{</a><a id="7195" href="/20.07/Compositional/#7195" class="Bound">Ξ</a><a id="7196" class="Symbol">}{</a><a id="7198" href="/20.07/Compositional/#7198" class="Bound">Ξ³</a><a id="7199" class="Symbol">}{</a><a id="7201" href="/20.07/Compositional/#7201" class="Bound">L</a><a id="7202" class="Symbol">}{</a><a id="7204" href="/20.07/Compositional/#7204" class="Bound">M</a><a id="7205" class="Symbol">}{</a><a id="7207" href="/20.07/Compositional/#7207" class="Bound">v</a><a id="7208" class="Symbol">}</a> <a id="7210" class="Symbol">(</a><a id="7211" href="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a> <a id="7215" href="/20.07/Compositional/#7215" class="Bound">d</a> <a id="7217" href="/20.07/Compositional/#7217" class="Bound">lt</a><a id="7219" class="Symbol">)</a> <a id="7225" class="Keyword">with</a> <a id="7230" href="/20.07/Compositional/#6224" class="Function">β°Β·βββ°</a> <a id="7236" href="/20.07/Compositional/#7215" class="Bound">d</a> <a id="7238" class="Symbol">...</a> <a id="7242" class="Symbol">|</a> <a id="7244" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">injβ</a> <a id="7249" href="/20.07/Compositional/#7249" class="Bound">lt2</a> <a id="7253" class="Symbol">=</a> <a id="7255" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">injβ</a> <a id="7260" class="Symbol">(</a><a id="7261" href="/20.07/Denotational/#4798" class="InductiveConstructor">β-trans</a> <a id="7269" class="Bound">lt</a> <a id="7272" href="/20.07/Compositional/#7249" class="Bound">lt2</a><a id="7275" class="Symbol">)</a> <a id="7277" class="Symbol">...</a> <a id="7281" class="Symbol">|</a> <a id="7283" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">injβ</a> <a id="7288" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="7290" href="/20.07/Compositional/#7290" class="Bound">vβ</a> <a id="7293" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7295" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="7297" href="/20.07/Compositional/#7297" class="Bound">Lβv12</a> <a id="7303" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7305" href="/20.07/Compositional/#7305" class="Bound">Mβv3</a> <a id="7310" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="7312" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="7314" class="Symbol">=</a> <a id="7322" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">injβ</a> <a id="7327" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="7329" href="/20.07/Compositional/#7290" class="Bound">vβ</a> <a id="7332" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7334" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="7336" href="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a> <a id="7340" href="/20.07/Compositional/#7297" class="Bound">Lβv12</a> <a id="7346" class="Symbol">(</a><a id="7347" href="/20.07/Denotational/#4869" class="InductiveConstructor">β-fun</a> <a id="7353" href="/20.07/Denotational/#5638" class="Function">β-refl</a> <a id="7360" class="Bound">lt</a><a id="7362" class="Symbol">)</a> <a id="7364" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7366" href="/20.07/Compositional/#7305" class="Bound">Mβv3</a> <a id="7371" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="7373" 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="9439" href="/20.07/Compositional/#9439" class="Function">ββ°ββ°Β·</a> <a id="9445" class="Symbol">:</a> <a id="9447" class="Symbol">β{</a><a id="9449" href="/20.07/Compositional/#9449" class="Bound">Ξ</a><a id="9450" class="Symbol">}{</a><a id="9452" href="/20.07/Compositional/#9452" class="Bound">Ξ³</a> <a id="9454" class="Symbol">:</a> <a id="9456" href="/20.07/Denotational/#7288" class="Function">Env</a> <a id="9460" href="/20.07/Compositional/#9449" class="Bound">Ξ</a><a id="9461" class="Symbol">}{</a><a id="9463" href="/20.07/Compositional/#9463" class="Bound">L</a> <a id="9465" href="/20.07/Compositional/#9465" class="Bound">M</a> <a id="9467" class="Symbol">:</a> <a id="9469" href="/20.07/Compositional/#9449" class="Bound">Ξ</a> <a id="9471" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="9473" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="9474" class="Symbol">}{</a><a id="9476" href="/20.07/Compositional/#9476" class="Bound">v</a><a id="9477" class="Symbol">}</a> <a id="9481" class="Symbol">β</a> <a id="9483" class="Symbol">(</a><a id="9484" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="9486" href="/20.07/Compositional/#9463" class="Bound">L</a> <a id="9488" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="9490" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="9492" href="/20.07/Compositional/#9465" class="Bound">M</a><a id="9493" class="Symbol">)</a> <a id="9495" href="/20.07/Compositional/#9452" class="Bound">Ξ³</a> <a id="9497" href="/20.07/Compositional/#9476" class="Bound">v</a> <a id="9503" class="Comment">----------------</a> <a id="9522" class="Symbol">β</a> <a id="9524" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="9526" class="Symbol">(</a><a id="9527" href="/20.07/Compositional/#9463" class="Bound">L</a> <a id="9529" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="9531" href="/20.07/Compositional/#9465" class="Bound">M</a><a id="9532" class="Symbol">)</a> <a id="9534" href="/20.07/Compositional/#9452" class="Bound">Ξ³</a> <a id="9536" href="/20.07/Compositional/#9476" class="Bound">v</a> <a id="9538" href="/20.07/Compositional/#9439" class="Function">ββ°ββ°Β·</a> <a id="9544" class="Symbol">{</a><a id="9545" href="/20.07/Compositional/#9545" class="Bound">Ξ³</a><a id="9546" class="Symbol">}{</a><a id="9548" href="/20.07/Compositional/#9548" class="Bound">v</a><a id="9549" class="Symbol">}</a> <a id="9551" class="Symbol">(</a><a id="9552" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">injβ</a> <a id="9557" href="/20.07/Compositional/#9557" class="Bound">lt</a><a id="9559" class="Symbol">)</a> <a id="9561" class="Symbol">=</a> <a id="9563" href="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a> <a id="9567" href="/20.07/Denotational/#9709" class="InductiveConstructor">β₯-intro</a> <a id="9575" href="/20.07/Compositional/#9557" class="Bound">lt</a> <a id="9578" href="/20.07/Compositional/#9439" class="Function">ββ°ββ°Β·</a> <a id="9584" class="Symbol">{</a><a id="9585" href="/20.07/Compositional/#9585" class="Bound">Ξ³</a><a id="9586" class="Symbol">}{</a><a id="9588" href="/20.07/Compositional/#9588" class="Bound">v</a><a id="9589" class="Symbol">}</a> <a id="9591" class="Symbol">(</a><a id="9592" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">injβ</a> <a id="9597" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="9599" href="/20.07/Compositional/#9599" class="Bound">vβ</a> <a id="9602" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="9604" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="9606" href="/20.07/Compositional/#9606" class="Bound">d1</a> <a id="9609" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="9611" href="/20.07/Compositional/#9611" class="Bound">d2</a> <a id="9614" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="9616" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a><a id="9617" class="Symbol">)</a> <a id="9619" class="Symbol">=</a> <a id="9621" href="/20.07/Denotational/#9475" class="InductiveConstructor">β¦-elim</a> <a id="9628" href="/20.07/Compositional/#9606" class="Bound">d1</a> <a id="9631" href="/20.07/Compositional/#9611" 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="9770" href="/20.07/Compositional/#9770" class="Function">app-equiv</a> <a id="9780" class="Symbol">:</a> <a id="9782" class="Symbol">β{</a><a id="9784" href="/20.07/Compositional/#9784" class="Bound">Ξ</a><a id="9785" class="Symbol">}{</a><a id="9787" href="/20.07/Compositional/#9787" class="Bound">L</a> <a id="9789" href="/20.07/Compositional/#9789" class="Bound">M</a> <a id="9791" class="Symbol">:</a> <a id="9793" href="/20.07/Compositional/#9784" class="Bound">Ξ</a> <a id="9795" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="9797" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="9798" class="Symbol">}</a> <a id="9802" class="Symbol">β</a> <a id="9804" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="9806" class="Symbol">(</a><a id="9807" href="/20.07/Compositional/#9787" class="Bound">L</a> <a id="9809" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="9811" href="/20.07/Compositional/#9789" class="Bound">M</a><a id="9812" class="Symbol">)</a> <a id="9814" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="9816" class="Symbol">(</a><a id="9817" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="9819" href="/20.07/Compositional/#9787" class="Bound">L</a><a id="9820" class="Symbol">)</a> <a id="9822" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="9824" class="Symbol">(</a><a id="9825" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="9827" href="/20.07/Compositional/#9789" class="Bound">M</a><a id="9828" class="Symbol">)</a> <a id="9830" href="/20.07/Compositional/#9770" class="Function">app-equiv</a> <a id="9840" href="/20.07/Compositional/#9840" class="Bound">Ξ³</a> <a id="9842" href="/20.07/Compositional/#9842" class="Bound">v</a> <a id="9844" class="Symbol">=</a> <a id="9846" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="9848" href="/20.07/Compositional/#6224" class="Function">β°Β·βββ°</a> <a id="9854" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="9856" href="/20.07/Compositional/#9439" class="Function">ββ°ββ°Β·</a> <a id="9862" 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="10012" href="/20.07/Compositional/#10012" class="Function">var-inv</a> <a id="10020" class="Symbol">:</a> <a id="10022" class="Symbol">β</a> <a id="10024" class="Symbol">{</a><a id="10025" href="/20.07/Compositional/#10025" class="Bound">Ξ</a> <a id="10027" href="/20.07/Compositional/#10027" class="Bound">v</a> <a id="10029" href="/20.07/Compositional/#10029" class="Bound">x</a><a id="10030" class="Symbol">}</a> <a id="10032" class="Symbol">{</a><a id="10033" href="/20.07/Compositional/#10033" class="Bound">Ξ³</a> <a id="10035" class="Symbol">:</a> <a id="10037" href="/20.07/Denotational/#7288" class="Function">Env</a> <a id="10041" href="/20.07/Compositional/#10025" class="Bound">Ξ</a><a id="10042" class="Symbol">}</a> <a id="10046" class="Symbol">β</a> <a id="10048" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="10050" class="Symbol">(</a><a id="10051" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="10053" href="/20.07/Compositional/#10029" class="Bound">x</a><a id="10054" class="Symbol">)</a> <a id="10056" href="/20.07/Compositional/#10033" class="Bound">Ξ³</a> <a id="10058" href="/20.07/Compositional/#10027" class="Bound">v</a> <a id="10064" class="Comment">-------------------</a> <a id="10086" class="Symbol">β</a> <a id="10088" href="/20.07/Compositional/#10027" class="Bound">v</a> <a id="10090" href="/20.07/Denotational/#4508" class="Datatype Operator">β</a> <a id="10092" href="/20.07/Compositional/#10033" class="Bound">Ξ³</a> <a id="10094" href="/20.07/Compositional/#10029" class="Bound">x</a> <a id="10096" href="/20.07/Compositional/#10012" class="Function">var-inv</a> <a id="10104" class="Symbol">(</a><a id="10105" href="/20.07/Denotational/#9400" class="InductiveConstructor">var</a><a id="10108" class="Symbol">)</a> <a id="10110" class="Symbol">=</a> <a id="10112" href="/20.07/Denotational/#5638" class="Function">β-refl</a> <a id="10119" href="/20.07/Compositional/#10012" class="Function">var-inv</a> <a id="10127" class="Symbol">(</a><a id="10128" href="/20.07/Denotational/#9776" class="InductiveConstructor">β-intro</a> <a id="10136" href="/20.07/Compositional/#10136" class="Bound">dβ</a> <a id="10139" href="/20.07/Compositional/#10139" class="Bound">dβ</a><a id="10141" class="Symbol">)</a> <a id="10143" class="Symbol">=</a> <a id="10145" href="/20.07/Denotational/#4568" class="InductiveConstructor">β-conj-L</a> <a id="10154" class="Symbol">(</a><a id="10155" href="/20.07/Compositional/#10012" class="Function">var-inv</a> <a id="10163" href="/20.07/Compositional/#10136" class="Bound">dβ</a><a id="10165" class="Symbol">)</a> <a id="10167" class="Symbol">(</a><a id="10168" href="/20.07/Compositional/#10012" class="Function">var-inv</a> <a id="10176" href="/20.07/Compositional/#10139" class="Bound">dβ</a><a id="10178" class="Symbol">)</a> <a id="10180" href="/20.07/Compositional/#10012" class="Function">var-inv</a> <a id="10188" class="Symbol">(</a><a id="10189" href="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a> <a id="10193" href="/20.07/Compositional/#10193" class="Bound">d</a> <a id="10195" href="/20.07/Compositional/#10195" class="Bound">lt</a><a id="10197" class="Symbol">)</a> <a id="10199" class="Symbol">=</a> <a id="10201" href="/20.07/Denotational/#4798" class="InductiveConstructor">β-trans</a> <a id="10209" href="/20.07/Compositional/#10195" class="Bound">lt</a> <a id="10212" class="Symbol">(</a><a id="10213" href="/20.07/Compositional/#10012" class="Function">var-inv</a> <a id="10221" href="/20.07/Compositional/#10193" class="Bound">d</a><a id="10222" class="Symbol">)</a> <a id="10224" href="/20.07/Compositional/#10012" class="Function">var-inv</a> <a id="10232" href="/20.07/Denotational/#9709" class="InductiveConstructor">β₯-intro</a> <a id="10240" class="Symbol">=</a> <a id="10242" href="/20.07/Denotational/#4543" 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="10341" href="/20.07/Compositional/#10341" class="Function">var-equiv</a> <a id="10351" class="Symbol">:</a> <a id="10353" class="Symbol">β{</a><a id="10355" href="/20.07/Compositional/#10355" class="Bound">Ξ</a><a id="10356" class="Symbol">}{</a><a id="10358" href="/20.07/Compositional/#10358" class="Bound">x</a> <a id="10360" class="Symbol">:</a> <a id="10362" href="/20.07/Compositional/#10355" class="Bound">Ξ</a> <a id="10364" href="/20.07/Untyped/#3521" class="Datatype Operator">β</a> <a id="10366" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="10367" class="Symbol">}</a> <a id="10369" class="Symbol">β</a> <a id="10371" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="10373" class="Symbol">(</a><a id="10374" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="10376" href="/20.07/Compositional/#10358" class="Bound">x</a><a id="10377" class="Symbol">)</a> <a id="10379" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="10381" class="Symbol">(Ξ»</a> <a id="10384" href="/20.07/Compositional/#10384" class="Bound">Ξ³</a> <a id="10386" href="/20.07/Compositional/#10386" class="Bound">v</a> <a id="10388" class="Symbol">β</a> <a id="10390" href="/20.07/Compositional/#10386" class="Bound">v</a> <a id="10392" href="/20.07/Denotational/#4508" class="Datatype Operator">β</a> <a id="10394" href="/20.07/Compositional/#10384" class="Bound">Ξ³</a> <a id="10396" href="/20.07/Compositional/#10358" class="Bound">x</a><a id="10397" class="Symbol">)</a> <a id="10399" href="/20.07/Compositional/#10341" class="Function">var-equiv</a> <a id="10409" href="/20.07/Compositional/#10409" class="Bound">Ξ³</a> <a id="10411" href="/20.07/Compositional/#10411" class="Bound">v</a> <a id="10413" class="Symbol">=</a> <a id="10415" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="10417" href="/20.07/Compositional/#10012" class="Function">var-inv</a> <a id="10425" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="10427" class="Symbol">(Ξ»</a> <a id="10430" href="/20.07/Compositional/#10430" class="Bound">lt</a> <a id="10433" class="Symbol">β</a> <a id="10435" href="/20.07/Denotational/#9891" class="InductiveConstructor">sub</a> <a id="10439" href="/20.07/Denotational/#9400" class="InductiveConstructor">var</a> <a id="10443" href="/20.07/Compositional/#10430" class="Bound">lt</a><a id="10445" class="Symbol">)</a> <a id="10447" 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="11171" href="/20.07/Compositional/#11171" class="Function">β±-cong</a> <a id="11178" class="Symbol">:</a> <a id="11180" class="Symbol">β{</a><a id="11182" href="/20.07/Compositional/#11182" class="Bound">Ξ</a><a id="11183" class="Symbol">}{</a><a id="11185" href="/20.07/Compositional/#11185" class="Bound">D</a> <a id="11187" href="/20.07/Compositional/#11187" class="Bound">Dβ²</a> <a id="11190" class="Symbol">:</a> <a id="11192" href="/20.07/Denotational/#17273" class="Function">Denotation</a> <a id="11203" class="Symbol">(</a><a id="11204" href="/20.07/Compositional/#11182" class="Bound">Ξ</a> <a id="11206" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="11208" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="11209" class="Symbol">)}</a> <a id="11214" class="Symbol">β</a> <a id="11216" href="/20.07/Compositional/#11185" class="Bound">D</a> <a id="11218" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="11220" href="/20.07/Compositional/#11187" class="Bound">Dβ²</a> <a id="11227" class="Comment">-----------</a> <a id="11241" class="Symbol">β</a> <a id="11243" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="11245" href="/20.07/Compositional/#11185" class="Bound">D</a> <a id="11247" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="11249" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="11251" href="/20.07/Compositional/#11187" class="Bound">Dβ²</a> <a id="11254" href="/20.07/Compositional/#11171" class="Function">β±-cong</a><a id="11260" class="Symbol">{</a><a id="11261" href="/20.07/Compositional/#11261" class="Bound">Ξ</a><a id="11262" class="Symbol">}</a> <a id="11264" href="/20.07/Compositional/#11264" class="Bound">DβDβ²</a> <a id="11269" href="/20.07/Compositional/#11269" class="Bound">Ξ³</a> <a id="11271" href="/20.07/Compositional/#11271" class="Bound">v</a> <a id="11273" class="Symbol">=</a> <a id="11277" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="11279" class="Symbol">(Ξ»</a> <a id="11282" href="/20.07/Compositional/#11282" class="Bound">x</a> <a id="11284" class="Symbol">β</a> <a id="11286" href="/20.07/Compositional/#11349" class="Function">β±β</a><a id="11288" class="Symbol">{</a><a id="11289" href="/20.07/Compositional/#11269" class="Bound">Ξ³</a><a id="11290" class="Symbol">}{</a><a id="11292" href="/20.07/Compositional/#11271" class="Bound">v</a><a id="11293" class="Symbol">}</a> <a id="11295" href="/20.07/Compositional/#11282" class="Bound">x</a> <a id="11297" href="/20.07/Compositional/#11264" class="Bound">DβDβ²</a><a id="11301" class="Symbol">)</a> <a id="11303" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11305" class="Symbol">(Ξ»</a> <a id="11308" href="/20.07/Compositional/#11308" class="Bound">x</a> <a id="11310" class="Symbol">β</a> <a id="11312" href="/20.07/Compositional/#11349" class="Function">β±β</a><a id="11314" class="Symbol">{</a><a id="11315" href="/20.07/Compositional/#11269" class="Bound">Ξ³</a><a id="11316" class="Symbol">}{</a><a id="11318" href="/20.07/Compositional/#11271" class="Bound">v</a><a id="11319" class="Symbol">}</a> <a id="11321" href="/20.07/Compositional/#11308" class="Bound">x</a> <a id="11323" class="Symbol">(</a><a id="11324" href="/20.07/Denotational/#17940" class="Function">β-sym</a> <a id="11330" href="/20.07/Compositional/#11264" class="Bound">DβDβ²</a><a id="11334" class="Symbol">))</a> <a id="11337" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="11341" class="Keyword">where</a> <a id="11349" href="/20.07/Compositional/#11349" class="Function">β±β</a> <a id="11352" class="Symbol">:</a> <a id="11354" class="Symbol">β{</a><a id="11356" href="/20.07/Compositional/#11356" class="Bound">Ξ³</a> <a id="11358" class="Symbol">:</a> <a id="11360" href="/20.07/Denotational/#7288" class="Function">Env</a> <a id="11364" href="/20.07/Compositional/#11261" class="Bound">Ξ</a><a id="11365" class="Symbol">}{</a><a id="11367" href="/20.07/Compositional/#11367" class="Bound">v</a><a id="11368" class="Symbol">}{</a><a id="11370" href="/20.07/Compositional/#11370" class="Bound">D</a> <a id="11372" href="/20.07/Compositional/#11372" class="Bound">Dβ²</a> <a id="11375" class="Symbol">:</a> <a id="11377" href="/20.07/Denotational/#17273" class="Function">Denotation</a> <a id="11388" class="Symbol">(</a><a id="11389" href="/20.07/Compositional/#11261" class="Bound">Ξ</a> <a id="11391" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="11393" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="11394" class="Symbol">)}</a> <a id="11401" class="Symbol">β</a> <a id="11403" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="11405" href="/20.07/Compositional/#11370" class="Bound">D</a> <a id="11407" href="/20.07/Compositional/#11356" class="Bound">Ξ³</a> <a id="11409" href="/20.07/Compositional/#11367" class="Bound">v</a> <a id="11412" class="Symbol">β</a> <a id="11415" href="/20.07/Compositional/#11370" class="Bound">D</a> <a id="11417" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="11419" href="/20.07/Compositional/#11372" class="Bound">Dβ²</a> <a id="11422" class="Symbol">β</a> <a id="11424" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="11426" href="/20.07/Compositional/#11372" class="Bound">Dβ²</a> <a id="11429" href="/20.07/Compositional/#11356" class="Bound">Ξ³</a> <a id="11431" href="/20.07/Compositional/#11367" class="Bound">v</a> <a id="11435" href="/20.07/Compositional/#11349" class="Function">β±β</a> <a id="11438" class="Symbol">{</a><a id="11439" class="Argument">v</a> <a id="11441" class="Symbol">=</a> <a id="11443" href="/20.07/Denotational/#4171" class="InductiveConstructor">β₯</a><a id="11444" class="Symbol">}</a> <a id="11446" href="/20.07/Compositional/#11446" class="Bound">fd</a> <a id="11449" href="/20.07/Compositional/#11449" class="Bound">ddβ²</a> <a id="11453" class="Symbol">=</a> <a id="11455" href="Agda.Builtin.Unit.html#174" class="InductiveConstructor">tt</a> <a id="11460" href="/20.07/Compositional/#11349" class="Function">β±β</a> <a id="11463" class="Symbol">{</a><a id="11464" href="/20.07/Compositional/#11464" class="Bound">Ξ³</a><a id="11465" class="Symbol">}{</a><a id="11467" href="/20.07/Compositional/#11467" class="Bound">v</a> <a id="11469" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="11471" href="/20.07/Compositional/#11471" class="Bound">w</a><a id="11472" class="Symbol">}</a> <a id="11474" href="/20.07/Compositional/#11474" class="Bound">fd</a> <a id="11477" href="/20.07/Compositional/#11477" class="Bound">ddβ²</a> <a id="11481" class="Symbol">=</a> <a id="11483" href="Agda.Builtin.Sigma.html#225" class="Field">projβ</a> <a id="11489" class="Symbol">(</a><a id="11490" href="/20.07/Compositional/#11477" class="Bound">ddβ²</a> <a id="11494" class="Symbol">(</a><a id="11495" href="/20.07/Compositional/#11464" class="Bound">Ξ³</a> <a id="11497" href="/20.07/Denotational/#7445" class="Function Operator">`,</a> <a id="11500" href="/20.07/Compositional/#11467" class="Bound">v</a><a id="11501" class="Symbol">)</a> <a id="11503" href="/20.07/Compositional/#11471" class="Bound">w</a><a id="11504" class="Symbol">)</a> <a id="11506" href="/20.07/Compositional/#11474" class="Bound">fd</a> <a id="11511" href="/20.07/Compositional/#11349" class="Function">β±β</a> <a id="11514" class="Symbol">{</a><a id="11515" href="/20.07/Compositional/#11515" class="Bound">Ξ³</a><a id="11516" class="Symbol">}{</a><a id="11518" href="/20.07/Compositional/#11518" class="Bound">u</a> <a id="11520" href="/20.07/Denotational/#4213" class="InductiveConstructor Operator">β</a> <a id="11522" href="/20.07/Compositional/#11522" class="Bound">w</a><a id="11523" class="Symbol">}</a> <a id="11525" href="/20.07/Compositional/#11525" class="Bound">fd</a> <a id="11528" href="/20.07/Compositional/#11528" class="Bound">ddβ²</a> <a id="11532" class="Symbol">=</a> <a id="11534" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="11536" href="/20.07/Compositional/#11349" class="Function">β±β</a><a id="11538" class="Symbol">{</a><a id="11539" href="/20.07/Compositional/#11515" class="Bound">Ξ³</a><a id="11540" class="Symbol">}{</a><a id="11542" href="/20.07/Compositional/#11518" class="Bound">u</a><a id="11543" class="Symbol">}</a> <a id="11545" class="Symbol">(</a><a id="11546" href="Agda.Builtin.Sigma.html#225" class="Field">projβ</a> <a id="11552" href="/20.07/Compositional/#11525" class="Bound">fd</a><a id="11554" class="Symbol">)</a> <a id="11556" href="/20.07/Compositional/#11528" class="Bound">ddβ²</a> <a id="11560" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11562" href="/20.07/Compositional/#11349" class="Function">β±β</a><a id="11564" class="Symbol">{</a><a id="11565" href="/20.07/Compositional/#11515" class="Bound">Ξ³</a><a id="11566" class="Symbol">}{</a><a id="11568" href="/20.07/Compositional/#11522" class="Bound">w</a><a id="11569" class="Symbol">}</a> <a id="11571" class="Symbol">(</a><a id="11572" href="Agda.Builtin.Sigma.html#237" class="Field">projβ</a> <a id="11578" href="/20.07/Compositional/#11525" class="Bound">fd</a><a id="11580" class="Symbol">)</a> <a id="11582" href="/20.07/Compositional/#11528" class="Bound">ddβ²</a> <a id="11586" 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="11845" href="/20.07/Compositional/#11845" class="Function">lam-cong</a> <a id="11854" class="Symbol">:</a> <a id="11856" class="Symbol">β{</a><a id="11858" href="/20.07/Compositional/#11858" class="Bound">Ξ</a><a id="11859" class="Symbol">}{</a><a id="11861" href="/20.07/Compositional/#11861" class="Bound">N</a> <a id="11863" href="/20.07/Compositional/#11863" class="Bound">Nβ²</a> <a id="11866" class="Symbol">:</a> <a id="11868" href="/20.07/Compositional/#11858" class="Bound">Ξ</a> <a id="11870" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="11872" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a> <a id="11874" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="11876" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="11877" class="Symbol">}</a> <a id="11881" class="Symbol">β</a> <a id="11883" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="11885" href="/20.07/Compositional/#11861" class="Bound">N</a> <a id="11887" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="11889" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="11891" href="/20.07/Compositional/#11863" class="Bound">Nβ²</a> <a id="11898" class="Comment">-----------------</a> <a id="11918" class="Symbol">β</a> <a id="11920" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="11922" class="Symbol">(</a><a id="11923" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="11925" href="/20.07/Compositional/#11861" class="Bound">N</a><a id="11926" class="Symbol">)</a> <a id="11928" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="11930" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="11932" class="Symbol">(</a><a id="11933" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="11935" href="/20.07/Compositional/#11863" class="Bound">Nβ²</a><a id="11937" class="Symbol">)</a> <a id="11939" href="/20.07/Compositional/#11845" class="Function">lam-cong</a> <a id="11948" class="Symbol">{</a><a id="11949" href="/20.07/Compositional/#11949" class="Bound">Ξ</a><a id="11950" class="Symbol">}{</a><a id="11952" href="/20.07/Compositional/#11952" class="Bound">N</a><a id="11953" class="Symbol">}{</a><a id="11955" href="/20.07/Compositional/#11955" class="Bound">Nβ²</a><a id="11957" class="Symbol">}</a> <a id="11959" href="/20.07/Compositional/#11959" class="Bound">NβNβ²</a> <a id="11964" class="Symbol">=</a> <a id="11968" href="/20.07/Denotational/#19160" class="Function Operator">start</a> <a id="11978" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="11980" class="Symbol">(</a><a id="11981" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="11983" href="/20.07/Compositional/#11952" class="Bound">N</a><a id="11984" class="Symbol">)</a> <a id="11988" href="/20.07/Denotational/#19251" class="Function Operator">ββ¨</a> <a id="11991" href="/20.07/Compositional/#4552" class="Function">lam-equiv</a> <a id="12001" href="/20.07/Denotational/#19251" class="Function Operator">β©</a> <a id="12007" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="12009" class="Symbol">(</a><a id="12010" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="12012" href="/20.07/Compositional/#11952" class="Bound">N</a><a id="12013" class="Symbol">)</a> <a id="12017" href="/20.07/Denotational/#19251" class="Function Operator">ββ¨</a> <a id="12020" href="/20.07/Compositional/#11171" class="Function">β±-cong</a> <a id="12027" href="/20.07/Compositional/#11959" class="Bound">NβNβ²</a> <a id="12032" href="/20.07/Denotational/#19251" class="Function Operator">β©</a> <a id="12038" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="12040" class="Symbol">(</a><a id="12041" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="12043" href="/20.07/Compositional/#11955" class="Bound">Nβ²</a><a id="12045" class="Symbol">)</a> <a id="12049" href="/20.07/Denotational/#19251" class="Function Operator">ββ¨</a> <a id="12052" href="/20.07/Denotational/#17940" class="Function">β-sym</a> <a id="12058" href="/20.07/Compositional/#4552" class="Function">lam-equiv</a> <a id="12068" href="/20.07/Denotational/#19251" class="Function Operator">β©</a> <a id="12074" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="12076" class="Symbol">(</a><a id="12077" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="12079" href="/20.07/Compositional/#11955" class="Bound">Nβ²</a><a id="12081" class="Symbol">)</a> <a id="12085" href="/20.07/Denotational/#19498" 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="12338" href="/20.07/Compositional/#12338" class="Function">β-cong</a> <a id="12345" class="Symbol">:</a> <a id="12347" class="Symbol">β{</a><a id="12349" href="/20.07/Compositional/#12349" class="Bound">Ξ</a><a id="12350" class="Symbol">}{</a><a id="12352" href="/20.07/Compositional/#12352" class="Bound">Dβ</a> <a id="12355" href="/20.07/Compositional/#12355" class="Bound">Dββ²</a> <a id="12359" href="/20.07/Compositional/#12359" class="Bound">Dβ</a> <a id="12362" href="/20.07/Compositional/#12362" class="Bound">Dββ²</a> <a id="12366" class="Symbol">:</a> <a id="12368" href="/20.07/Denotational/#17273" class="Function">Denotation</a> <a id="12379" href="/20.07/Compositional/#12349" class="Bound">Ξ</a><a id="12380" class="Symbol">}</a> <a id="12384" class="Symbol">β</a> <a id="12386" href="/20.07/Compositional/#12352" class="Bound">Dβ</a> <a id="12389" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="12391" href="/20.07/Compositional/#12355" class="Bound">Dββ²</a> <a id="12395" class="Symbol">β</a> <a id="12397" href="/20.07/Compositional/#12359" class="Bound">Dβ</a> <a id="12400" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="12402" href="/20.07/Compositional/#12362" class="Bound">Dββ²</a> <a id="12408" class="Symbol">β</a> <a id="12410" class="Symbol">(</a><a id="12411" href="/20.07/Compositional/#12352" class="Bound">Dβ</a> <a id="12414" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="12416" href="/20.07/Compositional/#12359" class="Bound">Dβ</a><a id="12418" class="Symbol">)</a> <a id="12420" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="12422" class="Symbol">(</a><a id="12423" href="/20.07/Compositional/#12355" class="Bound">Dββ²</a> <a id="12427" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="12429" href="/20.07/Compositional/#12362" class="Bound">Dββ²</a><a id="12432" class="Symbol">)</a> <a id="12434" href="/20.07/Compositional/#12338" class="Function">β-cong</a> <a id="12441" class="Symbol">{</a><a id="12442" href="/20.07/Compositional/#12442" class="Bound">Ξ</a><a id="12443" class="Symbol">}</a> <a id="12445" href="/20.07/Compositional/#12445" class="Bound">d1</a> <a id="12448" href="/20.07/Compositional/#12448" class="Bound">d2</a> <a id="12451" href="/20.07/Compositional/#12451" class="Bound">Ξ³</a> <a id="12453" href="/20.07/Compositional/#12453" class="Bound">v</a> <a id="12455" class="Symbol">=</a> <a id="12457" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="12459" class="Symbol">(Ξ»</a> <a id="12462" href="/20.07/Compositional/#12462" class="Bound">x</a> <a id="12464" class="Symbol">β</a> <a id="12466" href="/20.07/Compositional/#12552" class="Function">ββ</a> <a id="12469" href="/20.07/Compositional/#12462" class="Bound">x</a> <a id="12471" href="/20.07/Compositional/#12445" class="Bound">d1</a> <a id="12474" href="/20.07/Compositional/#12448" class="Bound">d2</a><a id="12476" class="Symbol">)</a> <a id="12478" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12505" class="Symbol">(Ξ»</a> <a id="12508" href="/20.07/Compositional/#12508" class="Bound">x</a> <a id="12510" class="Symbol">β</a> <a id="12512" href="/20.07/Compositional/#12552" class="Function">ββ</a> <a id="12515" href="/20.07/Compositional/#12508" class="Bound">x</a> <a id="12517" class="Symbol">(</a><a id="12518" href="/20.07/Denotational/#17940" class="Function">β-sym</a> <a id="12524" href="/20.07/Compositional/#12445" class="Bound">d1</a><a id="12526" class="Symbol">)</a> <a id="12528" class="Symbol">(</a><a id="12529" href="/20.07/Denotational/#17940" class="Function">β-sym</a> <a id="12535" href="/20.07/Compositional/#12448" class="Bound">d2</a><a id="12537" class="Symbol">))</a> <a id="12540" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="12544" class="Keyword">where</a> <a id="12552" href="/20.07/Compositional/#12552" class="Function">ββ</a> <a id="12555" class="Symbol">:</a> <a id="12557" class="Symbol">β{</a><a id="12559" href="/20.07/Compositional/#12559" class="Bound">Ξ³</a> <a id="12561" class="Symbol">:</a> <a id="12563" href="/20.07/Denotational/#7288" class="Function">Env</a> <a id="12567" href="/20.07/Compositional/#12442" class="Bound">Ξ</a><a id="12568" class="Symbol">}{</a><a id="12570" href="/20.07/Compositional/#12570" class="Bound">v</a><a id="12571" class="Symbol">}{</a><a id="12573" href="/20.07/Compositional/#12573" class="Bound">Dβ</a> <a id="12576" href="/20.07/Compositional/#12576" class="Bound">Dββ²</a> <a id="12580" href="/20.07/Compositional/#12580" class="Bound">Dβ</a> <a id="12583" href="/20.07/Compositional/#12583" class="Bound">Dββ²</a> <a id="12587" class="Symbol">:</a> <a id="12589" href="/20.07/Denotational/#17273" class="Function">Denotation</a> <a id="12600" href="/20.07/Compositional/#12442" class="Bound">Ξ</a><a id="12601" class="Symbol">}</a> <a id="12607" class="Symbol">β</a> <a id="12609" class="Symbol">(</a><a id="12610" href="/20.07/Compositional/#12573" class="Bound">Dβ</a> <a id="12613" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="12615" href="/20.07/Compositional/#12580" class="Bound">Dβ</a><a id="12617" class="Symbol">)</a> <a id="12619" href="/20.07/Compositional/#12559" class="Bound">Ξ³</a> <a id="12621" href="/20.07/Compositional/#12570" class="Bound">v</a> <a id="12624" class="Symbol">β</a> <a id="12627" href="/20.07/Compositional/#12573" class="Bound">Dβ</a> <a id="12630" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="12632" href="/20.07/Compositional/#12576" class="Bound">Dββ²</a> <a id="12637" class="Symbol">β</a> <a id="12640" href="/20.07/Compositional/#12580" class="Bound">Dβ</a> <a id="12643" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="12645" href="/20.07/Compositional/#12583" class="Bound">Dββ²</a> <a id="12653" class="Symbol">β</a> <a id="12655" class="Symbol">(</a><a id="12656" href="/20.07/Compositional/#12576" class="Bound">Dββ²</a> <a id="12660" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="12662" href="/20.07/Compositional/#12583" class="Bound">Dββ²</a><a id="12665" class="Symbol">)</a> <a id="12667" href="/20.07/Compositional/#12559" class="Bound">Ξ³</a> <a id="12669" href="/20.07/Compositional/#12570" class="Bound">v</a> <a id="12673" href="/20.07/Compositional/#12552" class="Function">ββ</a> <a id="12676" class="Symbol">(</a><a id="12677" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">injβ</a> <a id="12682" href="/20.07/Compositional/#12682" class="Bound">vββ₯</a><a id="12685" class="Symbol">)</a> <a id="12687" href="/20.07/Compositional/#12687" class="Bound">eqβ</a> <a id="12691" href="/20.07/Compositional/#12691" class="Bound">eqβ</a> <a id="12695" class="Symbol">=</a> <a id="12697" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">injβ</a> <a id="12702" href="/20.07/Compositional/#12682" class="Bound">vββ₯</a> <a id="12708" href="/20.07/Compositional/#12552" class="Function">ββ</a> <a id="12711" class="Symbol">{</a><a id="12712" href="/20.07/Compositional/#12712" class="Bound">Ξ³</a><a id="12713" class="Symbol">}</a> <a id="12715" class="Symbol">{</a><a id="12716" href="/20.07/Compositional/#12716" class="Bound">w</a><a id="12717" class="Symbol">}</a> <a id="12719" class="Symbol">(</a><a id="12720" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">injβ</a> <a id="12725" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="12727" href="/20.07/Compositional/#12727" class="Bound">v</a> <a id="12729" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12731" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="12733" href="/20.07/Compositional/#12733" class="Bound">Dvβ¦w</a> <a id="12738" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12740" href="/20.07/Compositional/#12740" class="Bound">Dv</a> <a id="12743" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="12745" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a><a id="12746" class="Symbol">)</a> <a id="12748" href="/20.07/Compositional/#12748" class="Bound">eqβ</a> <a id="12752" href="/20.07/Compositional/#12752" class="Bound">eqβ</a> <a id="12756" class="Symbol">=</a> <a id="12762" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">injβ</a> <a id="12767" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="12769" href="/20.07/Compositional/#12727" class="Bound">v</a> <a id="12771" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12773" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="12775" href="Agda.Builtin.Sigma.html#225" class="Field">projβ</a> <a id="12781" class="Symbol">(</a><a id="12782" href="/20.07/Compositional/#12748" class="Bound">eqβ</a> <a id="12786" href="/20.07/Compositional/#12712" class="Bound">Ξ³</a> <a id="12788" class="Symbol">(</a><a id="12789" href="/20.07/Compositional/#12727" class="Bound">v</a> <a id="12791" href="/20.07/Denotational/#4183" class="InductiveConstructor Operator">β¦</a> <a id="12793" href="/20.07/Compositional/#12716" class="Bound">w</a><a id="12794" class="Symbol">))</a> <a id="12797" href="/20.07/Compositional/#12733" class="Bound">Dvβ¦w</a> <a id="12802" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12804" href="Agda.Builtin.Sigma.html#225" class="Field">projβ</a> <a id="12810" class="Symbol">(</a><a id="12811" href="/20.07/Compositional/#12752" class="Bound">eqβ</a> <a id="12815" href="/20.07/Compositional/#12712" class="Bound">Ξ³</a> <a id="12817" href="/20.07/Compositional/#12727" class="Bound">v</a><a id="12818" class="Symbol">)</a> <a id="12820" href="/20.07/Compositional/#12740" class="Bound">Dv</a> <a id="12823" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="12825" 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="13072" href="/20.07/Compositional/#13072" class="Function">app-cong</a> <a id="13081" class="Symbol">:</a> <a id="13083" class="Symbol">β{</a><a id="13085" href="/20.07/Compositional/#13085" class="Bound">Ξ</a><a id="13086" class="Symbol">}{</a><a id="13088" href="/20.07/Compositional/#13088" class="Bound">L</a> <a id="13090" href="/20.07/Compositional/#13090" class="Bound">Lβ²</a> <a id="13093" href="/20.07/Compositional/#13093" class="Bound">M</a> <a id="13095" href="/20.07/Compositional/#13095" class="Bound">Mβ²</a> <a id="13098" class="Symbol">:</a> <a id="13100" href="/20.07/Compositional/#13085" class="Bound">Ξ</a> <a id="13102" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="13104" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="13105" class="Symbol">}</a> <a id="13109" class="Symbol">β</a> <a id="13111" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13113" href="/20.07/Compositional/#13088" class="Bound">L</a> <a id="13115" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="13117" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13119" href="/20.07/Compositional/#13090" class="Bound">Lβ²</a> <a id="13124" class="Symbol">β</a> <a id="13126" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13128" href="/20.07/Compositional/#13093" class="Bound">M</a> <a id="13130" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="13132" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13134" href="/20.07/Compositional/#13095" class="Bound">Mβ²</a> <a id="13141" class="Comment">-------------------------</a> <a id="13169" class="Symbol">β</a> <a id="13171" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13173" class="Symbol">(</a><a id="13174" href="/20.07/Compositional/#13088" class="Bound">L</a> <a id="13176" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="13178" href="/20.07/Compositional/#13093" class="Bound">M</a><a id="13179" class="Symbol">)</a> <a id="13181" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="13183" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13185" class="Symbol">(</a><a id="13186" href="/20.07/Compositional/#13090" class="Bound">Lβ²</a> <a id="13189" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="13191" href="/20.07/Compositional/#13095" class="Bound">Mβ²</a><a id="13193" class="Symbol">)</a> <a id="13195" href="/20.07/Compositional/#13072" class="Function">app-cong</a> <a id="13204" class="Symbol">{</a><a id="13205" href="/20.07/Compositional/#13205" class="Bound">Ξ</a><a id="13206" class="Symbol">}{</a><a id="13208" href="/20.07/Compositional/#13208" class="Bound">L</a><a id="13209" class="Symbol">}{</a><a id="13211" href="/20.07/Compositional/#13211" class="Bound">Lβ²</a><a id="13213" class="Symbol">}{</a><a id="13215" href="/20.07/Compositional/#13215" class="Bound">M</a><a id="13216" class="Symbol">}{</a><a id="13218" href="/20.07/Compositional/#13218" class="Bound">Mβ²</a><a id="13220" class="Symbol">}</a> <a id="13222" href="/20.07/Compositional/#13222" class="Bound">Lβ Lβ²</a> <a id="13227" href="/20.07/Compositional/#13227" class="Bound">Mβ Mβ²</a> <a id="13232" class="Symbol">=</a> <a id="13236" href="/20.07/Denotational/#19160" class="Function Operator">start</a> <a id="13246" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13248" class="Symbol">(</a><a id="13249" href="/20.07/Compositional/#13208" class="Bound">L</a> <a id="13251" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="13253" href="/20.07/Compositional/#13215" class="Bound">M</a><a id="13254" class="Symbol">)</a> <a id="13258" href="/20.07/Denotational/#19251" class="Function Operator">ββ¨</a> <a id="13261" href="/20.07/Compositional/#9770" class="Function">app-equiv</a> <a id="13271" href="/20.07/Denotational/#19251" class="Function Operator">β©</a> <a id="13277" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13279" href="/20.07/Compositional/#13208" class="Bound">L</a> <a id="13281" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="13283" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13285" href="/20.07/Compositional/#13215" class="Bound">M</a> <a id="13289" href="/20.07/Denotational/#19251" class="Function Operator">ββ¨</a> <a id="13292" href="/20.07/Compositional/#12338" class="Function">β-cong</a> <a id="13299" href="/20.07/Compositional/#13222" class="Bound">Lβ Lβ²</a> <a id="13304" href="/20.07/Compositional/#13227" class="Bound">Mβ Mβ²</a> <a id="13309" href="/20.07/Denotational/#19251" class="Function Operator">β©</a> <a id="13315" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13317" href="/20.07/Compositional/#13211" class="Bound">Lβ²</a> <a id="13320" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="13322" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13324" href="/20.07/Compositional/#13218" class="Bound">Mβ²</a> <a id="13329" href="/20.07/Denotational/#19251" class="Function Operator">ββ¨</a> <a id="13332" href="/20.07/Denotational/#17940" class="Function">β-sym</a> <a id="13338" href="/20.07/Compositional/#9770" class="Function">app-equiv</a> <a id="13348" href="/20.07/Denotational/#19251" class="Function Operator">β©</a> <a id="13354" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="13356" class="Symbol">(</a><a id="13357" href="/20.07/Compositional/#13211" class="Bound">Lβ²</a> <a id="13360" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="13362" href="/20.07/Compositional/#13218" class="Bound">Mβ²</a><a id="13364" class="Symbol">)</a> <a id="13368" href="/20.07/Denotational/#19498" 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="13890" class="Keyword">data</a> <a id="Ctx"></a><a id="13895" href="/20.07/Compositional/#13895" class="Datatype">Ctx</a> <a id="13899" class="Symbol">:</a> <a id="13901" href="/20.07/Untyped/#3153" class="Datatype">Context</a> <a id="13909" class="Symbol">β</a> <a id="13911" href="/20.07/Untyped/#3153" class="Datatype">Context</a> <a id="13919" class="Symbol">β</a> <a id="13921" class="PrimitiveType">Set</a> <a id="13925" class="Keyword">where</a> <a id="Ctx.ctx-hole"></a><a id="13933" href="/20.07/Compositional/#13933" class="InductiveConstructor">ctx-hole</a> <a id="13942" class="Symbol">:</a> <a id="13944" class="Symbol">β{</a><a id="13946" href="/20.07/Compositional/#13946" class="Bound">Ξ</a><a id="13947" class="Symbol">}</a> <a id="13949" class="Symbol">β</a> <a id="13951" href="/20.07/Compositional/#13895" class="Datatype">Ctx</a> <a id="13955" href="/20.07/Compositional/#13946" class="Bound">Ξ</a> <a id="13957" href="/20.07/Compositional/#13946" class="Bound">Ξ</a> <a id="Ctx.ctx-lam"></a><a id="13961" href="/20.07/Compositional/#13961" class="InductiveConstructor">ctx-lam</a> <a id="13969" class="Symbol">:</a> <a id="13972" class="Symbol">β{</a><a id="13974" href="/20.07/Compositional/#13974" class="Bound">Ξ</a> <a id="13976" href="/20.07/Compositional/#13976" class="Bound">Ξ</a><a id="13977" class="Symbol">}</a> <a id="13979" class="Symbol">β</a> <a id="13981" href="/20.07/Compositional/#13895" class="Datatype">Ctx</a> <a id="13985" class="Symbol">(</a><a id="13986" href="/20.07/Compositional/#13974" class="Bound">Ξ</a> <a id="13988" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="13990" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="13991" class="Symbol">)</a> <a id="13993" class="Symbol">(</a><a id="13994" href="/20.07/Compositional/#13976" class="Bound">Ξ</a> <a id="13996" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="13998" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="13999" class="Symbol">)</a> <a id="14001" class="Symbol">β</a> <a id="14003" href="/20.07/Compositional/#13895" class="Datatype">Ctx</a> <a id="14007" class="Symbol">(</a><a id="14008" href="/20.07/Compositional/#13974" class="Bound">Ξ</a> <a id="14010" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="14012" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="14013" class="Symbol">)</a> <a id="14015" href="/20.07/Compositional/#13976" class="Bound">Ξ</a> <a id="Ctx.ctx-app-L"></a><a id="14019" href="/20.07/Compositional/#14019" class="InductiveConstructor">ctx-app-L</a> <a id="14029" class="Symbol">:</a> <a id="14031" class="Symbol">β{</a><a id="14033" href="/20.07/Compositional/#14033" class="Bound">Ξ</a> <a id="14035" href="/20.07/Compositional/#14035" class="Bound">Ξ</a><a id="14036" class="Symbol">}</a> <a id="14038" class="Symbol">β</a> <a id="14040" href="/20.07/Compositional/#13895" class="Datatype">Ctx</a> <a id="14044" href="/20.07/Compositional/#14033" class="Bound">Ξ</a> <a id="14046" href="/20.07/Compositional/#14035" class="Bound">Ξ</a> <a id="14048" class="Symbol">β</a> <a id="14050" href="/20.07/Compositional/#14035" class="Bound">Ξ</a> <a id="14052" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="14054" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a> <a id="14056" class="Symbol">β</a> <a id="14058" href="/20.07/Compositional/#13895" class="Datatype">Ctx</a> <a id="14062" href="/20.07/Compositional/#14033" class="Bound">Ξ</a> <a id="14064" href="/20.07/Compositional/#14035" class="Bound">Ξ</a> <a id="Ctx.ctx-app-R"></a><a id="14068" href="/20.07/Compositional/#14068" class="InductiveConstructor">ctx-app-R</a> <a id="14078" class="Symbol">:</a> <a id="14080" class="Symbol">β{</a><a id="14082" href="/20.07/Compositional/#14082" class="Bound">Ξ</a> <a id="14084" href="/20.07/Compositional/#14084" class="Bound">Ξ</a><a id="14085" class="Symbol">}</a> <a id="14087" class="Symbol">β</a> <a id="14089" href="/20.07/Compositional/#14084" class="Bound">Ξ</a> <a id="14091" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="14093" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a> <a id="14095" class="Symbol">β</a> <a id="14097" href="/20.07/Compositional/#13895" class="Datatype">Ctx</a> <a id="14101" href="/20.07/Compositional/#14082" class="Bound">Ξ</a> <a id="14103" href="/20.07/Compositional/#14084" class="Bound">Ξ</a> <a id="14105" class="Symbol">β</a> <a id="14107" href="/20.07/Compositional/#13895" class="Datatype">Ctx</a> <a id="14111" href="/20.07/Compositional/#14082" class="Bound">Ξ</a> <a id="14113" href="/20.07/Compositional/#14084" 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="14979" href="/20.07/Compositional/#14979" class="Function">plug</a> <a id="14984" class="Symbol">:</a> <a id="14986" class="Symbol">β{</a><a id="14988" href="/20.07/Compositional/#14988" class="Bound">Ξ</a><a id="14989" class="Symbol">}{</a><a id="14991" href="/20.07/Compositional/#14991" class="Bound">Ξ</a><a id="14992" class="Symbol">}</a> <a id="14994" class="Symbol">β</a> <a id="14996" href="/20.07/Compositional/#13895" class="Datatype">Ctx</a> <a id="15000" href="/20.07/Compositional/#14988" class="Bound">Ξ</a> <a id="15002" href="/20.07/Compositional/#14991" class="Bound">Ξ</a> <a id="15004" class="Symbol">β</a> <a id="15006" href="/20.07/Compositional/#14988" class="Bound">Ξ</a> <a id="15008" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="15010" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a> <a id="15012" class="Symbol">β</a> <a id="15014" href="/20.07/Compositional/#14991" class="Bound">Ξ</a> <a id="15016" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="15018" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a> <a id="15020" href="/20.07/Compositional/#14979" class="Function">plug</a> <a id="15025" href="/20.07/Compositional/#13933" class="InductiveConstructor">ctx-hole</a> <a id="15034" href="/20.07/Compositional/#15034" class="Bound">M</a> <a id="15036" class="Symbol">=</a> <a id="15038" href="/20.07/Compositional/#15034" class="Bound">M</a> <a id="15040" href="/20.07/Compositional/#14979" class="Function">plug</a> <a id="15045" class="Symbol">(</a><a id="15046" href="/20.07/Compositional/#13961" class="InductiveConstructor">ctx-lam</a> <a id="15054" href="/20.07/Compositional/#15054" class="Bound">C</a><a id="15055" class="Symbol">)</a> <a id="15057" href="/20.07/Compositional/#15057" class="Bound">N</a> <a id="15059" class="Symbol">=</a> <a id="15061" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="15063" href="/20.07/Compositional/#14979" class="Function">plug</a> <a id="15068" href="/20.07/Compositional/#15054" class="Bound">C</a> <a id="15070" href="/20.07/Compositional/#15057" class="Bound">N</a> <a id="15072" href="/20.07/Compositional/#14979" class="Function">plug</a> <a id="15077" class="Symbol">(</a><a id="15078" href="/20.07/Compositional/#14019" class="InductiveConstructor">ctx-app-L</a> <a id="15088" href="/20.07/Compositional/#15088" class="Bound">C</a> <a id="15090" href="/20.07/Compositional/#15090" class="Bound">N</a><a id="15091" class="Symbol">)</a> <a id="15093" href="/20.07/Compositional/#15093" class="Bound">L</a> <a id="15095" class="Symbol">=</a> <a id="15097" class="Symbol">(</a><a id="15098" href="/20.07/Compositional/#14979" class="Function">plug</a> <a id="15103" href="/20.07/Compositional/#15088" class="Bound">C</a> <a id="15105" href="/20.07/Compositional/#15093" class="Bound">L</a><a id="15106" class="Symbol">)</a> <a id="15108" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="15110" href="/20.07/Compositional/#15090" class="Bound">N</a> <a id="15112" href="/20.07/Compositional/#14979" class="Function">plug</a> <a id="15117" class="Symbol">(</a><a id="15118" href="/20.07/Compositional/#14068" class="InductiveConstructor">ctx-app-R</a> <a id="15128" href="/20.07/Compositional/#15128" class="Bound">L</a> <a id="15130" href="/20.07/Compositional/#15130" class="Bound">C</a><a id="15131" class="Symbol">)</a> <a id="15133" href="/20.07/Compositional/#15133" class="Bound">M</a> <a id="15135" class="Symbol">=</a> <a id="15137" href="/20.07/Compositional/#15128" class="Bound">L</a> <a id="15139" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="15141" class="Symbol">(</a><a id="15142" href="/20.07/Compositional/#14979" class="Function">plug</a> <a id="15147" href="/20.07/Compositional/#15130" class="Bound">C</a> <a id="15149" href="/20.07/Compositional/#15133" class="Bound">M</a><a id="15150" 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="15388" href="/20.07/Compositional/#15388" class="Function">compositionality</a> <a id="15405" class="Symbol">:</a> <a id="15407" class="Symbol">β{</a><a id="15409" href="/20.07/Compositional/#15409" class="Bound">Ξ</a> <a id="15411" href="/20.07/Compositional/#15411" class="Bound">Ξ</a><a id="15412" class="Symbol">}{</a><a id="15414" href="/20.07/Compositional/#15414" class="Bound">C</a> <a id="15416" class="Symbol">:</a> <a id="15418" href="/20.07/Compositional/#13895" class="Datatype">Ctx</a> <a id="15422" href="/20.07/Compositional/#15409" class="Bound">Ξ</a> <a id="15424" href="/20.07/Compositional/#15411" class="Bound">Ξ</a><a id="15425" class="Symbol">}</a> <a id="15427" class="Symbol">{</a><a id="15428" href="/20.07/Compositional/#15428" class="Bound">M</a> <a id="15430" href="/20.07/Compositional/#15430" class="Bound">N</a> <a id="15432" class="Symbol">:</a> <a id="15434" href="/20.07/Compositional/#15409" class="Bound">Ξ</a> <a id="15436" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="15438" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="15439" class="Symbol">}</a> <a id="15443" class="Symbol">β</a> <a id="15445" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="15447" href="/20.07/Compositional/#15428" class="Bound">M</a> <a id="15449" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="15451" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="15453" href="/20.07/Compositional/#15430" class="Bound">N</a> <a id="15459" class="Comment">---------------------------</a> <a id="15489" class="Symbol">β</a> <a id="15491" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="15493" class="Symbol">(</a><a id="15494" href="/20.07/Compositional/#14979" class="Function">plug</a> <a id="15499" href="/20.07/Compositional/#15414" class="Bound">C</a> <a id="15501" href="/20.07/Compositional/#15428" class="Bound">M</a><a id="15502" class="Symbol">)</a> <a id="15504" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="15506" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="15508" class="Symbol">(</a><a id="15509" href="/20.07/Compositional/#14979" class="Function">plug</a> <a id="15514" href="/20.07/Compositional/#15414" class="Bound">C</a> <a id="15516" href="/20.07/Compositional/#15430" class="Bound">N</a><a id="15517" class="Symbol">)</a> <a id="15519" href="/20.07/Compositional/#15388" class="Function">compositionality</a> <a id="15536" class="Symbol">{</a><a id="15537" class="Argument">C</a> <a id="15539" class="Symbol">=</a> <a id="15541" href="/20.07/Compositional/#13933" class="InductiveConstructor">ctx-hole</a><a id="15549" class="Symbol">}</a> <a id="15551" href="/20.07/Compositional/#15551" class="Bound">MβN</a> <a id="15555" class="Symbol">=</a> <a id="15559" href="/20.07/Compositional/#15551" class="Bound">MβN</a> <a id="15563" href="/20.07/Compositional/#15388" class="Function">compositionality</a> <a id="15580" class="Symbol">{</a><a id="15581" class="Argument">C</a> <a id="15583" class="Symbol">=</a> <a id="15585" href="/20.07/Compositional/#13961" class="InductiveConstructor">ctx-lam</a> <a id="15593" href="/20.07/Compositional/#15593" class="Bound">Cβ²</a><a id="15595" class="Symbol">}</a> <a id="15597" href="/20.07/Compositional/#15597" class="Bound">MβN</a> <a id="15601" class="Symbol">=</a> <a id="15605" href="/20.07/Compositional/#11845" class="Function">lam-cong</a> <a id="15614" class="Symbol">(</a><a id="15615" href="/20.07/Compositional/#15388" class="Function">compositionality</a> <a id="15632" class="Symbol">{</a><a id="15633" class="Argument">C</a> <a id="15635" class="Symbol">=</a> <a id="15637" href="/20.07/Compositional/#15593" class="Bound">Cβ²</a><a id="15639" class="Symbol">}</a> <a id="15641" href="/20.07/Compositional/#15597" class="Bound">MβN</a><a id="15644" class="Symbol">)</a> <a id="15646" href="/20.07/Compositional/#15388" class="Function">compositionality</a> <a id="15663" class="Symbol">{</a><a id="15664" class="Argument">C</a> <a id="15666" class="Symbol">=</a> <a id="15668" href="/20.07/Compositional/#14019" class="InductiveConstructor">ctx-app-L</a> <a id="15678" href="/20.07/Compositional/#15678" class="Bound">Cβ²</a> <a id="15681" href="/20.07/Compositional/#15681" class="Bound">L</a><a id="15682" class="Symbol">}</a> <a id="15684" href="/20.07/Compositional/#15684" class="Bound">MβN</a> <a id="15688" class="Symbol">=</a> <a id="15692" href="/20.07/Compositional/#13072" class="Function">app-cong</a> <a id="15701" class="Symbol">(</a><a id="15702" href="/20.07/Compositional/#15388" class="Function">compositionality</a> <a id="15719" class="Symbol">{</a><a id="15720" class="Argument">C</a> <a id="15722" class="Symbol">=</a> <a id="15724" href="/20.07/Compositional/#15678" class="Bound">Cβ²</a><a id="15726" class="Symbol">}</a> <a id="15728" href="/20.07/Compositional/#15684" class="Bound">MβN</a><a id="15731" class="Symbol">)</a> <a id="15733" class="Symbol">Ξ»</a> <a id="15735" href="/20.07/Compositional/#15735" class="Bound">Ξ³</a> <a id="15737" href="/20.07/Compositional/#15737" class="Bound">v</a> <a id="15739" class="Symbol">β</a> <a id="15741" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="15743" class="Symbol">(Ξ»</a> <a id="15746" href="/20.07/Compositional/#15746" class="Bound">x</a> <a id="15748" class="Symbol">β</a> <a id="15750" href="/20.07/Compositional/#15746" class="Bound">x</a><a id="15751" class="Symbol">)</a> <a id="15753" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15755" class="Symbol">(Ξ»</a> <a id="15758" href="/20.07/Compositional/#15758" class="Bound">x</a> <a id="15760" class="Symbol">β</a> <a id="15762" href="/20.07/Compositional/#15758" class="Bound">x</a><a id="15763" class="Symbol">)</a> <a id="15765" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a> <a id="15767" href="/20.07/Compositional/#15388" class="Function">compositionality</a> <a id="15784" class="Symbol">{</a><a id="15785" class="Argument">C</a> <a id="15787" class="Symbol">=</a> <a id="15789" href="/20.07/Compositional/#14068" class="InductiveConstructor">ctx-app-R</a> <a id="15799" href="/20.07/Compositional/#15799" class="Bound">L</a> <a id="15801" href="/20.07/Compositional/#15801" class="Bound">Cβ²</a><a id="15803" class="Symbol">}</a> <a id="15805" href="/20.07/Compositional/#15805" class="Bound">MβN</a> <a id="15809" class="Symbol">=</a> <a id="15813" href="/20.07/Compositional/#13072" class="Function">app-cong</a> <a id="15822" class="Symbol">(Ξ»</a> <a id="15825" href="/20.07/Compositional/#15825" class="Bound">Ξ³</a> <a id="15827" href="/20.07/Compositional/#15827" class="Bound">v</a> <a id="15829" class="Symbol">β</a> <a id="15831" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β¨</a> <a id="15833" class="Symbol">(Ξ»</a> <a id="15836" href="/20.07/Compositional/#15836" class="Bound">x</a> <a id="15838" class="Symbol">β</a> <a id="15840" href="/20.07/Compositional/#15836" class="Bound">x</a><a id="15841" class="Symbol">)</a> <a id="15843" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15845" class="Symbol">(Ξ»</a> <a id="15848" href="/20.07/Compositional/#15848" class="Bound">x</a> <a id="15850" class="Symbol">β</a> <a id="15852" href="/20.07/Compositional/#15848" class="Bound">x</a><a id="15853" class="Symbol">)</a> <a id="15855" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">β©</a><a id="15856" class="Symbol">)</a> <a id="15858" class="Symbol">(</a><a id="15859" href="/20.07/Compositional/#15388" class="Function">compositionality</a> <a id="15876" class="Symbol">{</a><a id="15877" class="Argument">C</a> <a id="15879" class="Symbol">=</a> <a id="15881" href="/20.07/Compositional/#15801" class="Bound">Cβ²</a><a id="15883" class="Symbol">}</a> <a id="15885" href="/20.07/Compositional/#15805" class="Bound">MβN</a><a id="15888" 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="16477" href="/20.07/Compositional/#16477" class="Function Operator">β¦_β§</a> <a id="16481" class="Symbol">:</a> <a id="16483" class="Symbol">β{</a><a id="16485" href="/20.07/Compositional/#16485" class="Bound">Ξ</a><a id="16486" class="Symbol">}</a> <a id="16488" class="Symbol">β</a> <a id="16490" class="Symbol">(</a><a id="16491" href="/20.07/Compositional/#16491" class="Bound">M</a> <a id="16493" class="Symbol">:</a> <a id="16495" href="/20.07/Compositional/#16485" class="Bound">Ξ</a> <a id="16497" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="16499" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="16500" class="Symbol">)</a> <a id="16502" class="Symbol">β</a> <a id="16504" href="/20.07/Denotational/#17273" class="Function">Denotation</a> <a id="16515" href="/20.07/Compositional/#16485" class="Bound">Ξ</a> <a id="16517" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="16519" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="16521" href="/20.07/Compositional/#16521" class="Bound">x</a> <a id="16523" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="16525" href="/20.07/Compositional/#16525" class="Bound">Ξ³</a> <a id="16527" href="/20.07/Compositional/#16527" class="Bound">v</a> <a id="16529" class="Symbol">=</a> <a id="16531" href="/20.07/Compositional/#16527" class="Bound">v</a> <a id="16533" href="/20.07/Denotational/#4508" class="Datatype Operator">β</a> <a id="16535" href="/20.07/Compositional/#16525" class="Bound">Ξ³</a> <a id="16537" href="/20.07/Compositional/#16521" class="Bound">x</a> <a id="16539" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="16541" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="16543" href="/20.07/Compositional/#16543" class="Bound">N</a> <a id="16545" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="16547" class="Symbol">=</a> <a id="16549" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="16551" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="16553" href="/20.07/Compositional/#16543" class="Bound">N</a> <a id="16555" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="16557" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="16559" href="/20.07/Compositional/#16559" class="Bound">L</a> <a id="16561" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="16563" href="/20.07/Compositional/#16563" class="Bound">M</a> <a id="16565" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="16567" class="Symbol">=</a> <a id="16569" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="16571" href="/20.07/Compositional/#16559" class="Bound">L</a> <a id="16573" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="16575" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="16577" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="16579" href="/20.07/Compositional/#16563" class="Bound">M</a> <a id="16581" href="/20.07/Compositional/#16477" 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="16802" href="/20.07/Compositional/#16802" class="Function">β°ββ¦β§</a> <a id="16807" class="Symbol">:</a> <a id="16809" class="Symbol">β</a> <a id="16811" class="Symbol">{</a><a id="16812" href="/20.07/Compositional/#16812" class="Bound">Ξ</a><a id="16813" class="Symbol">}</a> <a id="16815" class="Symbol">{</a><a id="16816" href="/20.07/Compositional/#16816" class="Bound">M</a> <a id="16818" class="Symbol">:</a> <a id="16820" href="/20.07/Compositional/#16812" class="Bound">Ξ</a> <a id="16822" href="/20.07/Untyped/#4294" class="Datatype Operator">β’</a> <a id="16824" href="/20.07/Untyped/#2888" class="InductiveConstructor">β </a><a id="16825" class="Symbol">}</a> <a id="16827" class="Symbol">β</a> <a id="16829" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="16831" href="/20.07/Compositional/#16816" class="Bound">M</a> <a id="16833" href="/20.07/Denotational/#17668" class="Function Operator">β</a> <a id="16835" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="16837" href="/20.07/Compositional/#16816" class="Bound">M</a> <a id="16839" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="16841" href="/20.07/Compositional/#16802" class="Function">β°ββ¦β§</a> <a id="16846" class="Symbol">{</a><a id="16847" href="/20.07/Compositional/#16847" class="Bound">Ξ</a><a id="16848" class="Symbol">}</a> <a id="16850" class="Symbol">{</a><a id="16851" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="16853" href="/20.07/Compositional/#16853" class="Bound">x</a><a id="16854" class="Symbol">}</a> <a id="16856" class="Symbol">=</a> <a id="16858" href="/20.07/Compositional/#10341" class="Function">var-equiv</a> <a id="16868" href="/20.07/Compositional/#16802" class="Function">β°ββ¦β§</a> <a id="16873" class="Symbol">{</a><a id="16874" href="/20.07/Compositional/#16874" class="Bound">Ξ</a><a id="16875" class="Symbol">}</a> <a id="16877" class="Symbol">{</a><a id="16878" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="16880" href="/20.07/Compositional/#16880" class="Bound">N</a><a id="16881" class="Symbol">}</a> <a id="16883" class="Symbol">=</a> <a id="16887" class="Keyword">let</a> <a id="16891" href="/20.07/Compositional/#16891" class="Bound">ih</a> <a id="16894" class="Symbol">=</a> <a id="16896" href="/20.07/Compositional/#16802" class="Function">β°ββ¦β§</a> <a id="16901" class="Symbol">{</a><a id="16902" class="Argument">M</a> <a id="16904" class="Symbol">=</a> <a id="16906" href="/20.07/Compositional/#16880" class="Bound">N</a><a id="16907" class="Symbol">}</a> <a id="16909" class="Keyword">in</a> <a id="16916" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="16918" class="Symbol">(</a><a id="16919" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="16921" href="/20.07/Compositional/#16880" class="Bound">N</a><a id="16922" class="Symbol">)</a> <a id="16926" href="/20.07/Denotational/#19251" class="Function Operator">ββ¨</a> <a id="16929" href="/20.07/Compositional/#4552" class="Function">lam-equiv</a> <a id="16939" href="/20.07/Denotational/#19251" class="Function Operator">β©</a> <a id="16945" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="16947" class="Symbol">(</a><a id="16948" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="16950" href="/20.07/Compositional/#16880" class="Bound">N</a><a id="16951" class="Symbol">)</a> <a id="16955" href="/20.07/Denotational/#19251" class="Function Operator">ββ¨</a> <a id="16958" href="/20.07/Compositional/#11171" class="Function">β±-cong</a> <a id="16965" class="Symbol">(</a><a id="16966" href="/20.07/Compositional/#16802" class="Function">β°ββ¦β§</a> <a id="16971" class="Symbol">{</a><a id="16972" class="Argument">M</a> <a id="16974" class="Symbol">=</a> <a id="16976" href="/20.07/Compositional/#16880" class="Bound">N</a><a id="16977" class="Symbol">})</a> <a id="16980" href="/20.07/Denotational/#19251" class="Function Operator">β©</a> <a id="16986" href="/20.07/Compositional/#1898" class="Function">β±</a> <a id="16988" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="16990" href="/20.07/Compositional/#16880" class="Bound">N</a> <a id="16992" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="16996" href="/20.07/Denotational/#19391" class="Function Operator">ββ¨β©</a> <a id="17004" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="17006" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">Ζ</a> <a id="17008" href="/20.07/Compositional/#16880" class="Bound">N</a> <a id="17010" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="17014" href="/20.07/Denotational/#19498" class="Function Operator">β</a> <a id="17016" href="/20.07/Compositional/#16802" class="Function">β°ββ¦β§</a> <a id="17021" class="Symbol">{</a><a id="17022" href="/20.07/Compositional/#17022" class="Bound">Ξ</a><a id="17023" class="Symbol">}</a> <a id="17025" class="Symbol">{</a><a id="17026" href="/20.07/Compositional/#17026" class="Bound">L</a> <a id="17028" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="17030" href="/20.07/Compositional/#17030" class="Bound">M</a><a id="17031" class="Symbol">}</a> <a id="17033" class="Symbol">=</a> <a id="17038" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="17040" class="Symbol">(</a><a id="17041" href="/20.07/Compositional/#17026" class="Bound">L</a> <a id="17043" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="17045" href="/20.07/Compositional/#17030" class="Bound">M</a><a id="17046" class="Symbol">)</a> <a id="17050" href="/20.07/Denotational/#19251" class="Function Operator">ββ¨</a> <a id="17053" href="/20.07/Compositional/#9770" class="Function">app-equiv</a> <a id="17063" href="/20.07/Denotational/#19251" class="Function Operator">β©</a> <a id="17068" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="17070" href="/20.07/Compositional/#17026" class="Bound">L</a> <a id="17072" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="17074" href="/20.07/Denotational/#17486" class="Function">β°</a> <a id="17076" href="/20.07/Compositional/#17030" class="Bound">M</a> <a id="17080" href="/20.07/Denotational/#19251" class="Function Operator">ββ¨</a> <a id="17083" href="/20.07/Compositional/#12338" class="Function">β-cong</a> <a id="17090" class="Symbol">(</a><a id="17091" href="/20.07/Compositional/#16802" class="Function">β°ββ¦β§</a> <a id="17096" class="Symbol">{</a><a id="17097" class="Argument">M</a> <a id="17099" class="Symbol">=</a> <a id="17101" href="/20.07/Compositional/#17026" class="Bound">L</a><a id="17102" class="Symbol">})</a> <a id="17105" class="Symbol">(</a><a id="17106" href="/20.07/Compositional/#16802" class="Function">β°ββ¦β§</a> <a id="17111" class="Symbol">{</a><a id="17112" class="Argument">M</a> <a id="17114" class="Symbol">=</a> <a id="17116" href="/20.07/Compositional/#17030" class="Bound">M</a><a id="17117" class="Symbol">})</a> <a id="17120" href="/20.07/Denotational/#19251" class="Function Operator">β©</a> <a id="17125" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="17127" href="/20.07/Compositional/#17026" class="Bound">L</a> <a id="17129" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="17131" href="/20.07/Compositional/#5745" class="Function Operator">β</a> <a id="17133" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="17135" href="/20.07/Compositional/#17030" class="Bound">M</a> <a id="17137" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="17141" href="/20.07/Denotational/#19391" class="Function Operator">ββ¨β©</a> <a id="17149" href="/20.07/Compositional/#16477" class="Function Operator">β¦</a> <a id="17151" href="/20.07/Compositional/#17026" class="Bound">L</a> <a id="17153" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">Β·</a> <a id="17155" href="/20.07/Compositional/#17030" class="Bound">M</a> <a id="17157" href="/20.07/Compositional/#16477" class="Function Operator">β§</a> <a id="17161" href="/20.07/Denotational/#19498" 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="/20.07/Denotational/">Prev</a> • <a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part3/Compositional.lagda.md">Source</a> • <a alt="Next chapter" href="/20.07/Soundness/">Next</a> </p> </article> </div> </main><footer class="site-footer h-card"> <data class="u-url" href="/20.07/"></data> <div class="wrapper"> <h2 class="footer-heading">Programming Language Foundations in Agda </h2><div class="footer-col-wrapper"> <div class="footer-col footer-col-1"> <ul class="contact-list"> <li class="p-name">Philip Wadler</li> <li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li> </ul> </div> <div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul> </div> <div class="footer-col footer-col-3"></div> </div><div class="footer-col-wrapper"> <div class="footer-col footer-col-1"> <ul class="contact-list"> <li class="p-name">Wen Kokke</li> <li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li> </ul> </div> <div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul> </div> <div class="footer-col footer-col-3"></div> </div><div class="footer-col-wrapper"> <div class="footer-col footer-col-1"> <ul class="contact-list"> <li class="p-name">Jeremy G. Siek</li> <li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li> </ul> </div> <div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul> </div> <div class="footer-col footer-col-3"></div> </div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a> </div> </footer> <!-- Import jQuery --> <script type="text/javascript" src="/20.07/assets/jquery.js"></script> <script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script> <script type="text/javascript"> anchors.add(); </script> <script type="text/javascript"> // Makes sandwhich menu works $('.menu-icon').click(function(){ $('.trigger').toggle(); }); // Script which allows for foldable code blocks $('div.foldable pre').each(function(){ var autoHeight = $(this).height(); var lineHeight = parseFloat($(this).css('line-height')); var plus = $("<div></div>"); var horLine = $("<div></div>"); var verLine = $("<div></div>"); $(this).prepend(plus); plus.css({ 'position' : 'relative', 'float' : 'right', 'right' : '-' + (0.5 * lineHeight - 1.5) + 'px', 'width' : lineHeight, 'height' : lineHeight}); verLine.css({ 'position' : 'relative', 'height' : lineHeight, 'width' : '3px', 'background-color' : '#C1E0FF'}); horLine.css({ 'position' : 'relative', 'top' : '-' + (0.5 * lineHeight + 1.5) + 'px', 'left' : '-' + (0.5 * lineHeight - 1.5) + 'px', 'height' : '3px', 'width' : lineHeight, 'background-color' : '#C1E0FF'}); plus.append(verLine); plus.append(horLine); $(this).height(2.0 * lineHeight); $(this).css('overflow','hidden'); $(this).click(function(){ if ($(this).height() == autoHeight) { $(this).height(2.0 * lineHeight); plus.show(); } else { $(this).height('auto'); plus.hide(); } }); }); </script> <!-- Import KaTeX --> <script type="text/javascript" src="/20.07/assets/katex.js"></script> <!-- Script which renders TeX using KaTeX --> <script type="text/javascript"> $("script[type='math/tex']").replaceWith( function(){ var tex = $(this).text(); return "<span class=\"inline-equation\">" + katex.renderToString(tex) + "</span>"; }); $("script[type='math/tex; mode=display']").replaceWith( function(){ var tex = $(this).text().replace(/%.*?(\n|$)/g,""); return "<div class=\"equation\">" + katex.renderToString("\\displaystyle "+tex) + "</div>"; }); </script> </body> </html>