650 questions
0
votes
1
answer
62
views
Lean4 : Unknown Identifier 'Implies' in Lean4
When I am testing the examples in Theorem Proving in Lean4 , I find out that command #check Implies threw an error :
unknown identifier Implies.
I tried #print And and find out that it is a struct :
...
- 3
1
vote
0
answers
97
views
Is it possible to bound type-level recursion?
I'm trying to construct a typed lambda calculus, something along the lines of:
struct Fun<T>(T); // actual definition elided for simplicity
struct TypeErasedExpr { /* elided for simplicity */ }
...
- 89
1
vote
1
answer
75
views
Lean4 lambda calculus DSL macro
I would like to define a DSL for writing lambda terms in Lean using macros a la the arithmetic example. I want to support syntax for multiple arguments in the lambda, and left-associativity. Thus far, ...
- 57
1
vote
1
answer
186
views
How to perform beta reduction on a lambda abstraction?
In Will Kurt's book on Haskell, there is an example on how to overwrite a variable x in Haskell using lambda abstraction (not to be tried at home!). Here is the example:
(\x -> (\x -> (\x -> ...
- 441
0
votes
1
answer
113
views
Theorem for lambda calculus
I have to solve this exercise:
Formulate and prove a confluence theorem for lambda calculus (ie, prove that if a λ-expression e reduces to both e1 and e2, then there exists e' such that e1 and e2 ...
- 3
0
votes
1
answer
108
views
Parsing extended lambda calculus using recursive descent
I'm writing interpreter for simple lambda calculus based language in C. EBNF for language is
S ::= E
E ::= 'fn' var '->' E | T {'+' T} | T {'-' T}
T ::= F {'*' F} | F {'/' F}
F ::= P {P}
P ::= var |...
- 3
1
vote
1
answer
80
views
define equality predicate Lambda-Calculus nltk
I am trying to define a Lambda-Calculus representation of the word 'are', which is an equality predicate for this ccg:
ccg = '''
# CCG grammar
# complete the lexical entries with their categories and ...
- 49
1
vote
0
answers
29
views
How to strictly prove that call/cc cannot be presented by lambda calculus?
I known this could be more of a mathematical question. All the answers I've found talks about something like "control flow" but I don't think that is mathematically well-defined.
- 126
2
votes
2
answers
124
views
Execute a list of purrr-style lambda formulas on a data frame
The following toy data has 5 variables, X1 to X5.
set.seed(123)
df <- data.frame(matrix(rnorm(500), 100, 5))
I want to perform specific operations on specific variables, using a named list of ...
- 533
0
votes
1
answer
85
views
Why would this $vau calculi snippet lead to an infinite loop?
No idea if anyone on this site happens to know about $vau calculi, but anyway, for some reason, this snippet leads to an infinite loop, and I'm not sure if it's due to the $vau implementation I use, ...
- 4,060
2
votes
0
answers
46
views
How do I solve this infinitely recursive type problem I've created in Haskell with Church Numerals [duplicate]
data ChurchN a = ChurchN
{ numeral :: (a -> a) -> a -> a
, litRep :: String
}
next :: ChurchN a -> ChurchN a
next x = ChurchN
{
numeral = \f y -> f (numeral x f ...
0
votes
1
answer
151
views
How to Implement Sum Type Semantic Rules in a Haskell Lambda Calculus Interpreter?
I'm working on a lambda calculus interpreter in Haskell, and I need help implementing semantic rules for sum types. Below is a simplified version of my code with lexer, interpreter, and typechecker ...
- 31
-2
votes
1
answer
229
views
Excel Formula to Stack a Variable Number of Variable-Length Arrays with Conditional Spacing
Given a list of sequential, variable-length (rx1) arrays, dynamically stack the arrays (vertically) such that they follow a particular set of rules -- ordered first by the Order column in the States ...
- 65
0
votes
0
answers
29
views
Scalar and quantitative problem with code to define null and void counterparts in binary partitions
I'm currently working on code for an equation dictating the values of "null" and "void, using these motives as baseline material the code is to quantify ley lines of isotopes, ...
4
votes
1
answer
138
views
Implementation of Church numeral multiplication in Haskell not working
I'm currently learning about Church encoding and I'm trying to implement the mul (multiply) function.
This is the correct implementation
mul cn cm = \f x -> cn (cm f) x
This (my implementation) ...
