Questions tagged [lambda-calculus]

λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.

402 questions
Filter by
Sorted by
Tagged with
20 views

How does the function to curry and uncurrying another function work?

The following is the code to curry or uncurry a function in Haskell: ...
16 views

An operational semantics for lambda-calculus normal order evaluation strategy

TAPL book, page 56 reads: Under the normal order strategy, the leftmost, outermost redex is always reduced first. I understand this as a restriction of the full beta-reduction evaluation ...
14 views

Mapping a free variable of type A to a cartesian closed category

In From Lambda Calculus to Cartesian Closed Categories, the author explains the interpretation of lambda calculus in cartesian closed category and at one point he explains how a term representing a ...
32 views

Is monoid the category for untyped lambda calculus?

If cartesian closed categories are the model for simply typed lambda calculus, then can it be said that a monoid is a categorical model for untyped lambda calculus?
22 views

lambda-calc program which halts on only one input

Does there exist a normal-form lambda calculus program $f$ such that $f (\lambda x . x)$ normalizes For all normal form $e \ne \lambda x . x$, $f e$ does not normalize
33 views

How is β-reduction a 2-morphism in Category theory?

According to Categorifying CCCs: Computation as a Process, computation or β-reduction process in untyped-lambda calculus is in fact a 2-morphism in category theory. Can someone please describe me ...
19 views

61 views

Are the definitions of constructs in terms of lambda terms issues in implementation/design or uses of functional languages?

In Lambda Calculus, natural numbers, boolean values, list processing functions, recursion, if function are defined in terms of lambda terms. For example, natural numbers are defined as Church numerals,...
85 views

64 views

Difference between “functional programming languages” and “lambda calculus based languages”?

In "Can programming be liberated from the Von Neumann Style?", John Backus states: The main reason FP systems are considerably simpler than either conventional languages or lambda-calculus-based ...