Beta Conversion and Substitution in Functional Programming

Lecture 4; TIL Foundations Beta conversion Substitution method 1

The rule of -conversion Fundamental computational rule of -calculi and functional programming languages It specifies how to apply of a functionf to the argument A to obtain the value of f at A. Example. [ x [0+ x 01] 03] we want the value of the successor function at the number 3; -reduction (sometimes also -reduction) by name : [ x [0+ x 01] 03] [0+ 0301] -expansion (or -expansion): [0+ 0301] [ x [0+ x 01] 03] In general: [[ x1 xm Y] D1 Dm] Y(Di/xi) where Y(Di/xi) arises from Y by a collision-less substitution of Difor all the free occurrences of the variable xiin Y (1 i m) (= 04) 2

-conversion: [ x C(x) A] | C(A/x) Procedure of applying the function produced by x C(x) to an argument produced by A. The fundamental computational rule of -calculi and functional programming languages The fundamental inference rule of HOL (higher-order logics) by name ; all the free occurrences of the variable x in C are replaced by the procedure A Problems: not operationally equivalent, less efficient, loss of info by value ; the value presented by A is substituted for all the free occurrences of the variable x in C 3

-conversion: [ x C(x) A] | C(A/x) In programming languages the difference between by value and by name revolves around the programmer s choice of evaluation strategy. Algol 60: call-by-value and call-by-name Java: manipulates objects by name , however, procedures are called by-value Clean and Haskell: call-by-name Similar work has been done since the early 1970s; for instance, Plotkin (1975) proved that the two strategies are not operationally equivalent. Chang & Felleisen (2012) call-by-need reduction by value. But their work is couched in an untyped -calculus. 4

[ x C(x) A] | C(A/x) Conversion by name three problems. conversion of this kind is not guaranteed to be an equivalent transformation as soon as partial functions are involved. even in those cases when -reduction is an equivalent transformation, it can yield a loss of analytic information on which function has been applied to which argument In practice less efficient than by value 1. 2. 3. 5

Problems with -reduction by name 1) non-equivalence [ x [ y [0+ x y]] [0Cotg0 ]] is an improper construction; it does not construct anything, because there is no value of the cotangent function at the argument but its -reduced Composition [ y [0+ [0Cotg0 ] y]] constructs a degenerate function The improper construction [0Cotg0 ] has been drawn into the intensional ( -generic) context of the Closure [ y [0+ x y]]. We should avoid such a collision of contexts 6

-conversion by name: 2) loss of analytic information [ x [x + 1] 3] [3 + 1] [ y [3 + y] 1] which function has been applied to which argument? Two backward paths of -expansion; Does it matter? 7

Problems with -reduction 2) Loss of analytic information John loves his wife, and so does Peter exemplary husbands (sloppy reading) But the sentence is ambiguous between two readings because two different properties are involved here; loving one s own wife vs. loving John s wife Lown(John): w t [ x [0Lovewtx [0Wife_ofwtx]] 0John] LJohn(John): w t [ x [0Lovewtx [0Wife_ofwt Both -reduce to LJohn(John): w t [0Lovewt so does Peter Peter loves John s wife trouble on the horizon 0John]] 0John] 0John [0Wife_ofwt 0John]] 8

-conversion by name: loss of info w t [ x [0Lovewtx [0Wife_ofwt w t [ x [0Lovewtx [0Wife_ofwtx]] 0John] (1) (2) 0John]] 0John] w t [0Lovewt (3) 0John [0Wife_ofwt 0John]] It is uncontroversial that the contractum (3) can be equivalently expanded back both to (1) and (2). The problem is, of course, that there is no way to reconstruct which of (1), (2) would be the correct redex 9

Does it matter? HOL tools are broadly used in automatic theorem checking and applied as interactive proof assistants. The underlying logic is usually a version of simply typed -calculus of total functions. However, there is another application natural language processing hyperintensional logic is needed so that the underlying inference machine is neither over- inferring (that yields inconsistencies) nor under-inferring (that causes lack of knowledge). agents attitudes like knowing, believing, seeking, solving, designing, etc.; attitudinal sentences are part and parcel of our everyday vernacular. 10

-reduction by value [ x C(x) A] | C(A/x) The rule is underspecified: How to execute C(A/x)? a) by name : procedure A is substituted for the occurrences of the variable x problems b) by value : execute A first, and only if it does not fail, substitute the produced value for x substitution method bingo, no problems !!! 11

Substitution by value [ x F(x) A] = 2[0Sub [0Tr A] 0x 0F(x)] 1. A: execute A in order to obtain the value a; ifA is v-improper, then the whole Composition is v-improper (stop); else: 2. [0Tr A]: obtain Trivialization of ( pointer at ) the argument a produced byA 3. [0Sub [0Tr A]0x 0F]: substitute this pointer at a for x into the body F 4. 2[0Sub [0Tr A] 0x 0F]: execute the result 12

Substitution by value Theoretical computer science is typically careful to draw a distinction between Eval and Apply. Eval is understood to be the step of converting a quoted string into a callable procedure and its arguments (Step 3) whereas Apply is the actual call of the procedure with a given set of arguments (step 4). The distinction is particularly noticeable in functional languages and languages based on the -calculus, such as Lisp and Scheme. 13

Substitution by value Sub/( n n n n) operates on constructions in this way: [0Sub C1 C2 C3] what for-what into-what Let C1v-construct D1,C2v-construct a variable x,C3v- construct D3; then Sub v-constructs the construction D, that is the result of correct (collision-less) substituting D1 for all the occurrence of x in D3 Tr/( n ) v-constructs the Trivialization of an -object [0Tr x] v-constructs the Trivialization of the object v-constructed by the variable x; x is free 0x constructs x regardless of a valuation, the variable x is bound by Trivialization, o-bound 14

Substitution by value Example [0Sub [0Tr 0 ] 0x 0[0Sin x]] constructs the Composition [0Sin 0 ] 2[0Sub [0Tr 0 ] 0x 0[0Sin x]] constructs the value of the function Sine at , i.e. the number 0 [0Sub [0Tr y] 0x 0[0Sin x]] v( /y)-constructs the Composition [0Sin 0 ] 15

Substitution by value Let = be the identity of -objects. Then, we can write: [0Sub [0Tr 0 ] 0x 0[0Sin x]] =*1 0[0Sin 0 ] 2[0Sub [0Tr 0 ] 0x 0[0Sin x]] = 00 [0Sub [0Tr y] 0x 0[0Sin x]] (=*1 0[0Sin 0 ] for v( /y)) v( /y)-constructs the Composition [0Sin 0 ] 16

Substitution method; Application of a function to an argument ( -reduction by value) Existential quantification into hyper- intensional contexts Hyperintensional attitudes de re Anaphoric preprocessing Topic/focus articulation; presuppositions; active vs. passive voice 17

Substitution method; broadly applied de re attitudes Tilman believes of the Pope that he is wise w t [0Believewt 0Tilman2[0Of [0Tr 0Popewt]0he 0[ w* t* [0Wisew*t* he]]] Of = Sub operates on the (hyper)intensional context of that he is wise ; it substitutes the individual (if any) that holds the papal office for the variable he 18

Substitution method; broadly applied Quantifying into Tom is seeking the last decimal of There is a number such that Tom is seeking its last decimal Seek*/( 1) ; Seek cannot be the relation of an individual to a number; there is no such number here; and even if there were one, it d make no sense to seek a number without any operation 19

Substitution method; broadly applied w t [0 x [0Seek*wt is incorrect; why? the variable x is o-bound in the hyperintensional context of 0[0Last_Dec x]; hence, valuation of x is irrelevant and x does not bind x 0Tom 0[0Last_Dec x]]] w t [0Seek*wt w t [0 x [0Seek*wt [0Sub [0Tr x]0y 0[0Last_Dec y]]]] 0Tom 0[0Last_Dec0 ]] 0Tom the variable x is free in [0Tr x] 20

Paradox of omniscience resolved John knows that 1+1=2 1+1=2 Sin( ) = 0 John knows that Sin( ) = 0 The paradox of logical/mathematical omniscience ??? Types: John/ ; Know/( n) ; 0,1,2, / ; Sin/( ); = /( ); =o/( ). w t [0Knowwt [0= [0+ 01 01] 02] =o[0= [0Sin 0 ] 00] Substitution of [0= [0Sin 0 ] 00] for [0= [0+ 01 01] 02] is blocked. Though both constructions produce the same truth-value T, John is not related to the truth-value. Rather, he is related to the very construction hyperintensional context. Only procedurally isomorphic construction could be substituted. 0John 0[0= [0+ 01 01] 02]] 21

Hyperintensionality was born out of a negative need, to block invalid inferences Carnap (1947, 13ff); there are contexts that are neither extensional nor intensional (e.g. attitudes) Cresswell; any context in which substitution of necessarilly equivalent terms fails is hyperintensional Yet, which inferences are valid in hyperintensional contexts? How hyper are hyperintensions? procedural isomorphism Which contexts are hyperintensional? TIL definition is positive: a context is hyperintensional if the very meaning procedure is an object of predication; TIL is a hyperintensional, partial typed -calculus 22 22

How hyper are hyperintensions procedural isomorphism Maybe that it is philosophically wise to adopt several notions of procedural isomorphism. It is not improbable that several degrees of hyperintensional individuation are called for, depending on which sort of discourse happens to be analysed. What appears to be synonymous in an ordinary vernacular might not be synonymous in a professional language like the language of logic, mathematics, computer science or physics. 23

Procedural isomorphism Church s Alternatives Ordinary vernacular no -bound variables (A1 ): -conversion + -conversion by value + restricted -conversion by name; [ x [0+ x 00] y] [0+ y 00] + pairs of simple synonyms Programming language variables matter (A0 ): -conversion (?) + pairs of simple synonyms Du , M. (2019): If structured propositions are logical procedures then how are procedures individuated? Synthese special issue on the Unity of propositions, vol. 196, No. 4, pp. 1249-1283. DOI: 10.1007/s11229-017- 1595-5 24