Functional programming is a programming paradigm which primarily uses functions as means for building abstractions and expressing computations that comprise a computer program.
2
votes
0answers
29 views
Structural induction in non-local program transformation
Assume a functional language and a specialization operation (pulling out sub-expressions):
let f x y = (h 23 x) + (g 42 y)
becomes
...
4
votes
1answer
52 views
In what cases is graph rewriting not enough to avoid duplicate work?
As I understand, evaluating something like the following in normal order evaluation is inefficient due to duplicate work:
...
13
votes
3answers
1k views
How to make a language homoiconic
According to this article the following line of Lisp code prints "Hello world" to standard output.
(format t "hello, world")
Lisp, which is a homoiconic language,...
3
votes
1answer
112 views
Does the closure of a function include the actual parameter passed to the function?
A closure of a function includes the environment when calling the function.
Does the environment included in a closure of a function include the actual parameters for the function?
If I am correct, ...
9
votes
4answers
150 views
What are common formal techniques for proving functional code correct?
I want to provide proofs for parts of a Haskell program I'm writing as part of my thesis. So far however, I failed to find a good reference work.
Graham Hutton's introductory book Programming in ...
4
votes
1answer
34 views
What are some possible “functional” memory structures?
With my thin knowledge on embedded systems, compilers, and computer architectures, I know that the basics of computer memory(physical) are sort of like an array, with addressing which work like ...
3
votes
1answer
56 views
Why is Church-Rosser so important for basing programming languages on lamdba-calculus?
So, I know Church-Rosser has 2 thesis:
CR1: If $ E_1 \leftrightarrow E_2 $, then there exists an Expression E so $ E_1 \rightarrow E $ and $ E_2 \rightarrow E $
CR2: If $ E \rightarrow N $ (with N ...
9
votes
2answers
110 views
Is there a paradigm for composing “incremental update” functions in a pure dataflow style?
I don't know the correct terminology for asking this question, so I'll describe it with lots of words instead, bear with me.
Background, just so we're on the same page: Programs often contain caches -...
6
votes
1answer
79 views
Safe way to explicitly define new types instead of using Algebraic data types for my functional language
Question:
As I'm working on a Hindley-Milner typed lambda calculus, in order to make it usable I need to add some types such as list and pairs. The way I currently do it is, I have an ...
0
votes
3answers
75 views
Should a pure function take all of the functions it calls as arguments?
After Wikipedia, if a function is pure, then:
[it] always evaluates the same result value given the same argument value(s).
So: if a function, let's call it ...
15
votes
0answers
166 views
Why hasn't functional programming researched dynamic trees?
By dynamic trees I am referring the definition stated in Sleator & Tarjan's paper "A data structure for dynamic trees" in 1983. Since then, few efforts have been done in the functional programming ...
0
votes
0answers
28 views
what is the connection between evaluation context and call by value?
I been reading about $\lambda$-calculus and related stuff, but I got some confusions which i want to clarify.
The call by value reduction is expressed with two rules
$$
\frac{e_1 \rightarrow e_1'}{...
4
votes
1answer
58 views
call by value: what is a value?
In the 'call by value' evaluation of lambda-calculus, I am bit confused with 'value'.
On page 57 of the book Types and Programming languages, it is said:
The definition of call by value, in ...
6
votes
1answer
100 views
Is it possible to prevent arithmetic errors with a dependent type system?
In a functional programming language I have functions like
$$f\colon Int \times Int \times \cdots \times Int \to Int$$ which do some computation. However for certain arguments $(x_0, \dots, x_n)$ the ...
4
votes
2answers
112 views
Is there a point to an all-encompassing programming language? [duplicate]
There are many programming languages in use throughout the world today, including languages that specialize in database manipulation, functionality, object-orientation, concurrency, etc. Would there ...
0
votes
1answer
40 views
Is function application actually a memory manipulation algorithm?
I thought about how in lambda calculus (and many implementations of functional programming languages) function (lambda) application and lambda itself, as a construct, are "primitive things", usually ...
0
votes
1answer
75 views
Recursive definition of Matrix
Like Linked-list for Array, is there a recursive counter-part for Matrix?
Is there a persistent data structure which can be used in place of Matrix in pure functional language like Haskell?
1
vote
0answers
43 views
Tricks, Tips and Nontrivial Insights with Higher-Order Functions
Many years ago I briefly skimmed a physical book (or perhaps a preprint?) on programming in Racket that included lots of really unique uses of map and ...
5
votes
1answer
83 views
How to find time complexity for functions in lazy functional languages?
So far, I have looked around the internet for information how to find the time complexity for functions in lazy functional languages, but most of the resources on time complexity focus on strict ...
8
votes
1answer
72 views
Why is `map insertionsort` not to equal to`map mergesort`?
In the type theory podcast ep. 3, Dan Licata claims that the fact that for every input, insertionsort and mergesort give the same result does not imply that the result would be equal when used as ...
0
votes
0answers
24 views
How would one prove that the following scheme definition is an ordered stream of integers
How would one prove that the following scheme definition is an ordered stream of integers
(define integers (cons-stream 1 (add-streams ones integers)))
4
votes
3answers
59 views
Is Applicative-order and Normal-order evaluation model's definition contradictory as per sicp text book?
As per this explaination, it defines applicative and normal order evaluation in one form saying:
This alternative "fully expand and then reduce" evaluation method is known as normal-order ...
3
votes
2answers
58 views
Functional programming with branches that have no order?
I was wondering if there is any programming style in which the outcome does not depend on the order of statements or groups of statements such as guards. Vaguely, I imagine this would leave room for ...
1
vote
1answer
306 views
What are differences between Static Scope and Dynamic Scope?
My teacher has provided the following pseudo-code, and says that the output using static scope is 1 2 3, but the output using dynamic scope is ...
0
votes
1answer
62 views
What are functions called that yield the same result when applied to one of their result values
Suppose one of the following holds for all x, or all y, or all z:
...
5
votes
0answers
41 views
Can we simulate any dependent datatype with `Eq`?
Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
5
votes
0answers
59 views
Flaw with Cross Entropy Error in Neural Networks
I've recently been working on creating a neural network to classify handwritten digits. I implemented 1-of-N encoding such that there are the same number of output nodes as possible digits (The ...
10
votes
1answer
88 views
No Naive Set Theoretic Models of Polymorphic Lambda Calculus?
In Philip Wadler's paper on Theorems for Free he states in Section 2 on Parametricity that
there are no naive set-theoretic models of polymorphic lambda calculus
In the naive set-theoretic model ...
9
votes
2answers
217 views
Proving a sorting operation in type system
I want to know how far a type system in a programming language can be beneficial. For example, I know that in a dependently typed programming language, we can create a ...
7
votes
1answer
115 views
Can we do everything in imperative languages with a functional language if it does not allow for a 'state'?
I was reading Structure and Interpretation of Computer Programs (SICP), MIT. What I have understood is that in pure functional programming language, there is no such thing as a local state. SICP, pg ...
0
votes
1answer
24 views
The symbolic differentiation of univariate expressions
I was reading "Doug McIlroy: McCarthy Presents Lisp" and the phrase "symbolic differentiation of univariate expressions" triggered a faint memory of a demonstration of differentiation done in haskell ...
5
votes
1answer
88 views
Do Self Types make the Calculus of Inductive Constructions obsolete?
Self Types are an extension of the Calculus of Constructions [1] that allow the language to express algebraic datatypes encoded through the Scott Encoding. The Scott Encoding provides one the ability ...
2
votes
1answer
75 views
Why do we distinguish between term abstraction and type abstraction in System F?
In System F, we distinguish between types and terms. Types are defined by the following BNF:
\begin{align}
A, B ::=&~\alpha && \text{(type variable)} \\
&|~A \rightarrow B &...
3
votes
1answer
36 views
What is a proof of normalization of Morte?
It is said that any term on the calculus of construction halts. I am studying it through Morte, which is a bare bone implementation of the coc available on github. Is there any simple proof of ...
24
votes
3answers
251 views
What is a brief but complete explanation of a pure/dependent type system?
If something is simple, then it should be completely explainable with a few words. This can be done for the λ-calculus:
The λ-calculus is a syntactical grammar (basically, a structure) with a ...
4
votes
2answers
36 views
What terms type systems exclude?
I understand type systems like the simply typed lambda calculus, system F and the calculus of constructions include a different subset of all lambda terms. But what, precisely, are the terms each of ...
6
votes
2answers
370 views
In the Curry-Howard isomorphism as applied to Hindley-Milner types, what proposition corresponds to a -> [a]?
(Using Haskell syntax, since the question is inspired by Haskell, but it applies to general Hindley-Milner polymorphic type systems, such as SML or Elm).
If I have a type signature ...
0
votes
1answer
33 views
How can a device decipher spoken English words?
I want to know how it can process spoken English words and Pull out a matching response? Is it a chip or a installed software? Does it take up a lot of space? Thanks.
5
votes
1answer
86 views
What is the Curry-Howard analogue for linear logics?
As defined by Wikipedia,
(The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ...
6
votes
1answer
206 views
Can a functional language be homoiconic?
According to the wikipedia page on homoiconicity:
In a homoiconic language the primary representation of programs is also a data structure in a primitive type of the language itself.
I was ...
5
votes
0answers
38 views
Is it possible to reduce functional equations to SAT?
The problem of finding a solution for functional equations can be defined as:
Let A0, A1, A2... An, B0, B1, B2... Bn, X be terms of the lambda calculus, all terms known, except for X, unknown. ...
8
votes
0answers
163 views
Are CPU architectures biased towards procedural runtimes?
Are there any changes that could be made to CPUs to make them perform better for concurrent runtimes like Rust? For instance, are there changes to branch prediction implementations or cache sizes ...
0
votes
1answer
31 views
Proving equality between foldl recursive and iterative fold
Hi I have two definitions of fold. I will call them foldl which is recursive and fold$_{itr}$ which is iterative.
I am looking for an algebraic proof that the two definitions are equal ideally ...
0
votes
2answers
65 views
Expressing iterative version of fold in terms of recursive version
1st Definition. Recursive definition of fold
fold$_{recur}$ (c,h) nil = c
fold$_{recur}$ (c,h) (cons(a, x)) = h(a, fold$_{recur}$ (c,h) x)
2nd definition of fold. Iterative definition
fold$_{itr}$ ...
1
vote
1answer
126 views
Can we prove mathematical induction statements in Lisp?
My previous question Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program? has a problem that it tries to cover too much ground. Here is a related question motivated by ...
3
votes
2answers
166 views
Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?
Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion.
Haskell is strongly typed and we can define the natural numbers
...
3
votes
2answers
27 views
Is there a formal term for functions that have static state across executions?
Two examples, one in PHP:
function adder($i){
static $a = 0;
$a += $i;
return $a;
}
A similar effect can be achieved with closures in javascript:
...
5
votes
3answers
60 views
Is there any meaning behind the classification of “λ-terms” in classes such as “church number” and “church list”?
λ-calculus terms can be informally/intuitively categorized, such as:
(λ f x . (f (f (f x))))) is a church natural (3)
...
0
votes
1answer
124 views
Why are functional programs considered slower than procedural counterparts asymptotically, if the opposite appears true?
I've read and been told way too many times that functional algorithms and data structures have an obligatory O(log(N)) slowdown in respect to their procedural (for-...
6
votes
2answers
158 views
Eliminate non-local references from closure
For a code similarity detection framework I need to eliminate references to non-local variables, for example having the following closure:
...
