Functional programming is a programming paradigm which primarily uses functions as means for building abstractions and expressing computations that comprise a computer program.

learn more… | top users | synonyms

-6
votes
0answers
29 views

Translate Assembly to C Code [on hold]

00000000 < randomfunc>: 0: e92d40f8 push {r3, r4, r5, r6, r7, lr} 4: e1a04000 mov r4, r0 8: e1a05001 mov r5, r1 c: e1a00080 lsl r0, r0, #1 10: e2800001 add r0, r0, #1 14: e2846001 add r6, r4, ...
0
votes
1answer
49 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?
-3
votes
0answers
31 views

Recursive functions [closed]

Write a recursive function that prints the following story: A child couldn't sleep, so her mother told a story about a little frog, who couldn't sleep, so the frog's mother told a story about a little ...
1
vote
0answers
38 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
55 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 ...
7
votes
1answer
52 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
49 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
48 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
52 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
56 views
5
votes
0answers
38 views

Can we simulate any dependent datatype with `Eq`?

Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
4
votes
0answers
51 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 ...
9
votes
1answer
62 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 ...
8
votes
2answers
187 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 Vector class incorporating size ...
7
votes
1answer
84 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
21 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 ...
4
votes
1answer
76 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
69 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 ...
1
vote
0answers
21 views

What is a proof of normalization of Motte?

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 ...
21
votes
3answers
163 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
34 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
325 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
25 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
71 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
167 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
34 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
144 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
25 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
62 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
87 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
154 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: ...
4
votes
3answers
55 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
102 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 ...
6
votes
2answers
147 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: ...
8
votes
1answer
113 views

Are combinatory logic terms always larger?

So there is an algorithm to convert lambda calculus terms to combinatory logic using SK combinators. It produces things that explode in size. I would like to know more about this explosion in size. I ...
6
votes
0answers
22 views

Is there any type system which can assign a type to any halting lambda calculus term? [duplicate]

Some lambda terms, such as the church number 3: (f x -> (f (f (f x)))), are easily typeable on the simply typed lambda calculus. Others, such as ...
2
votes
1answer
109 views

Do functional algorithms require more memory than imperative algorithms? [closed]

Let's suppose we are counting words in string. We split it so what we have is an array of strings. I'll use Python as an example. The imperative approach would as follows: ...
1
vote
1answer
146 views

Intuition behind F-algebra

I looked at here for getting an intuition about F-algebra, but I am still left with some questions. Suppose I have a group signature as $\Sigma= (* : X \times X \rightarrow X, \thicksim: X ...
2
votes
2answers
37 views

Occurrences notation in “Compiling Pattern Matching to Good Decision Trees”

From Compiling Pattern Matching to Good Decision Trees (Luc Maranget, Proceedings of ML '08, pp. 35–46. ACM, 2008.) We also consider the usual occurrences. Occurrences are ...
1
vote
2answers
86 views

Curry Howard correspondence and Church-Turing thesis

Curry-Howard correspondence states the equivalence between logic/deduction and types/programs. The Church-Turing thesis states the equivalence of some models of computation. Specifically, all ...
0
votes
0answers
18 views

Proxy for lazy evaluation?

Can lazy evaluation be substituted in an eagerly evaluated language by the following setup?... Higher-order functions. Generalized left associativity. Infinite structures like ...
3
votes
1answer
32 views

What additional expressivity does polyvariance give in pushdown CFA?

I'm reading through Pushdown Control-Flow Analysis of Higher-Order Programs, which presents a synthesis of the Abstracting Abstract Machines technique and pushdown automata to get static analysis ...
2
votes
1answer
169 views

What is the difference between the Mogensen-Scott and the Boehm-Berarducci encoding for ADTs on the Lambda Calculus?

On the Lambda Calculus, there are several different ways to represent a list. For example, one can encode it as its right fold: ...
2
votes
1answer
56 views

Guessing the structure of a finger tree from the number of elements

I'm writing a data structure library, and I want to write an efficient algorithm for adding many elements to a finger tree (from an iterable sequence). I'm going to do this by constructing a finger ...
0
votes
1answer
58 views

Suggestions for Short Examples Contrasting Functional Programming Languages [closed]

A fellow student and I are writing a paper on functional programming for a programming languages course, part of which will be comparing and contrasting Lisp (Scheme), ML (SML), and Haskell. We'll be ...
1
vote
1answer
772 views

Difference between normal-order and applicative-order evaluation

The language I'm learning is Scheme and I'm working on an exercise that gives this: ...
1
vote
1answer
59 views

Definition of opposite category

From page 29 of The algebra of programming : For any category C the opposite category $C^{op}$ is defined to have the same objects and arrows as C, but the source and target operators are ...
0
votes
1answer
28 views

Something wrong with this definition of factorial with structural recursion? [closed]

In The Algebra of Programming page 5, the authors defined structural recursion foldn (c, h) over natural numbers: ...