735 lines
163 KiB
HTML
735 lines
163 KiB
HTML
<!DOCTYPE html>
|
||
<html lang="en"><head>
|
||
<meta charset="utf-8">
|
||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1">
|
||
<title>Compositional: The denotational semantics is compositional 🚧 | Programming Language Foundations in Agda
|
||
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
|
||
<meta name="generator" content="Jekyll v3.9.0" />
|
||
<meta property="og:title" content="Compositional: The denotational semantics is compositional 🚧" />
|
||
<meta property="og:locale" content="en_US" />
|
||
<meta name="description" content="Programming Language Foundations in Agda" />
|
||
<meta property="og:description" content="Programming Language Foundations in Agda" />
|
||
<link rel="canonical" href="https://plfa.github.io/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>
|