Deploying to web from @ 0561a70 🚀

Adequacy/index.html

@@ -23,7 +23,7 @@
             <a id="plfa_plfa-part3-Adequacy-3707" href="../Denotational/#plfa_plfa-part3-Denotational-9271" class="InductiveConstructor">var</a><a id="plfa_plfa-part3-Adequacy-3710" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3712" href="../Denotational/#plfa_plfa-part3-Denotational-9346" class="InductiveConstructor">↦-elim</a><a id="plfa_plfa-part3-Adequacy-3718" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3720" href="../Denotational/#plfa_plfa-part3-Denotational-9468" class="InductiveConstructor">↦-intro</a><a id="plfa_plfa-part3-Adequacy-3727" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3729" href="../Denotational/#plfa_plfa-part3-Denotational-9647" class="InductiveConstructor">⊔-intro</a><a id="plfa_plfa-part3-Adequacy-3736" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3738" href="../Denotational/#plfa_plfa-part3-Denotational-9580" class="InductiveConstructor">⊥-intro</a><a id="plfa_plfa-part3-Adequacy-3745" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3747" href="../Denotational/#plfa_plfa-part3-Denotational-9762" class="InductiveConstructor">sub</a><a id="plfa_plfa-part3-Adequacy-3750" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3752" href="../Denotational/#plfa_plfa-part3-Denotational-17409" class="Function">ℰ</a><a id="plfa_plfa-part3-Adequacy-3753" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3755" href="../Denotational/#plfa_plfa-part3-Denotational-17595" class="Function Operator">_≃_</a><a id="plfa_plfa-part3-Adequacy-3758" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3760" href="../Denotational/#plfa_plfa-part3-Denotational-16922" class="Function Operator">_iff_</a><a id="plfa_plfa-part3-Adequacy-3765" class="Symbol">;</a>
             <a id="plfa_plfa-part3-Adequacy-3779" href="../Denotational/#plfa_plfa-part3-Denotational-4625" class="InductiveConstructor">⊑-trans</a><a id="plfa_plfa-part3-Adequacy-3786" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3788" href="../Denotational/#plfa_plfa-part3-Denotational-4479" class="InductiveConstructor">⊑-conj-R1</a><a id="plfa_plfa-part3-Adequacy-3797" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3799" href="../Denotational/#plfa_plfa-part3-Denotational-4552" class="InductiveConstructor">⊑-conj-R2</a><a id="plfa_plfa-part3-Adequacy-3808" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3810" href="../Denotational/#plfa_plfa-part3-Denotational-4395" class="InductiveConstructor">⊑-conj-L</a><a id="plfa_plfa-part3-Adequacy-3818" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3820" href="../Denotational/#plfa_plfa-part3-Denotational-5469" class="Function">⊑-refl</a><a id="plfa_plfa-part3-Adequacy-3826" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3828" href="../Denotational/#plfa_plfa-part3-Denotational-4696" class="InductiveConstructor">⊑-fun</a><a id="plfa_plfa-part3-Adequacy-3833" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3835" href="../Denotational/#plfa_plfa-part3-Denotational-4370" class="InductiveConstructor">⊑-bot</a><a id="plfa_plfa-part3-Adequacy-3840" class="Symbol">;</a>
             <a id="plfa_plfa-part3-Adequacy-3854" href="../Denotational/#plfa_plfa-part3-Denotational-4799" class="InductiveConstructor">⊑-dist</a><a id="plfa_plfa-part3-Adequacy-3860" class="Symbol">;</a> <a id="plfa_plfa-part3-Adequacy-3862" href="../Denotational/#plfa_plfa-part3-Denotational-42552" class="Function">sub-inv-fun</a><a id="plfa_plfa-part3-Adequacy-3873" class="Symbol">)</a>
-<a id="plfa_plfa-part3-Adequacy-3875" class="Keyword">open</a> <a id="plfa_plfa-part3-Adequacy-3880" class="Keyword">import</a> <a id="plfa_plfa-part3-Adequacy-3887" href="../Soundness/#" class="Module">plfa.part3.Soundness</a> <a id="plfa_plfa-part3-Adequacy-3908" class="Keyword">using</a> <a id="plfa_plfa-part3-Adequacy-3914" class="Symbol">(</a><a id="plfa_plfa-part3-Adequacy-3915" href="../Soundness/#plfa_plfa-part3-Soundness-23457" class="Function">soundness</a><a id="plfa_plfa-part3-Adequacy-3924" class="Symbol">)</a>
+<a id="plfa_plfa-part3-Adequacy-3875" class="Keyword">open</a> <a id="plfa_plfa-part3-Adequacy-3880" class="Keyword">import</a> <a id="plfa_plfa-part3-Adequacy-3887" href="../Soundness/#" class="Module">plfa.part3.Soundness</a> <a id="plfa_plfa-part3-Adequacy-3908" class="Keyword">using</a> <a id="plfa_plfa-part3-Adequacy-3914" class="Symbol">(</a><a id="plfa_plfa-part3-Adequacy-3915" href="../Soundness/#plfa_plfa-part3-Soundness-23460" class="Function">soundness</a><a id="plfa_plfa-part3-Adequacy-3924" class="Symbol">)</a>
 
 </pre><h2 id="the-property-of-being-greater-or-equal-to-a-function">The property of being greater or equal to a function</h2><p>We define the following short-hand for saying that a value is greater-than or equal to a function value.</p><pre class="Agda"><a id="plfa_plfa-part3-Adequacy-above-fun"></a><a id="plfa_plfa-part3-Adequacy-4104" href="../Adequacy/#plfa_plfa-part3-Adequacy-4104" class="Function">above-fun</a> <a id="plfa_plfa-part3-Adequacy-4114" class="Symbol">:</a> <a id="plfa_plfa-part3-Adequacy-4116" href="../Denotational/#plfa_plfa-part3-Denotational-3974" class="Datatype">Value</a> <a id="plfa_plfa-part3-Adequacy-4122" class="Symbol">→</a> <a id="plfa_plfa-part3-Adequacy-4124" href="https://agda.github.io/agda-stdlib/v1.7.2/Agda.Primitive.html#320" class="Primitive">Set</a>
 <a id="plfa_plfa-part3-Adequacy-4128" href="../Adequacy/#plfa_plfa-part3-Adequacy-4104" class="Function">above-fun</a> <a id="plfa_plfa-part3-Adequacy-4138" href="../Adequacy/#plfa_plfa-part3-Adequacy-4138" class="Bound">u</a> <a id="plfa_plfa-part3-Adequacy-4140" class="Symbol">=</a> <a id="plfa_plfa-part3-Adequacy-4142" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">Σ[</a> <a id="plfa_plfa-part3-Adequacy-4145" href="../Adequacy/#plfa_plfa-part3-Adequacy-4145" class="Bound">v</a> <a id="plfa_plfa-part3-Adequacy-4147" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">∈</a> <a id="plfa_plfa-part3-Adequacy-4149" href="../Denotational/#plfa_plfa-part3-Denotational-3974" class="Datatype">Value</a> <a id="plfa_plfa-part3-Adequacy-4155" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">]</a> <a id="plfa_plfa-part3-Adequacy-4157" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">Σ[</a> <a id="plfa_plfa-part3-Adequacy-4160" href="../Adequacy/#plfa_plfa-part3-Adequacy-4160" class="Bound">w</a> <a id="plfa_plfa-part3-Adequacy-4162" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">∈</a> <a id="plfa_plfa-part3-Adequacy-4164" href="../Denotational/#plfa_plfa-part3-Denotational-3974" class="Datatype">Value</a> <a id="plfa_plfa-part3-Adequacy-4170" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">]</a> <a id="plfa_plfa-part3-Adequacy-4172" href="../Adequacy/#plfa_plfa-part3-Adequacy-4145" class="Bound">v</a> <a id="plfa_plfa-part3-Adequacy-4174" href="../Denotational/#plfa_plfa-part3-Denotational-4006" class="InductiveConstructor Operator">↦</a> <a id="plfa_plfa-part3-Adequacy-4176" href="../Adequacy/#plfa_plfa-part3-Adequacy-4160" class="Bound">w</a> <a id="plfa_plfa-part3-Adequacy-4178" href="../Denotational/#plfa_plfa-part3-Denotational-4335" class="Datatype Operator">⊑</a> <a id="plfa_plfa-part3-Adequacy-4180" href="../Adequacy/#plfa_plfa-part3-Adequacy-4138" class="Bound">u</a>
@@ -252,7 +252,7 @@
            <a id="plfa_plfa-part3-Adequacy-22473" class="Symbol">→</a> <a id="plfa_plfa-part3-Adequacy-22475" href="../Adequacy/#plfa_plfa-part3-Adequacy-22435" class="Bound">M</a> <a id="plfa_plfa-part3-Adequacy-22477" href="../Untyped/#plfa_plfa-part2-Untyped-10990" class="Datatype Operator">—↠</a> <a id="plfa_plfa-part3-Adequacy-22480" class="InductiveConstructor Operator">ƛ</a> <a id="plfa_plfa-part3-Adequacy-22482" href="../Adequacy/#plfa_plfa-part3-Adequacy-22447" class="Bound">N</a>
            <a id="plfa_plfa-part3-Adequacy-22495" class="Symbol">→</a> <a id="plfa_plfa-part3-Adequacy-22497" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">Σ[</a> <a id="plfa_plfa-part3-Adequacy-22500" href="../Adequacy/#plfa_plfa-part3-Adequacy-22500" class="Bound">Δ</a> <a id="plfa_plfa-part3-Adequacy-22502" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">∈</a> <a id="plfa_plfa-part3-Adequacy-22504" href="../Untyped/#plfa_plfa-part2-Untyped-2782" class="Datatype">Context</a> <a id="plfa_plfa-part3-Adequacy-22512" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">]</a> <a id="plfa_plfa-part3-Adequacy-22514" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">Σ[</a> <a id="plfa_plfa-part3-Adequacy-22517" href="../Adequacy/#plfa_plfa-part3-Adequacy-22517" class="Bound">N′</a> <a id="plfa_plfa-part3-Adequacy-22520" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">∈</a> <a id="plfa_plfa-part3-Adequacy-22522" href="../Adequacy/#plfa_plfa-part3-Adequacy-22500" class="Bound">Δ</a> <a id="plfa_plfa-part3-Adequacy-22524" href="../Untyped/#plfa_plfa-part2-Untyped-2820" class="InductiveConstructor Operator">,</a> <a id="plfa_plfa-part3-Adequacy-22526" href="../Untyped/#plfa_plfa-part2-Untyped-2509" class="InductiveConstructor">★</a> <a id="plfa_plfa-part3-Adequacy-22528" href="../Untyped/#plfa_plfa-part2-Untyped-3935" class="Datatype Operator">⊢</a> <a id="plfa_plfa-part3-Adequacy-22530" href="../Untyped/#plfa_plfa-part2-Untyped-2509" class="InductiveConstructor">★</a> <a id="plfa_plfa-part3-Adequacy-22532" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">]</a> <a id="plfa_plfa-part3-Adequacy-22534" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">Σ[</a> <a id="plfa_plfa-part3-Adequacy-22537" href="../Adequacy/#plfa_plfa-part3-Adequacy-22537" class="Bound">δ</a> <a id="plfa_plfa-part3-Adequacy-22539" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">∈</a> <a id="plfa_plfa-part3-Adequacy-22541" href="../BigStep/#plfa_plfa-part2-BigStep-2381" class="Function">ClosEnv</a> <a id="plfa_plfa-part3-Adequacy-22549" href="../Adequacy/#plfa_plfa-part3-Adequacy-22500" class="Bound">Δ</a> <a id="plfa_plfa-part3-Adequacy-22551" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">]</a>
              <a id="plfa_plfa-part3-Adequacy-22566" href="../BigStep/#plfa_plfa-part2-BigStep-2598" class="Function">∅&#39;</a> <a id="plfa_plfa-part3-Adequacy-22569" href="../BigStep/#plfa_plfa-part2-BigStep-2973" class="Datatype Operator">⊢</a> <a id="plfa_plfa-part3-Adequacy-22571" href="../Adequacy/#plfa_plfa-part3-Adequacy-22435" class="Bound">M</a> <a id="plfa_plfa-part3-Adequacy-22573" href="../BigStep/#plfa_plfa-part2-BigStep-2973" class="Datatype Operator">⇓</a> <a id="plfa_plfa-part3-Adequacy-22575" href="../BigStep/#plfa_plfa-part2-BigStep-2430" class="InductiveConstructor">clos</a> <a id="plfa_plfa-part3-Adequacy-22580" class="Symbol">(</a><a id="plfa_plfa-part3-Adequacy-22581" class="InductiveConstructor Operator">ƛ</a> <a id="plfa_plfa-part3-Adequacy-22583" href="../Adequacy/#plfa_plfa-part3-Adequacy-22517" class="Bound">N′</a><a id="plfa_plfa-part3-Adequacy-22585" class="Symbol">)</a> <a id="plfa_plfa-part3-Adequacy-22587" href="../Adequacy/#plfa_plfa-part3-Adequacy-22537" class="Bound">δ</a>
-<a id="plfa_plfa-part3-Adequacy-22589" href="../Adequacy/#plfa_plfa-part3-Adequacy-22419" class="Function">reduce→cbn</a> <a id="plfa_plfa-part3-Adequacy-22600" href="../Adequacy/#plfa_plfa-part3-Adequacy-22600" class="Bound">M—↠ƛN</a> <a id="plfa_plfa-part3-Adequacy-22606" class="Symbol">=</a> <a id="plfa_plfa-part3-Adequacy-22608" href="../Adequacy/#plfa_plfa-part3-Adequacy-21033" class="Function">↓→⇓</a> <a id="plfa_plfa-part3-Adequacy-22612" class="Symbol">(</a><a id="plfa_plfa-part3-Adequacy-22613" href="../Soundness/#plfa_plfa-part3-Soundness-23457" class="Function">soundness</a> <a id="plfa_plfa-part3-Adequacy-22623" href="../Adequacy/#plfa_plfa-part3-Adequacy-22600" class="Bound">M—↠ƛN</a><a id="plfa_plfa-part3-Adequacy-22628" class="Symbol">)</a>
+<a id="plfa_plfa-part3-Adequacy-22589" href="../Adequacy/#plfa_plfa-part3-Adequacy-22419" class="Function">reduce→cbn</a> <a id="plfa_plfa-part3-Adequacy-22600" href="../Adequacy/#plfa_plfa-part3-Adequacy-22600" class="Bound">M—↠ƛN</a> <a id="plfa_plfa-part3-Adequacy-22606" class="Symbol">=</a> <a id="plfa_plfa-part3-Adequacy-22608" href="../Adequacy/#plfa_plfa-part3-Adequacy-21033" class="Function">↓→⇓</a> <a id="plfa_plfa-part3-Adequacy-22612" class="Symbol">(</a><a id="plfa_plfa-part3-Adequacy-22613" href="../Soundness/#plfa_plfa-part3-Soundness-23460" class="Function">soundness</a> <a id="plfa_plfa-part3-Adequacy-22623" href="../Adequacy/#plfa_plfa-part3-Adequacy-22600" class="Bound">M—↠ƛN</a><a id="plfa_plfa-part3-Adequacy-22628" class="Symbol">)</a>
 </pre><p>Suppose <code>M —↠ ƛ N</code>. Soundness of the denotational semantics gives us <code>ℰ M ≃ ℰ (ƛ N)</code>. Then by <code>↓→⇓</code> we conclude that <code>∅&#39; ⊢ M ⇓ clos (ƛ N′) δ</code> for some <code>N′</code> and <code>δ</code>.</p><p>Putting the two directions of the if-and-only-if together, we establish that call-by-name evaluation is equivalent to beta reduction in the following sense.</p><pre class="Agda"><a id="plfa_plfa-part3-Adequacy-cbn↔reduce"></a><a id="plfa_plfa-part3-Adequacy-22963" href="../Adequacy/#plfa_plfa-part3-Adequacy-22963" class="Function">cbn↔reduce</a> <a id="plfa_plfa-part3-Adequacy-22974" class="Symbol">:</a> <a id="plfa_plfa-part3-Adequacy-22976" class="Symbol">∀</a> <a id="plfa_plfa-part3-Adequacy-22978" class="Symbol">{</a><a id="plfa_plfa-part3-Adequacy-22979" href="../Adequacy/#plfa_plfa-part3-Adequacy-22979" class="Bound">M</a> <a id="plfa_plfa-part3-Adequacy-22981" class="Symbol">:</a> <a id="plfa_plfa-part3-Adequacy-22983" href="../Untyped/#plfa_plfa-part2-Untyped-2804" class="InductiveConstructor">∅</a> <a id="plfa_plfa-part3-Adequacy-22985" href="../Untyped/#plfa_plfa-part2-Untyped-3935" class="Datatype Operator">⊢</a> <a id="plfa_plfa-part3-Adequacy-22987" href="../Untyped/#plfa_plfa-part2-Untyped-2509" class="InductiveConstructor">★</a><a id="plfa_plfa-part3-Adequacy-22988" class="Symbol">}</a>
            <a id="plfa_plfa-part3-Adequacy-23001" class="Symbol">→</a> <a id="plfa_plfa-part3-Adequacy-23003" class="Symbol">(</a><a id="plfa_plfa-part3-Adequacy-23004" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">Σ[</a> <a id="plfa_plfa-part3-Adequacy-23007" href="../Adequacy/#plfa_plfa-part3-Adequacy-23007" class="Bound">N</a> <a id="plfa_plfa-part3-Adequacy-23009" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">∈</a> <a id="plfa_plfa-part3-Adequacy-23011" href="../Untyped/#plfa_plfa-part2-Untyped-2804" class="InductiveConstructor">∅</a> <a id="plfa_plfa-part3-Adequacy-23013" href="../Untyped/#plfa_plfa-part2-Untyped-2820" class="InductiveConstructor Operator">,</a> <a id="plfa_plfa-part3-Adequacy-23015" href="../Untyped/#plfa_plfa-part2-Untyped-2509" class="InductiveConstructor">★</a> <a id="plfa_plfa-part3-Adequacy-23017" href="../Untyped/#plfa_plfa-part2-Untyped-3935" class="Datatype Operator">⊢</a> <a id="plfa_plfa-part3-Adequacy-23019" href="../Untyped/#plfa_plfa-part2-Untyped-2509" class="InductiveConstructor">★</a> <a id="plfa_plfa-part3-Adequacy-23021" href="https://agda.github.io/agda-stdlib/v1.7.2/Data.Product.html#925" class="Function">]</a> <a id="plfa_plfa-part3-Adequacy-23023" class="Symbol">(</a><a id="plfa_plfa-part3-Adequacy-23024" href="../Adequacy/#plfa_plfa-part3-Adequacy-22979" class="Bound">M</a> <a id="plfa_plfa-part3-Adequacy-23026" href="../Untyped/#plfa_plfa-part2-Untyped-10990" class="Datatype Operator">—↠</a> <a id="plfa_plfa-part3-Adequacy-23029" class="InductiveConstructor Operator">ƛ</a> <a id="plfa_plfa-part3-Adequacy-23031" href="../Adequacy/#plfa_plfa-part3-Adequacy-23007" class="Bound">N</a><a id="plfa_plfa-part3-Adequacy-23032" class="Symbol">))</a>
              <a id="plfa_plfa-part3-Adequacy-23048" href="../Denotational/#plfa_plfa-part3-Denotational-16922" class="Function Operator">iff</a>