New answers tagged lambda-calculus
0
votes
Can Church numerals division be performed in direct top-down manner?
Yes, following the same approach, we can do the same bouncing off back and forth skipping the entries on both numbers in unison – after turning the divisor into an infinitely repeating cycle, emitting ...
- 378
2
votes
A program that cannot be written in (simply-)typed lambda calculus but only in lambda calculus or Turing-complete language
Church numerals can be represented at a type in STLC. Define
Nat[X] = (X -> X) -> (X -> X)
Then we can write zero, successor, addition, and multiplication as operations on Nat[X]. ...
- 21
1
vote
How to "read" the λC encoding of the existential quantifier $\Pi \alpha:*. (\Pi x:S.(Px \to \alpha)) \to \alpha$
So if "P(x)" is always $False$, we have "for all $x$ in $S$, $P(x) \implies \alpha$" is always $True$, which in turn leads to the full expression to be $True$.
No. If $\forall (x:...
- 1,031
1
vote
How to "read" the λC encoding of the existential quantifier $\Pi \alpha:*. (\Pi x:S.(Px \to \alpha)) \to \alpha$
I "read" the formula $\exists (x\in S).~ P~x = \Pi \alpha:*.~(\Pi x:S.~ (P~x\to \alpha))\to \alpha$ in two somewhat different ways.
The first way of reading it is as a type of a program in a ...
- 301
0
votes
Why we can not define factorial in lambda calculus
The factorial semantics can indeed be expressed as
$\qquad fact \triangleq \lambda n. if(iszero~n) (1) (mult~n~(fact~(pred~n)))$
where $fact$ is expressed with lambda calculus syntax, as a lambda ...
- 378
Top 50 recent answers are included