I've been reading up on Church's simple type theory and much of the concepts make sense to me. However, I can't actually figure out how to define functions explicitly using the notation provided.

Notationally, let's say that $\ast$ is the type of boolean truth values, and that $T$ and $F$ are the two constants of that type.

Suppose that I want to define some basic logic gates in STT. The NOT gate is going to be of type $(\ast \to \ast)$, and we can define as $\lambda x:\ast. (x=F)$.

For XNOR, we can curry to obtain a gate of type $(\ast \to (\ast \to \ast))$, which we can define as $\lambda x:\ast. \lambda y:\ast. (x=y)$.

For XOR, we can instead go with $\lambda x:\ast. \lambda y:\ast. ((x=y)=F)$.

But how do we handle something like AND, OR, etc?

In general, is there any way to specify a boolean function by specifying its truth table, or something like that?

EDIT: to be clear, I'm not looking at their embedding of propositional logic into STT further down the page, where they have alternate definitions of $\mathsf{T}$ and $\mathsf{F}$ that differ from the primitive constants $\small{T}$ and $\small{F}$. I'm just trying to figure out how to define functions, period, and I'm using the type $\ast$ for the sake of constructing simple examples.

In short, I want to figure out how to explicitly define a function of type $(\ast \to (\ast \to \ast))$, or $(\ast \to (\ast \to (\ast \to \ast)))$, and so on. How do I do that?

  • $\begingroup$ I have never seen $=$ listed as a primitive in type theory. Whether 2 lambda expressions can be determined to be equivalent isn't trivial, although it is at least easier for typable lambda expressions IIRC. Usually $\top$ is defined as $\lambda xy.x$ and $\bot$ is defined as $\lambda xy.y$ (thus the $* \to * \to *$ notation), but this author is doing things weirdly. $\endgroup$ – DanielV Oct 23 '17 at 17:24
  • 1
    $\begingroup$ I thought that it was much easier to determine equivalence of two lambda expressions in the typed vs the untyped lambda calculus. As far as the typed lambda calculus goes, Henkin, at least, has explicit T and F constants in this paper. The Church booleans you list, as far as I am aware, are typically used in untyped lambda calculus -- even the alternate embedding of $\mathsf{T}$ and $\mathsf{F}$ described in the answer below are not the same as those definitions. $\endgroup$ – Mike Battaglia Oct 23 '17 at 17:26
  • $\begingroup$ Are you aware that this "William M. Farmer" is not using the term "Type Theory" (or Simple Type Theory) in the way that everyone else uses it? What he is really talking about is an attempt to add types to lambda logic. Modern "type theory" is a method of encoding proofs of FOL in lambda calculus, "simple type theory" refers to the method of encoding proofs of positive propositional logic into lambda calculus. Not at all what this guy is talking about. $\endgroup$ – DanielV Oct 23 '17 at 17:47
  • $\begingroup$ It seems the same as the article here: en.m.wikipedia.org/wiki/Simply_typed_lambda_calculus $\endgroup$ – Mike Battaglia Oct 23 '17 at 17:51
  • $\begingroup$ No, what is referred to on the wikipedia page is actually the method of encoding positive propositional proofs into typed lambda calculus. You notice the page never says something like "and this is the lambda expression representing true...". That is because propositions there are the types, not the lambda expression being typed. And don't get me wrong, I think what Farmer is presenting is interesting, maybe even better. It just is something totally different than simply typed lambda calculus which is based on the curry howard isomorphism. $\endgroup$ – DanielV Oct 23 '17 at 17:59

The paper gives a definition of AND and OR when it describes the embedding of propositional logic into STT. In particular, AND was defined as: $$A_*\land B_* \equiv (\lambda f:* \to * \to *.f(\mathsf{T})(\mathsf{T}))=(\lambda f:*\to*\to *.f(A_*)(B_*))$$

Given $\neg$ and $\land$, we can define the other classical propositional connectives as usual which is what they proceed to do.

You can understand this definition as $$A_*\land B_*\equiv \langle\mathsf{T},\mathsf{T}\rangle = \langle A_*, B_* \rangle$$ where $\langle A_*, B_* \rangle$ represents the pair of $A_*$ and $B_*$. Of course, the calculus presented doesn't have pairs, so a Church-encoded representation is used instead. You could then, if you like, directly encode OR as the Church-encoded form of $A_*\lor B_* \equiv\langle\mathsf{F},\mathsf{F}\rangle\neq\langle A_*,B_*\rangle$.

Alternatively, you can use the $\mathsf{if}$ construct defined via definite description to simply define whichever Boolean function you want via cases, though I'd personally prefer not relying on definite description.

You can also peruse the definitions used in implementations, such as this one from HOL Light: https://github.com/jrh13/hol-light/blob/7ea931a7d9925fa4abaa14767ba2510c0ad28c62/bool.ml#L97 You can see that it is the definition above.

  • $\begingroup$ I think I responded to this in the comment section of the other question, but the $\textsf{T}$ and $\textsf{F}$ that they're using there are not the same as the $\small{T}$ and $\small{F}$ that they treat as primitive boolean constants earlier in the paper. They're actually just using Henkin's technique from this paper. Here, he denotes the actual Boolean constant by $T$, whereas the thing they're calling $\mathsf{T}$ he calls $T^n$, and likewise with $F$ and $F^n$. (cont'd) $\endgroup$ – Mike Battaglia Oct 23 '17 at 17:02
  • $\begingroup$ Beyond that I'm really just trying to get the basics of how to define functions, avoiding all of these complex meta-logical embeddings for the moment. $\ast$ is a primitive type with domain equal to $\{\small{T}, \small{F}\}$, and $(\ast \to \ast)$ is likewise well defined. Is there some way to modify your answer to handle these basic cases? $\endgroup$ – Mike Battaglia Oct 23 '17 at 17:05
  • $\begingroup$ In short, the question really is: I want to define explicitly the truth table for some function of type $(\ast \to (\ast \to \ast))$. How do I do this? $\endgroup$ – Mike Battaglia Oct 23 '17 at 17:09
  • $\begingroup$ There's nothing meta-logical going on. $$\lambda A:*.\lambda B:*.(\lambda f:*\to*\to*.f((\lambda x.*.x)=(\lambda x:*.x))((\lambda x.*.x)=(\lambda x:*.x)))=(\lambda f:*\to*\to*.f(A)(B))$$ is a term of STT. $\mathsf{T}$ and $\mathsf{F}$ are terms of STT. $T$ and $F$ are elements of the semantic domain; they are not terms of STT. You can define the meaning of STT with a collection of (syntactic) rules, i.e. proof theoretically. You don't need the semantics at all to understand or define STT. (Indeed, a set-theoretic semantics is arguably overly narrow-minded.) $\endgroup$ – Derek Elkins Oct 23 '17 at 17:31
  • $\begingroup$ You define a function of type $*\to*\to*$ by writing a lambda term for it. The lambda terms are the syntax of STT. They are not a meta-notation. $\endgroup$ – Derek Elkins Oct 23 '17 at 17:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.