Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>Some textbooks define <strong>I</strong> as mere alias for <strong>((S K) K)</strong>. In this case they are identical (as terms) <em>per definitionem</em>. To prove their equality (as functions), we need only to prove that equality is reflexive, which can be achieved by a reflexivity axiom scheme:</p> <ul> <li>Proposition ``<em>E</em> = <em>E</em>'' is deducible (<strong>Reflexivity</strong> axiom scheme, instantiated for each possible terms denoted here by metavariable <em>E</em>)</li> </ul> <p>Thus, I suppose in the followings, that Your questions investigates another approach: when combinator <strong>I</strong> is not defined as a <strong>mere alias</strong> for compound term <strong>((S K) K)</strong>, but introduced as a <strong>standalone basic combinator</strong> constant on its own, whose operational semantics is declared <strong>explicitly by axiom</strong> scheme</p> <ul> <li>``(<strong>I</strong> <em>E</em>) = <em>E</em>'' is deducible (<strong>I-axiom</strong> scheme)</li> </ul> <p>I suppose Your question asks</p> <blockquote> <p>whether we can deduce formally (remaining inside the system), that such a standalone-defined <strong>I</strong> behaves exactly as <strong>((S K) K)</strong>, when used as functions in reductions?</p> </blockquote> <p>I think we can, but we must resort to stronger tools. I conjecture that the usual axiom schemes are not enough, we have to declare also the extensionality property (equality of functions), that's the main point. If we want to formalize extensionality as an axiom, we have to augment our object language with <strong>free variables</strong>.</p> <p>I think, we have to adopt such an approach for building combinatory logic, that we have to allow also the use of variables in the object langauge. Oof course, I mean "just" <strong>free</strong> valuables. Using bound variables would be cheating, we have to remain inside the realm of combinatory logic. Using free varaibles is not cheating, it's a honest tool. Thus, we can do the formal proof You required.</p> <p>Besides the straightforward equality axioms and rules of inference (transitivity, reflexivity, symmetry, Leibniz rules), we must add an <strong>extensionality</strong> rule of inference for equality. Here is the point where free variables matter.</p> <p>In Csörnyei 2007: 157-158, I have found the following approach. I think this way the proof can be done.</p> <p>Some remarks:</p> <p>Most of the axioms are in fact <em>axiom schemes</em>, consisting of infinitely many axiom instances. The instances must be instantiated for for every possible <em>E</em>, <em>F</em>, <em>G</em> terms. Here, I use italics for metavariables.</p> <p>The superficial infinite nature of axiom schemes won't raise computability problems, because they can be tackled in a finite time: our axiom system is <strong>recursive</strong>. It means that a clever parser can decide in a finite time (moreover, very effectively), whether a given proposition is an instance of an axiom scheme, or not. Thus, the usage of axiom schemes does not raise neither theoretical nor practical problems.</p> <p>Now let us seem our framework:</p> <h2>Language</h2> <p><strong><em>ALPHABET</em></strong></p> <p><strong>Constants</strong>: The following three are called constants: <strong>K</strong>, <strong>S</strong>, <strong>I</strong>.</p> <p>I added the constant <strong>I</strong> only because Your question presupposes that we have not defined the combinator <strong>I</strong> as an mere <strong>alias/macro</strong> for compound term <strong>S</strong> <strong>K</strong> <strong>K</strong>, but it is a standalone constant on its own.</p> <p>I shall denote constants by boldface roman capitals.</p> <p><strong>Sign of application</strong>: A sign @ of ``application'' is enough (prefix notation with arity 2). As syntactic sugar, I use here parantheses instead of the explicit application sign: I shall use the explicit both opening ( and closing ) signs.</p> <p><strong>Variables</strong>: Although combinator logic does not make use of bound variables, scope etc, but we can introduce free variables. I suspect, they are not only syntactic sugar, they can strengthen the deduction system, too. I conjecture, that Your question will require their usage. Any enumerable infinite set (disjoint of the constants and parenthesis signs) will serve as the alphabet of variables, I will denote them here with unformatted roman lowercase letters x, y, z... </p> <p><strong><em>TERMS</em></strong></p> <p>Terms are defined inductively:</p> <ul> <li>Any constant is a term</li> <li>Any variable is a term</li> <li>If <em>E</em> is a term, and <em>F</em> is a term too, then also (<em>E</em> <em>F</em>) is a term</li> </ul> <p>I sometimes use practical conventions as syntactic sugar, e.g. write</p> <blockquote> <p><em>E</em> <em>F</em> <em>G</em> <em>H</em></p> </blockquote> <p>instead of</p> <blockquote> <p>(((<em>E</em> <em>F</em>) <em>G</em>) <em>H</em>).</p> </blockquote> <h2>Deduction</h2> <p><strong>Conversion axiom schemes:</strong></p> <ul> <li>``<strong>K</strong> <em>E</em> <em>F</em> = <em>E</em>'' is deducible (<strong>K-axiom</strong> scheme)</li> <li>``<strong>S</strong> <em>F</em> <em>G</em> <em>H</em> = <em>F</em> <em>H</em> (<em>G</em> <em>H</em>)'' is deducible (<strong>S-axiom</strong> scheme)</li> <li>``<strong>I</strong> <em>E</em> = <em>E</em>'' is deducible (<strong>I-axiom</strong> scheme)</li> </ul> <p>I added the third conversion axiom (<strong>I</strong> rule) only because Your question presupposes that we have not <strong>defined</strong> the combinator <strong>I</strong> as an alias/macro for <strong>S</strong> <strong>K</strong> <strong>K</strong>.</p> <p><strong>Equality axiom schemes and rules of inference</strong></p> <ul> <li>``<em>E</em> = <em>E</em>'' is deducible (<strong>Reflexivity</strong> axiom)</li> <li>If "<em>E</em> = <em>F</em>" is deducible, then "<em>F</em> = <em>E</em>" is also deducible (<strong>Symmetry</strong> rule of inference)</li> <li>If "<em>E</em> = <em>F</em>" is deducible, and "<em>F</em> = <em>G</em>" is deducible too, then also "<em>E</em> = <em>G</em>" is reducible (<strong>Transitivity</strong> rule)</li> <li>If "<em>E</em> = <em>F</em>" is deducible, then "<em>E</em> <em>G</em> = <em>F</em> <em>G</em>" is also deducible (<strong>Leibniz rule I</strong>)</li> <li>If "<em>E</em> = <em>F</em>" is deducible, then "<em>G</em> <em>E</em> = <em>G</em> <em>F</em>" is also deducible (<strong>Leibniz rule II</strong>)</li> </ul> <h2>Question</h2> <p>Now let us investigate Your question. I conjecture that the deduction system defined so far is not strong enough to prove Your question.</p> <blockquote> <p>Is proposition "<strong>I</strong> = <strong>S</strong> <strong>K</strong> <strong>K</strong>" deducible?</p> </blockquote> <p>The problem is, that we have to prove the equivalence of functions. We regard two functions equivalent if they behave the same way. Functions act so that they are applied to arguments. We should prove that both functions act the same way if applied to each possible arguments. Again, the problem with infinity! I suspect, axioms schemes can't help us here. Something like</p> <blockquote> <p>If <em>E</em> <em>F</em> = <em>G</em> <em>F</em> is deducible, then also <em>E</em> = <em>G</em> is deducible</p> </blockquote> <p>would fail to do the job: we can see that this does not yield what we want. Using it, we can prove that</p> <blockquote> <p>``<strong>I</strong> <em>E</em> = <strong>S</strong> <strong>K</strong> <strong>K</strong> <em>E</em>'' is deducible</p> </blockquote> <p>for each <em>E</em> term instance, but these results are only separated instances of, and cannot be used as a whole for further deductions. We have only concrete results (infinitely many), not being able to summarize them:</p> <ul> <li>it holds for <em>E</em> := <strong>K</strong></li> <li>holds for <em>E</em> := <strong>S</strong></li> <li>it holds for <em>E</em> := <strong>K</strong> <strong>K</strong></li> <li>.</li> <li>.</li> <li>.</li> </ul> <p>...</p> <p>we cannot summarize these fragmented result instances into a single great result, stating extensionality! We cannot pour these low-value fragment into the funnel a rule of inference that would melt them together into a single more valuable result.</p> <p>We have to augment the power of our deduction system. We have to find a formal tool that can grasps the problem. Your questions leads to extensionality, and I think, declaring extensionality needs that we can pose propositions that hold for *****arbitrary***** instances. That's why I think we must allow free variables inside our object language. I conjecture that the following additional rule of inference will do the work:</p> <ul> <li>If variable x is not part of terms neither <em>E</em> nor <em>F</em>, and statement (<em>E</em> x) = (<em>F</em> x) is deducible, then <em>E</em> = <em>F</em> is also deducible (<strong>Extensionality</strong> rule of inference)</li> </ul> <p>The hard thing in this axiom, easily leading to confusion: x is an <strong>object</strong> variables, fully emancipated and respected parts of our object language, while <em>E</em> and <em>G</em> are <strong>meta</strong>variables, not parts of the object language, but used only for a concise notation of axiom schemes.</p> <p>(Remark: More precisely, the extensionality rule of inference should be formalized in a more careful way, introducing a <strong>meta</strong>variable <em>x</em> over all possible <strong>object</strong> variables x, y, z..., and also another kind of <strong>meta</strong>variable <em>E</em> over all possible <strong>term instances</strong>. But this distinction among the two kinds of metavariables plus the object variables is not so didactic here, it does not affect Your question too much.)</p> <h2>Proof</h2> <p>Let us prove now the proposition that ``<strong>I</strong> = <strong>S</strong> <strong>K</strong> <strong>K</strong>''.</p> <p>Steps for left-hand side:</p> <ul> <li>proposition ``<strong>I</strong> x = x'' is an instance of <strong>I-axiom</strong> scheme with instatiation [<em>E</em> := x]</li> </ul> <p>Steps for right-hand side:</p> <ul> <li>Proposition "<strong>S</strong> <strong>K</strong> <strong>K</strong> x = <strong>K</strong> x (<strong>K</strong> x)" is an instance of <strong>S-axiom</strong> scheme with instantiations [<em>E</em> := <strong>K</strong>, <em>F</em> := <strong>K</strong>, <em>G</em> := x], thus it is deducible</li> <li>Proposition "<strong>K</strong> x (<strong>K</strong> x) = x" is an instance of <strong>K-axiom</strong> scheme with instantiations [<em>E</em> := x, <em>F</em> := <strong>K</strong> x], thus it is deducible</li> </ul> <p>Transitivity of equality:</p> <ul> <li>Statement "<strong>S</strong> <strong>K</strong> <strong>K</strong> x = <strong>K</strong> x (<strong>K</strong> x)" matches the first premise of <strong>transitivity</strong> rule of inference, and statement "<strong>K</strong> x (<strong>K</strong> x) = x" matches the second premise of this rule of inference. The instantiations are [<em>E</em> := <strong>S</strong> <strong>K</strong> <strong>K</strong> x, <em>F</em> := <strong>K</strong> x (<strong>K</strong> x), <em>G</em> = x]. Thus the conclusion holds too: <em>E</em> = <em>G</em>. Rewriting the conclusion with the same instantiations, we get statement "<strong>S</strong> <strong>K</strong> <strong>K</strong> x = x", thus, this is deducible.</li> </ul> <p>Symmetry of equality:</p> <ul> <li>Using "<strong>S</strong> <strong>K</strong> <strong>K</strong> x = x", we can infer "x = <strong>S</strong> <strong>K</strong> <strong>K</strong> x"</li> </ul> <p>Transitivity of equality:</p> <ul> <li>Using "<strong>I</strong> x = x" and "x = <strong>S</strong> <strong>K</strong> <strong>K</strong> x", we can infer "<strong>I</strong> x = <strong>S</strong> <strong>K</strong> <strong>K</strong> x"</li> </ul> <p>Now we have paved the way for the crucial point:</p> <ul> <li>Proposition "<strong>I</strong> x = <strong>S</strong> <strong>K</strong> <strong>K</strong> x" matches with the first premise of <strong>Extension</strong> rule of inference: (<em>E</em> x) = (<em>F</em> x), with instantiations [<em>E</em> := <strong>I</strong>, <em>F</em> := <strong>S</strong> <strong>K</strong> <strong>K</strong>]. Thus the conclusion must also hold, that is, "<em>E</em> = <em>F</em>" with the same instantiations ([<em>E</em> := <strong>I</strong>, <em>F</em> := <strong>S</strong> <strong>K</strong> <strong>K</strong>]), yielding proposition "<strong>I</strong> = <strong>S</strong> <strong>K</strong> <strong>K</strong>", quod erat demonstrandum.</li> </ul> <hr> <p>Csörnyei, Zoltán (2007): <em>Lambda-kalkulus. A funkcionális programozás alapjai.</em> Budapest: Typotex. ISBN-978-963-9664-46-3.</p>
    singulars
    1. This table or related slice is empty.
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. VO
      singulars
      1. This table or related slice is empty.
    2. VO
      singulars
      1. This table or related slice is empty.
    3. VO
      singulars
      1. This table or related slice is empty.
    1. This table or related slice is empty.
 

Querying!

 
Guidance

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload