I'm working through Bacon's Philosophical Introduction to Higher Order Logic. I am looking for help on the following problem:
Exercise 3.17 Calculate the following, assuming that $\wedge : t \to t \to t, F : e \to t \in \Sigma.:$
Rather than translating into combinatory logic without variables, these exercises include arbitrary variables. Basically, I'm meant to be calculating terms of $CL^v(\{S,K,I\},\Sigma)$
(The only things needed to solve this problem are $S, K, I$, constants, and the arbitary variables).
so, the first problem is
- $[x].Sxy$ where $x : t \to t \to t, y : t \to t$, and $S: (t\to t \to t) \to (t \to t) \to t \to t$
If I understand the combinators correctly,
$ \begin{align*} [x].Sxy &= S([x].x)([x].y) \\ &= \boxed{S(I)(Ky)} \end{align*} $
Is this right? I'm honestly pretty confused. And it gets worse :(
- $[x].Fx$, where $F : e \to t$ is a constant and $x : e$
In this case since F is a constant, which makes me confused, are you supposed to do:
$ \begin{align*} [x].Fx &= S([x].F)([x].x) \\ &= \boxed{S(KF)(I)} \end{align*} $ ??
This seems right to me, since $[x]PQ = S([x].P)([x].Q)$, but, am I right in assuming that for a constant $F$, $[x].F = KF$?? I feel like it has to be since $F : e \to t \in \Sigma$.
- $[x].(Fx \wedge Gx)$
At this point I'm losing my marbles... (also, for this problem I will format my solution with prefix notation after setting up the problem).
$ \begin{align*} [x].(Fx \wedge Gx) &= S([x].\wedge Fx)([x].Gx) \\ &= S(S([x].\wedge)([x].Fx))(S([x].G)([x].x)) \\ &= S(S([x].\wedge)(S([x].F)([x].x)))(S([x].G)([x].x)) \\ &= \boxed{S(S(\wedge)(S(KF)(I)))(S(KG)(I))} \end{align*} $
My solution to that one is really dependent on my understanding what is happening in (2). Unfortunately, I do not know from where to start (4) without first understanding that I've done 1-3 correctly, but I'll include it here:
- $[x].SK$, choosing appropriate type subscripts.
Any advice or hints would be massively appreciated, thank you.
These answers look good to me. In the final line of Q3 it looks like you missed a $K$ (you should have $K\wedge$ where you have $\wedge$).
For 4 I won't do the type superscripts. We have $[x].SK$ then $S([x].S)([x].K)$, and then $S(KS)(KK)$.