Functional programming is a programming paradigm which primarily uses functions as means for building abstractions and expressing computations that comprise a computer program.
3
votes
0answers
39 views
Inferring ranking functions in a general code graph with partial information
Let me define the notion of call graph:
A program consists on a set of functions $f,g,h,\ldots$ where each
function $n$ is as a mapping $n: D^l \to D^m$. Here $D$ is the
datatype representing ...
1
vote
0answers
13 views
Nested Function stuck on iteration update
I want to solve the Sparse Extended Information Filter Slam described by Dr. Sebestian Thrun in Probabilistic Robotics.I stuck in some nested function.
The algorithm is described in page 309 in this ...
1
vote
1answer
46 views
how to deduce a function subtype rule from a given function type definition
This question relates to liskov substitution principle seems to have two conventional meanings but is really a different question, so I'm posing it as a new question.
I'm doing a bit of research into ...
1
vote
1answer
51 views
Stablishing termination of the construction of infinite stream with ranking functions
I'm working with Turing's paradigm to prove termination of programs by annotating functions with ranking functions and I encounter the following example:
...
1
vote
1answer
52 views
Reducing lambda expression to normal form
Can someone explain the steps to reduce
$$ (\lambda n. \lambda m. \lambda f. \lambda x.\ n\ (m\ f)\ x)\ (\lambda f. \lambda x.\ f\ (f\ x))\ (\lambda f. \lambda x.\ f\ x) $$
to $\lambda y. \lambda z.\...
2
votes
2answers
66 views
Proving parametricity for Gallina functions
I have the following definitions
Definition nat'' {X : Type} := (X -> X) -> X -> X.
Definition nat' := forall (X : Type), @nat'' X.
And when I wanted to ...
-2
votes
0answers
14 views
Creating class instance from a function
I'm trying to create an instance of a class from a function that takes user inputs. However, I'm unsure as to how to use those user inputs from the separately defined function to be the attributes of ...
17
votes
0answers
138 views
Can a calculus have incremental copying and closed scopes?
A few days ago, I proposed the Abstract Calculus, a minimal untyped language that is very similar to the Lambda Calculus, except for the main difference that substitutions are ...
5
votes
1answer
98 views
Best way to translate while loops to functions for software verification
I have a verification engine where while loops are translated into functional code, like this:
...
2
votes
2answers
74 views
Inference of a measure for a decreasing chain
Given integers $v_0,\dots,v_{n-1} \in \mathbb{N}$, I want to find an integer $t>0$, a map $f:\mathbb{N} \times \{0,1,\dots,n-1\} \to \mathbb{N}^t$, and a well-founded order $>_t$ on $\mathbb{N}^...
1
vote
1answer
49 views
pure function in C
There does not seem to be a canonical definition of "pure function", but the widespread language-agnostic understanding seems to be a function that
has no side effects
produces a value that is ...
-1
votes
2answers
40 views
Defining an HTML Template as an Algebraic Type
Wondering if/how you could define a highly nested structure as a Dependent Type (or an Algebraic or Parameterized type). Specifically, an HTML template. Not that they work like this (HTML templates ...
1
vote
2answers
93 views
functional vs state-based
As mentioned in Lambda Calculus - Computerphile,
Alonzo Church's method is functional where a function as a blackbox,
takes an input, processes, and produces an output, and Turing machines
...
4
votes
0answers
58 views
Why most purely functional red-black trees are left-leaning?
Is there any particular reason for picking a left-leaning red-black tree over a regular red-black tree when trying to do a purely functional implementation?
I've not researched very deeply into this ...
0
votes
1answer
49 views
Are there any known implementations of a functional Heap's Algorithm?
TL;DR: Is an implementation of the Heap's Algorithm adhering to the principals of functional programming possible, and are any implementations of it known? And by "adhering to the principals of ...
2
votes
0answers
47 views
Term for weak head normal forms that cannot be reduced in any environment
In my understanding, a lambda expression is a normal form (NF) when it has no redexes. For instance, $\lambda x.x$ is a NF, but $(\lambda x.x)y$ is not. A lambda expression is a weak head normal form (...
-2
votes
1answer
27 views
Erlang- Creating a function which only adds/subtracts positive integers
I want to create a function which allows me to input a list, and then add all of the positive numbers from the list together, leaving any that are negative.
([3,1,-1])
For example only 3 and 1 would ...
2
votes
0answers
58 views
How would a priority queue be implemented in a functional programming language?
How would a priority queue be coded efficiently in a functional programming language? I'm new to functional programming, but I'm having difficulty understanding how a data structure that seems to ...
-2
votes
2answers
79 views
Are mathematical functions used in computer science? [closed]
Well, I know the difference between functions used in math and C language. But what are those specific areas where mathematical functions are used?
1
vote
1answer
43 views
Is there a combinator that introduces brackets to a combinatory logic expression using just B?
Suppose I have the expression $abcdef$ and I want a combinator $X$ that does this:
$Xabcdef=a(bcd)(ef)$.
Is it possible to express $X$ using just the $B$ combinator, defined by
$Babc=a(bc)$?
Is ...
0
votes
1answer
62 views
Can we define the Functor Category in Haskell (or any other language with a more expressive type system)?
Here I am talking about the Functor category, which is defined as a category whose objects are functors and morphisms are natural transformations.
For reference: https://ncatlab.org/nlab/show/functor+...
3
votes
2answers
67 views
Can we define a program by means of a walk of a graph induced by the category of types?
After reading about Category Theory at https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ I was wondering whether we can represent any program by means of a walk of a ...
3
votes
3answers
146 views
Is it possible to make a language that can build upon itself perfectly?
First of all, note that I'll have to explain my thoughts in a layman's terms.
There are so many high-level programming languages out there that compete with each other. This means we have to build ...
1
vote
2answers
41 views
What mathematical terminology exists for “embellished trees”?
I'm looking for some pointers on proper mathematical (FP?, category-theory?) terminology.
My apologies if the below is somewhat imprecise; I suppose the precision is precisely what I'm looking for in ...
2
votes
1answer
53 views
How is this lamda function beeing executed in an example for the Y combinator
I have spent a few hours now trying to understand how the Y Combinator is working and how it allows us to construct recursive functions with higher order functions.
I have been going through this ...
3
votes
1answer
50 views
Can we implement every algorithm using only immutable variables?
Can we implement every algorithm using only immutable variables such that their space and time complexity is the same as using mutable variables?
1
vote
0answers
26 views
What extent of difference is considered significant in runtime?
I have a task to test the time required to evaluate a specialised function and a generalized function that aims to get the same output, and conclude whether there is a speed advantage of using one ...
2
votes
1answer
108 views
explaining $\lambda$-calculus/functional programming to someone used to Turing machines/procedural programming?
I have the following background:
I have experience with object-oriented programming languages
I find Turing machines and the concept of a "procedure" very intuitive.
Yet I'm interested to ...
1
vote
1answer
59 views
Why does functional map() operation not permit operating on two elements of a list at a time?
Mathematically it seems so easy to use two elements of a vector as two arguments to a function.
$$f(\boldsymbol{x_{i+1}},\boldsymbol{x_{i}})$$
In functional programming however a map (function) allows ...
2
votes
2answers
69 views
General term for map/fmap
The general term for folds is a catamorphism. The general term for unfold is an Anamorphism. Is there an equivalent term for map? I know that a map is a type of fold however restriction is ...
7
votes
1answer
92 views
Y combinator, function composition
I am trying to understand Y combinators. Could you please explain why the following are equivalent
(Y (f ∘ g))
(f (Y (g ∘ f)))
(Y is a fixed point combination)...
4
votes
1answer
47 views
How to explain/understand brackets of applicative functor [[f u1… un]]?
I am reading article about Applicative Abstract Categorial Grammars http://okmij.org/ftp/gengo/applicative-symantics/AACG.pdf and this article uses brackets [[...]] for action on terms inside ...
0
votes
0answers
36 views
Proof problem in Haskell with take and drop
Im learning Haskell and i want to prove
take m (drop n xs) = drop n (take (m+n) xs)
and
drop m (drop n xs) = drop (m+n) xs
Somebody can help me please? :)
0
votes
0answers
25 views
How is this defined in an iterative style?
This is the so-called recursive style:
And this is the so-called iterative style:
It seems like it is defined recursively to me. The function doesn't hide the next call of the function defined in it ...
4
votes
2answers
90 views
When does a type generalise another type?
In languages like Haskell, with a Hindley-Milner type system, when does a type $t$ generalise a type $u$? I use the definition: $t$ generalises $u$ iff $\forall\ v: v \text{ unifies with } u \...
1
vote
0answers
20 views
Order of domino tiles function [closed]
The domino tiles can be listed in an orderly way as shown in the figure :
figure link
Write a function such that given two variables ("minor" and "major") where "minor" is the lowest value and "...
1
vote
0answers
44 views
Design considerations for a language to support automatic parallelization [closed]
Automatic parallelization isn't a new thing by any means, and lots of questions have been asked about whether Java or C or C++ or a host of other languages or specific compilers (gcc 5 v 6, clang, ...
2
votes
2answers
147 views
Proving monad laws for flatMap and unit, given laws for compose and unit
I'll use scala notation but hopefully things will make sense in general (I'm trying to prove that you can define a monad using either [flatMap (aka bind) and unit] or [compose and unit])
The book ...
0
votes
1answer
47 views
Could the execution of a Haskell program be considered as a proof in equational logic
Could the execution of a Haskell program be considered as a proof in equational logic. This follows on from my earlier question on Haskell and inductive proof. Currently I am stuck between morally yes,...
3
votes
1answer
221 views
Does a Haskell program count as an inductive proof?
Is the following statement from [1] true?
"Since recursion is the main computational technique, a terminating pure Haskell program counts as an inductive proof of a theorem."
My intuition is that ...
4
votes
1answer
71 views
Writing the coherence conditions for a monad in a functional laguage
i recently asked a related question about the relationship between monads in category theory and Haskell. The answerer showed me the following classes and instances:
...
3
votes
2answers
56 views
Is there a universal identity or zero value for folding?
I'm using Haskell notation for illustration, hopefully it is known widely enough for this to make sense.
In the following fold function the second argument is what I'm calling the identity:
...
5
votes
1answer
131 views
How is the definition of monads in category theory equivalent to the definition in functional programming?
In Haskell, Monad is a class of type constructors which act on types that have the following functions implemented:
...
0
votes
0answers
27 views
What is the nomenclature or theory for determining an overall status of multiple enumerations?
I am writing a method which evaluates multiple status enumerations and determines an overall status. I'm looking for what this process might be called and perhaps some theory on it.
It may be best to ...
0
votes
2answers
94 views
Mutation considered harmful, but is there a safe set
Functional programming does not have mutation. Mutation is usually harmful, however mutation is sometimes beneficial. e.g. Creating a [random number] generator.
In the same way that ...
5
votes
2answers
239 views
Why don't imperative languages like C or Go support Haskell-like parametric polymorphism?
Why don't imperative languages support parametric polymorphism as powerful as whats in Haskell and OCaml?
More specifically if I call a function foo(x) that ...
4
votes
1answer
88 views
Mathematical equivalent of reduce()?
filter() in functional programming can be thought of as being analogous to an equation that filters the range of the variable.
map() can be through of as a function mapping domain to codomain.
...
6
votes
1answer
139 views
Why are the laws of an applicative functor defined the way they are?
Let's recall the definition of an applicative functor. Throughout this question, I write $x: T$ to denote that the value $x$ has type $T$.
Definition: An applicative functor consists of a type ...
4
votes
1answer
191 views
How do you represent LISP as mathematical / logical model?
I asked this in stackoverflow, but the question probably fits here better.
This question arose from the objection that LISP is regarded as a functional language with some simple principles, namely ...
3
votes
1answer
150 views
Type Inference and Generalization
I've been trying to understand type inference for Hindley-Milner-based languages, and I'm struggling to understand how generalization works. Let's say I have the following program in Haskell:
...
