lambda-calculus

7calore

1risposta

È possibile implementare `max` efficientemente sul calcolo lambda non tipizzato?

min è di solito definito sul lambda calcolo non tipizzata come (usando Caramel's syntax): sub a b = (b pred a) <= a b = (is_zero (sub b a)) min a b = (<= a b a b) Questo è terribilmente inefficien

5calore

1risposta

operazioni relazionali utilizzando solo incremento, loop, assegnare, pari a zero

Si tratta di un follow-up domanda per: Subtraction operation using only increment, loop, assign, zero Stiamo solo permesso di utilizzare le seguenti operazioni: incr (x) - Una volta questa funzione è

11calore

1risposta

Forma corretta di letrec nel sistema di tipo Hindley-Milner?

Sto avendo difficoltà a capire la definizione letrec per HM sistema che viene data su Wikipedia, qui: https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions Per me, la

5calore

1risposta

Sottrazione operazione utilizzando solo incremento, cappio, assegnare zero

Sto cercando di costruire sottrazione, addizione, divisione, moltiplicazione e altre operazioni utilizzando solo seguenti: incr (x) - Una volta che questa funzione è chiamato assegnerà x + 1 a x assig

6calore

1risposta

È effettivamente possibile rimuovere "Pi" da Calculus of Constructions?

L'articolo Simpler, Easier! afferma che potrebbe essere possibile codificare i sistemi di tipi dipendenti anche senza la presenza di "Pi", ovvero, è possibile riutilizzare il costruttore "Lam" per que

8calore

3risposta

Esiste un modo efficace per convertire un numero unario in un numero binario?

lasciare che quei tipi di dati rappresentano numeri naturali unarie e binari rispettivamente: data UNat = Succ UNat | Zero data BNat = One BNat | Zero BNat | End u0 = Zero u1 = Succ Zero u2 = Suc

22calore

1risposta

Qual è il modo corretto di astrazione lambda typecheck dependent usando 'bound'?

Sto implementando un semplice linguaggio tipizzato, simile a quello described by Lennart Augustsson, mentre uso anche bound per gestire i binding. : mentre controlla un termine lambda dipendente, come

6calore

1risposta

Perché GHC non ridurrà la mia famiglia di tipi?

Ecco un calcolo lambda non tipizzato i cui termini sono indicizzati dalle loro variabili libere. Sto usando la libreria singletons per i valori singleton delle stringhe a livello di testo. {-# LANGUAG

5calore

1risposta

Esiste un termine non ricorsivo che si ripiega su un elenco codificato in scott?

Supponiamo che ho una lista scott-encoded come ad esempio: scott = (\ c n -> c 1 (\ c n -> c 2 (\ c n -> c 3 (\ c n -> n)))) Voglio una funzione che riceve questo tipo di lista e lo converte in un e

12calore

2risposta

Quali sono i metodi più avanzati per la risoluzione di equazioni funzionali?

Si supponga di voler trovare un programma λ-calcolo, T, che soddisfa le seguenti equazioni: (T (λ f x . x)) = (λ a t . a) (T (λ f x . (f x))) = (λ a t . (t a)) (T (λ f x . (f (f x)))) = (λ a b t